From 7e4936b9a0660e9500f3ce7e448a34c95bd06950 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Mon, 12 Aug 2019 21:02:35 +0100 Subject: [PATCH 1/9] Removed core ontology from list of ontologies (mkroot_DOF -h output). --- README.md | 1 - 1 file changed, 1 deletion(-) diff --git a/README.md b/README.md index bca091e4..9621aaed 100644 --- a/README.md +++ b/README.md @@ -101,7 +101,6 @@ Usage: isabelle mkroot_DOF [OPTIONS] [DIR] -o ONTOLOGY (default: scholarly_paper) Available ontologies: * cenelec_50128 - * core * mathex * scholarly_paper -t TEMPLATE (default: scrartcl) From 86b57a21a545d4fa80f0b81a393dbe234a03dfc4 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Tue, 13 Aug 2019 00:02:01 +0100 Subject: [PATCH 2/9] Initial commit. --- .ci/mk_release | 177 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 177 insertions(+) create mode 100755 .ci/mk_release diff --git a/.ci/mk_release b/.ci/mk_release new file mode 100755 index 00000000..5eba8578 --- /dev/null +++ b/.ci/mk_release @@ -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 From cb91c970288a9d13ead9d117fb4a50453719171b Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Tue, 13 Aug 2019 08:55:43 +0100 Subject: [PATCH 3/9] Configured secnumdepth to not number paragraphs and subsubsections. --- .../technical_report/Isabelle_DOF-Manual/document/preamble.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex b/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex index d1104eae..76d8f102 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex +++ b/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex @@ -31,7 +31,7 @@ \usepackage[caption]{subfig} \usepackage[size=footnotesize]{caption} \usepackage{railsetup} -\setcounter{secnumdepth}{4} +\setcounter{secnumdepth}{2} \usepackage{index} \newcommand{\bindex}[1]{\index{#1|textbf}} %\makeindex From 803fea739e9c609d88b3e5dc98bef3c548cf1f30 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Tue, 13 Aug 2019 08:55:57 +0100 Subject: [PATCH 4/9] Fixed link to the Isabelle website. --- examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy index faae7d7c..9df83df2 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy @@ -41,7 +41,7 @@ text\ paragraph\Installing Isabelle\ text\ 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 command line: From e2a752ab554bfa6c8282542c05c7766bb21f6adc Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Tue, 13 Aug 2019 09:18:47 +0100 Subject: [PATCH 5/9] Removed no longer required inpara-package. --- .../technical_report/Isabelle_DOF-Manual/document/preamble.tex | 1 - 1 file changed, 1 deletion(-) diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex b/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex index 76d8f102..638e3a69 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex +++ b/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex @@ -22,7 +22,6 @@ \usepackage{upquote}% \usepackage{textcomp} \usepackage{xcolor} -\usepackage{paralist} \usepackage{listings} \usepackage{listingsutf8} \usepackage{lstisadof-manual} From 40bb39c89cea259b3020d27212c0edd7f2d419d9 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Tue, 13 Aug 2019 09:21:33 +0100 Subject: [PATCH 6/9] Moved loading of listings-package into lstisadof-manual.sty. --- .../Isabelle_DOF-Manual/document/lstisadof-manual.sty | 2 ++ .../technical_report/Isabelle_DOF-Manual/document/preamble.tex | 2 -- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/lstisadof-manual.sty b/examples/technical_report/Isabelle_DOF-Manual/document/lstisadof-manual.sty index c46e2d54..00cb2464 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/document/lstisadof-manual.sty +++ b/examples/technical_report/Isabelle_DOF-Manual/document/lstisadof-manual.sty @@ -1,3 +1,5 @@ +\usepackage{listings} +\usepackage{listingsutf8} \usepackage{tikz} \usepackage[many]{tcolorbox} \tcbuselibrary{listings} diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex b/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex index 638e3a69..abd6980e 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex +++ b/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex @@ -22,8 +22,6 @@ \usepackage{upquote}% \usepackage{textcomp} \usepackage{xcolor} -\usepackage{listings} -\usepackage{listingsutf8} \usepackage{lstisadof-manual} \usepackage{xspace} \usepackage{dtk-logos} From d00cf8d4c30137ae57fbe6a145890e9a536c0cd9 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Tue, 13 Aug 2019 09:24:32 +0100 Subject: [PATCH 7/9] Use default tt font instead of beramono. --- .../technical_report/Isabelle_DOF-Manual/document/preamble.tex | 1 - 1 file changed, 1 deletion(-) diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex b/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex index abd6980e..9eecbeee 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex +++ b/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex @@ -18,7 +18,6 @@ \usepackage{dirtree} \renewcommand*\DTstylecomment{\ttfamily\itshape} -\usepackage[scaled=0.88]{beramono}% \usepackage{upquote}% \usepackage{textcomp} \usepackage{xcolor} From 2b2826a83f9426fa2c34ffe153a60f2ce1859442 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Tue, 13 Aug 2019 09:32:15 +0100 Subject: [PATCH 8/9] Removed no longer required packages. --- .../technical_report/Isabelle_DOF-Manual/document/preamble.tex | 3 --- 1 file changed, 3 deletions(-) diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex b/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex index 9eecbeee..8638c698 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex +++ b/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex @@ -18,14 +18,11 @@ \usepackage{dirtree} \renewcommand*\DTstylecomment{\ttfamily\itshape} -\usepackage{upquote}% \usepackage{textcomp} \usepackage{xcolor} \usepackage{lstisadof-manual} \usepackage{xspace} \usepackage{dtk-logos} -\usepackage[caption]{subfig} -\usepackage[size=footnotesize]{caption} \usepackage{railsetup} \setcounter{secnumdepth}{2} \usepackage{index} From 731ba1c1e415b3f3469d387d251dd33af44256fc Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Tue, 13 Aug 2019 09:46:20 +0100 Subject: [PATCH 9/9] Use Isabelle/DOF URL from config file. --- install | 1 + src/document-templates/root-eptcs-UNSUPPORTED.tex | 4 ++-- src/document-templates/root-lipics-v2019-UNSUPPORTED.tex | 4 ++-- src/document-templates/root-lncs.tex | 4 ++-- src/document-templates/root-scrartcl.tex | 4 ++-- src/document-templates/root-scrreprt-modern.tex | 4 ++-- src/document-templates/root-scrreprt.tex | 4 ++-- src/scripts/build | 2 +- src/scripts/build_lib.sh | 2 +- 9 files changed, 15 insertions(+), 14 deletions(-) diff --git a/install b/install index 3133b5f9..18544ff7 100755 --- a/install +++ b/install @@ -232,6 +232,7 @@ install_and_register(){ echo 'ISABELLE_TOOLS=$ISABELLE_TOOLS:$ISABELLE_HOME_USER/DOF/Tools' \ >> "$DIR/settings" fi + sed -i -e "s||$DOF_URL|" $ISABELLE_HOME_USER/DOF/*/* grep -q $PWD\$ $ISABELLE_HOME_USER/ROOTS || echo "$PWD" >> $ISABELLE_HOME_USER/ROOTS } diff --git a/src/document-templates/root-eptcs-UNSUPPORTED.tex b/src/document-templates/root-eptcs-UNSUPPORTED.tex index 7259a50a..55fe4204 100644 --- a/src/document-templates/root-eptcs-UNSUPPORTED.tex +++ b/src/document-templates/root-eptcs-UNSUPPORTED.tex @@ -39,10 +39,10 @@ This is a Isabelle_DOF project. The document preparation requires the Isabelle_DOF framework. Please obtain the framework by cloning the Isabelle_DOF git repository, i.e.: - "git clone https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF" + "git clone " You can install the framework as follows: "cd Isabelle_DOF/document-generator && ./install"}{% - For further help, see https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF} + For further help, see } } \newcommand{\subtitle}[1]{% diff --git a/src/document-templates/root-lipics-v2019-UNSUPPORTED.tex b/src/document-templates/root-lipics-v2019-UNSUPPORTED.tex index 73401845..b43da517 100644 --- a/src/document-templates/root-lipics-v2019-UNSUPPORTED.tex +++ b/src/document-templates/root-lipics-v2019-UNSUPPORTED.tex @@ -35,10 +35,10 @@ This is a Isabelle_DOF project. The document preparation requires the Isabelle_DOF framework. Please obtain the framework by cloning the Isabelle_DOF git repository, i.e.: - "git clone https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF" + "git clone " You can install the framework as follows: "cd Isabelle_DOF/document-generator && ./install"}{% - For further help, see https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF} + For further help, see } } diff --git a/src/document-templates/root-lncs.tex b/src/document-templates/root-lncs.tex index 0e76c47d..efbd393e 100644 --- a/src/document-templates/root-lncs.tex +++ b/src/document-templates/root-lncs.tex @@ -39,10 +39,10 @@ This is a Isabelle_DOF project. The document preparation requires the Isabelle_DOF framework. Please obtain the framework by cloning the Isabelle_DOF git repository, i.e.: - "git clone https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF" + "git clone " You can install the framework as follows: "cd Isabelle_DOF/document-generator && ./install"}{% - For further help, see https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF} + For further help, see } } \input{ontologies} \IfFileExists{preamble.tex}{\input{preamble.tex}}{}% diff --git a/src/document-templates/root-scrartcl.tex b/src/document-templates/root-scrartcl.tex index 7624ccca..8ed5a07e 100644 --- a/src/document-templates/root-scrartcl.tex +++ b/src/document-templates/root-scrartcl.tex @@ -34,10 +34,10 @@ This is a Isabelle_DOF project. The document preparation requires the Isabelle_DOF framework. Please obtain the framework by cloning the Isabelle_DOF git repository, i.e.: - "git clone https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF" + "git clone " You can install the framework as follows: "cd Isabelle_DOF/document-generator && ./install"}{% - For further help, see https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF} + For further help, see } } \input{ontologies} \IfFileExists{preamble.tex}{\input{preamble.tex}}{}% diff --git a/src/document-templates/root-scrreprt-modern.tex b/src/document-templates/root-scrreprt-modern.tex index 974754fb..d30da358 100644 --- a/src/document-templates/root-scrreprt-modern.tex +++ b/src/document-templates/root-scrreprt-modern.tex @@ -55,10 +55,10 @@ This is a Isabelle_DOF project. The document preparation requires the Isabelle_DOF framework. Please obtain the framework by cloning the Isabelle_DOF git repository, i.e.: - "git clone https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF" + "git clone " You can install the framework as follows: "cd Isabelle_DOF/document-generator && ./install"}{% - For further help, see https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF} + For further help, see } } \input{ontologies} \IfFileExists{preamble.tex}{\input{preamble.tex}}{}% diff --git a/src/document-templates/root-scrreprt.tex b/src/document-templates/root-scrreprt.tex index dd6c6463..c892a403 100644 --- a/src/document-templates/root-scrreprt.tex +++ b/src/document-templates/root-scrreprt.tex @@ -34,10 +34,10 @@ This is a Isabelle_DOF project. The document preparation requires the Isabelle_DOF framework. Please obtain the framework by cloning the Isabelle_DOF git repository, i.e.: - "git clone https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF" + "git clone " You can install the framework as follows: "cd Isabelle_DOF/document-generator && ./install"}{% - For further help, see https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF} + For further help, see } } \input{ontologies} \IfFileExists{preamble.tex}{\input{preamble.tex}}{}% diff --git a/src/scripts/build b/src/scripts/build index 71e478ad..c6aeaad4 100755 --- a/src/scripts/build +++ b/src/scripts/build @@ -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 "the Isabelle/DOF framework. Please obtain the framework by cloning" >&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 " >&2 echo "You can install the framework as follows:" >&2 echo " cd Isabelle_DOF/document-generator" >&2 echo " ./install" diff --git a/src/scripts/build_lib.sh b/src/scripts/build_lib.sh index 606a0f26..e6b88613 100755 --- a/src/scripts/build_lib.sh +++ b/src/scripts/build_lib.sh @@ -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 "the Isabelle/DOF framework. Please obtain the framework by cloning" >&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 " >&2 echo "You can install the framework as follows:" >&2 echo " cd Isabelle_DOF/document-generator" >&2 echo " ./install"