Email Gateway (Aug 22 2022 at 16:13): Email Gateway (Aug 22 2022 at 16:13):From: Makarius <makarius@sketis.net>
Dear Isabelle users,
the new Isabelle2017 distribution provides a Docker image via the Docker
Hub repository https://hub.docker.com/r/makarius/isabelle
The Docker image contains Ubuntu Linux with Isabelle2017. It can be
used, e.g. on another Linux host like this:
docker pull makarius/isabelle:Isabelle2017
docker run makarius/isabelle:Isabelle2017
That provides command-line access to the regular isabelle tool wrapper,
with indirection through the Docker container infrastructure.
The image already contains ML heaps for Isabelle/Pure and Isabelle/HOL.
Here is an example to build more:
docker run makarius/isabelle:Isabelle2017 -s -b HOL-Library
Note that Docker is mainly for command-line tools on the "Cloud". There
is presently no Isabelle Prover IDE support, although very old-fashioned
X11 connections can be made to work with extra tinkering.
Makarius
Email Gateway (Aug 22 2022 at 16:13):From: Makarius <makarius@sketis.net>
There is a small mistake in the Isabelle2017/NEWS file: it claims the
existence of a tool "isabelle build_docker", but that is actually an
internal administrative tool and thus not accessible in the release.
The Isabelle/Scala source is here:
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2017/src/Pure/Admin/build_docker.scala
If anybody wants to experiment with that, it requires a repository
snapshot of Isabelle2017 to get access to all such "admin" tools.
Makarius
Last updated: Apr 24 2024 at 04:17 UTC