Zulip Chat Archive

Stream: new members

Topic: Check Project is Error-Free


view this post on Zulip Marcus Rossel (Mar 31 2021 at 12:04):

Is there a way to have Lean tell me, whether my project contains any errors/sorrys?
I use Lean in VS Code and I don't know how I can be sure, that all files are checked and error/sorry-free.
I'm hoping there's some invocation from the command line that plainly says something like "0 errors / 0 sorrys".

view this post on Zulip Johan Commelin (Mar 31 2021 at 12:06):

leanproject build

view this post on Zulip Johan Commelin (Mar 31 2021 at 12:07):

or lean --make src/

view this post on Zulip Johan Commelin (Mar 31 2021 at 12:07):

Of course you can also grep sorry if you want to quickly find sorrys, but that won't find errors :smile:

view this post on Zulip Marcus Rossel (Mar 31 2021 at 12:08):

Ahhh, how can I avoid checking all of Mathlib in the process? :sweat_smile:

view this post on Zulip Johan Commelin (Mar 31 2021 at 12:09):

leanproject get-mathlib-cache

view this post on Zulip Marcus Rossel (Mar 31 2021 at 12:13):

Johan Commelin said:

leanproject get-mathlib-cache

Hmmm, that didn't work for me:

marcus@Code: ls
README.md   _target     leanpkg.path    leanpkg.toml    src

marcus@Code: leanproject get-mathlib-cache
Looking for local mathlib oleans
Found local mathlib oleans

marcus@Code: leanproject build
Building project Code
configuring Code 0.1
mathlib: trying to update _target/deps/mathlib to revision 22e34370e62f4338d73889dc93094829439eb420
> git checkout --detach 22e34370e62f4338d73889dc93094829439eb420    # in directory _target/deps/mathlib
HEAD is now at 22e34370e feat(algebra/big_operators/basic): lemmas prod_range_add, sum_range_add (#6484)
> lean --make src
/Users/marcus/Code/_target/deps/mathlib/src/tactic/scc.lean: parsing at line
```

view this post on Zulip Marcus Rossel (Mar 31 2021 at 12:14):

Do I need to let it do Mathlib once, and then I'm set for future builds?

view this post on Zulip Johan Commelin (Mar 31 2021 at 12:14):

did you modify files in mathlib, by chance?

view this post on Zulip Marcus Rossel (Mar 31 2021 at 12:14):

Johan Commelin said:

did you modify files in mathlib, by chance?

Not that I'm aware of.

view this post on Zulip Johan Commelin (Mar 31 2021 at 12:15):

try lean --old --make src/

view this post on Zulip Johan Commelin (Mar 31 2021 at 12:15):

that should trick lean into using the oleans from the cache

view this post on Zulip Scott Morrison (Mar 31 2021 at 12:15):

leanproject -f get-mathlib-cache perhaps?

view this post on Zulip Scott Morrison (Mar 31 2021 at 12:15):

(And/or nuke your _target directory in case you did accidentally modify mathlib itself)

view this post on Zulip Marcus Rossel (Mar 31 2021 at 12:16):

Johan Commelin said:

try lean --old --make src/

Ok, that simply completed without any output. I'm guessing that means everything is fine? ¯\_(ツ)_/¯

view this post on Zulip Scott Morrison (Mar 31 2021 at 12:16):

Well... I would say that anytime you've run it with --old you don't know anything. :-)

view this post on Zulip Scott Morrison (Mar 31 2021 at 12:17):

That is only really intended to speed things up while hacking around, not for being sure everything is working.

view this post on Zulip Kevin Buzzard (Mar 31 2021 at 12:17):

I would just remove the entire _target directory and leanproject build in the root of your project.

view this post on Zulip Scott Morrison (Mar 31 2021 at 12:19):

Don't you need leanproject get-mathlib-cache before the leanproject build?

view this post on Zulip Marcus Rossel (Mar 31 2021 at 12:19):

So I removed _target but still get:

marcus@Code: leanproject build
Building project Code
configuring Code 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: 1223, done.
remote: Counting objects: 100% (1223/1223), done.
remote: Compressing objects: 100% (615/615), done.
remote: Total 136788 (delta 797), reused 904 (delta 606), pack-reused 135565
Receiving objects: 100% (136788/136788), 58.45 MiB | 8.70 MiB/s, done.
Resolving deltas: 100% (107855/107855), done.
> git checkout --detach 22e34370e62f4338d73889dc93094829439eb420    # in directory _target/deps/mathlib
HEAD is now at 22e34370e feat(algebra/big_operators/basic): lemmas prod_range_add, sum_range_add (#6484)
configuring Code 0.1
mathlib: trying to update _target/deps/mathlib to revision 22e34370e62f4338d73889dc93094829439eb420
> git checkout --detach 22e34370e62f4338d73889dc93094829439eb420    # in directory _target/deps/mathlib
HEAD is now at 22e34370e feat(algebra/big_operators/basic): lemmas prod_range_add, sum_range_add (#6484)
> lean --make src
/Users/marcus/Library/Mobile Documents/com~apple~CloudDocs/Bachelorarbeit/Code/_target/deps/mathlib/src/...

view this post on Zulip Scott Morrison (Mar 31 2021 at 12:19):

Or may it does that step automatically if _target is entirely missing.

view this post on Zulip Scott Morrison (Mar 31 2021 at 12:20):

Yeah, that looks like it didn't attempt to download oleans. Try my suggestion.

view this post on Zulip Kevin Buzzard (Mar 31 2021 at 12:20):

Scott's suggestion should do it now -- break out the build, get-mathlib-cache, and then build again.

view this post on Zulip Marcus Rossel (Mar 31 2021 at 12:23):

Ok, removing _target and then running leanproject build worked.
It still did whatever it was doing in my last post, but that only took like 1min and now I just get:

marcus@Code: leanproject build
Building project Code
configuring Code 0.1
mathlib: trying to update _target/deps/mathlib to revision 22e34370e62f4338d73889dc93094829439eb420
> git checkout --detach 22e34370e62f4338d73889dc93094829439eb420    # in directory _target/deps/mathlib
HEAD is now at 22e34370e feat(algebra/big_operators/basic): lemmas prod_range_add, sum_range_add (#6484)
> lean --make src

Thank you all :)


Last updated: May 12 2021 at 05:19 UTC