Email Gateway (Feb 24 2021 at 14:42): Email Gateway (Feb 24 2021 at 14:42):From: Boris Shminke via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Dear Isabelle developers,
on the page https://hub.docker.com/r/makarius/isabelle
there is a block 'Docker Pull Command'. But when using the command from it, docker fails to pull any image:
docker pull makarius/isabelle
Using default tag: latest
Error response from daemon: manifest for makarius/isabelle:latest not found: manifest unknown: manifest unknown
I guess that the reason is the absence of 'latest' tag (the default one). The following command work perfectly:
docker pull makarius/isabelle:Isabelle2021
Regards,
Boris
Email Gateway (Feb 24 2021 at 18:01):From: Makarius <makarius@sketis.net>
I have stared at the Docker website a few minutes, with the conclusion that it
implicitly assumes the existance of a "latest" tag. So I have added one, to
make the default pull command generated by the Website work.
Further note the other tags and corresponding pull commands:
https://hub.docker.com/r/makarius/isabelle/tags
Anyway, do you want to say a few words about your docker application with
Isabelle?
I don't use it myself and find the extra resource requirements a bit odd.
Usually I just take the package dependencies from the Dockerfile as a starting
point of a regular Ubuntu installation, or use Isabelle/Scala to do it
automatically, e.g. in "isabelle phabricator_setup":
https://isabelle.sketis.net/repos/isabelle-release/file/Isabelle2021/src/Pure/Tools/phabricator.scala#l18
Makarius
Email Gateway (Feb 24 2021 at 19:38):From: Boris Shminke via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
I have stared at the Docker website a few minutes, with the conclusion that it
implicitly assumes the existance of a "latest" tag. So I have added one, to
make the default pull command generated by the Website work.
Thanks!
Anyway, do you want to say a few words about your docker application with Isabelle?
I was interested in using Isabelle server as a remote server through TCP. I mean, you can run Isabelle server in a container (or on a remote physical server) and communicate with it from any other container/machine, which doesn't have anything except telnet or netcast.
Unfortunately, now it seems to be impossible because Isabelle server doesn't have an IP starting argument. It's always 127.0.0.1, and not accessible from remote hosts. Am I right?
Email Gateway (Feb 24 2021 at 19:53):From: Makarius <makarius@sketis.net>
Yes. I did this on purpose, because I don't understand all the fine points
that are required to make a secure server with the Java platform.
Some years ago, my idea was to use something like ssh port forwarding to
access the local port remotely.
There might be better ways that I don't know of yet.
Makarius
Email Gateway (Feb 25 2021 at 09:18):From: Boris Shminke via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Some years ago, my idea was to use something like ssh port forwarding to access the local port remotely.
Yes, that's possible but I think that 127.0.0.1 can be the default binding, and the user starting the server should have an option to change it. Jupyter server works the same way, e.g. Also, I can imagine a situation when Isabelle server is running inside a university VPN on some machine to which one doesn't want to have ssh connections from Isabelle users, even authenticated through VPN.
Best,
Boris
Email Gateway (Feb 28 2021 at 11:00):From: Makarius <makarius@sketis.net>
On 25/02/2021 10:18, Boris Shminke wrote:
Some years ago, my idea was to use something like ssh port forwarding to access the local port remotely.
Yes, that's possible but I think that 127.0.0.1 can be the default binding, and the user starting the server should have an option to change it.
The present approach has an implicit assumption that the connection is local
and the password (UUID) for the connection can be provided by a file that is
private to the user. I presently don't know how to do better, and do not want
to pretend that I do, e.g. by allowing the user to do non-sense at his own
descretion.
Jupyter server works the same way, e.g.
Can you provide a pointer to the relevant documentation of Jupyter?
Also, I can imagine a situation when Isabelle server is running inside a university VPN on some machine to which one doesn't want to have ssh connections from Isabelle users, even authenticated through VPN.
Is the absence of ssh theoretical or based on concrete experience? Isn't VPN
about forwarding ports in the first place?
Makarius
Email Gateway (Mar 01 2021 at 11:59):From: Boris Shminke via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Dear Makarius,
The present approach has an implicit assumption that the connection is local
and the password (UUID) for the connection can be provided by a file that is
private to the user.
Yes, you're right that simply adding this option to isabelle server command is not very useful.
Can you provide a pointer to the relevant documentation of Jupyter?
Sure, https://jupyter-notebook.readthedocs.io/en/stable/public_server.html#running-a-public-notebook-server (for a config file)
https://jupyter-notebook.readthedocs.io/en/stable/public_server.html#docker-cmd (for a command line option)
Of course, they have SSL support, as well as possibility to set password to a server.
Is the absence of ssh theoretical or based on concrete experience?
Yes, it's based on a situation in which I use Jupyter server provided by my lab. I don't have ssh access to it, although the ports are open for me through VPN.
Regards,
Boris
Email Gateway (Mar 01 2021 at 14:09):From: Makarius <makarius@sketis.net>
On 01/03/2021 12:59, Boris Shminke via Cl->
Can you provide a pointer to the relevant documentation of Jupyter?
Sure, https://jupyter-notebook.readthedocs.io/en/stable/public_server.html#running-a-public-notebook-server (for a config file)
https://jupyter-notebook.readthedocs.io/en/stable/public_server.html#docker-cmd (for a command line option)
Of course, they have SSL support, as well as possibility to set password to a server.
I see a lot of side-conditions to the "secure" setup: To do something like
this with "isabelle server" would require careful thoughts.
Since you are using docker anyway, you could also try to remap the port as
documented here: https://docs.docker.com/config/containers/container-networking
Of course this will be still "insecure" as it is by default on 127.0.0.1.
Is the absence of ssh theoretical or based on concrete experience?
Yes, it's based on a situation in which I use Jupyter server provided by my lab. I don't have ssh access to it, although the ports are open for me through VPN.
So the remaining question: Are there notable VPN configurations where ports
are not forwarded like that?
Makarius
Last updated: Jan 04 2025 at 20:18 UTC