Hello,

I'm trying to connect Lean's Research Docker Jupyter server to VSCode.

Jupyter works properly with the run_docker_notebook.sh script and everything works fine with a browser.

But when I try to connect Jupyter Server to VSCode, the connection fails. I've tried the ip-addresses, which can be found in the Docker logs. When I try the URI http://localhost:8888/lab/workspaces/auto-S, VSCode asks for a username and password for the server, where could these be found?

If someone has experience on this and knows how to connect the Research Notebook to the VSCode using the Docker container, a tutorial on this would be great.

Thank you.

-Lassi Puurunen

Author