forked from Isabelle_DOF/Isabelle_DOF
Merge branch 'master' of https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF
This commit is contained in:
commit
c046471d10
|
@ -40,11 +40,9 @@ The installer will
|
||||||
the AFP archive into the directory to `/home/myself/afp`, you should
|
the AFP archive into the directory to `/home/myself/afp`, you should
|
||||||
run the following command to make the AFP session `ROOTS` available to
|
run the following command to make the AFP session `ROOTS` available to
|
||||||
Isabelle:
|
Isabelle:
|
||||||
|
|
||||||
```console
|
```console
|
||||||
echo "/home/myself/afp/thys" >> ~/.isabelle/Isabelle2017/ROOTS
|
echo "/home/myself/afp/thys" >> ~/.isabelle/Isabelle2017/ROOTS
|
||||||
```
|
```
|
||||||
|
|
||||||
* install the Isabelle/DOF-plugin into the Isabelle user directory
|
* install the Isabelle/DOF-plugin into the Isabelle user directory
|
||||||
(the exact location depends on the Isabelle version).
|
(the exact location depends on the Isabelle version).
|
||||||
* check that the AFP has been installed successfully.
|
* check that the AFP has been installed successfully.
|
||||||
|
|
|
@ -135,19 +135,24 @@ fi
|
||||||
if [ "$DOC" = true ]; then
|
if [ "$DOC" = true ]; then
|
||||||
$ISABELLE_TOOL mkroot -d -n "$NAME" "$DIR"
|
$ISABELLE_TOOL mkroot -d -n "$NAME" "$DIR"
|
||||||
echo " \"preamble.tex\"" >> "$DIR"/ROOT
|
echo " \"preamble.tex\"" >> "$DIR"/ROOT
|
||||||
echo " \"ontologies.tex\"" >> "$DIR"/ROOT
|
|
||||||
echo " \"build\"" >> "$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
|
rm -f "$DIR"/document/root.tex
|
||||||
|
|
||||||
|
# Creating isadof.cfg
|
||||||
|
echo "Template: $TEMPLATE" > "$DIR"/document/isadof.cfg
|
||||||
|
cp "$ISABELLE_HOME_USER/DOF/document-template/build" "$DIR"/document/
|
||||||
|
for o in $ONTOLOGY; do
|
||||||
|
echo "Ontology: $o" >> "$DIR"/document/isadof.cfg;
|
||||||
|
done
|
||||||
|
|
||||||
|
# Creating praemble.tex
|
||||||
TITLE=$(echo "$NAME" | tr _ - | tr -d '\\')
|
TITLE=$(echo "$NAME" | tr _ - | tr -d '\\')
|
||||||
AUTHOR=$(echo "By $USER" | tr _ - | tr -d '\\')
|
AUTHOR=$(echo "By $USER" | tr _ - | tr -d '\\')
|
||||||
echo $TEMPLATE > "$DIR"/document/root.inf
|
echo "%% This is a placeholder for user-specific configuration and packages." >> "$DIR"/document/preamble.tex
|
||||||
cp "$ISABELLE_HOME_USER/DOF/document-template/build" "$DIR"/document/
|
echo "\\title{$TITLE}" >> "$DIR"/document/preamble.tex
|
||||||
cp "$ISABELLE_HOME_USER/DOF/document-template/ontologies.tex" "$DIR"/document/
|
echo "\\author{$AUTHOR}" >> "$DIR"/document/preamble.tex
|
||||||
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/preamble.tex" > "$DIR"/document/preamble.tex
|
|
||||||
else
|
else
|
||||||
$ISABELLE_TOOL mkroot -n "$NAME"
|
$ISABELLE_TOOL mkroot -n "$NAME"
|
||||||
fi
|
fi
|
||||||
|
|
|
@ -49,17 +49,64 @@ if [ ! -f $ISABELLE_HOME_USER/DOF/latex/DOF-core.sty ]; then
|
||||||
exit 1
|
exit 1
|
||||||
fi
|
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 ""
|
||||||
echo "Error: Isabelle/DOF document setup not correct"
|
echo "Error: Isabelle/DOF document setup not correct"
|
||||||
echo "====="
|
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."
|
echo "setup manually."
|
||||||
exit 1
|
exit 1
|
||||||
fi
|
fi
|
||||||
|
|
||||||
ROOT="$ISABELLE_HOME_USER/DOF/document-template/root-$(cat root.inf).tex"
|
TEMPLATE=""
|
||||||
if [ ! -f $ROOT]; then
|
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 ""
|
||||||
echo "Error: Isabelle/DOF document setup not correct"
|
echo "Error: Isabelle/DOF document setup not correct"
|
||||||
echo "====="
|
echo "====="
|
||||||
|
@ -72,10 +119,10 @@ cp $ROOT root.tex
|
||||||
cp $ISABELLE_HOME_USER/DOF/latex/*.sty .
|
cp $ISABELLE_HOME_USER/DOF/latex/*.sty .
|
||||||
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 sty "root.tex" && \
|
||||||
$ISABELLE_TOOL latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \
|
$ISABELLE_TOOL latex -o "$OUTFORMAT" "root.tex" && \
|
||||||
{ [ ! -f "$ROOT_NAME.bib" ] || $ISABELLE_TOOL latex -o bbl "$ROOT_NAME.tex"; } && \
|
{ [ ! -f "$ROOT_NAME.bib" ] || $ISABELLE_TOOL latex -o bbl "root.tex"; } && \
|
||||||
{ [ ! -f "$ROOT_NAME.idx" ] || $ISABELLE_TOOL latex -o idx "$ROOT_NAME.tex"; } && \
|
{ [ ! -f "$ROOT_NAME.idx" ] || $ISABELLE_TOOL latex -o idx "root.tex"; } && \
|
||||||
$ISABELLE_TOOL latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \
|
$ISABELLE_TOOL latex -o "$OUTFORMAT" "root.tex" && \
|
||||||
$ISABELLE_TOOL latex -o "$OUTFORMAT" "$ROOT_NAME.tex"
|
$ISABELLE_TOOL latex -o "$OUTFORMAT" "root.tex"
|
||||||
|
|
||||||
|
|
|
@ -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.
|
|
|
@ -1,17 +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 is a placeholder for user-specific configuration and packages.
|
|
||||||
|
|
||||||
\title{<TITLE>}
|
|
||||||
\author{<AUTHOR>}
|
|
|
@ -6,7 +6,6 @@ session "BAC2017" = "Isabelle_DOF" +
|
||||||
theories
|
theories
|
||||||
BAC2017
|
BAC2017
|
||||||
document_files
|
document_files
|
||||||
"root.inf"
|
"isadof.cfg"
|
||||||
"preamble.tex"
|
"preamble.tex"
|
||||||
"ontologies.tex"
|
|
||||||
"build"
|
"build"
|
||||||
|
|
|
@ -0,0 +1,2 @@
|
||||||
|
Template: scrartcl
|
||||||
|
Ontology: mathex
|
|
@ -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 +0,0 @@
|
||||||
scrartcl
|
|
|
@ -4,8 +4,7 @@ session "MathExam" = "Isabelle_DOF" +
|
||||||
MathExam
|
MathExam
|
||||||
document_files
|
document_files
|
||||||
"preamble.tex"
|
"preamble.tex"
|
||||||
"root.inf"
|
"isadof.cfg"
|
||||||
"ontologies.tex"
|
|
||||||
"preamble.tex"
|
"preamble.tex"
|
||||||
"build"
|
"build"
|
||||||
"figures/Polynomialdeg5.png"
|
"figures/Polynomialdeg5.png"
|
||||||
|
|
|
@ -0,0 +1,2 @@
|
||||||
|
Template: scrartcl
|
||||||
|
Ontology: mathex
|
|
@ -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 +0,0 @@
|
||||||
scrartcl
|
|
|
@ -3,12 +3,11 @@ session "IsaDofApplications" = "Isabelle_DOF" +
|
||||||
theories
|
theories
|
||||||
IsaDofApplications
|
IsaDofApplications
|
||||||
document_files
|
document_files
|
||||||
"root.inf"
|
"isadof.cfg"
|
||||||
"root.bib"
|
"root.bib"
|
||||||
"preamble.tex"
|
"preamble.tex"
|
||||||
"build"
|
"build"
|
||||||
"lstisadof.sty"
|
"lstisadof.sty"
|
||||||
"ontologies.tex"
|
|
||||||
"figures/isabelle-architecture.pdf"
|
"figures/isabelle-architecture.pdf"
|
||||||
"figures/Dogfood-Intro.png"
|
"figures/Dogfood-Intro.png"
|
||||||
"figures/InteractiveMathSheet.png"
|
"figures/InteractiveMathSheet.png"
|
||||||
|
|
|
@ -0,0 +1,2 @@
|
||||||
|
Template: scrartcl
|
||||||
|
Ontology: scholarly_paper
|
|
@ -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 +0,0 @@
|
||||||
scrartcl
|
|
|
@ -3,12 +3,11 @@ session "IsaDof_Manual" = "Isabelle_DOF" +
|
||||||
theories
|
theories
|
||||||
IsaDofManual
|
IsaDofManual
|
||||||
document_files
|
document_files
|
||||||
"root.inf"
|
"isadof.cfg"
|
||||||
"root.bib"
|
"root.bib"
|
||||||
"preamble.tex"
|
"preamble.tex"
|
||||||
"build"
|
"build"
|
||||||
"lstisadof.sty"
|
"lstisadof.sty"
|
||||||
"ontologies.tex"
|
|
||||||
"figures/isabelle-architecture.pdf"
|
"figures/isabelle-architecture.pdf"
|
||||||
"figures/Dogfood-Intro.png"
|
"figures/Dogfood-Intro.png"
|
||||||
"figures/InteractiveMathSheet.png"
|
"figures/InteractiveMathSheet.png"
|
||||||
|
|
|
@ -0,0 +1,2 @@
|
||||||
|
Template: scrreprt
|
||||||
|
Ontology: technical_report
|
|
@ -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 +0,0 @@
|
||||||
scrreprt
|
|
|
@ -3,9 +3,8 @@ session "TR_mycommentedisabelle" = "Isabelle_DOF" +
|
||||||
theories
|
theories
|
||||||
"MyCommentedIsabelle"
|
"MyCommentedIsabelle"
|
||||||
document_files
|
document_files
|
||||||
"root.inf"
|
"isadof.cfg"
|
||||||
"preamble.tex"
|
"preamble.tex"
|
||||||
"ontologies.tex"
|
|
||||||
"prooftree.sty"
|
"prooftree.sty"
|
||||||
"build"
|
"build"
|
||||||
"figures/text-element.pdf"
|
"figures/text-element.pdf"
|
||||||
|
|
|
@ -0,0 +1,2 @@
|
||||||
|
Template: scrreprt
|
||||||
|
Ontology: technical_report
|
|
@ -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 +0,0 @@
|
||||||
scrreprt
|
|
1
install
1
install
|
@ -94,6 +94,7 @@ check_afp_entries() {
|
||||||
for e in $missing; do
|
for e in $missing; do
|
||||||
extract="$extract afp-2018-08-14/thys/$e"
|
extract="$extract afp-2018-08-14/thys/$e"
|
||||||
done
|
done
|
||||||
|
mkdir -p .afp
|
||||||
if curl -s -L $AFP_URL | tar zxf - -C .afp $extract; then
|
if curl -s -L $AFP_URL | tar zxf - -C .afp $extract; then
|
||||||
for e in $missing; do
|
for e in $missing; do
|
||||||
echo " Registering $e in $ISABELLE_HOME_USER/ROOTS"
|
echo " Registering $e in $ISABELLE_HOME_USER/ROOTS"
|
||||||
|
|
Loading…
Reference in New Issue