forked from Isabelle_DOF/Isabelle_DOF
Merge branch 'master' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF
This commit is contained in:
commit
8a3622c125
|
@ -0,0 +1,177 @@
|
||||||
|
#!/usr/bin/env bash
|
||||||
|
# Copyright (c) 2019The University of Exeter.
|
||||||
|
# 2019 The University of Paris-Saclay.
|
||||||
|
#
|
||||||
|
# Redistribution and use in source and binary forms, with or without
|
||||||
|
# modification, are permitted provided that the following conditions
|
||||||
|
# are met:
|
||||||
|
# 1. Redistributions of source code must retain the above copyright
|
||||||
|
# notice, this list of conditions and the following disclaimer.
|
||||||
|
# 2. 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
|
||||||
|
shopt -s nocasematch
|
||||||
|
|
||||||
|
|
||||||
|
print_help()
|
||||||
|
{
|
||||||
|
echo "Usage: mk_release [OPTION] "
|
||||||
|
echo ""
|
||||||
|
echo " A tool for building $ISADOF_TAR.tar.xz"
|
||||||
|
echo ""
|
||||||
|
echo "Run ..."
|
||||||
|
echo ""
|
||||||
|
echo " --help, -h display this help message"
|
||||||
|
echo " --sign -s sign release archive"
|
||||||
|
echo " (default: $SIGN)"
|
||||||
|
echo " --isabelle, -i isabelle isabelle command used for installation"
|
||||||
|
echo " (default: $ISABELLE)"
|
||||||
|
echo " --tag -t tag use tag for release archive"
|
||||||
|
echo " --p --publish publish generated artefact"
|
||||||
|
echo " (use master: $PUBLISH)"
|
||||||
|
}
|
||||||
|
|
||||||
|
read_config() {
|
||||||
|
if [ ! -f .config ]; then
|
||||||
|
echo "Error: .config not found (not started in the main directory?)!"
|
||||||
|
exit 1
|
||||||
|
else
|
||||||
|
source .config
|
||||||
|
fi
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
check_isabelle_version() {
|
||||||
|
ACTUAL_ISABELLE_VERSION=`$ISABELLE version`
|
||||||
|
echo "* Checking Isabelle version:"
|
||||||
|
if [ "$ISABELLE_VERSION" != "$ACTUAL_ISABELLE_VERSION" ]; then
|
||||||
|
echo "* Expecting $ISABELLE_VERSION, found $ACTUAL_ISABELLE_VERSION: ERROR"
|
||||||
|
exit 1
|
||||||
|
else
|
||||||
|
echo "* Expecting $ISABELLE_VERSION, found $ACTUAL_ISABELLE_VERSION: success"
|
||||||
|
fi
|
||||||
|
}
|
||||||
|
|
||||||
|
clone_repo()
|
||||||
|
{
|
||||||
|
echo "* Cloning into $ISADOF_DIR"
|
||||||
|
git clone . $ISADOF_DIR
|
||||||
|
if [ "$USE_TAG" = "true" ]; then
|
||||||
|
echo " * Switching to tag $DOF_VERSION/$ISABELLE_SHORT_VERSION"
|
||||||
|
(cd $ISADOF_DIR && git checkout $DOF_VERSION/$ISABELLE_SHORT_VERSION)
|
||||||
|
else
|
||||||
|
echo " * Not tag specified, using master branch"
|
||||||
|
fi
|
||||||
|
}
|
||||||
|
|
||||||
|
build_and_install_manual()
|
||||||
|
{
|
||||||
|
echo "* Building manual"
|
||||||
|
ROOTS=$ISABELLE_HOME_USER/ROOTS
|
||||||
|
if [ -f $ROOTS ]; then
|
||||||
|
mv $ROOTS $ROOTS.backup
|
||||||
|
fi
|
||||||
|
(cd $ISADOF_DIR && ./install)
|
||||||
|
(cd $ISADOF_DIR && $ISABELLE build -c Isabelle_DOF-Manual)
|
||||||
|
mkdir -p $ISADOF_DIR/doc
|
||||||
|
cp $ISADOF_DIR/examples/technical_report/Isabelle_DOF-Manual/output/document.pdf \
|
||||||
|
$ISADOF_DIR/doc/Isabelle_DOF-Manual.pdf
|
||||||
|
find $ISADOF_DIR -type d -name "output" -exec rm -rf {} \; || true
|
||||||
|
rm -rf $ISADOF_DIR/.git* $ISADOF_DIR/.ci $ISADOF_DIR/.afp
|
||||||
|
if [ -f $ROOTS.backup ]; then
|
||||||
|
mv $ROOTS.backup $ROOTS
|
||||||
|
fi
|
||||||
|
}
|
||||||
|
|
||||||
|
create_archive()
|
||||||
|
{
|
||||||
|
echo "* Creating archive"
|
||||||
|
(cd $BUILD_DIR && tar cf $ISADOF_TAR.tar $ISADOF_TAR && xz $ISADOF_DIR.tar)
|
||||||
|
mv $BUILD_DIR/$ISADOF_TAR.tar.xz .
|
||||||
|
rm -rf $BUILD_DIR
|
||||||
|
}
|
||||||
|
|
||||||
|
sign_archive()
|
||||||
|
{
|
||||||
|
echo "* Publish archive not yet implemented"
|
||||||
|
gpg --armor --output $ISADOF_TAR.tar.xz.asc --detach-sig $ISADOF_TAR.tar.xz
|
||||||
|
}
|
||||||
|
|
||||||
|
publish_archive()
|
||||||
|
{
|
||||||
|
echo "* Publish archive"
|
||||||
|
ssh 0x5f.org mkdir -p www/$DOF_ARTIFACT_HOST/htdocs/$DOF_ARTIFACT_DIR
|
||||||
|
scp $ISADOF_TAR.tar.xz* 0x5f.org:www/$DOF_ARTIFACT_HOST/htdocs/$DOF_ARTIFACT_DIR/
|
||||||
|
ssh 0x5f.org chmod go+u-w -R www/$DOF_ARTIFACT_HOST/htdocs/$DOF_ARTIFACT_DIR
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
read_config
|
||||||
|
ISABELLE=`which isabelle`
|
||||||
|
USE_TAG="false"
|
||||||
|
SIGN="false"
|
||||||
|
PUBLISH="false"
|
||||||
|
ISABELLE_SHORT_VERSION=`echo $ISABELLE_VERSION | sed -e 's/:.*$//'`
|
||||||
|
TAG="$DOF_VERSION/$ISABELLE_SHORT_VERSION"
|
||||||
|
BUILD_DIR=`mktemp -d`
|
||||||
|
ISADOF_TAR="Isabelle_DOF-"$DOF_VERSION"_"$ISABELLE_SHORT_VERSION
|
||||||
|
ISADOF_DIR="$BUILD_DIR/$ISADOF_TAR"
|
||||||
|
while [ $# -gt 0 ]
|
||||||
|
do
|
||||||
|
case "$1" in
|
||||||
|
--isabelle|-i)
|
||||||
|
ISABELLE="$2";
|
||||||
|
shift;;
|
||||||
|
--tag|-t)
|
||||||
|
TAG="$2";
|
||||||
|
USE_TAG="true"
|
||||||
|
shift;;
|
||||||
|
--sign|-s)
|
||||||
|
SIGN="true";;
|
||||||
|
--publish|-p)
|
||||||
|
PUBLISH="true";;
|
||||||
|
--help|-h)
|
||||||
|
print_help
|
||||||
|
exit 0;;
|
||||||
|
*) print_help
|
||||||
|
exit 1;;
|
||||||
|
esac
|
||||||
|
shift
|
||||||
|
done
|
||||||
|
|
||||||
|
check_isabelle_version
|
||||||
|
VARS=`$ISABELLE getenv ISABELLE_HOME_USER`
|
||||||
|
for i in $VARS; do
|
||||||
|
export "$i"
|
||||||
|
done
|
||||||
|
|
||||||
|
clone_repo
|
||||||
|
build_and_install_manual
|
||||||
|
create_archive
|
||||||
|
|
||||||
|
if [ "$SIGN" = "true" ]; then
|
||||||
|
sign_archive
|
||||||
|
fi
|
||||||
|
|
||||||
|
if [ "$PUBLISH" = "true" ]; then
|
||||||
|
publish_archive
|
||||||
|
fi
|
||||||
|
|
||||||
|
exit 0
|
|
@ -101,7 +101,6 @@ Usage: isabelle mkroot_DOF [OPTIONS] [DIR]
|
||||||
-o ONTOLOGY (default: scholarly_paper)
|
-o ONTOLOGY (default: scholarly_paper)
|
||||||
Available ontologies:
|
Available ontologies:
|
||||||
* cenelec_50128
|
* cenelec_50128
|
||||||
* core
|
|
||||||
* mathex
|
* mathex
|
||||||
* scholarly_paper
|
* scholarly_paper
|
||||||
-t TEMPLATE (default: scrartcl)
|
-t TEMPLATE (default: scrartcl)
|
||||||
|
|
|
@ -41,7 +41,7 @@ text\<open>
|
||||||
paragraph\<open>Installing Isabelle\<close>
|
paragraph\<open>Installing Isabelle\<close>
|
||||||
text\<open>
|
text\<open>
|
||||||
Please download and install the Isabelle \isabelleversion distribution for your operating system
|
Please download and install the Isabelle \isabelleversion distribution for your operating system
|
||||||
from the \href{\isabelleurl}{Isabelle website} (\url{isabelleurl}). After the successful
|
from the \href{\isabelleurl}{Isabelle website} (\url{\isabelleurl}). After the successful
|
||||||
installation of Isabelle, you should be able to call the \inlinebash|isabelle| tool on the
|
installation of Isabelle, you should be able to call the \inlinebash|isabelle| tool on the
|
||||||
command line:
|
command line:
|
||||||
|
|
||||||
|
|
|
@ -1,3 +1,5 @@
|
||||||
|
\usepackage{listings}
|
||||||
|
\usepackage{listingsutf8}
|
||||||
\usepackage{tikz}
|
\usepackage{tikz}
|
||||||
\usepackage[many]{tcolorbox}
|
\usepackage[many]{tcolorbox}
|
||||||
\tcbuselibrary{listings}
|
\tcbuselibrary{listings}
|
||||||
|
|
|
@ -18,20 +18,13 @@
|
||||||
|
|
||||||
\usepackage{dirtree}
|
\usepackage{dirtree}
|
||||||
\renewcommand*\DTstylecomment{\ttfamily\itshape}
|
\renewcommand*\DTstylecomment{\ttfamily\itshape}
|
||||||
\usepackage[scaled=0.88]{beramono}%
|
|
||||||
\usepackage{upquote}%
|
|
||||||
\usepackage{textcomp}
|
\usepackage{textcomp}
|
||||||
\usepackage{xcolor}
|
\usepackage{xcolor}
|
||||||
\usepackage{paralist}
|
|
||||||
\usepackage{listings}
|
|
||||||
\usepackage{listingsutf8}
|
|
||||||
\usepackage{lstisadof-manual}
|
\usepackage{lstisadof-manual}
|
||||||
\usepackage{xspace}
|
\usepackage{xspace}
|
||||||
\usepackage{dtk-logos}
|
\usepackage{dtk-logos}
|
||||||
\usepackage[caption]{subfig}
|
|
||||||
\usepackage[size=footnotesize]{caption}
|
|
||||||
\usepackage{railsetup}
|
\usepackage{railsetup}
|
||||||
\setcounter{secnumdepth}{4}
|
\setcounter{secnumdepth}{2}
|
||||||
\usepackage{index}
|
\usepackage{index}
|
||||||
\newcommand{\bindex}[1]{\index{#1|textbf}}
|
\newcommand{\bindex}[1]{\index{#1|textbf}}
|
||||||
%\makeindex
|
%\makeindex
|
||||||
|
|
1
install
1
install
|
@ -232,6 +232,7 @@ install_and_register(){
|
||||||
echo 'ISABELLE_TOOLS=$ISABELLE_TOOLS:$ISABELLE_HOME_USER/DOF/Tools' \
|
echo 'ISABELLE_TOOLS=$ISABELLE_TOOLS:$ISABELLE_HOME_USER/DOF/Tools' \
|
||||||
>> "$DIR/settings"
|
>> "$DIR/settings"
|
||||||
fi
|
fi
|
||||||
|
sed -i -e "s|<isadofurl>|$DOF_URL|" $ISABELLE_HOME_USER/DOF/*/*
|
||||||
grep -q $PWD\$ $ISABELLE_HOME_USER/ROOTS || echo "$PWD" >> $ISABELLE_HOME_USER/ROOTS
|
grep -q $PWD\$ $ISABELLE_HOME_USER/ROOTS || echo "$PWD" >> $ISABELLE_HOME_USER/ROOTS
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
@ -39,10 +39,10 @@
|
||||||
This is a Isabelle_DOF project. The document preparation requires
|
This is a Isabelle_DOF project. The document preparation requires
|
||||||
the Isabelle_DOF framework. Please obtain the framework by cloning
|
the Isabelle_DOF framework. Please obtain the framework by cloning
|
||||||
the Isabelle_DOF git repository, i.e.:
|
the Isabelle_DOF git repository, i.e.:
|
||||||
"git clone https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF"
|
"git clone <isadofurl>"
|
||||||
You can install the framework as follows:
|
You can install the framework as follows:
|
||||||
"cd Isabelle_DOF/document-generator && ./install"}{%
|
"cd Isabelle_DOF/document-generator && ./install"}{%
|
||||||
For further help, see https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF}
|
For further help, see <isadofurl>}
|
||||||
}
|
}
|
||||||
|
|
||||||
\newcommand{\subtitle}[1]{%
|
\newcommand{\subtitle}[1]{%
|
||||||
|
|
|
@ -35,10 +35,10 @@
|
||||||
This is a Isabelle_DOF project. The document preparation requires
|
This is a Isabelle_DOF project. The document preparation requires
|
||||||
the Isabelle_DOF framework. Please obtain the framework by cloning
|
the Isabelle_DOF framework. Please obtain the framework by cloning
|
||||||
the Isabelle_DOF git repository, i.e.:
|
the Isabelle_DOF git repository, i.e.:
|
||||||
"git clone https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF"
|
"git clone <isadofurl>"
|
||||||
You can install the framework as follows:
|
You can install the framework as follows:
|
||||||
"cd Isabelle_DOF/document-generator && ./install"}{%
|
"cd Isabelle_DOF/document-generator && ./install"}{%
|
||||||
For further help, see https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF}
|
For further help, see <isadofurl>}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
|
@ -39,10 +39,10 @@
|
||||||
This is a Isabelle_DOF project. The document preparation requires
|
This is a Isabelle_DOF project. The document preparation requires
|
||||||
the Isabelle_DOF framework. Please obtain the framework by cloning
|
the Isabelle_DOF framework. Please obtain the framework by cloning
|
||||||
the Isabelle_DOF git repository, i.e.:
|
the Isabelle_DOF git repository, i.e.:
|
||||||
"git clone https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF"
|
"git clone <isadofurl>"
|
||||||
You can install the framework as follows:
|
You can install the framework as follows:
|
||||||
"cd Isabelle_DOF/document-generator && ./install"}{%
|
"cd Isabelle_DOF/document-generator && ./install"}{%
|
||||||
For further help, see https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF}
|
For further help, see <isadofurl>}
|
||||||
}
|
}
|
||||||
\input{ontologies}
|
\input{ontologies}
|
||||||
\IfFileExists{preamble.tex}{\input{preamble.tex}}{}%
|
\IfFileExists{preamble.tex}{\input{preamble.tex}}{}%
|
||||||
|
|
|
@ -34,10 +34,10 @@
|
||||||
This is a Isabelle_DOF project. The document preparation requires
|
This is a Isabelle_DOF project. The document preparation requires
|
||||||
the Isabelle_DOF framework. Please obtain the framework by cloning
|
the Isabelle_DOF framework. Please obtain the framework by cloning
|
||||||
the Isabelle_DOF git repository, i.e.:
|
the Isabelle_DOF git repository, i.e.:
|
||||||
"git clone https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF"
|
"git clone <isadofurl>"
|
||||||
You can install the framework as follows:
|
You can install the framework as follows:
|
||||||
"cd Isabelle_DOF/document-generator && ./install"}{%
|
"cd Isabelle_DOF/document-generator && ./install"}{%
|
||||||
For further help, see https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF}
|
For further help, see <isadofurl>}
|
||||||
}
|
}
|
||||||
\input{ontologies}
|
\input{ontologies}
|
||||||
\IfFileExists{preamble.tex}{\input{preamble.tex}}{}%
|
\IfFileExists{preamble.tex}{\input{preamble.tex}}{}%
|
||||||
|
|
|
@ -55,10 +55,10 @@
|
||||||
This is a Isabelle_DOF project. The document preparation requires
|
This is a Isabelle_DOF project. The document preparation requires
|
||||||
the Isabelle_DOF framework. Please obtain the framework by cloning
|
the Isabelle_DOF framework. Please obtain the framework by cloning
|
||||||
the Isabelle_DOF git repository, i.e.:
|
the Isabelle_DOF git repository, i.e.:
|
||||||
"git clone https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF"
|
"git clone <isadofurl>"
|
||||||
You can install the framework as follows:
|
You can install the framework as follows:
|
||||||
"cd Isabelle_DOF/document-generator && ./install"}{%
|
"cd Isabelle_DOF/document-generator && ./install"}{%
|
||||||
For further help, see https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF}
|
For further help, see <isadofurl>}
|
||||||
}
|
}
|
||||||
\input{ontologies}
|
\input{ontologies}
|
||||||
\IfFileExists{preamble.tex}{\input{preamble.tex}}{}%
|
\IfFileExists{preamble.tex}{\input{preamble.tex}}{}%
|
||||||
|
|
|
@ -34,10 +34,10 @@
|
||||||
This is a Isabelle_DOF project. The document preparation requires
|
This is a Isabelle_DOF project. The document preparation requires
|
||||||
the Isabelle_DOF framework. Please obtain the framework by cloning
|
the Isabelle_DOF framework. Please obtain the framework by cloning
|
||||||
the Isabelle_DOF git repository, i.e.:
|
the Isabelle_DOF git repository, i.e.:
|
||||||
"git clone https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF"
|
"git clone <isadofurl>"
|
||||||
You can install the framework as follows:
|
You can install the framework as follows:
|
||||||
"cd Isabelle_DOF/document-generator && ./install"}{%
|
"cd Isabelle_DOF/document-generator && ./install"}{%
|
||||||
For further help, see https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF}
|
For further help, see <isadofurl>}
|
||||||
}
|
}
|
||||||
\input{ontologies}
|
\input{ontologies}
|
||||||
\IfFileExists{preamble.tex}{\input{preamble.tex}}{}%
|
\IfFileExists{preamble.tex}{\input{preamble.tex}}{}%
|
||||||
|
|
|
@ -35,7 +35,7 @@ if [ ! -f $ISABELLE_HOME_USER/DOF/document-template/build_lib.sh ]; then
|
||||||
>&2 echo "This is a Isabelle/DOF project. The document preparation requires"
|
>&2 echo "This is a Isabelle/DOF project. The document preparation requires"
|
||||||
>&2 echo "the Isabelle/DOF framework. Please obtain the framework by cloning"
|
>&2 echo "the Isabelle/DOF framework. Please obtain the framework by cloning"
|
||||||
>&2 echo "the Isabelle/DOF git repository, i.e.: "
|
>&2 echo "the Isabelle/DOF git repository, i.e.: "
|
||||||
>&2 echo " git clone https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF"
|
>&2 echo " git clone <isadofurl>"
|
||||||
>&2 echo "You can install the framework as follows:"
|
>&2 echo "You can install the framework as follows:"
|
||||||
>&2 echo " cd Isabelle_DOF/document-generator"
|
>&2 echo " cd Isabelle_DOF/document-generator"
|
||||||
>&2 echo " ./install"
|
>&2 echo " ./install"
|
||||||
|
|
|
@ -42,7 +42,7 @@ if [ ! -f $ISABELLE_HOME_USER/DOF/document-template/DOF-core.sty ]; then
|
||||||
>&2 echo "This is a Isabelle/DOF project. The document preparation requires"
|
>&2 echo "This is a Isabelle/DOF project. The document preparation requires"
|
||||||
>&2 echo "the Isabelle/DOF framework. Please obtain the framework by cloning"
|
>&2 echo "the Isabelle/DOF framework. Please obtain the framework by cloning"
|
||||||
>&2 echo "the Isabelle/DOF git repository, i.e.: "
|
>&2 echo "the Isabelle/DOF git repository, i.e.: "
|
||||||
>&2 echo " git clone https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF"
|
>&2 echo " git clone <isadofurl>"
|
||||||
>&2 echo "You can install the framework as follows:"
|
>&2 echo "You can install the framework as follows:"
|
||||||
>&2 echo " cd Isabelle_DOF/document-generator"
|
>&2 echo " cd Isabelle_DOF/document-generator"
|
||||||
>&2 echo " ./install"
|
>&2 echo " ./install"
|
||||||
|
|
Loading…
Reference in New Issue