mathematics in Lean

Stream: new members

[Alexandre Rademaker]

I followed the step-by-step from the introduction. but almost all examples when I loaded in VS Code, I got a memory error in the import statement. I am using Lean 3.18.4. I did one extra step running lean --make --memory 6000 in the mathematics_in_lean directory.

[Alexandre Rademaker]

I see errors like this too

imported file '/Users/ar/Sites/MD-2020/mathematics_in_lean/_target/deps/mathlib/src/data/int/basic.lean' uses sorry

[Bryan Gin-ge Chen]

These memory errors are because the VS Code extension is trying to compile mathlib. You should run leanproject get-mathlib-cache to get the precompiled binary files.

[Alexandre Rademaker]

I removed the directory, did again the setup and executed the leanproject get-mathlib-cache. But again, I am getting

invalid import: data.option.defs
excessive memory consumption detected at 'replace' (potential solution: increase memory consumption threshold)

[Bryan Gin-ge Chen]

For some reason, your VS code extension is still trying to compile mathlib. From what I can tell, Mathematics in Lean is still on Lean 3.17.1. If you're using elan as recommended, then the VS Code extension should automatically use the correct version of Lean. The only thing I can think of at the moment is that you may have to either close and re-open VS Code or hit cmd+P and search for "restart Lean" to (1) get the correct version of Lean to run and (2) get Lean to look for the new olean files.

[Alexandre Rademaker]

But my command above lean --make --memory 6000 shouldn't be able to recompile everything with Lean 3.18.4?

[Bryan Gin-ge Chen]

If you're using elan, the version of lean that's run when you enter that will be the one which is specified in leanpkg.toml, which is 3.17.1 (unless you've edited it or run leanproject up).

[Alexandre Rademaker]

I edited the toml changing to 3.18.4

[Bryan Gin-ge Chen]

And you didn't get any errors when you ran lean --make --memory 6000?

[Bryan Gin-ge Chen]

Did you edit the mathlib commit too in leanpkg.toml? The one specified there might not be compatible with 3.18.4.

[Bryan Gin-ge Chen]

An easier way to upgrade the version of mathlib that a Lean project depends on is to run leanproject up. This will also download precompiled mathlib for you so you don't have to wait for lean --make to finish.

[Alexandre Rademaker]

No, i didn't changed the commit hash for mathlib... I got some warnings but the process finished.

[Bryan Gin-ge Chen]

Are you sure they were just warnings and not errors? Errors will cause olean files not to be built, which will then lead to VS Code trying to rebuild the missing files (which will probably lead to errors again).

[Alexandre Rademaker]

Hum, just checking now https://leanprover-community.github.io/install/macos.html and it seems that use the lean from brew may not be a good idea.

[Bryan Gin-ge Chen]

Yes, it's not recommended at the moment. We recommend using elan.

[Alexandre Rademaker]

I see many lines such

/Users/ar/Sites/MD-2020/mathematics_in_lean/examples/basics/unnamed_1319.lean:2:0: warning: imported file '/Users/ar/Sites/MD-2020/mathematics_in_lean/_target/deps/mathlib/src/algebra/order_functions.lean' uses sorry
...
/Users/ar/Sites/MD-2020/mathematics_in_lean/_target/deps/mathlib/src/analysis/calculus/iterated_deriv.lean:7:0: warning: imported file '/Users/ar/Sites/MD-2020/mathematics_in_lean/_target/deps/mathlib/src/linear_algebra/finsupp.lean' uses sorry

[Bryan Gin-ge Chen]

There was some discussion about replacing the homebrew version of Lean with elan recently.

[Bryan Gin-ge Chen]

The reason that those files are importing files with sorry is most likely that some transitive dependency had an error in it.

[Bryan Gin-ge Chen]

And that is ultimately due to trying to compile an older version of mathlib with a newer version of Lean.

[Alexandre Rademaker]

I see. OK, I will uninstall the brew version and try to follow the step-by-step suggested.

[Bryan Gin-ge Chen]

Feel free to ask again if you have any more trouble!

[Alexandre Rademaker]

thank you so much!

[Kevin Buzzard]

@Alexandre Rademaker don't edit the toml because mathlib is not backwards compatible so this might make your problems worse -- the designer of any package is only guaranteeing that it will compile with the exact version of lean and mathlib stated in the toml

[Alexandre Rademaker]

Thank you @Kevin Buzzard . In my case, the problem is that I didn't want to downgrade Lean to the previous version. I finally managed to have examples running with

[package]
name = "mathematics_in_lean_source"
version = "0.1"
lean_version = "leanprover-community/lean:3.18.4"
path = "src"

[dependencies]
mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "17c4651c593391462d55f7f990dc05e54ec8ee39"}

But I understood your point. I am doing something risky! You can't guarantee that code will work with Lean 3.18.4 and the commit 17c46... from mathlib!

[Alexandre Rademaker]

ps: I hope to experiment with elan in the next days... It seems that it is the solution to have more than one version of Lean available.

[Alexandre Rademaker]

I liked the magic in VS Code to open the files in the buffer once I click in the try it. It would be nice to have this option in the Emacs too! ;-)

I saw that you use a tryitfile parameter in the href tag! Somehow the VS Code can interpret it and use this information instead of open the web editor remotely.... But I don't know VS enough to going deep into it.

[Bryan Gin-ge Chen]

(The relevant part of the VS Code extension is in this file.)

[Scott Morrison]

Alexandre Rademaker said:

ps: I hope to experiment with elan in the next days... It seems that it is the solution to have more than one version of Lean available.

Yes, we try to encourage people to not install Lean at all, only elan, and let handle things from there.

[Scott Morrison]

One option, of course, is to propose a pull request to MiL (or any other project, I guess) that helpfully upgrades (and fixes all the resulting problems!) to the latest version.