Inital commit of Dockerfile for Isabelle/DOF.
This commit is contained in:
parent
355588690a
commit
1f51468201
23
README.md
23
README.md
|
|
@ -1,18 +1,25 @@
|
|||
# [Dockerfiles for Isabelle and Related Projects](https://git.logicalhacking.com/lh-docker/lh-docker-isabelle)
|
||||
|
||||
This repository contains Dockerfiles for running [Isabelle](https://isabelle.in.tum.de)
|
||||
and projects based on [Isabelle](https://isabelle.in.tum.de).
|
||||
This repository contains Dockerfiles for running [Isabelle](https://isabelle.in.tum.de)
|
||||
and projects based on [Isabelle](https://isabelle.in.tum.de).
|
||||
|
||||
## List of Dockerfiles
|
||||
|
||||
* [debian4isabelle](debian4isabelle/Dockerfile) provides a generic [Debian](https://www.debian.org)
|
||||
image that serves as basis for the Isabelle docker files. This image is not
|
||||
eagerly optimised for size, as it goal is to include all tools that are required for
|
||||
image that serves as basis for the Isabelle docker files. This image is not
|
||||
eagerly optimized for size, as it goal is to include all tools that are required for
|
||||
running Isabelle and tools based on Isabelle (e.g., HOL-TestGen).
|
||||
|
||||
* [isabelle](isabelle/Dockerfile) provides a parametrized Dockerfile to generate docker
|
||||
images for various Isabelle versions, including a copy of the most recent version of
|
||||
the [AFP](https://www.isa-afp.org) available for the specified version of Isabelle.
|
||||
* [isabelle](isabelle/Dockerfile) provides a parametrized Dockerfile to generate docker
|
||||
images for various version of Isabelle. The image will also contain a copy of the most
|
||||
recent version of the [AFP](https://www.isa-afp.org) available for the specified
|
||||
version of Isabelle.
|
||||
|
||||
* [isabelle_dof](isabelle_dof/Dockerfile) provides a parametrized Dockerfile to generate
|
||||
docker images of [Isabelle/DOF](https://git.logicalhacking.com/isabelle_dof/isabelle_dof).
|
||||
[Isabelle/DOF](https://git.logicalhacking.com/isabelle_dof/isabelle_dof) is a document
|
||||
authoring framework for Isabelle, provided by the University of Exeter and the University
|
||||
of Paris-Saclay.
|
||||
|
||||
## Authors
|
||||
|
||||
|
|
@ -20,7 +27,7 @@ Main author: [Achim D. Brucker](http://www.brucker.ch/)
|
|||
|
||||
## License
|
||||
|
||||
If not otherwise stated, all hacks are licensed under a 2-clause
|
||||
If not otherwise stated, all hacks are licensed under a 2-clause
|
||||
BSD-style license.
|
||||
|
||||
SPDX-License-Identifier: BSD-2-Clause
|
||||
|
|
|
|||
4
build.sh
4
build.sh
|
|
@ -38,3 +38,7 @@ docker build -t logicalhacking/debian4isabelle debian4isabelle
|
|||
|
||||
# Generate Isabelle image(s)
|
||||
( cd isabelle && source hooks/build)
|
||||
|
||||
# Generate Isabelle/DOF image
|
||||
# ISADOF_VERSION=1.0.0
|
||||
( cd isabelle_dof && source hooks/build)
|
||||
|
|
|
|||
|
|
@ -0,0 +1,52 @@
|
|||
# Copyright (c) 2019 Achim D. Brucker
|
||||
#
|
||||
# All rights reserved.
|
||||
#
|
||||
# Redistribution and use in source and binary forms, with or without
|
||||
# modification, are permitted provided that the following conditions are met:
|
||||
#
|
||||
# * Redistributions of source code must retain the above copyright notice, this
|
||||
#
|
||||
# * Redistributions in binary form must reproduce the above copyright notice,
|
||||
# this list of conditions and the following disclaimer in the documentation
|
||||
# and/or other materials provided with the distribution.
|
||||
#
|
||||
# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
|
||||
# AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
|
||||
# IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
|
||||
# DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
|
||||
# FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
|
||||
# DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
|
||||
# SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
|
||||
# CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
|
||||
# OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
|
||||
# OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
|
||||
#
|
||||
# SPDX-License-Identifier: BSD-2-Clause
|
||||
|
||||
FROM logicalhacking/isabelle2019
|
||||
|
||||
ARG tag
|
||||
|
||||
LABEL isadof.tag="$tag"
|
||||
|
||||
SHELL ["/bin/bash", "-c"]
|
||||
|
||||
# Install Isabelle and corresponding AFP
|
||||
WORKDIR /home/isabelle
|
||||
|
||||
USER root
|
||||
RUN apt-get -y update && apt-get install -y imagemagick && \
|
||||
apt-get clean && \
|
||||
rm -rf /usr/share/doc
|
||||
|
||||
USER isabelle
|
||||
RUN git clone https://git.logicalhacking.com/isabelle_dof/isabelle_dof/ && \
|
||||
(cd isabelle_dof && git checkout "$tag") && \
|
||||
(cd isabelle_dof && ./install) && \
|
||||
(cd isabelle_dof && isabelle build -D .) && \
|
||||
echo "ISABELLE_LOGIC=Isabelle_DOF" >> Isabelle/etc/settings && \
|
||||
rm Isabelle/lib/logo/isabelle.gif && \
|
||||
convert isabelle_dof/examples/technical_report/Isabelle_DOF-Manual/document/figures/Isabelle_DOF-logo.pdf -resize 200 Isabelle/lib/logo/isabelle.gif && \
|
||||
for o in `find isabelle_dof/examples -name "output"`; do mv $o/document.pdf $o/..; done && \
|
||||
find isabelle_dof/examples -name output -exec rm -rf {} \; &> /dev/null || true
|
||||
|
|
@ -0,0 +1,39 @@
|
|||
#!/bin/bash
|
||||
# Copyright (c) 2019 Achim D. Brucker
|
||||
#
|
||||
# All rights reserved.
|
||||
#
|
||||
# Redistribution and use in source and binary forms, with or without
|
||||
# modification, are permitted provided that the following conditions are met:
|
||||
#
|
||||
# * Redistributions of source code must retain the above copyright notice, this
|
||||
#
|
||||
# * Redistributions in binary form must reproduce the above copyright notice,
|
||||
# this list of conditions and the following disclaimer in the documentation
|
||||
# and/or other materials provided with the distribution.
|
||||
#
|
||||
# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
|
||||
# AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
|
||||
# IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
|
||||
# DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
|
||||
# FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
|
||||
# DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
|
||||
# SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
|
||||
# CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
|
||||
# OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
|
||||
# OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
|
||||
#
|
||||
# SPDX-License-Identifier: BSD-2-Clause
|
||||
|
||||
set -e
|
||||
|
||||
if [ -z "$ISADOF_VERSION" ] ; then
|
||||
IMAGE="isadof"
|
||||
TAG="master"
|
||||
else
|
||||
TAG="v"$VERSION"/Isabelle2019"
|
||||
IMAGE="Isabelle_DOF-"$ISADOF_VERSION"_Isabelle2019"
|
||||
fi
|
||||
|
||||
docker build -t logicalhacking/$IMAGE . \
|
||||
--build-arg tag="$TAG"
|
||||
Loading…
Reference in New Issue