Re: [isabelle] Error in DockerHub documentation



On 24/02/2021 11:33, Boris Shminke via Cl-isabelle-users wrote:
> 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

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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.