Zulip Chat Archive

Stream: general

Topic: random recompiling

Kenny Lau (Apr 06 2020 at 16:41):

I'm using VSCode on Windows and sometimes after I open the source code of some dependencies somehow Lean thinks I've changed the source code and has to recompile everything. I remember Mario explained it before, but I forgot the explanation.

Kenny Lau (Apr 06 2020 at 16:41):

Maybe can we set up an FAQ or something?

Sebastien Gouezel (Apr 06 2020 at 16:52):

This also happens to me sometimes (also on windows). In this case, I quit Vscode and restart it, and everything is back to normal.

Kenny Lau (May 24 2020 at 10:44):

I feel like this is stopping me from peeking into definitions and printing definitions

Kenny Lau (May 24 2020 at 10:44):

Every time I have to do one of those, I need to ~~sell my soul to the devil~~ restart the Lean server

Kenny Lau (May 24 2020 at 10:45):

This is very annoying.

Bryan Gin-ge Chen (May 24 2020 at 11:11):

@Wojciech Nawrocki @Gabriel Ebner any idea what might be going on or how to debug this?

Wojciech Nawrocki (May 24 2020 at 13:20):

I'm trying to reproduce this now but I'm on Linux and it doesn't seem to happen. I was hoping that we'd handled the Windows differences by stripping the CR from CRLF line endings but there might be something else. Could you give me an example mathlib file that causes the recompilation when opened?

Wojciech Nawrocki (May 24 2020 at 16:55):

Okay, I think I can see the problem. Steps to reproduce:

Restart Lean
Open a file foo.lean which imports bar.lean
Make a change to foo.lean. Lean only recompiles the changed function
Now open bar.lean via Vscode goto definition
Make the same change to foo.lean. Lean recompiles the whole file now?!

I can see this on Linux, and I checked that the Windows CRLF clearing works fine, so most likely it's not Windows-specific

Kevin Buzzard (May 24 2020 at 16:58):

I get this sometimes on Linux and you're describing my usual workflow

Kevin Buzzard (May 24 2020 at 17:00):

I'm forever hopping to other files to read definitions of things, I find mathlib easier to read than hovering over a definition when doing algebra, because the hover gives you ten definitions of things which are rings and modules and algebras and implicit

Ryan Lahfa (May 24 2020 at 17:01):

Maybe it's a bug in the VSCode extension or VSCode is updating silently the times/contents of the file :/

Wojciech Nawrocki (May 24 2020 at 17:05):

I think it's more likely a bug in the server's invalidation logic. There's some code to explicitly prevent rebuilding reverse dependencies of newly opened files if the on-disk contents are the same but it doesn't seem to always work

Ryan Lahfa (May 24 2020 at 17:12):

Wojciech Nawrocki said:

I think it's more likely a bug in the server's invalidation logic. There's some code to explicitly prevent rebuilding reverse dependencies of newly opened files if the on-disk contents are the same but it doesn't seem to always work

In that case, can you reproduce it without VSCode?

Wojciech Nawrocki (May 24 2020 at 17:15):

It should be possible but really annoying, since you'd have to manually start a Lean server and send a bunch of JSON sync commands to it

Johan Commelin (May 24 2020 at 17:17):

There is the new python library for doing that

Ryan Lahfa (May 24 2020 at 17:17):

Wojciech Nawrocki said:

It should be possible but really annoying, since you'd have to manually start a Lean server and send a bunch of JSON sync commands to it

Isn't a simple way to just do monitor of one file and recompile smartly so that we can see if it's indeed the Lean server which is doing some improper cache invalidation, or VSCode

Bryan Gin-ge Chen (May 24 2020 at 17:20):

Maybe trying to reproduce it in emacs is easier.

Bryan Gin-ge Chen (May 24 2020 at 18:00):

I haven't been able to reproduce this yet, but I'm on macOS and maybe I'm not doing it right.

Here are the contents of my bar.lean:

lemma blah : true := trivial

Here are the contents of my foo.lean:

import system.io
import bar

run_cmd do tactic.unsafe_run_io (io.proc.sleep 1).

run_cmd do tactic.unsafe_run_io (io.proc.sleep 1).

run_cmd do tactic.unsafe_run_io (io.proc.sleep 1).

run_cmd do tactic.unsafe_run_io (io.proc.sleep 1).

run_cmd do tactic.unsafe_run_io (io.proc.sleep 1).

run_cmd do tactic.unsafe_run_io (io.proc.sleep 1).

run_cmd do tactic.unsafe_run_io (io.proc.sleep 1).

run_cmd do tactic.unsafe_run_io (io.proc.sleep 1).

run_cmd do tactic.unsafe_run_io (io.proc.sleep 1).

/- comment to prevent crash from https://github.com/leanprover-community/lean/issues/85 -/

All of the following is done with VS Code and Lean 3.14.0.

First, I restart Lean and open foo.lean. The whole file recompiles, which takes 10 seconds or so. Then I add a comment near the 3rd to last run_cmd. The entire file recompiles when I make my first edit, but if I make more edits, the orange bars only appear below where I edit.

Next, I right click on import bar and go to definition so that bar.lean appears. Without making any changes to bar.lean, I return to foo.lean. Then I add a comment again near the bottom of the file. I haven't been seeing the entirety of foo.lean recompiling here -- the orange bars still only appear below where I edit. Same behavior if I keep making more edits.

Wojciech Nawrocki (May 24 2020 at 18:17):

@Bryan Gin-ge Chen I can reproduce it with just these two files (in vscode, on linux). On the other hand, this part

The entire file recompiles when I make my first edit

is not true for me

Bryan Gin-ge Chen (May 24 2020 at 19:17):

@Wojciech Nawrocki I just tested the pair of files on Windows and while foo.lean doesn't fully recompile when I make my first edit, I also don't see it fully recompile after I switch back and forth from bar.lean. Very puzzling...

Gabriel Ebner (May 25 2020 at 12:29):

Just skimming over this issue and the PR. This seems kind of expected. We only store one copy of a module, either from olean or from source. (This is pretty important to keep memory usage down.) So when you open a dependency, lean will load the file from source. The problem should begin when you get back to the original file and make a change there, then it will wait for the olean of the dependency to be ready.

Reid Barton (May 25 2020 at 12:48):

Suppose I open A and B in my editor (emacs if it matters) where B imports A. I edit the buffer of A, but don't save it. If I now switch to B, will lean use my modifications to A (and therefore recompile possibly a lot of things)?

Reid Barton (May 25 2020 at 12:48):

I imagined I could avoid this by not saving A, but maybe this was a bad assumption.

Gabriel Ebner (May 25 2020 at 12:49):

Yes, you don't even need to save A!

Reid Barton (May 25 2020 at 12:49):

Good to know. I should try out this --old flag then.

Reid Barton (May 25 2020 at 12:50):

However, because of the switch to using hashes for recompilation detection, I should be able to undo my changes to A and then lean will switch back to using the oleans, right?

Wojciech Nawrocki (May 25 2020 at 13:28):

@Reid Barton Afaik in this scenario, if you want to have A open and things like tactic/goal states visible, Lean has to compile A from source. This is because the .oleans do not store this information. If you then make a change to the A buffer (even without saving), Lean will recompile the file and overwrite the environment stored in-memory. Undoing the change cannot just pull the old information from the olean since it's not there, so Lean has to recompile again.

Wojciech Nawrocki (May 25 2020 at 13:29):

The above behaviour is fine in my view. What's not fine is that the act of simply opening the source corresponding to an already-loaded .olean forces a recompilation of the environment for that module and also all its reverse dependencies.