windows recompiling

Stream: general

[Jeremy Avigad]

I recently installed Lean 3.4.2 from binaries on a Windows laptop, but I noticed that whenever I opened a file in VS code, the yellow bars stuck around for a while. On investigating, I came across a problem I have come across before. When I went to the lean-3.4.2-windows folder and typed lean --make, it would compile a bunch of files. If I did it again, it would compile some more. If I typed lean --make yet again, it would go back and recompile the first set, and cycle back and forth.

The only way I could break the cycle was to delete all the .olean files and do a fresh lean --make. After that, subsequent lean --makes were a no-op.

Has anyone else come across this problem? I told my students they could install Lean from the binaries, so I will warn them and ask them to let me know if they see funny behavior with the yellow bars.

[Kenny Lau]

https://gist.github.com/kckennylau/611cc453c67df074ad492b4939ddd356

[Kenny Lau]

@Jeremy Avigad this is how I build Lean

[Jeremy Avigad]

Thanks. I know that I can build Lean from source, but I think it is easier for my students to install the binary, even if it means that they should delete all the .olean files and recompile.

[Patrick Massot]

@Jeremy Avigad I know nothing about Windows (the last one I used was Windows 98). How do you delete all olean with Windows?

[Rob Lewis]

@Neil Strickland posted about a Windows installer recently. https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/cheap.20Windows.20install/near/156729004

[Rob Lewis]

This doesn't directly address your problem, but it could work around it.

[Jeremy Avigad]

@Patrick Massot I was using an MSYS terminal, so I used a bash command. But I had to Google to find it: https://askubuntu.com/questions/377438/how-can-i-recursively-delete-all-files-of-a-specific-extension-in-the-current-di

Google also tells me that del /S *.olean should work from a command prompt.

@Rob Lewis Thanks. I'll post links to both Kenny's instructions and Neil's web page.

[Floris van Doorn]

I sometimes use git clean -Xf. This removes all ignored files from your repository, like .olean files and _target. (Warning: if you omit the -X tag it will remove untracked files, which could be bad.)

[Jeremy Avigad]

Thanks. The point is well taken, but it won't work for the "install from binaries" folder -- it is not a git repo.

[Koundinya Vajjha]

(Warning: if you omit the -X tag it will remove untracked files, which could be bad.)

I have had first-hand experience of how bad this can be. Do not recommend it.