Zulip Chat Archive

Stream: general

Topic: Looking for help with Code-Sever not showing InfoView


Phillip (Sep 26 2021 at 06:15):

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 (Sep 26 2021 at 06:18):

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

Phillip (Sep 26 2021 at 06:18):

This is an example of what I mean

Johan Commelin (Sep 26 2021 at 06:29):

@Phillip where is your cursor, in that screenshot?

Phillip (Sep 26 2021 at 06:30):

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 (Sep 26 2021 at 06:32):

@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 (Sep 26 2021 at 06:49):

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

Marc Masdeu (Sep 30 2021 at 10:42):

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 (Sep 30 2021 at 10:52):

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 (Sep 30 2021 at 14:25):

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 (Sep 30 2021 at 14:51):

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 (Sep 30 2021 at 15:00):

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 (Sep 30 2021 at 15:46):

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 (Sep 30 2021 at 15:53):

(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 (Sep 30 2021 at 16:26):

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 (Sep 30 2021 at 19:24):

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

Alex J. Best (Sep 30 2021 at 20:06):

Oh no i didn't manually install vscode

Alex J. Best (Sep 30 2021 at 20:06):

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

Alex J. Best (Sep 30 2021 at 20:07):

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

Alex J. Best (Sep 30 2021 at 20:08):

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 (Sep 30 2021 at 20:08):

I had to refresh the window after installing the lean plugin

Alex J. Best (Sep 30 2021 at 20:09):

To get it to load properly

Marc Masdeu (Oct 01 2021 at 06:58):

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 (Oct 01 2021 at 06:58):

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

Alex J. Best (Oct 01 2021 at 13:45):

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 (Oct 01 2021 at 15:49):

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 (Oct 01 2021 at 15:53):

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 (Oct 01 2021 at 17:28):

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 (Oct 06 2021 at 16:02):

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).


Last updated: Dec 20 2023 at 11:08 UTC