diff --git a/examples/math_exam/BAC2017/ROOT b/examples/math_exam/BAC2017/ROOT index 9c8866ca..158ed13d 100644 --- a/examples/math_exam/BAC2017/ROOT +++ b/examples/math_exam/BAC2017/ROOT @@ -9,4 +9,3 @@ session "BAC2017" = "Functional-Automata" + document_files "root.tex" "preamble.tex" - "build" diff --git a/examples/math_exam/BAC2017/document/build b/examples/math_exam/BAC2017/document/build deleted file mode 100755 index bdba009f..00000000 --- a/examples/math_exam/BAC2017/document/build +++ /dev/null @@ -1,80 +0,0 @@ -#!/usr/bin/env bash -# Copyright (c) 2018 The University of Sheffield. All rights reserved. -# 2018 The University of Paris-Sud. All rights reserved. -# -# 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 - -OUTFORMAT=${1:-pdf} -NAME=${2:-root} - -set -e - -ROOT_NAME="root_$NAME" -[ ! -f "$DIR/$ROOT_NAME.tex" ] && ROOT_NAME="root" - -if [ ! -f $ISABELLE_HOME_USER/DOF/lib/dof_latex_converter.jar ]; then - echo "" - echo "Warning: Isabelle DOF not installed" - echo "========" - echo "This is a Isabelle_DOF project. The document preparation requires" - echo "the Isabelle_DOF framework. Please obtain the framework by cloning" - echo "the Isabelle_DOF git repository, i.e.: " - echo " git clone https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF" - echo "You can install the framework as follows:" - echo " cd Isabelle_DOF/document-generator" - echo " ./install" - echo "" - exit 1 -fi - -VERSION=$($ISABELLE_TOOL scala $ISABELLE_HOME_USER/DOF/lib/dof_latex_converter.jar -v) || true - -if [ "$VERSION" != "DOF LaTeX converter version 0.0.3" ]; then - echo "" - echo "Warning: Isabelle DOF version mismatch" - echo "========" - echo " Build script version: DOF LaTeX converter version 0.0.3" - echo " DOF LaTeX Converter version: $VERSION" - echo " Please take one of the following actions:" - echo " * If the build script is more recent than the converter, " - echo " then update the build script from your your Isabelle DOF" - echo " installation:" - echo " $ISABELLE_HOME_USER/DOF/document-template/build" - echo " * If the converter is more recent than the build script," - echo " please update your Isabelle DOF installation." - exit 1 -fi - -$ISABELLE_TOOL scala $ISABELLE_HOME_USER/DOF/lib/dof_latex_converter.jar . - -cp $ISABELLE_HOME_USER/DOF/latex/*.sty . - -$ISABELLE_TOOL latex -o sty "$ROOT_NAME.tex" && \ -$ISABELLE_TOOL latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \ -{ [ ! -f "$ROOT_NAME.bib" ] || $ISABELLE_TOOL latex -o bbl "$ROOT_NAME.tex"; } && \ -{ [ ! -f "$ROOT_NAME.idx" ] || $ISABELLE_TOOL latex -o idx "$ROOT_NAME.tex"; } && \ -$ISABELLE_TOOL latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \ -$ISABELLE_TOOL latex -o "$OUTFORMAT" "$ROOT_NAME.tex" - diff --git a/examples/math_exam/MathExam/ROOT b/examples/math_exam/MathExam/ROOT index 08ccfc79..5b35f123 100644 --- a/examples/math_exam/MathExam/ROOT +++ b/examples/math_exam/MathExam/ROOT @@ -10,5 +10,4 @@ session "MathExam" = "Functional-Automata" + "root.tex" "ontologies.tex" "preamble.tex" - "build" "figures/Polynomialdeg5.png" diff --git a/examples/math_exam/MathExam/document/build b/examples/math_exam/MathExam/document/build deleted file mode 100755 index bdba009f..00000000 --- a/examples/math_exam/MathExam/document/build +++ /dev/null @@ -1,80 +0,0 @@ -#!/usr/bin/env bash -# Copyright (c) 2018 The University of Sheffield. All rights reserved. -# 2018 The University of Paris-Sud. All rights reserved. -# -# 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 - -OUTFORMAT=${1:-pdf} -NAME=${2:-root} - -set -e - -ROOT_NAME="root_$NAME" -[ ! -f "$DIR/$ROOT_NAME.tex" ] && ROOT_NAME="root" - -if [ ! -f $ISABELLE_HOME_USER/DOF/lib/dof_latex_converter.jar ]; then - echo "" - echo "Warning: Isabelle DOF not installed" - echo "========" - echo "This is a Isabelle_DOF project. The document preparation requires" - echo "the Isabelle_DOF framework. Please obtain the framework by cloning" - echo "the Isabelle_DOF git repository, i.e.: " - echo " git clone https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF" - echo "You can install the framework as follows:" - echo " cd Isabelle_DOF/document-generator" - echo " ./install" - echo "" - exit 1 -fi - -VERSION=$($ISABELLE_TOOL scala $ISABELLE_HOME_USER/DOF/lib/dof_latex_converter.jar -v) || true - -if [ "$VERSION" != "DOF LaTeX converter version 0.0.3" ]; then - echo "" - echo "Warning: Isabelle DOF version mismatch" - echo "========" - echo " Build script version: DOF LaTeX converter version 0.0.3" - echo " DOF LaTeX Converter version: $VERSION" - echo " Please take one of the following actions:" - echo " * If the build script is more recent than the converter, " - echo " then update the build script from your your Isabelle DOF" - echo " installation:" - echo " $ISABELLE_HOME_USER/DOF/document-template/build" - echo " * If the converter is more recent than the build script," - echo " please update your Isabelle DOF installation." - exit 1 -fi - -$ISABELLE_TOOL scala $ISABELLE_HOME_USER/DOF/lib/dof_latex_converter.jar . - -cp $ISABELLE_HOME_USER/DOF/latex/*.sty . - -$ISABELLE_TOOL latex -o sty "$ROOT_NAME.tex" && \ -$ISABELLE_TOOL latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \ -{ [ ! -f "$ROOT_NAME.bib" ] || $ISABELLE_TOOL latex -o bbl "$ROOT_NAME.tex"; } && \ -{ [ ! -f "$ROOT_NAME.idx" ] || $ISABELLE_TOOL latex -o idx "$ROOT_NAME.tex"; } && \ -$ISABELLE_TOOL latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \ -$ISABELLE_TOOL latex -o "$OUTFORMAT" "$ROOT_NAME.tex" - diff --git a/examples/scholarly_paper/2018_cicm/ROOT b/examples/scholarly_paper/2018_cicm/ROOT index 0bce4fa7..b82e2054 100644 --- a/examples/scholarly_paper/2018_cicm/ROOT +++ b/examples/scholarly_paper/2018_cicm/ROOT @@ -8,7 +8,6 @@ session "IsaDofApplications" = "Functional-Automata" + "root.tex" "root.bib" "preamble.tex" - "build" "lstisadof.sty" "ontologies.tex" "figures/isabelle-architecture.pdf" diff --git a/examples/scholarly_paper/2018_cicm/document/build b/examples/scholarly_paper/2018_cicm/document/build deleted file mode 100755 index 893af0ef..00000000 --- a/examples/scholarly_paper/2018_cicm/document/build +++ /dev/null @@ -1,60 +0,0 @@ -#!/usr/bin/env bash -# Copyright (c) 2018 The University of Sheffield. All rights reserved. -# 2018 The University of Paris-Sud. All rights reserved. -# -# 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 - -OUTFORMAT=${1:-pdf} -NAME=${2:-root} - -set -e - -ROOT_NAME="root_$NAME" -[ ! -f "$DIR/$ROOT_NAME.tex" ] && ROOT_NAME="root" - -if [ ! -f $ISABELLE_HOME_USER/DOF/latex/DOF-core.sty ]; then - echo "" - echo "Warning: Isabelle DOF not installed" - echo "========" - echo "This is a Isabelle_DOF project. The document preparation requires" - echo "the Isabelle_DOF framework. Please obtain the framework by cloning" - echo "the Isabelle_DOF git repository, i.e.: " - echo " git clone https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF" - echo "You can install the framework as follows:" - echo " cd Isabelle_DOF/document-generator" - echo " ./install" - echo "" - exit 1 -fi - -cp $ISABELLE_HOME_USER/DOF/latex/*.sty . - -$ISABELLE_TOOL latex -o sty "$ROOT_NAME.tex" && \ -$ISABELLE_TOOL latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \ -{ [ ! -f "$ROOT_NAME.bib" ] || $ISABELLE_TOOL latex -o bbl "$ROOT_NAME.tex"; } && \ -{ [ ! -f "$ROOT_NAME.idx" ] || $ISABELLE_TOOL latex -o idx "$ROOT_NAME.tex"; } && \ -$ISABELLE_TOOL latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \ -$ISABELLE_TOOL latex -o "$OUTFORMAT" "$ROOT_NAME.tex" - diff --git a/examples/technical_report/IsaDof_Manual/ROOT b/examples/technical_report/IsaDof_Manual/ROOT index 3ee3f6c6..ae87ce74 100644 --- a/examples/technical_report/IsaDof_Manual/ROOT +++ b/examples/technical_report/IsaDof_Manual/ROOT @@ -9,7 +9,6 @@ session "IsaDof_Manual" = "Functional-Automata" + "root.tex" "root.bib" "preamble.tex" - "build" "lstisadof.sty" "ontologies.tex" "figures/isabelle-architecture.pdf" diff --git a/examples/technical_report/IsaDof_Manual/document/build b/examples/technical_report/IsaDof_Manual/document/build deleted file mode 100755 index 893af0ef..00000000 --- a/examples/technical_report/IsaDof_Manual/document/build +++ /dev/null @@ -1,60 +0,0 @@ -#!/usr/bin/env bash -# Copyright (c) 2018 The University of Sheffield. All rights reserved. -# 2018 The University of Paris-Sud. All rights reserved. -# -# 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 - -OUTFORMAT=${1:-pdf} -NAME=${2:-root} - -set -e - -ROOT_NAME="root_$NAME" -[ ! -f "$DIR/$ROOT_NAME.tex" ] && ROOT_NAME="root" - -if [ ! -f $ISABELLE_HOME_USER/DOF/latex/DOF-core.sty ]; then - echo "" - echo "Warning: Isabelle DOF not installed" - echo "========" - echo "This is a Isabelle_DOF project. The document preparation requires" - echo "the Isabelle_DOF framework. Please obtain the framework by cloning" - echo "the Isabelle_DOF git repository, i.e.: " - echo " git clone https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF" - echo "You can install the framework as follows:" - echo " cd Isabelle_DOF/document-generator" - echo " ./install" - echo "" - exit 1 -fi - -cp $ISABELLE_HOME_USER/DOF/latex/*.sty . - -$ISABELLE_TOOL latex -o sty "$ROOT_NAME.tex" && \ -$ISABELLE_TOOL latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \ -{ [ ! -f "$ROOT_NAME.bib" ] || $ISABELLE_TOOL latex -o bbl "$ROOT_NAME.tex"; } && \ -{ [ ! -f "$ROOT_NAME.idx" ] || $ISABELLE_TOOL latex -o idx "$ROOT_NAME.tex"; } && \ -$ISABELLE_TOOL latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \ -$ISABELLE_TOOL latex -o "$OUTFORMAT" "$ROOT_NAME.tex" - diff --git a/examples/technical_report/TR_my_commented_isabelle/ROOT b/examples/technical_report/TR_my_commented_isabelle/ROOT index ae3d82fc..ace17965 100644 --- a/examples/technical_report/TR_my_commented_isabelle/ROOT +++ b/examples/technical_report/TR_my_commented_isabelle/ROOT @@ -10,7 +10,6 @@ session "TR_mycommentedisabelle" = "Functional-Automata" + "preamble.tex" "ontologies.tex" "prooftree.sty" - "build" "figures/text-element.pdf" "figures/isabelle-architecture.pdf" "figures/pure-inferences-I.pdf" diff --git a/examples/technical_report/TR_my_commented_isabelle/document/build b/examples/technical_report/TR_my_commented_isabelle/document/build deleted file mode 100755 index 893af0ef..00000000 --- a/examples/technical_report/TR_my_commented_isabelle/document/build +++ /dev/null @@ -1,60 +0,0 @@ -#!/usr/bin/env bash -# Copyright (c) 2018 The University of Sheffield. All rights reserved. -# 2018 The University of Paris-Sud. All rights reserved. -# -# 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 - -OUTFORMAT=${1:-pdf} -NAME=${2:-root} - -set -e - -ROOT_NAME="root_$NAME" -[ ! -f "$DIR/$ROOT_NAME.tex" ] && ROOT_NAME="root" - -if [ ! -f $ISABELLE_HOME_USER/DOF/latex/DOF-core.sty ]; then - echo "" - echo "Warning: Isabelle DOF not installed" - echo "========" - echo "This is a Isabelle_DOF project. The document preparation requires" - echo "the Isabelle_DOF framework. Please obtain the framework by cloning" - echo "the Isabelle_DOF git repository, i.e.: " - echo " git clone https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF" - echo "You can install the framework as follows:" - echo " cd Isabelle_DOF/document-generator" - echo " ./install" - echo "" - exit 1 -fi - -cp $ISABELLE_HOME_USER/DOF/latex/*.sty . - -$ISABELLE_TOOL latex -o sty "$ROOT_NAME.tex" && \ -$ISABELLE_TOOL latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \ -{ [ ! -f "$ROOT_NAME.bib" ] || $ISABELLE_TOOL latex -o bbl "$ROOT_NAME.tex"; } && \ -{ [ ! -f "$ROOT_NAME.idx" ] || $ISABELLE_TOOL latex -o idx "$ROOT_NAME.tex"; } && \ -$ISABELLE_TOOL latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \ -$ISABELLE_TOOL latex -o "$OUTFORMAT" "$ROOT_NAME.tex" -