Zulip Chat Archive

Stream: new members

Topic: MIL is broken?

Geno Racklin Asher (Jun 17 2023 at 18:56):

The latest commit to MIL seems to have deleted everything? Resetting to a prior commit to get the files back but not sure what happened here

Mario Carneiro (Jun 17 2023 at 18:59):

@Jeremy Avigad

Patrick Massot (Jun 17 2023 at 19:11):

No idea what happened but I think I fixed it.

Geno Racklin Asher (Jun 17 2023 at 19:35):

Thanks - just to doublecheck, now it's showing the following: [399/768] Building Mathlib.Data.Tree (etc.)
Is this expected behaviour, given the lake exe cache get? I sort of figured it should be prebuilt.

Jeremy Avigad (Jun 18 2023 at 01:29):

Thanks, Patrick. I probably made the same mistake I made a week and a half ago, i.e. deployed from Windows (which doesn't know about symbolic links) rather than Linux.

@Geno Racklin Asher When do you see that message? After downloading and decompressing the cached files, everything should work. Does the "building" take more than a minute or so?

Geno Racklin Asher (Jun 18 2023 at 08:34):

Maybe I messed up the installation somehow, but after the lake exe cache get downloading and decompression it does this when I import mathlib, and can take a good few minutes (on a high end pc). I'm running Windows btw

Scott Morrison (Jun 18 2023 at 08:36):

Does lake build immediately after lake exe cache get start rebuilding? Or only when you open in VSCode?

Geno Racklin Asher (Jun 18 2023 at 08:49):

It certainly seems to: here's the (intermediate) output from lake build immediately after the cache get.

Scott Morrison (Jun 18 2023 at 09:12):

What did lake exe cache get output?

Scott Morrison (Jun 18 2023 at 09:13):

Just to confirm, this is in the mathematics in lean repository? Perhaps try a fresh checkout in case you've done something weird somewhere? :-)

Geno Racklin Asher (Jun 18 2023 at 11:22):

Yes - I did a fresh checkout, and even a fresh install of the lean4 toolchain. lake exe cache get did a bunch of downloads, then output Decompressing 2972 file(s).

Scott Morrison (Jun 18 2023 at 11:49):

You haven't done anything weird with elan override have you? (Hopefully not! If you have, undo it with elan override unset in this directory.)

Scott Morrison (Jun 18 2023 at 11:50):

Maybe double check before lake exe cache get && lake build that there are no running lean processes (e.g. with sudo pkill lake lean)?

Scott Morrison (Jun 18 2023 at 11:50):

Sorry, I'm running out of ideas here and telling you the emergency measures. :-)

Scott Morrison (Jun 18 2023 at 11:51):

If still no luck, could you confirm that git status says you are on master with no local changes?

Geno Racklin Asher (Jun 18 2023 at 12:08):

Hmm, still the same issue even after all that. I'm stumped honestly - maybe it's a windows issue? I might try again later when I'm at my linux machine.

Patrick Massot (Jun 18 2023 at 16:52):

Two weeks ago at MSRI we did have completely random failure like this on Windows machines.

Mauricio Collares (Jun 19 2023 at 08:04):

Depending on the Lake version, this could be because Git for Windows enables autocrlf (line ending conversion) by default. Try running git config --global core.autocrlf false on the command line and re-cloning the project from scratch. This shouldn't be a problem starting from the June 1st nightly (https://github.com/leanprover/lake/pull/170), but MIL uses the May 31st nightly.

Patrick Massot (Jun 19 2023 at 08:58):

Very interesting, I'll update MIL's toolchain very soon.

Last updated: Dec 20 2023 at 11:08 UTC