Zulip Chat Archive

Stream: general

Topic: Lots of errors in mathlib, is this normal?


view this post on Zulip YH (Dec 09 2019 at 17:11):

pasted image

I am looking at some lean files in mathlib, but it seems like lean gives a lot of errors like "unknown identifier '𝓝'". Is this normal? The files are never altered by me.

view this post on Zulip Mario Carneiro (Dec 09 2019 at 17:12):

You probably have outdated .oleans

view this post on Zulip Mario Carneiro (Dec 09 2019 at 17:12):

you might also try restarting the lean server in case it's bad vscode caching

view this post on Zulip YH (Dec 09 2019 at 17:26):

What do I do in these cases? is restarting vscode enough? And how about the .olean ?

view this post on Zulip YH (Dec 09 2019 at 17:29):

Is purge_olean.sh* for this?

view this post on Zulip Johan Commelin (Dec 09 2019 at 17:55):

@YH Are you working on mathlib directly, or on a project that has mathlib as dep?

view this post on Zulip YH (Dec 09 2019 at 17:57):

YH Are you working on mathlib directly, or on a project that has mathlib as dep?

I just opened some mathlib file directly (I grep'ed and opened) and I saw these error.

view this post on Zulip Johan Commelin (Dec 09 2019 at 17:59):

Ok, I see. The best thing might be to checkout lean-3.4.2 and then cache-olean --fetch

view this post on Zulip Johan Commelin (Dec 09 2019 at 17:59):

That will give you a reasonable recent mathlib (yesterdays' in fact), with precompiled olean files

view this post on Zulip Johan Commelin (Dec 09 2019 at 18:00):

Unless there is some stupid git tag polluting your system, in which case you might need to do something like git tag -D lean-3.4.2 first.

view this post on Zulip YH (Dec 09 2019 at 18:00):

How do I checkout?

view this post on Zulip YH (Dec 09 2019 at 18:00):

Oh git checkout

view this post on Zulip Bryan Gin-ge Chen (Dec 09 2019 at 18:04):

I just opened some mathlib file directly

Note also that you should always open the root directory of a Lean project (the one with leanpkg.toml), not individual files, as otherwise the Lean extension may not be able to find the correct path to dependencies.

view this post on Zulip YH (Dec 09 2019 at 18:07):

Oh OK. The problems are mostly solved. I opened the same file (after opening the root directory) and there is a lot less errors. The only errors left are (deterministic) timeout

view this post on Zulip Kevin Buzzard (Dec 09 2019 at 18:32):

close and re-open VS Code?

view this post on Zulip YH (Dec 09 2019 at 18:59):

close and re-open VS Code?

Still, this particular lemma always times out.
https://github.com/leanprover-community/mathlib/blob/master/src/topology/algebra/infinite_sum.lean#L635-L638

view this post on Zulip Kevin Buzzard (Dec 09 2019 at 19:07):

try finding it in mathlib and compiling it from the command line? I guess you could have changed the VS Code deterministic timeout parameter?


Last updated: May 14 2021 at 04:22 UTC