Check Project is Error-Free

Stream: new members

[Marcus Rossel]

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

[Johan Commelin]

leanproject build

[Johan Commelin]

or lean --make src/

[Johan Commelin]

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

[Marcus Rossel]

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

[Johan Commelin]

leanproject get-mathlib-cache

[Marcus Rossel]

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
```

[Marcus Rossel]

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

[Johan Commelin]

did you modify files in mathlib, by chance?

[Marcus Rossel]

Johan Commelin said:

did you modify files in mathlib, by chance?

Not that I'm aware of.

[Johan Commelin]

try lean --old --make src/

[Johan Commelin]

that should trick lean into using the oleans from the cache

[Scott Morrison]

leanproject -f get-mathlib-cache perhaps?

[Scott Morrison]

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

[Marcus Rossel]

Johan Commelin said:

try lean --old --make src/

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

[Scott Morrison]

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

[Scott Morrison]

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

[Kevin Buzzard]

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

[Scott Morrison]

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

[Marcus Rossel]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Kevin Buzzard]

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

[Marcus Rossel]

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