## 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?

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: May 14 2021 at 04:22 UTC