william (hi!)

Stream: new members

[william]

Hi all,

I'm a bachelor student at Uni Bonn. I'm really new to Lean and I'm very interested in this language, although I have had a bit of experiences with coq in the past. I was introduced to Lean by a professor, with whom I'm doing my thesis and I'm interested in formalizing the results that we've done in the thesis using Lean. Now I'm using vscode for Lean and somehow I often get the following error code "The Lean Server has stopped processing this file". I'd really appreciate it if someone could help me out on this.

And I apologize if I might be a little bit too picky, but is there any way to stop Lean from type-checking everything in real-time? I'm pretty used to how things worked in coq where I had to press ctrl+enter to evaluate one line. Thank you!

[Johan Commelin]

Welcome!

[Johan Commelin]

Just to check: can you please confirm that you have a local cache for mathlib? (I assume you are working on (top of) mathlib.)

[Johan Commelin]

Do you get that error at random moments? Or is there some pattern? (Like just after pulling from github.)

[william]

@Johan Commelin thank you! I'm still a newbie when it comes to this, how do I check if I have a local cache?
And to answer your second question, yes there seems to be a pattern, at least the one I'm noticing is that when I do "#print Nat.rec" (or any other _.rec) the lean server stops processing and I need to restart the file

[Johan Commelin]

Could you please run lake exe cache get in the root dir of your project?

[Johan Commelin]

If that starts downloading things, then you didn't have a cache.

[william]

This is what I get,

Attempting to download 1 file(s)
Downloaded: 0 file(s) [attempted 1/1 = 100%] (0% success)
Warning: some files were not found in the cache.
This usually means that your local checkout of mathlib4 has diverged from upstream.
If you push your commits to a branch of the mathlib4 repository, CI will build the oleans and they will be available later.
Decompressing 4449 file(s)
unpacked in 252 ms

Does this mean I didn't have a cache? It's a little confusing since it says "Downloaded: 0 file(s)"

[Johan Commelin]

Yeah that means you already had the cache

[Johan Commelin]

It only tried to download cache for the file that you edited, but it didn't find a cache for that

[Johan Commelin]

Which version of mathlib are you on? And which version of the VScode extension for Lean 4?

[william]

The extension is of version v0.0.144, and I sadly have no idea how to check which version of mathlib I'm on. How to do this? Thank you

[Johan Commelin]

Please paste the top 5 lines of the output of git log

[Johan Commelin]

Or maybe of git show master, that might be more useful

[Jakob von Raumer]

And I apologize if I might be a little bit too picky, but is there any way to stop Lean from type-checking everything in real-time?

Pretty sure there was an option to just check the visible code. Not sure where it has gone in the current version of the extension?

[Johan Commelin]

I think it existed in the Lean 3 extension.