chore: use toolchain for leanprover/lean4#2749

[kim-em]

• Lean 4 PR: refactor: .lake directory for Lake outputs leanprover/lean4#2749
• Mathlib bump that we need to get working, currently failing with a ProofWidgets error: chore: fixes for leanprover/lean4#2749 mathlib4#8216

[kim-em]

This is broken, and needs fixing! @tydeu, @Vtec234, would one of you be able to sort this out?

[Vtec234]

Ah, this isn't an issue caused by the bump; the macOS CI just deadlocks nondeterministically. I have observed this before. It may be due to the mutex here, but I don't know of another way to achieve what the lakefile does.

[kim-em]

Ah, this isn't an issue caused by the bump; the macOS CI just deadlocks nondeterministically. I have observed this before. It may be due to the mutex here, but I don't know of another way to achieve what the lakefile does.

Ah, I think I've noticed this locally as well!

[kim-em]

Okay, separately from sorting out the CI failure here, the point is that leanprover-community/mathlib4#8216 is currently failing when trying to compile Mathlib on the toolchain from leanprover/lean4#2749, and the failure is from ProofWidgets!

[Vtec234]

Okay, separately from sorting out the CI failure here, the point is that leanprover-community/mathlib4#8216 is currently failing when trying to compile Mathlib on the toolchain from leanprover/lean4#2749, and the failure is from ProofWidgets!

I see, I think it's because that PR points at the lean-pr-testing-2749 branch which does not have an associated cloud release. Note that even if the build here succeeded, the mathlib build would still fail since we do not upload cloud releases for PRs, only for tagged commits. If you just point mathlib back at the latest release (v0.0.21), I think the build should succeed.

[Vtec234]

Ah, no, am I reading correctly that it also failed while pointed at v0.0.21? It does look like a cloud release failure in any case, implying that somehow the release archive was not downloaded correctly.

[tydeu]

@Vtec234 The underlying compatibility issue with the PR is that the ProofWidgets hard-codes references to build directory in its code (see below) and its default location changes in the PR.

ProofWidgets4/ProofWidgets/Compat.lean

Line 174 in f1a5c78

javascript := include_str ".." / "build" / "js" / "compat.js"

A forward-compatible fix would be to manually set buildDir := "build" in the lakefile.lean package configuration rather than relying on the changing default.

[kim-em]

Shouldn't it be the other way? That Compat.lean should use the build dir?

As long as it will work downstream in Mathlib I don't really mind!

[tydeu]

@semorrison True, one solution is to change the hard-coded value to the new default. However, I think setting buildDir to an explicit value (or, alternatively, outputting the JS to a specific unique directory e.g. dist) is a good idea because ProofWidgets is relying on the JS being in a specific place for its correctness. It avoids any repeat of this problem should any further reorganization happen in the future (which could be in the cards).

[kim-em]

Oh, I meant that Compat.lean should ask where the build dir is!

[tydeu]

@semorrison Loading the workspace for this seems like undesirable overhead. In the future, it may be able to get this information without paying that cost, but that is not currently the case. To me, the best long-term solution is to to stick the JS files in a fixed location the code can rely on them being in (and Lake currently doesn't provide that and is unlikely to do so in the near future).

[kim-em]

Hmm... my reaction to all of this is that we should not provide any ability to customize the build directory, if providing customization leaves us in this situation! But that is not a discussion for this PR.

@Vtec234, are you happy with buildDir := "build"?

[tydeu]

@Vtec234 Or buildDir := "dist" if you want to be more JS-like. 😉

[Vtec234]

buildDir := "build" is okay. Let's try it here.

[Vtec234]

I made a release, v0.0.22-pre, which you can point to in the mathlib PR.

[kim-em]

Okay, I have updated leanprover-community/mathlib4#8216 to use the pre-release.

[tydeu]

@Vtec234 Since this is a backwards- and forwards-compatible fix, it seems like it can be merged independently of the upstream PR. What do you think?

[Vtec234]

For sure. I made that change on main and released v0.0.22. Does the existence of both releases imply we can close this?