Zulip Chat Archive

Stream: new members

Topic: mathematics in Lean


view this post on Zulip Alexandre Rademaker (Sep 04 2020 at 02:46):

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.

view this post on Zulip Alexandre Rademaker (Sep 04 2020 at 02:57):

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

view this post on Zulip Bryan Gin-ge Chen (Sep 04 2020 at 02:58):

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.

view this post on Zulip Alexandre Rademaker (Sep 04 2020 at 03:05):

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)

view this post on Zulip Bryan Gin-ge Chen (Sep 04 2020 at 03:10):

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.

view this post on Zulip Alexandre Rademaker (Sep 04 2020 at 03:12):

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

view this post on Zulip Bryan Gin-ge Chen (Sep 04 2020 at 03:14):

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).

view this post on Zulip Alexandre Rademaker (Sep 04 2020 at 03:15):

I edited the toml changing to 3.18.4

view this post on Zulip Bryan Gin-ge Chen (Sep 04 2020 at 03:16):

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

view this post on Zulip Bryan Gin-ge Chen (Sep 04 2020 at 03:17):

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

view this post on Zulip Bryan Gin-ge Chen (Sep 04 2020 at 03:17):

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.

view this post on Zulip Alexandre Rademaker (Sep 04 2020 at 03:18):

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

view this post on Zulip Bryan Gin-ge Chen (Sep 04 2020 at 03:18):

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).

view this post on Zulip Alexandre Rademaker (Sep 04 2020 at 03:19):

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.

view this post on Zulip Bryan Gin-ge Chen (Sep 04 2020 at 03:19):

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

view this post on Zulip Alexandre Rademaker (Sep 04 2020 at 03:20):

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

view this post on Zulip Bryan Gin-ge Chen (Sep 04 2020 at 03:21):

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

view this post on Zulip Bryan Gin-ge Chen (Sep 04 2020 at 03:21):

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

view this post on Zulip Bryan Gin-ge Chen (Sep 04 2020 at 03:22):

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

view this post on Zulip Alexandre Rademaker (Sep 04 2020 at 03:22):

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

view this post on Zulip Bryan Gin-ge Chen (Sep 04 2020 at 03:23):

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

view this post on Zulip Alexandre Rademaker (Sep 04 2020 at 03:23):

thank you so much!

view this post on Zulip Kevin Buzzard (Sep 04 2020 at 08:21):

@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

view this post on Zulip Alexandre Rademaker (Sep 04 2020 at 18:13):

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!

view this post on Zulip Alexandre Rademaker (Sep 04 2020 at 18:15):

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.

view this post on Zulip Alexandre Rademaker (Sep 04 2020 at 18:16):

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.

view this post on Zulip Bryan Gin-ge Chen (Sep 04 2020 at 18:30):

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

view this post on Zulip Scott Morrison (Sep 05 2020 at 01:57):

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.

view this post on Zulip Scott Morrison (Sep 05 2020 at 01:57):

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.


Last updated: May 15 2021 at 22:14 UTC