Zulip Chat Archive

Stream: mathlib4

Topic: Update lean?

Daniel Selsam (Sep 24 2021 at 21:28):

I was about to try to get the mathport binaries to import Mathlib4 so the tactics would work, but I see that Mathlib4 is using a lean4-nightly that is a month old now. Are there any plans to update the lean4 version?

Scott Morrison (Sep 25 2021 at 01:43):

Wasn't too hard: https://github.com/leanprover-community/mathlib4/pull/50

Daniel Selsam (Sep 27 2021 at 13:14):

Scott Morrison said:

Wasn't too hard: https://github.com/leanprover-community/mathlib4/pull/50

Excellent, thanks. I will try to connect it to mathport today.

Johan Commelin (Sep 27 2021 at 15:15):

Exciting! Thanks so much for doing this!

Mac (Oct 01 2021 at 22:22):

@Scott Morrison fyi, the nightly you updated to (09-24) doesn't have a Windows release. Thus, all the projects tied to that release (mathlib4, mathport, test-mathport, etc.) are broken on Windows without manually changing the Lean version.

Scott Morrison (Oct 01 2021 at 22:22):

Oh! Was that a one off? How are the release OSes determined?

Scott Morrison (Oct 01 2021 at 22:23):

I'll look into updating again.

Mac (Oct 01 2021 at 22:25):

The nightly CI builds a release for all 3 platforms (Windows, MacOS, Linux) via separate jobs and if one of those fails the nightly doesn't get a release for that platform. One of the Lean 4 tests fails non-deterministically on Windows resulting in some nightlies not getting a Windows release.

Thus, you pretty much have to check the release page manually to see if there are actually binaries for all platforms for a given release. And if some else deeper went wrong, even that may not be sufficient (like with the recent leanc issue).

Mac (Oct 01 2021 at 22:26):

Ideally, it would be a good idea for any major project to have a CI that test their build on all 3 platforms.

Mac (Oct 01 2021 at 22:28):

Scott Morrison said:

I'll look into updating again.

I'd wait until tonight's nightly is released (i.e., the 10-02 nightly) because all the nightlies from 09-025 to 10-01 where broken on Linux (without Nix) due to the leanc issue I mentioned. That is, assuming tonight's nightly does successfully release on all platforms. XD

Scott Morrison (Oct 01 2021 at 22:45):

Okay, https://github.com/leanprover-community/mathlib4/pull/54 gets us up to 10-01, and I'll wait for the next one!

Mac (Oct 02 2021 at 01:37):

@Scott Morrison fyi, 10-02 does appear to work properly on all platforms! :grinning:

Scott Morrison (Oct 02 2021 at 01:41):

Updated the PR!

Mac (Oct 02 2021 at 19:38):

@Daniel Selsam could you update mathport to 10-02 as well? I am testing a fix for the bug @Scott Morrison found and currently the build is failing from what appears to be an error in mathport due to the change in well founded relations sin the Lean core since 09-24. Thus, that makes hit hard to verify my fix actual works for mathport.

Daniel Selsam (Oct 02 2021 at 20:00):

I pushed mathport, updated to 10-02. Running it now and will update the release (~30m).

Daniel Selsam (Oct 02 2021 at 20:39):

@Mac updated the mathport release

Mac (Oct 02 2021 at 20:43):

@Daniel Selsam a minor note: it would be nice if you could hyperlink the commits in the release info to their respective GitHub URL (like is done for mathport itself)

Mac (Oct 02 2021 at 20:45):

In fact, if I am not mistaken, you can just stick the GitHub link to the commit directly in the release Markdown and GitHub will magically pretty print it

Mac (Oct 02 2021 at 21:50):

@Daniel Selsam question: why is there a lakefile.lean~ in liquidbin?

Scott Morrison (Oct 03 2021 at 02:56):

@Daniel Selsam, I made a PR with two fixes to your update, https://github.com/leanprover/mathport/pull/27.

  • lake now expects dependencies to be an Array, not a List.
  • the lean-toolchain files in the Lib/ subdirectories were still pointing at 09-24, so I've bumped those to 10-02.

Scott Morrison (Oct 03 2021 at 02:56):

(Oh, and I deleted the liquidbin/lakefile.lean~.)

Scott Morrison (Oct 03 2021 at 03:01):

(You'll need to regenerate the release artefact after merging, because I've changed files in Lib/.)

Daniel Selsam (Oct 04 2021 at 14:21):

@Scott Morrison Thanks. I merged and am regenerating now.

Scott Morrison (Oct 06 2021 at 02:11):

@Daniel Selsam, sorry, another request to rebuild the artifact: https://github.com/leanprover/mathport/pull/28

Scott Morrison (Oct 06 2021 at 02:12):

I'm working on the Makefile for mathport now, to try to get something that builds without external copies of lean/mathlib/lean-liquid. I'd like to be able to build the artifact myself.

Daniel Selsam (Oct 06 2021 at 02:13):

@Scott Morrison My computer's power supply broke randomly today :( I am on an 8-year-old laptop. I will look into cloud processes.

Scott Morrison (Oct 06 2021 at 02:14):

In fact, just merging that PR may be enough for me.

Scott Morrison (Oct 06 2021 at 02:16):

Oh, no, it's the mathlib4 lakefile.lean that I need to update as well.

Scott Morrison (Oct 06 2021 at 02:23):

@Daniel Selsam, could you merge https://github.com/dselsam/mathlib4/pull/1?

Daniel Selsam (Oct 06 2021 at 02:26):

Merged both (but didn't get to sanity-check either).

Scott Morrison (Oct 06 2021 at 02:31):

Sorry, missed one of the four lakefiles, there's another PR for the last: https://github.com/leanprover/mathport/pull/29

Last updated: Dec 20 2023 at 11:08 UTC