Zulip Chat Archive

Stream: new members

Topic: Peter Nelson

Peter Nelson (Aug 12 2020 at 15:48):

Hi everyone! I'm a combinatorialist trying to get my head around using lean, and my first problem is that I'm running into some install issues and not technically competent enough to fix them. I'm wondering if someone is able to help me with this?

Alex J. Best (Aug 12 2020 at 15:50):

We can try and help, the more detail you give us the better, which instructions did you follow? Which operating system and what errors are you seeing?

Peter Nelson (Aug 12 2020 at 15:53):

Thanks! I'm using mac os, and installed by typing the command at https://leanprover-community.github.io/install/macos.html . I also have vscode with the extension; I'm getting a lean infoview on the right etc. But when I import the project from https://github.com/bryangingechen/lean-matroids , I get a large number of errors - unknown identifier, uses sorry, etc

Peter Nelson (Aug 12 2020 at 15:54):

I suspect the problem is with my version, which shows as 3.18.4 on the command line and when I include the version code snippet on vscode. I probably want something else, but don't know how to update or change

Bryan Gin-ge Chen (Aug 12 2020 at 15:56):

Ah, that code is pretty old and relies on an old version of Lean and mathlib. However, running leanproject get bryangingechen/lean-matroids should check out a usable copy.

Alex J. Best (Aug 12 2020 at 15:56):

How are you importing the project? And how did you get the https://github.com/bryangingechen/lean-matroids project. Have you read https://leanprover-community.github.io/install/project.html

Mario Carneiro (Aug 12 2020 at 15:56):

do you have leanproject? It should handle getting the version right

Peter Nelson (Aug 12 2020 at 15:56):

yes, I used leanproject, but with the github url

Peter Nelson (Aug 12 2020 at 15:57):

I will try what Bryan said - if leanproject is supposed to get the version right, is there still something that's not working, though?

Bryan Gin-ge Chen (Aug 12 2020 at 15:59):

I just tried running leanproject get https://github.com/bryangingechen/lean-matroids in a new directory and then opened the lean-matroids directory in VS Code and got it to work.

Bryan Gin-ge Chen (Aug 12 2020 at 15:59):

Make sure you open the entire directory in VS Code, not just an individual file.

Alex J. Best (Aug 12 2020 at 15:59):

Same as Bryan, the following works for me (on osx):

+alex:~ 🐌  leanproject get bryangingechen/lean-matroids
Please provide password for encrypted SSH private key:
Cloning from git@github.com:bryangingechen/lean-matroids.git
Enter passphrase for key '/Users/alex/.ssh/id_rsa':
configuring lean-matroids 0.1
mathlib: cloning https://github.com/leanprover-community/mathlib to _target/deps/mathlib
> mkdir -p _target/deps/mathlib
> git clone https://github.com/leanprover-community/mathlib _target/deps/mathlib
Cloning into '_target/deps/mathlib'...
remote: Enumerating objects: 317, done.
remote: Counting objects: 100% (317/317), done.
remote: Compressing objects: 100% (251/251), done.
remote: Total 68346 (delta 142), reused 137 (delta 50), pack-reused 68029
Receiving objects: 100% (68346/68346), 30.02 MiB | 18.88 MiB/s, done.
Resolving deltas: 100% (52937/52937), done.
> git checkout --detach 827e78b1638868734de786baac70b5d3f1d5118e    # in directory _target/deps/mathlib
HEAD is now at 827e78b16 feat(lint): avoid Travis error when declarations are renamed (#1771)
Looking for local mathlib oleans
Looking for remote mathlib oleans
Trying to download https://oleanstorage.azureedge.net/mathlib/827e78b1638868734de786baac70b5d3f1d5118e.tar.xz to /Users/alex/.mathlib/827e78b1638868734de786baac70b5d3f1d5118e.tar.xz
100%|████████████████████████████████████████████████████████████| 15.9M/15.9M [00:00<00:00, 21.5MiB/s]
Found mathlib oleans at https://oleanstorage.azureedge.net/mathlib/
+alex:~ 🐌 cd lean-matroids/
+alex:~/lean-matroids (master) 🐌 code .

Peter Nelson (Aug 12 2020 at 16:01):

ok, I did what Bryan suggested, and there is a massive improvement, however I get exactly one error: matroid.lean:1051:0
declaration 'matroid.indep_of_rank' uses sorry

Peter Nelson (Aug 12 2020 at 16:02):

oh, now I see that lemma is a work in progress - presumably that's not a problem then

Peter Nelson (Aug 12 2020 at 16:02):

thanks for all your help!

Bryan Gin-ge Chen (Aug 12 2020 at 16:03):

Yeah, I never finished those proofs, unfortunately.

By the way, the fintype2 branch has slightly better Lean code with a few more comments (though it doesn't quite get as far as the master branch). You can inspect that branch by running (from within lean-matroids):

git checkout fintype2
leanproject get-mathlib-cache

(If you have the project open in VS Code then you'll have to restart Lean by hitting ctrl+shift+P and searching for "Lean: Restart")

Last updated: Dec 20 2023 at 11:08 UTC