Looking for help with Code-Sever not showing InfoView

Stream: general

[Phillip]

I am learning lean via using Code-Server; however, the Lean Infoview doesn’t seem to show anything. Does anyone have any ideas as to why this may be?

[Phillip]

5C5C1A73-35C7-46D7-A8D9-8C6EF5A11DBE.jpg

[Phillip]

This is an example of what I mean

[Johan Commelin]

@Phillip where is your cursor, in that screenshot?

[Phillip]

At the end of the eval line. I can move it anywhere and it isn’t working. I am hoping it isn’t just an issue within the Code-Server environment.

[Phillip]

@Johan Commelin As you can see, it shows the current line down the bottom in the “Problems” section, but it isn’t quite as verbose as the infoview iirc.

[Johan Commelin]

@Phillip hmmz, frustrating. I don't know where to lok for a solution...

[Marc Masdeu]

I am experiencing the same problem. I was trying to set-up a local Cocalc (docker) with its VS Code Server to make it easier for students to join in, I got stuck at exactly this.

[Alex J. Best]

Do you all have some more precise steps to reproduce this? I just installed code-server and added the vscode plugin and from my local machine (i.e. code server on 127.0.0.1:8080 the infoview works fine

[Marc Masdeu]

1) Get cocalc-docker
2) From the docker shell (root), do mv /usr/local/bin/lean to /usr/local/bin/lean_orig
3) Also get extra stuff sudo apt install git curl python3 python3-pip python3-venv
4) From a new project (now as user) run curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
5) Finally, run

python3 -m pip install --user pipx
python3 -m pipx ensurepath
source ~/.profile
pipx install mathlibtools

This would be the set-up. From there, this user can do leanproject get tutorials, and then File / New / VSCode server. This opens a new tab in the browser with code-server running. You can add the lean extension as usual, and open the tutorials folder. All goes as planned, but Infoview doesn't work.

[Alex J. Best]

Thanks, I'll take a look, this reminds me a lot of https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/gitpod/near/228173022 but I have no idea how cocalc via docker works

[Marc Masdeu]

Probably @William Stein would have something to say about what to do here (I don't have right now a paid Cocalc.com account, so there is no way to try this in it...). Also, I don't know if this problem arises in other extensions, or only in the Lean one.

[William Stein]

Unfortunately, I don't have much to say. Maybe check the Chrome dev tools, e.g., is there are failed network request? Also, what happens if you try to use Cocalc's own lean editor in this example -- does it also not work?

[William Stein]

(I don't have right now a paid Cocalc.com account, so there is no way to try this in it...).

If you direct message a project id to me (or send a support request) I can upgrade it so you can test on cocalc.com if you want... though the above steps aren't something you can do on cocalc.com, exactly. You can install cocalc-docker on your laptop though...

[Alex J. Best]

Marc Masdeu said:

1) Get cocalc-docker
2) From the docker shell (root), do mv /usr/local/bin/lean to /usr/local/bin/lean_orig
3) Also get extra stuff sudo apt install git curl python3 python3-pip python3-venv
4) From a new project (now as user) run curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
5) Finally, run

python3 -m pip install --user pipx
python3 -m pipx ensurepath
source ~/.profile
pipx install mathlibtools

This would be the set-up. From there, this user can do leanproject get tutorials, and then File / New / VSCode server. This opens a new tab in the browser with code-server running. You can add the lean extension as usual, and open the tutorials folder. All goes as planned, but Infoview doesn't work.

(un)fortunately I can't reproduce, I just followed all your steps and installed lean and vscode and everything in cocalc in docker and the infoview works fine for me

[Marc Masdeu]

Aha so you manually installed vscode in cocalc? That I hadn't done...are you sure you followed my steps?

[Alex J. Best]

Oh no i didn't manually install vscode

[Alex J. Best]

Yeah I'm pretty sure i did exactly what you said

[Alex J. Best]

I guess with docker we can share our images with each other right?

[Alex J. Best]

And check that way, it could be some browser security feature interfering i guess. And for what it's worth my os is Ubuntu that i installed fresh a few days ago, and I'm using Firefox

[Alex J. Best]

I had to refresh the window after installing the lean plugin

[Alex J. Best]

To get it to load properly

[Marc Masdeu]

I have just tried with Firefox and it works (Arch Linux). I haven't yet figured out how to make it work with Chromium, though.

[Marc Masdeu]

@Alex J. Best Could you try your luck with Chromium and see if you observe the same problem?

[Alex J. Best]

I'm trying again on my laptop and I just read https://github.com/sagemathinc/cocalc-docker#you-cannot-use-chrome-or-safari-you-must-use-firefox which certainly implies using chrome is less well supported by cocalc-docker

[Alex J. Best]

Yeah i really think this is a security problem with localhost not having a valid https certificate and chrome not liking that. What are you actually trying to do @Marc Masdeu ? If you want to host a local (university) server students can play on, can you host it on a site with a https certificate (idk what that actually entails) rather than your localhost?

[Alex J. Best]

The error message in the chromium tab is

Error loading webview: Error: Could not register service workers: SecurityError: Failed to register a ServiceWorker for scope ('https://localhost/7cb40d8f-94aa-42ad-8edd-d29bf872f835/server/code/webview/') with script ('https://localhost/7cb40d8f-94aa-42ad-8edd-d29bf872f835/server/code/webview/service-worker.js?id=f809f4e0-5f84-425c-a006-66d12ecfbcfd&swVersion=2&extensionId=jroesch.lean&vscode-resource-base-authority=vscode-resource.vscode-webview.net'): An unknown error occurred when fetching the script..

even though that url looks to load fine, once you convince chromium to let you access localhost despite it not having a valid certificate

[Marc Masdeu]

Thanks for looking into this. Indeed, my department has some computer to play with, and we want students to use it to play with Lean easily. We will eventually host it with a https certificate (if we manage to do it through docker). It's possible that you can trick chrome to accept these kind of certificates when you access a site, but not when the browser access this site through whatever tricks code-server uses...

[Matthew Ballard]

I am curious about the current status.

Originally I had code-server running on an arm64 raspberry pi and was sshing via my iPad to use it. The infoview was missing. I have since switched to a x86 vm with gcloud where I have no issue.

Do these issues exist for a bare code-server install?

If you are exposing it, it is probably simplest to put it behind a reverse proxy using caddy + let's encrypt. I did this in the past and it worked quite well. I never had a problem (beyond the PWA experience on the iPad and the built in pdf viewer for the latex workshop extension).