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

Reworked root.tex setup. 

The root.tex is now copied from the user installation directory
on each build to avoid problems with an outdated document setup.
This commit is contained in:
Achim D. Brucker 2019-01-06 17:01:13 +00:00
parent 5f5e8694d1
commit d03052f4d6
30 changed files with 220 additions and 518 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
document-generator/Tools/DOF_mkroot
View File

@ -1,5 +1,5 @@
#/usr/bin/env bash
# Copyright (c) 2018 The University of Sheffield. All rights reserved.
# Copyright (c) 2018-2019 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
@ -137,15 +137,17 @@ if [ "$DOC" = true ]; then
echo " \"preamble.tex\"" >> "$DIR"/ROOT
echo " \"ontologies.tex\"" >> "$DIR"/ROOT
echo " \"build\"" >> "$DIR"/ROOT
sed -i -e "s/root.tex/root.inf/" "$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
cp "$ISABELLE_HOME_USER/DOF/document-template/build" "$DIR"/document/
cp "$ISABELLE_HOME_USER/DOF/document-template/preamble.tex" "$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;
done
sed -e "s/<AUTHOR>/$AUTHOR/" -e "s/<TITLE>/$TITLE/" "$ISABELLE_HOME_USER/DOF/document-template/root-$TEMPLATE.tex" > "$DIR"/document/root.tex
sed -e "s/<AUTHOR>/$AUTHOR/" -e "s/<TITLE>/$TITLE/" "$ISABELLE_HOME_USER/DOF/document-template/preamble.tex" > "$DIR"/document/preamble.tex
else
$ISABELLE_TOOL mkroot -n "$NAME"
fi

33
document-generator/document-template/build
View File

@ -1,5 +1,5 @@
#!/usr/bin/env bash
# Copyright (c) 2018 The University of Sheffield. All rights reserved.
# Copyright (c) 2018-2019 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
@ -36,11 +36,11 @@ ROOT_NAME="root_$NAME"
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 "Error: 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"
@ -49,6 +49,27 @@ if [ ! -f $ISABELLE_HOME_USER/DOF/latex/DOF-core.sty ]; then
exit 1
fi
if [ ! -f root.inf ]; then
echo ""
echo "Error: Isabelle/DOF document setup not correct"
echo "====="
echo "Could not find root.inf. 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
echo ""
echo "Error: Isabelle/DOF document setup not correct"
echo "====="
echo "Could not find root file ($ROOT)."
echo "Please upgrade your Isabelle/DOF document setup manually."
exit 1
fi
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" && \

3
document-generator/document-template/preamble.tex
View File

@ -12,3 +12,6 @@
%% SPDX-License-Identifier: LPPL-1.0+ OR BSD-2-Clause
%% This is a placeholder for user-specific configuration and packages.
\title{<TITLE>}
\author{<AUTHOR>}

2
document-generator/document-template/root-scrartcl.tex
View File

@ -67,8 +67,6 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\title{<TITLE>}
\author{<AUTHOR>}
\begin{document}
\maketitle
\tableofcontents

2
document-generator/document-template/root-scrreprt.tex
View File

@ -67,8 +67,6 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\title{<TITLE>}
\author{<AUTHOR>}
\begin{document}
\maketitle
\tableofcontents

2
examples/math_exam/BAC2017/ROOT
View File

@ -7,6 +7,6 @@ session "BAC2017" = "Functional-Automata" +
theories
BAC2017
document_files
"root.tex"
"root.inf"
"preamble.tex"
"build"

45
examples/math_exam/BAC2017/document/build
View File

@ -1,5 +1,5 @@
#!/usr/bin/env bash
# Copyright (c) 2018 The University of Sheffield. All rights reserved.
# Copyright (c) 2018-2019 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
@ -34,13 +34,13 @@ 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
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 "Error: 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"
@ -49,26 +49,27 @@ if [ ! -f $ISABELLE_HOME_USER/DOF/lib/dof_latex_converter.jar ]; then
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
if [ ! -f root.inf ]; 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."
echo "Error: Isabelle/DOF document setup not correct"
echo "====="
echo "Could not find root.inf. Please upgrade your Isabelle/DOF document"
echo "setup manually."
exit 1
fi
$ISABELLE_TOOL scala $ISABELLE_HOME_USER/DOF/lib/dof_latex_converter.jar .
ROOT="$ISABELLE_HOME_USER/DOF/document-template/root-$(cat root.inf).tex"
if [ ! -f $ROOT]; then
echo ""
echo "Error: Isabelle/DOF document setup not correct"
echo "====="
echo "Could not find root file ($ROOT)."
echo "Please upgrade your Isabelle/DOF document setup manually."
exit 1
fi
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" && \

3
examples/math_exam/BAC2017/document/preamble.tex
View File

@ -13,6 +13,9 @@
%% This is a placeholder for user-specific configuration and packages.
\title{<TITLE>}
\author{<AUTHOR>}
\newkeycommand\isaDofTextExercise[label=,type=,Exercise.content=,content=,concerns=,][1]{%
\begin{Exercise}
#1

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

@ -0,0 +1 @@
scrartcl

86
examples/math_exam/BAC2017/document/root.tex
View File

@ -1,86 +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
%% Warning: Do Not Edit!
%% =====================
%% This is the root file for the Isabelle/DOF.
%% All customization and/or additional packages should be added to the file
%% preamble.tex.
\RequirePackage{ifvtex}
\documentclass[fontsize=11pt,DIV12,paper=a4]{scrartcl}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{textcomp}
\usepackage[english]{babel}
\usepackage{isabelle}
\usepackage{isabellesym}
\IfFileExists{DOF-core.sty}{}{%
\PackageError{DOF-core}{Isabelle/DOF not installed.
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/HOL-OCL/Isabelle_DOF"
You can install the framework as follows:
"cd Isabelle_DOF/document-generator && ./install"}{%
For further help, see https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF}
}
\input{ontologies}
\IfFileExists{preamble.tex}{\input{preamble.tex}}{}%
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage[numbers, sort&compress, sectionbib]{natbib}
\usepackage{graphicx}
\usepackage{hyperref}
\setcounter{tocdepth}{3}
\hypersetup{%
bookmarksdepth=3
,pdfpagelabels
,pageanchor=true
,bookmarksnumbered
,plainpages=false
} % more detailed digital TOC (aka bookmarks)
\sloppy
\allowdisplaybreaks[4]
\urlstyle{rm}
\isabellestyle{it}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Overrides the (rightfully issued) warning by Koma Script that \rm
%%% etc. should not be used (they are deprecated since more than a
%%% decade)
\DeclareOldFontCommand{\rm}{\normalfont\rmfamily}{\mathrm}
\DeclareOldFontCommand{\sf}{\normalfont\sffamily}{\mathsf}
\DeclareOldFontCommand{\tt}{\normalfont\ttfamily}{\mathtt}
\DeclareOldFontCommand{\bf}{\normalfont\bfseries}{\mathbf}
\DeclareOldFontCommand{\it}{\normalfont\itshape}{\mathit}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\title{}
\author{}
\begin{document}
\maketitle
\tableofcontents
\input{session}
% optional bibliography
\IfFileExists{root.bib}{%
\bibliographystyle{abbrvnat}
\bibliography{root}
}{}
\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:

2
examples/math_exam/MathExam/ROOT
View File

@ -7,7 +7,7 @@ session "MathExam" = "Functional-Automata" +
MathExam
document_files
"preamble.tex"
"root.tex"
"root.inf"
"ontologies.tex"
"preamble.tex"
"build"

45
examples/math_exam/MathExam/document/build
View File

@ -1,5 +1,5 @@
#!/usr/bin/env bash
# Copyright (c) 2018 The University of Sheffield. All rights reserved.
# Copyright (c) 2018-2019 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
@ -34,13 +34,13 @@ 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
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 "Error: 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"
@ -49,26 +49,27 @@ if [ ! -f $ISABELLE_HOME_USER/DOF/lib/dof_latex_converter.jar ]; then
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
if [ ! -f root.inf ]; 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."
echo "Error: Isabelle/DOF document setup not correct"
echo "====="
echo "Could not find root.inf. Please upgrade your Isabelle/DOF document"
echo "setup manually."
exit 1
fi
$ISABELLE_TOOL scala $ISABELLE_HOME_USER/DOF/lib/dof_latex_converter.jar .
ROOT="$ISABELLE_HOME_USER/DOF/document-template/root-$(cat root.inf).tex"
if [ ! -f $ROOT]; then
echo ""
echo "Error: Isabelle/DOF document setup not correct"
echo "====="
echo "Could not find root file ($ROOT)."
echo "Please upgrade your Isabelle/DOF document setup manually."
exit 1
fi
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" && \

4
examples/math_exam/MathExam/document/preamble.tex
View File

@ -12,3 +12,7 @@
%% SPDX-License-Identifier: LPPL-1.0+ OR BSD-2-Clause
%% This is a placeholder for user-specific configuration and packages.
\title{<TITLE>}
\author{<AUTHOR>}

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

@ -0,0 +1 @@
scrartcl

86
examples/math_exam/MathExam/document/root.tex
View File

@ -1,86 +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
%% Warning: Do Not Edit!
%% =====================
%% This is the root file for the Isabelle/DOF.
%% All customization and/or additional packages should be added to the file
%% preamble.tex.
\RequirePackage{ifvtex}
\documentclass[fontsize=11pt,DIV12,paper=a4]{scrartcl}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{textcomp}
\usepackage[english]{babel}
\usepackage{isabelle}
\usepackage{isabellesym}
\IfFileExists{DOF-core.sty}{}{%
\PackageError{DOF-core}{Isabelle/DOF not installed.
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/HOL-OCL/Isabelle_DOF"
You can install the framework as follows:
"cd Isabelle_DOF/document-generator && ./install"}{%
For further help, see https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF}
}
\input{ontologies}
\IfFileExists{preamble.tex}{\input{preamble.tex}}{}%
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage[numbers, sort&compress, sectionbib]{natbib}
\usepackage{graphicx}
\usepackage{hyperref}
\setcounter{tocdepth}{3}
\hypersetup{%
bookmarksdepth=3
,pdfpagelabels
,pageanchor=true
,bookmarksnumbered
,plainpages=false
} % more detailed digital TOC (aka bookmarks)
\sloppy
\allowdisplaybreaks[4]
\urlstyle{rm}
\isabellestyle{it}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Overrides the (rightfully issued) warning by Koma Script that \rm
%%% etc. should not be used (they are deprecated since more than a
%%% decade)
\DeclareOldFontCommand{\rm}{\normalfont\rmfamily}{\mathrm}
\DeclareOldFontCommand{\sf}{\normalfont\sffamily}{\mathsf}
\DeclareOldFontCommand{\tt}{\normalfont\ttfamily}{\mathtt}
\DeclareOldFontCommand{\bf}{\normalfont\bfseries}{\mathbf}
\DeclareOldFontCommand{\it}{\normalfont\itshape}{\mathit}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\title{<TITLE>}
\author{<AUTHOR>}
\begin{document}
\maketitle
\tableofcontents
\input{session}
% optional bibliography
\IfFileExists{root.bib}{%
\bibliographystyle{abbrvnat}
\bibliography{root}
}{}
\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:

2
examples/scholarly_paper/2018_cicm/ROOT
View File

@ -5,7 +5,7 @@ session "IsaDofApplications" = "Functional-Automata" +
theories
IsaDofApplications
document_files
"root.tex"
"root.inf"
"root.bib"
"preamble.tex"
"build"

33
examples/scholarly_paper/2018_cicm/document/build
View File

@ -1,5 +1,5 @@
#!/usr/bin/env bash
# Copyright (c) 2018 The University of Sheffield. All rights reserved.
# Copyright (c) 2018-2019 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
@ -36,11 +36,11 @@ ROOT_NAME="root_$NAME"
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 "Error: 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"
@ -49,6 +49,27 @@ if [ ! -f $ISABELLE_HOME_USER/DOF/latex/DOF-core.sty ]; then
exit 1
fi
if [ ! -f root.inf ]; then
echo ""
echo "Error: Isabelle/DOF document setup not correct"
echo "====="
echo "Could not find root.inf. 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
echo ""
echo "Error: Isabelle/DOF document setup not correct"
echo "====="
echo "Could not find root file ($ROOT)."
echo "Please upgrade your Isabelle/DOF document setup manually."
exit 1
fi
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" && \

21
examples/scholarly_paper/2018_cicm/document/preamble.tex
View File

@ -1,4 +1,19 @@
% 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 is a placeholder for user-specific configuration and packages.
\IfFileExists{beramono.sty}{\usepackage[scaled=0.88]{beramono}}{}%
\IfFileExists{upquote.sty}{\usepackage{upquote}}{}%
\usepackage{textcomp}
@ -60,6 +75,10 @@
\isadof{}.
}}
\title{<TITLE>}
\author{<AUTHOR>}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root.tex"

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

@ -0,0 +1 @@
scrartcl

85
examples/scholarly_paper/2018_cicm/document/root.tex
View File

@ -1,85 +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
%% Warning: Do Not Edit!
%% =====================
%% This is the root file for the Isabelle/DOF.
%% All customization and/or additional packages should be added to the file
%% preamble.tex.
\RequirePackage{ifvtex}
\documentclass[fontsize=11pt,DIV12,paper=a4]{scrartcl}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{textcomp}
\usepackage[english]{babel}
\usepackage{isabelle}
\usepackage{isabellesym}
\IfFileExists{DOF-core.sty}{}{%
\PackageError{DOF-core}{Isabelle/DOF not installed.
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/HOL-OCL/Isabelle_DOF"
You can install the framework as follows:
"cd Isabelle_DOF/document-generator && ./install"}{%
For further help, see https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF}
}
\input{ontologies}
\IfFileExists{preamble.tex}{\input{preamble.tex}}{}%
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage[numbers, sort&compress, sectionbib]{natbib}
\usepackage{graphicx}
\usepackage{hyperref}
\setcounter{tocdepth}{3}
\hypersetup{%
bookmarksdepth=3
,pdfpagelabels
,pageanchor=true
,bookmarksnumbered
,plainpages=false
} % more detailed digital TOC (aka bookmarks)
\sloppy
\allowdisplaybreaks[4]
\urlstyle{rm}
\isabellestyle{it}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Overrides the (rightfully issued) warning by Koma Script that \rm
%%% etc. should not be used (they are deprecated since more than a
%%% decade)
\DeclareOldFontCommand{\rm}{\normalfont\rmfamily}{\mathrm}
\DeclareOldFontCommand{\sf}{\normalfont\sffamily}{\mathsf}
\DeclareOldFontCommand{\tt}{\normalfont\ttfamily}{\mathtt}
\DeclareOldFontCommand{\bf}{\normalfont\bfseries}{\mathbf}
\DeclareOldFontCommand{\it}{\normalfont\itshape}{\mathit}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\title{<TITLE>}
\author{<AUTHOR>}
\begin{document}
\maketitle
\input{session}
% optional bibliography
\IfFileExists{root.bib}{%
\bibliographystyle{abbrvnat}
\bibliography{root}
}{}
\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:

2
examples/technical_report/IsaDof_Manual/ROOT
View File

@ -6,7 +6,7 @@ session "IsaDof_Manual" = "Functional-Automata" +
theories
IsaDofManual
document_files
"root.tex"
"root.inf"
"root.bib"
"preamble.tex"
"build"

33
examples/technical_report/IsaDof_Manual/document/build
View File

@ -1,5 +1,5 @@
#!/usr/bin/env bash
# Copyright (c) 2018 The University of Sheffield. All rights reserved.
# Copyright (c) 2018-2019 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
@ -36,11 +36,11 @@ ROOT_NAME="root_$NAME"
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 "Error: 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"
@ -49,6 +49,27 @@ if [ ! -f $ISABELLE_HOME_USER/DOF/latex/DOF-core.sty ]; then
exit 1
fi
if [ ! -f root.inf ]; then
echo ""
echo "Error: Isabelle/DOF document setup not correct"
echo "====="
echo "Could not find root.inf. 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
echo ""
echo "Error: Isabelle/DOF document setup not correct"
echo "====="
echo "Could not find root file ($ROOT)."
echo "Please upgrade your Isabelle/DOF document setup manually."
exit 1
fi
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" && \

25
examples/technical_report/IsaDof_Manual/document/preamble.tex
View File

@ -1,4 +1,18 @@
% 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 is a placeholder for user-specific configuration and packages.
\IfFileExists{beramono.sty}{\usepackage[scaled=0.88]{beramono}}{}%
\IfFileExists{upquote.sty}{\usepackage{upquote}}{}%
\usepackage{textcomp}
@ -41,10 +55,5 @@
\newcommand{\ie}{i.e.}
\newcommand{\eg}{e.g.}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root.tex"
%%% End:
\title{<TITLE>}
\author{<AUTHOR>}

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

@ -0,0 +1 @@
scrreprt

86
examples/technical_report/IsaDof_Manual/document/root.tex
View File

@ -1,86 +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
%% Warning: Do Not Edit!
%% =====================
%% This is the root file for the Isabelle/DOF.
%% All customization and/or additional packages should be added to the file
%% preamble.tex.
\RequirePackage{ifvtex}
\documentclass[fontsize=10pt,DIV12,paper=a4,open=right,twoside,abstract=true]{scrreprt}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{textcomp}
\usepackage[english]{babel}
\usepackage{isabelle}
\usepackage{isabellesym}
\IfFileExists{DOF-core.sty}{}{%
\PackageError{DOF-core}{Isabelle/DOF not installed.
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/HOL-OCL/Isabelle_DOF"
You can install the framework as follows:
"cd Isabelle_DOF/document-generator && ./install"}{%
For further help, see https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF}
}
\input{ontologies}
\IfFileExists{preamble.tex}{\input{preamble.tex}}{}%
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage[numbers, sort&compress, sectionbib]{natbib}
\usepackage{graphicx}
\usepackage{hyperref}
\setcounter{tocdepth}{3}
\hypersetup{%
bookmarksdepth=3
,pdfpagelabels
,pageanchor=true
,bookmarksnumbered
,plainpages=false
} % more detailed digital TOC (aka bookmarks)
\sloppy
\allowdisplaybreaks[4]
\urlstyle{rm}
\isabellestyle{it}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Overrides the (rightfully issued) warning by Koma Script that \rm
%%% etc. should not be used (they are deprecated since more than a
%%% decade)
\DeclareOldFontCommand{\rm}{\normalfont\rmfamily}{\mathrm}
\DeclareOldFontCommand{\sf}{\normalfont\sffamily}{\mathsf}
\DeclareOldFontCommand{\tt}{\normalfont\ttfamily}{\mathtt}
\DeclareOldFontCommand{\bf}{\normalfont\bfseries}{\mathbf}
\DeclareOldFontCommand{\it}{\normalfont\itshape}{\mathit}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\title{\isadof Technical Report Example}
\author{By Achim D. Brucker}
\begin{document}
\maketitle
\tableofcontents
\input{session}
% optional bibliography
\IfFileExists{root.bib}{%
\bibliographystyle{abbrvnat}
\bibliography{root}
}{}
\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:

2
examples/technical_report/TR_my_commented_isabelle/ROOT
View File

@ -6,7 +6,7 @@ session "TR_mycommentedisabelle" = "Functional-Automata" +
theories
"MyCommentedIsabelle"
document_files
"root.tex"
"root.inf"
"preamble.tex"
"ontologies.tex"
"prooftree.sty"

33
examples/technical_report/TR_my_commented_isabelle/document/build
View File

@ -1,5 +1,5 @@
#!/usr/bin/env bash
# Copyright (c) 2018 The University of Sheffield. All rights reserved.
# Copyright (c) 2018-2019 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
@ -36,11 +36,11 @@ ROOT_NAME="root_$NAME"
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 "Error: 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"
@ -49,6 +49,27 @@ if [ ! -f $ISABELLE_HOME_USER/DOF/latex/DOF-core.sty ]; then
exit 1
fi
if [ ! -f root.inf ]; then
echo ""
echo "Error: Isabelle/DOF document setup not correct"
echo "====="
echo "Could not find root.inf. 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
echo ""
echo "Error: Isabelle/DOF document setup not correct"
echo "====="
echo "Could not find root file ($ROOT)."
echo "Please upgrade your Isabelle/DOF document setup manually."
exit 1
fi
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" && \

4
examples/technical_report/TR_my_commented_isabelle/document/preamble.tex
View File

@ -12,4 +12,8 @@
%% SPDX-License-Identifier: LPPL-1.0+ OR BSD-2-Clause
%% This is a placeholder for user-specific configuration and packages.
\usepackage{prooftree}
\title{<TITLE>}
\author{<AUTHOR>}

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

@ -0,0 +1 @@
scrreprt

86
examples/technical_report/TR_my_commented_isabelle/document/root.tex
View File

@ -1,86 +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
%% Warning: Do Not Edit!
%% =====================
%% This is the root file for the Isabelle/DOF.
%% All customization and/or additional packages should be added to the file
%% preamble.tex.
\RequirePackage{ifvtex}
\documentclass[fontsize=10pt,DIV12,paper=a4,open=right,twoside,abstract=true]{scrreprt}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{textcomp}
\usepackage[english]{babel}
\usepackage{isabelle}
\usepackage{isabellesym}
\IfFileExists{DOF-core.sty}{}{%
\PackageError{DOF-core}{Isabelle/DOF not installed.
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/HOL-OCL/Isabelle_DOF"
You can install the framework as follows:
"cd Isabelle_DOF/document-generator && ./install"}{%
For further help, see https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF}
}
\input{ontologies}
\IfFileExists{preamble.tex}{\input{preamble.tex}}{}%
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage[numbers, sort&compress, sectionbib]{natbib}
\usepackage{graphicx}
\usepackage{hyperref}
\setcounter{tocdepth}{3}
\hypersetup{%
bookmarksdepth=3
,pdfpagelabels
,pageanchor=true
,bookmarksnumbered
,plainpages=false
} % more detailed digital TOC (aka bookmarks)
\sloppy
\allowdisplaybreaks[4]
\urlstyle{rm}
\isabellestyle{it}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Overrides the (rightfully issued) warning by Koma Script that \rm
%%% etc. should not be used (they are deprecated since more than a
%%% decade)
\DeclareOldFontCommand{\rm}{\normalfont\rmfamily}{\mathrm}
\DeclareOldFontCommand{\sf}{\normalfont\sffamily}{\mathsf}
\DeclareOldFontCommand{\tt}{\normalfont\ttfamily}{\mathtt}
\DeclareOldFontCommand{\bf}{\normalfont\bfseries}{\mathbf}
\DeclareOldFontCommand{\it}{\normalfont\itshape}{\mathit}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\title{.}
\author{By bu}
\begin{document}
\maketitle
\tableofcontents
\input{session}
% optional bibliography
\IfFileExists{root.bib}{%
\bibliographystyle{abbrvnat}
\bibliography{root}
}{}
\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: