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, not leanproject 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