Zulip Chat Archive
Stream: new members
Topic: making a repo compatible with leanproject
Jalex Stark (May 27 2020 at 17:52):
This is probably a not-fun game of "guess which instructions i failed to follow"
I have a repo with a src folder and a leanpackage.toml in the top level directory.
On my local machine, I navigate to a folder which is not a git repo (and contains my other git repos in subfolders)
I run leanproject get https://github.com/jalex-stark/lean-at-MC2020.git
I use VSCode to open the lean-at-MC2020 folder, which has src and _target subfolders.
I open an arbitrary file in src/, and the Lean messages are full of errors that look like this:
invalid import: data.option.defs
excessive memory consumption detected at 'replace' (potential solution: increase memory consumption threshold)
Kevin Buzzard (May 27 2020 at 17:52):
Ctrl-shift-P Lean:Restart?
Kevin Buzzard (May 27 2020 at 17:53):
Wait -- you are supposed to have a leanpkg.toml not what you said
Bryan Gin-ge Chen (May 27 2020 at 17:53):
Also, I hope "I open an arbitrary file in src/" is short for "I open the lean-at-MC2020 folder in VS Code and then from there open an arbitrary file from src/"
Kevin Buzzard (May 27 2020 at 17:54):
Restarting Lean often fixes the excessive memory consumption errors
Jalex Stark (May 27 2020 at 17:54):
yes, the "open folder" bit was two steps earlier,
Johan Commelin (May 27 2020 at 17:54):
Bryan, see the line before.
Jalex Stark (May 27 2020 at 17:54):
i restarted lean and am waiting at an orange bar
Bryan Gin-ge Chen (May 27 2020 at 17:54):
Ah, OK. Sorry I missed that.
I looked at https://github.com/jalex-stark/lean-at-MC2020 and it seems OK, though you shouldn't need to commit leanpkg.path.
Kevin Buzzard (May 27 2020 at 17:55):
Did leanproject get all your mathlib oleans?
Rob Lewis (May 27 2020 at 17:56):
I don't think leanproject get downloads a mathlib cache, does it? Isn't it just git clone?
Jalex Stark (May 27 2020 at 17:56):
I think yes.
jstark@Jalexs-MBP lean-projects % leanproject get https://github.com/jalex-stark/lean-at-MC2020.git
Cloning from https://github.com/jalex-stark/lean-at-MC2020.git
configuring Mathcamp2020 0.1
mathlib: cloning https://github.com/leanprover-community/mathlib to _target/deps/mathlib
> git clone https://github.com/leanprover-community/mathlib _target/deps/mathlib
Cloning into '_target/deps/mathlib'...
remote: Enumerating objects: 336, done.
remote: Counting objects: 100% (336/336), done.
remote: Compressing objects: 100% (216/216), done.
remote: Total 50297 (delta 197), reused 165 (delta 119), pack-reused 49961
Receiving objects: 100% (50297/50297), 21.67 MiB | 6.16 MiB/s, done.
Resolving deltas: 100% (38738/38738), done.
> git checkout --detach c812ebebde49c0409c5a93e41e3a36431f72b0a5 # in directory _target/deps/mathlib
HEAD is now at c812ebeb feat(category_theory/abelian): abelian categories (#2817)
Looking for local mathlib oleans
Found local mathlib oleans
Rob Lewis (May 27 2020 at 17:56):
Disclaimer, I've never used leanproject get.
Kevin Buzzard (May 27 2020 at 17:57):
Your project works fine for me Jalex
Jalex Stark (May 27 2020 at 17:57):
hmm okay maybe the local mathlib oleans that leanproject finds are bad
Jalex Stark (May 27 2020 at 17:58):
probably reinstalling the whole elan toolchain will be enough
Rob Lewis (May 27 2020 at 17:58):
That sounds excessive...
Jalex Stark (May 27 2020 at 17:58):
but maybe I'll think for a moment about whether there's an easier solution
Rob Lewis (May 27 2020 at 17:58):
leanproject get -f?
Rob Lewis (May 27 2020 at 17:58):
leanproject get-mathlib-cache -f?
Jalex Stark (May 27 2020 at 17:59):
% leanproject get-mathlib-cache -f
Usage: leanproject get-mathlib-cache [OPTIONS]
Try 'leanproject get-mathlib-cache -h' for help.
Error: no such option: -f
Bryan Gin-ge Chen (May 27 2020 at 17:59):
--force?
Kevin Buzzard (May 27 2020 at 17:59):
leanproject get jalex-stark/lean-at-MC2020
cd lean-at-MC2020/
code .
works for me, but as you pointed out I have
Looking for local mathlib oleans
Looking for remote mathlib oleans
Trying to download https://oleanstorage.azureedge.net/mathlib/c812ebebde49c0409c5a93e41e3a36431f72b0a5.tar.xz to /home/buzzard/.mathlib/c812ebebde49c0409c5a93e41e3a36431f72b0a5.tar.xz
100%|███████████████████████████████████████████████████████████████████████████████████████████████████████████████████| 21.9M/21.9M [00:03<00:00, 5.56MiB/s]
Found mathlib oleans at https://oleanstorage.azureedge.net/mathlib/
Kevin Buzzard (May 27 2020 at 17:59):
Just delete your local oleans
Jalex Stark (May 27 2020 at 17:59):
% leanproject get-mathlib-cache --force
Usage: leanproject get-mathlib-cache [OPTIONS]
Try 'leanproject get-mathlib-cache -h' for help.
Error: no such option: --force
Rob Lewis (May 27 2020 at 18:00):
leanproject --help says
-f, --force-download Download olean cache without looking for a local
version.
Jalex Stark (May 27 2020 at 18:00):
okay, i guess i have a stale leanproject
Jalex Stark (May 27 2020 at 18:00):
(so i should reinstall the whole elan toolchain now?)
Rob Lewis (May 27 2020 at 18:01):
It also implies leanproject get is just git clone so maybe that's not trustworthy.
Bryan Gin-ge Chen (May 27 2020 at 18:01):
elan and leanproject are separate.
Yury G. Kudryashov (May 27 2020 at 18:01):
Cached oleans are in ~/.mathlib/git-hash.tar.(bz2_or_xz)
Yury G. Kudryashov (May 27 2020 at 18:02):
You can manually delete some of these files.
Bryan Gin-ge Chen (May 27 2020 at 18:02):
pip install --upgrade mathlibtools should upgrade leanproject to the latest, which is 0.0.8.
Jalex Stark (May 27 2020 at 18:02):
Thanks Yury!
Bryan Gin-ge Chen (May 27 2020 at 18:02):
Maybe pip3 depending on your python setup.
Jalex Stark (May 27 2020 at 18:02):
oh okay it's leanproject -f get-mathlib-cache, not leanproject get-mathlib-cache -f
Jalex Stark (May 27 2020 at 18:20):
i'm still in a sad state after forcing the mathlib cache, so i'll go delete oleans manually and then do leanproject up
Kevin Buzzard (May 27 2020 at 18:21):
delete the project and re-clone
Kevin Buzzard (May 27 2020 at 18:21):
maybe?
Jalex Stark (May 27 2020 at 18:23):
when i do that it still finds local oleans
Jalex Stark (May 27 2020 at 18:23):
so i have oleans somewhere sticky
Kevin Buzzard (May 27 2020 at 18:23):
What exactly is your problem at this point? Your repo worked fine for me
Kevin Buzzard (May 27 2020 at 18:23):
(although you should remove the path file)
Jalex Stark (May 27 2020 at 18:25):
I added a line import data.nat.basic to the header of a .lean file in src/ and it went back to the error message about memory
Kevin Buzzard (May 27 2020 at 18:25):
I can't reproduce :-(
Jalex Stark (May 27 2020 at 18:26):
you mean you took the same action and didn't get a catastrophic result?
Jalex Stark (May 27 2020 at 18:26):
(or the action was underspecified so you didn't try?)
Kevin Buzzard (May 27 2020 at 18:26):
I added import data.nat.basic to function_equation.lean and nothing bad happened
Jalex Stark (May 27 2020 at 18:27):
thanks, that's great news
Kevin Buzzard (May 27 2020 at 18:28):
If the issue is oleans, then this can definitely be fixed by firstly removing the offending local oleans from .mathlib and then recloning the project with leanproject and verifying that they're downloaded from the azure site
Jalex Stark (May 27 2020 at 18:29):
yep, I agree, that's next on my queue
Kevin Buzzard (May 27 2020 at 18:30):
buzzard@bob:~/.mathlib$ md5sum c812ebebde49c0409c5a93e41e3a36431f72b0a5.tar.xz
b28742d6de88f719309e235138d12124 c812ebebde49c0409c5a93e41e3a36431f72b0a5.tar.xz
FWIW
Jalex Stark (May 27 2020 at 18:36):
It looks like i succeeded at replacing my oleans!
jstark@Jalexs-MBP .mathlib % md5sum c812ebebde49c0409c5a93e41e3a36431f72b0a5.tar.xz
b28742d6de88f719309e235138d12124 c812ebebde49c0409c5a93e41e3a36431f72b0a5.tar.xz
Patrick Massot (May 27 2020 at 19:05):
Jalex Stark said:
oh okay it's
leanproject -f get-mathlib-cache, notleanproject get-mathlib-cache -f
I'm sorry about that. This is a limitation of the cli building tool I'm using. The -f option is a shared option used by many command hence it must come before the command name.
Jalex Stark (May 27 2020 at 19:07):
it seems like a fine choice to me! Rob just made an incorrect guess about the right command to use
Jalex Stark (May 27 2020 at 19:51):
okay, i'm still in a bad state when i do leanproject new test then open the folder test in VSCode, start up a new .lean file, and write import tactic as a header. I'm going to go reinstall everything.
Last updated: Dec 20 2023 at 11:08 UTC