MIL is broken?

Stream: new members

[Geno Racklin Asher]

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]

@Jeremy Avigad

[Patrick Massot]

No idea what happened but I think I fixed it.

[Geno Racklin Asher]

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]

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]

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]

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

[Geno Racklin Asher]

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

[Scott Morrison]

What did lake exe cache get output?

[Scott Morrison]

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]

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]

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]

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]

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

[Scott Morrison]

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

[Geno Racklin Asher]

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]

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

[Mauricio Collares]

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]

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