infoview failing on codespaces

Stream: lean4

[Floris van Doorn]

I just gave a tutorial on Lean4 and mathlib4 using Github Codespaces, and it worked well for most participants, but 2 participants ran into the following issue:
After Lean finished loading, the syntax highlighting, and mouse-over pop-ups would work correctly, but the infoview would show nothing, not even "No info found."
I tried the following, but none of them fixed the issue

• running Lean 4: Restart Server
• closing the infoview, and reopening with Lean 4 Infoview: Toggle.
• closing the tab, stopping the codespace instance, restarting the codespace instance and opening it up

Since the mouse-over pop-ups work, Lean is definitely doing something, and I don't actually know if this is an issue with Lean, codespaces, or an internet connection issue.
Does anyone have any ideas of things to try to fix this issue? I have the second part of the tutorial tomorrow, and it would be nice if I can fix it then on the affected laptops (if it didn't resolve by itself).

[Alex J. Best]

Is codespaces being accessed via a web browser? You could first ask them to try a different browser, and if not ask them to open the browser console and see if there are any obvious error messages there?

[Floris van Doorn]

Yes, it is indeed accessed via a browser. Checking the browser console is a good idea.

One potentially important tidbit: for one of the participants initially everything worked fine, but after a while the infoview stopped working. I don't know what they did in the meantime.

[Kevin Buzzard]

I just demand that my students install lean locally to avoid issues like this, although of course it would be great if we could get to the bottom of issues like this so that I wouldn't have to demand it :-)

[Floris van Doorn]

I would have expected way more people to struggle / fail on the installation instructions, so I'm happy I didn't choose that for a tutorial that is 3 hours or less.

[Kevin Buzzard]

I thought that Lean 4 was supposed to Just Work -- I guess the issue is mathlib oleans

[Floris van Doorn]

I had 1 participant actually installing Lean on their own machine, and he ran into the issue that lake was not in the PATH.
Are the Lean 4 installation (quickstart) instructions supposed to add Lean to your PATH automatically?

[Mario Carneiro]

elan-init.sh should do that

[Floris van Doorn]

and this is run if you hit "Install Lean using Elan" after getting the Lean4 VSCode extension?
Is there anything I can ask them to debug what went wrong for them?

[Adam Topaz]

Does it also update the path, or just update .profile?

[Adam Topaz]

I seem to remember having to source .profile at some point after installing elan, but maybe that’s just my imagination

[Sebastian Ullrich]

The VS Code extension is not actually dependent on PATH, it dfaults to $HOME/.elan/bin. So if the extension didn't work, that would be quite weird.

[Floris van Doorn]

the extension worked, AFAIK. The problem was running lake exe cache get in the terminal.

[Mauricio Collares]

In the VS Code terminal?

[Sebastian Ullrich]

I don't think the extension affects the VS Code terminal. And indeed the elan installation log (which you might not see when installing from inside VS Code...?) tells you to use source or log out and in again. https://github.com/leanprover/elan/blob/933ff726aa5dcfc38f9155c8ee85f303fb7d317d/src/elan-cli/self_update.rs#L123-L127

[Patrick Massot]

Kevin Buzzard said:

I thought that Lean 4 was supposed to Just Work -- I guess the issue is mathlib oleans

I can tell you it Just Doesn't Work. We had a two hours long install party here in MSRI and it was a nightmare.

[Patrick Massot]

To be clear, I consider Lean 4 installed when you can edit files depending on Mathlib without having recompiled Mathlib on your machine.

[Mario Carneiro]

what stage of the process went wrong?

[Mario Carneiro]

in theory, it should be install elan -> lake new foo math -> lake exe cache get -> lake build -> profit

[Mario Carneiro]

the process is more complicated if the user has a pre-existing install, e.g. an old lake

[Kevin Buzzard]

So that's not Lean not working, it sounds like that's mathlib's infrastructure not working.

[Patrick Massot]

Mario, first your theory is not what the official instructions say. They say to install the VSCode extension and then try to open a lean file to have the extension download lean. And then the answer to your question is that we have seen all stages failing randomly. But clearly the worst kind of failure is when lake exe cache get seems to work but Lean still recompiles everything as soon as you open a Lean file.

[Mario Carneiro]

what is "the official instructions"? The mathlib4 readme?

[Mario Carneiro]

Most lean 4 docs from leanprover org don't set you up to use mathlib very well, so I would assume that in a tutorial for mathematicians you would not use those instructions

[Patrick Massot]

Yes the official instructions are at https://github.com/leanprover/lean4/blob/master/doc/quickstart.md and they are indeed not suitable.

[Johan Commelin]

Does lake exe cache get! help fix the recompile issue? There might be something dirty in the cache that a redownload will fix...

[Shreyas Srinivas]

Why doesn't lake (and whatever the extension uses) use a lock?

[Shreyas Srinivas]

I have not had any problems with cache corruption and rebuilding in two months because I always run the project set up steps in a terminal before opening vscode. The only issues I had before that happened when I ran cache inside the vscode terminal or opened vscode too soon. It seems a lot of problems are caused when vscode is open while cache is running, one way or another.

[Shreyas Srinivas]

But it seems this issue would be better handled if there was a lockfile and all tools using touching lake-packages and/or build had to acquire a lock first.

[Shreyas Srinivas]

The other kind of rebuild problems happen when the mathlib version is updated with lake update , but the project lean-toolchain file doesn't get updated. But this was discussed in a different thread recently.

[Mac Malone]

Lake used to have a lockfile, but it was removed. I believe the reason was that lake print-paths in the server cannot fail or the worker for a file would stop. Thus, if anything else had the lock while a file was loading all interactivity features would be disabled without a manual restart. I also believe that there was some problem with the fact that the lean server spawns multiple workers and they would end up locking each other out essentially all the time.

[Mac Malone]

But it has been a long time, so I may be misremembering and/or things may have been fixed to allow locking to work in the interim.

[Sebastian Ullrich]

As far as I remember, the leanpkg4 lockfile did not make leanpkg fail but wait. Was there any reason for changing that?

[Mac Malone]

@Sebastian Ullrich by wait, you mean busy waiting until the lockfile is deleted?

[Mac Malone]

I honestly do not remember what the reason for changing the lock file was. I only have some vague feeling there was some problem that necessitated it, but I may be mistaken. For all I know, it may have just been a causality of the rewrite from using make to the using in-Lean building.

[Sebastian Ullrich]

Mac said:

Sebastian Ullrich by wait, you mean busy waiting until the lockfile is deleted?

Yes: https://github.com/leanprover/lean4/commit/343036cf00e2944a7729f510f83755650f5b3613

[Mac Malone]

Ah. Yeah, I probably should I have just looked at the old code instead of asking. :man_facepalming:

[Mac Malone]

@Sebastian Ullrich Working on this today, I did discover one reason why code can no longer exists -- "wx" is no longer a supported file mode for IO.FS.Handle.mk. I plan on adding it back, but it is interesting to note it would have broken at some point.