nicolas.meric
/
Isabelle_DOF
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Changed project configuration to a single configuration file.

This commit is contained in:
Achim D. Brucker 2019-01-08 11:06:33 +00:00
parent 209c9aaca8
commit a0a6c47fc6
23 changed files with 75 additions and 127 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
document-generator/Tools/DOF_mkroot
View File

@ -135,17 +135,15 @@ fi
if [ "$DOC" = true ]; then
$ISABELLE_TOOL mkroot -d -n "$NAME" "$DIR"
echo " \"preamble.tex\"" >> "$DIR"/ROOT
echo " \"ontologies.tex\"" >> "$DIR"/ROOT
echo " \"build\"" >> "$DIR"/ROOT
sed -i -e "s/root.tex/root.inf/" "$DIR"/ROOT
sed -i -e "s/root.tex/isadof.cfg/" "$DIR"/ROOT
rm -f "$DIR"/document/root.tex
TITLE=$(echo "$NAME" | tr _ - | tr -d '\\')
AUTHOR=$(echo "By $USER" | tr _ - | tr -d '\\')
echo $TEMPLATE > "$DIR"/document/root.inf
echo "Template: $TEMPLATE" > "$DIR"/document/isadof.cfg
cp "$ISABELLE_HOME_USER/DOF/document-template/build" "$DIR"/document/
cp "$ISABELLE_HOME_USER/DOF/document-template/ontologies.tex" "$DIR"/document/
for o in $ONTOLOGY; do
echo "\usepackage{DOF-$o}" >> "$DIR"/document/ontologies.tex;
echo "Ontology: $o" >> "$DIR"/document/isadof.cfg;
done
sed -e "s/<AUTHOR>/$AUTHOR/" -e "s/<TITLE>/$TITLE/" "$ISABELLE_HOME_USER/DOF/document-template/preamble.tex" > "$DIR"/document/preamble.tex
else

67
document-generator/document-template/build_lib.sh
View File

@ -49,17 +49,64 @@ if [ ! -f $ISABELLE_HOME_USER/DOF/latex/DOF-core.sty ]; then
exit 1
fi
if [ ! -f root.inf ]; then
if [ -f "$DIR/$ROOT_NAME.tex" ]; then
echo ""
echo "Error: Found root file ($DIR/$ROOT_NAME.tex)"
echo "====="
echo "Isabelle/DOF does not use the Isabelle root file setup. Please check"
echo "your project setup. Your $DIR/isadof.cfg should define a Isabelle/DOF"
echo "template and your project should not include a root file."
echo ""
exit 1
fi
if [ -f "$DIR/ontologies.tex" ]; then
echo ""
echo "Error: Old project setup, found a ontologies file ($DIR/ontologies.tex)"
echo "====="
echo "Isabelle/DOF does no longer support the use of $DIR/ontologies.tex. The"
echo "required ontologies should be defined in $DIR/isadof.cfg."
echo ""
exit 1
fi
if [ -f "$DIR/$ROOT_NAME.tex" ]; then
echo ""
echo "Error: Found root file ($DIR/$ROOT_NAME.tex)"
echo "====="
echo "Isabelle/DOF does not make use of the Isabelle root file mechanism."
echo "Please check your Isabelle/DOF setup."
exit 1
fi
if [ ! -f isadof.cfg ]; then
echo ""
echo "Error: Isabelle/DOF document setup not correct"
echo "====="
echo "Could not find root.inf. Please upgrade your Isabelle/DOF document"
echo "Could not find isadof.cfg. Please upgrade your Isabelle/DOF document"
echo "setup manually."
exit 1
fi
ROOT="$ISABELLE_HOME_USER/DOF/document-template/root-$(cat root.inf).tex"
if [ ! -f $ROOT]; then
TEMPLATE=""
ONTOLOGY="core"
CONFIG="isadof.cfg"
while IFS= read -r line;do
fields=($(printf "%s" "$line"|cut -d':' --output-delimiter=' ' -f1-))
if [[ "${fields[0]}" = "Template" ]]; then
TEMPLATE="${fields[1]}"
fi
if [[ "${fields[0]}" = "Ontology" ]]; then
ONTOLOGY="$ONTOLOGY ${fields[1]}"
fi
done < $CONFIG
for o in $ONTOLOGY; do
echo "\usepackage{DOF-$o}" >> ontologies.tex;
done
ROOT="$ISABELLE_HOME_USER/DOF/document-template/root-$TEMPLATE.tex"
if [ ! -f $ROOT ]; then
echo ""
echo "Error: Isabelle/DOF document setup not correct"
echo "====="
@ -72,10 +119,10 @@ cp $ROOT root.tex
cp $ISABELLE_HOME_USER/DOF/latex/*.sty .
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"
$ISABELLE_TOOL latex -o sty "root.tex" && \
$ISABELLE_TOOL latex -o "$OUTFORMAT" "root.tex" && \
{ [ ! -f "$ROOT_NAME.bib" ] || $ISABELLE_TOOL latex -o bbl "root.tex"; } && \
{ [ ! -f "$ROOT_NAME.idx" ] || $ISABELLE_TOOL latex -o idx "root.tex"; } && \
$ISABELLE_TOOL latex -o "$OUTFORMAT" "root.tex" && \
$ISABELLE_TOOL latex -o "$OUTFORMAT" "root.tex"

14
document-generator/document-template/ontologies.tex
View File

@ -1,14 +0,0 @@
%% Copyright (C) 2018 The University of Sheffield
%% 2018 The University of Paris-Sud
%%
%% License:
%% This program can be redistributed and/or modified under the terms
%% of the LaTeX Project Public License Distributed from CTAN
%% archives in directory macros/latex/base/lppl.txt; either
%% version 1 of the License, or any later version.
%% OR
%% The 2-clause BSD-style license.
%%
%% SPDX-License-Identifier: LPPL-1.0+ OR BSD-2-Clause
%% This file is used for including the LaTeX ontology mappings.

3
examples/math_exam/BAC2017/ROOT
View File

@ -6,7 +6,6 @@ session "BAC2017" = "Isabelle_DOF" +
theories
BAC2017
document_files
"root.inf"
"isadof.cfg"
"preamble.tex"
"ontologies.tex"
"build"

2
examples/math_exam/BAC2017/document/isadof.cfg Normal file
View File

@ -0,0 +1,2 @@
Template: scrartcl
Ontology: mathex

17
examples/math_exam/BAC2017/document/ontologies.tex
View File

@ -1,17 +0,0 @@
% This file was modified by the DOF LaTeX converter, version 0.0.3
%% Copyright (C) 2018 The University of Sheffield
%% 2018 The University of Paris-Sud
%%
%% License:
%% This program can be redistributed and/or modified under the terms
%% of the LaTeX Project Public License Distributed from CTAN
%% archives in directory macros/latex/base/lppl.txt; either
%% version 1 of the License, or any later version.
%% OR
%% The 2-clause BSD-style license.
%%
%% SPDX-License-Identifier: LPPL-1.0+ OR BSD-2-Clause
%% This file is used for including the LaTeX ontology mappings.
\usepackage{DOF-core}
\usepackage{DOF-mathex}

1
examples/math_exam/BAC2017/document/root.inf
View File

@ -1 +0,0 @@
scrartcl

3
examples/math_exam/MathExam/ROOT
View File

@ -4,8 +4,7 @@ session "MathExam" = "Isabelle_DOF" +
MathExam
document_files
"preamble.tex"
"root.inf"
"ontologies.tex"
"isadof.cfg"
"preamble.tex"
"build"
"figures/Polynomialdeg5.png"

2
examples/math_exam/MathExam/document/isadof.cfg Normal file
View File

@ -0,0 +1,2 @@
Template: scrartcl
Ontology: mathex

17
examples/math_exam/MathExam/document/ontologies.tex
View File

@ -1,17 +0,0 @@
% This file was modified by the DOF LaTeX converter, version 0.0.3
%% Copyright (C) 2018 The University of Sheffield
%% 2018 The University of Paris-Sud
%%
%% License:
%% This program can be redistributed and/or modified under the terms
%% of the LaTeX Project Public License Distributed from CTAN
%% archives in directory macros/latex/base/lppl.txt; either
%% version 1 of the License, or any later version.
%% OR
%% The 2-clause BSD-style license.
%%
%% SPDX-License-Identifier: LPPL-1.0+ OR BSD-2-Clause
%% This file is used for including the LaTeX ontology mappings.
\usepackage{DOF-core}
\usepackage{DOF-mathex}

1
examples/math_exam/MathExam/document/root.inf
View File

@ -1 +0,0 @@
scrartcl

3
examples/scholarly_paper/2018_cicm/ROOT
View File

@ -3,12 +3,11 @@ session "IsaDofApplications" = "Isabelle_DOF" +
theories
IsaDofApplications
document_files
"root.inf"
"isadof.cfg"
"root.bib"
"preamble.tex"
"build"
"lstisadof.sty"
"ontologies.tex"
"figures/isabelle-architecture.pdf"
"figures/Dogfood-Intro.png"
"figures/InteractiveMathSheet.png"

2
examples/scholarly_paper/2018_cicm/document/isadof.cfg Normal file
View File

@ -0,0 +1,2 @@
Template: scrartcl
Ontology: scholarly_paper

17
examples/scholarly_paper/2018_cicm/document/ontologies.tex
View File

@ -1,17 +0,0 @@
% This file was modified by the DOF LaTeX converter, version 0.0.3
%% Copyright (C) 2018 The University of Sheffield
%% 2018 The University of Paris-Sud
%%
%% License:
%% This program can be redistributed and/or modified under the terms
%% of the LaTeX Project Public License Distributed from CTAN
%% archives in directory macros/latex/base/lppl.txt; either
%% version 1 of the License, or any later version.
%% OR
%% The 2-clause BSD-style license.
%%
%% SPDX-License-Identifier: LPPL-1.0+ OR BSD-2-Clause
%% This file is used for including the LaTeX ontology mappings.
\usepackage{DOF-core}
\usepackage{DOF-scholarly_paper}

1
examples/scholarly_paper/2018_cicm/document/root.inf
View File

@ -1 +0,0 @@
scrartcl

3
examples/technical_report/IsaDof_Manual/ROOT
View File

@ -3,12 +3,11 @@ session "IsaDof_Manual" = "Isabelle_DOF" +
theories
IsaDofManual
document_files
"root.inf"
"isadof.cfg"
"root.bib"
"preamble.tex"
"build"
"lstisadof.sty"
"ontologies.tex"
"figures/isabelle-architecture.pdf"
"figures/Dogfood-Intro.png"
"figures/InteractiveMathSheet.png"

2
examples/technical_report/IsaDof_Manual/document/isadof.cfg Normal file
View File

@ -0,0 +1,2 @@
Template: scrreprt
Ontology: technical_report

16
examples/technical_report/IsaDof_Manual/document/ontologies.tex
View File

@ -1,16 +0,0 @@
%% Copyright (C) 2018 The University of Sheffield
%% 2018 The University of Paris-Sud
%%
%% License:
%% This program can be redistributed and/or modified under the terms
%% of the LaTeX Project Public License Distributed from CTAN
%% archives in directory macros/latex/base/lppl.txt; either
%% version 1 of the License, or any later version.
%% OR
%% The 2-clause BSD-style license.
%%
%% SPDX-License-Identifier: LPPL-1.0+ OR BSD-2-Clause
%% This file is used for including the LaTeX ontology mappings.
\usepackage{DOF-core}
\usepackage{DOF-technical_report}

1
examples/technical_report/IsaDof_Manual/document/root.inf
View File

@ -1 +0,0 @@
scrreprt

3
examples/technical_report/TR_my_commented_isabelle/ROOT
View File

@ -3,9 +3,8 @@ session "TR_mycommentedisabelle" = "Isabelle_DOF" +
theories
"MyCommentedIsabelle"
document_files
"root.inf"
"isadof.cfg"
"preamble.tex"
"ontologies.tex"
"prooftree.sty"
"build"
"figures/text-element.pdf"

2
examples/technical_report/TR_my_commented_isabelle/document/isadof.cfg Normal file
View File

@ -0,0 +1,2 @@
Template: scrreprt
Ontology: technical_report

16
examples/technical_report/TR_my_commented_isabelle/document/ontologies.tex
View File

@ -1,16 +0,0 @@
%% Copyright (C) 2018 The University of Sheffield
%% 2018 The University of Paris-Sud
%%
%% License:
%% This program can be redistributed and/or modified under the terms
%% of the LaTeX Project Public License Distributed from CTAN
%% archives in directory macros/latex/base/lppl.txt; either
%% version 1 of the License, or any later version.
%% OR
%% The 2-clause BSD-style license.
%%
%% SPDX-License-Identifier: LPPL-1.0+ OR BSD-2-Clause
%% This file is used for including the LaTeX ontology mappings.
\usepackage{DOF-core}
\usepackage{DOF-technical_report}

1
examples/technical_report/TR_my_commented_isabelle/document/root.inf
View File

@ -1 +0,0 @@
scrreprt