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
> 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:

Anyway, do you want to say a few words about your docker application with

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":


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