Zulip Chat Archive
Stream: general
Topic: Lots of errors in mathlib, is this normal?
YH (Dec 09 2019 at 17:11):
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.
Mario Carneiro (Dec 09 2019 at 17:12):
You probably have outdated .oleans
Mario Carneiro (Dec 09 2019 at 17:12):
you might also try restarting the lean server in case it's bad vscode caching
YH (Dec 09 2019 at 17:26):
What do I do in these cases? is restarting vscode enough? And how about the .olean ?
YH (Dec 09 2019 at 17:29):
Is purge_olean.sh* for this?
Johan Commelin (Dec 09 2019 at 17:55):
@YH Are you working on mathlib directly, or on a project that has mathlib as dep?
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.
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
Johan Commelin (Dec 09 2019 at 17:59):
That will give you a reasonable recent mathlib (yesterdays' in fact), with precompiled olean files
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.
YH (Dec 09 2019 at 18:00):
How do I checkout?
YH (Dec 09 2019 at 18:00):
Oh git checkout
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.
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
Kevin Buzzard (Dec 09 2019 at 18:32):
close and re-open VS Code?
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
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: Dec 20 2023 at 11:08 UTC