Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Merge branch 'config_as_options'

This commit is contained in:
Achim D. Brucker 2022-06-25 16:36:46 +01:00
parent c16ec333f1 aa7d0aec09
commit a54373ad2f
37 changed files with 386 additions and 613 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
CHANGELOG.md
View File

@ -10,13 +10,15 @@ and this project adheres to [Semantic Versioning](http://semver.org/spec/v2.0.0.
### Added
### Changed
- removed explicit use of build script. Requires removing "build" script entry
- The project-specific configuration is not part of the `ROOT` file, the formerly
used `isadof.cfg` is obsolete and no longer supported.
- Removed explicit use of build script. Requires removing "build" script entry
from ROOT files.
- lipics support is now official, requires document option "document_comment_latex=true"
in the ROOT file.
- Isabelle/DOF is now a proper Isabelle component that should be installed using the
"isabelle components" command. The installation script is now only an convenience
- Support for the `lipics` LaTeX style is now official. This requires document
option `document_comment_latex=true` in the ROOT file.
- Isabelle/DOF is now a proper Isabelle component that should be installed using the
`isabelle components` command. The installation script is now only a convenience
means for installing the required AFP entries.
## 1.2.0 - 2022-03-26

52
README.md
View File

@ -2,34 +2,36 @@
Isabelle/DOF is a novel Document Ontology Framework on top of Isabelle.
Isabelle/DOF allows for both conventional typesetting as well as formal
development. The manual for [Isabelle/DOF 1.2.0/Isabelle2021 is available
development. The manual for [Isabelle/DOF 1.2.0/Isabelle2021 is available
online.](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.2.0_Isabelle2021.pdf)
## Pre-requisites
Isabelle/DOF has three major pre-requisites:
Isabelle/DOF has three major prerequisites:
* **Isabelle:** Isabelle/DOF requires [Isabelle 2021-1](http://isabelle.in.tum.de/website-Isabelle2021-1/).
Please download the Isabelle 2021-1 distribution for your operating
system from the [Isabelle
website](http://isabelle.in.tum.de/website-Isabelle2021-1/).
* **AFP:** Isabelle/DOF requires two entries from the [Archive of
Formal Proofs (AFP)](https://www.isa-afp.org/). Please install the
Formal Proofs (AFP)](https://www.isa-afp.org/). Please install the
AFP following the instructions given at
<https://www.isa-afp.org/using.html>. For your convenience, we also
provide a script that only installs the two entries required by
Isabelle/DOF into the local Isabelle/DOF directory. You can use this
Isabelle/DOF into the local Isabelle/DOF directory. You can use this
script as follows:
```console
foo@bar:~$ isabelle env ./install-afp
```
* **LaTeX:** Isabelle/DOF requires a modern LaTeX installation, i.e., at least
* **LaTeX:** Isabelle/DOF requires a modern LaTeX installation, i.e., at least
[TeX Live 2022](https://www.tug.org/texlive/) with all available updates applied.
## Installation
Isabelle/DOF is provided as a Isabelle component. After installing the
pre-requisites the Isabelle/Archive needs to be unpacked and
prerequisites the Isabelle/Archive needs to be unpacked and
registered. Change into the directory you unpacked Isabelle/DOF (this
should be the directory containing this `README.md` file) and execute
@ -78,16 +80,16 @@ Isabelle projects that use DOF need to be created using
foo@bar:~$ isabelle mkroot_DOF
```
The ``mkroot_DOF`` command takes the same parameter as the standard
The ``dof_mkroot`` command takes the same parameter as the standard
``mkroot`` command of Isabelle. Thereafter, the normal Isabelle
command for building documents can be used.
Using the ``-o`` option, different ontology setups can be
selected and using the ``-t`` option, different LaTeX setups
selected and using the ``-t`` option, different LaTeX setups
can be selected. For example,
```console
foo@bar:~$ isabelle mkroot_DOF -o scholarly_paper -t scrartcl
foo@bar:~$ isabelle dof_mkroot -o scholarly_paper -t scrartcl
```
creates a setup using the scholarly_paper ontology and the article
@ -97,31 +99,21 @@ The help (option ``-h``) show a list of all supported ontologies and
document templates:
```console
foo@bar:~$ isabelle mkroot_DOF -h
Usage: isabelle mkroot_DOF [OPTIONS] [DIR]
foo@bar:~$ isabelle dof_mkroot -h
Usage: isabelle dof_mkroot [OPTIONS] [DIRECTORY]
Options are:
-h print this help text and exit
-n NAME alternative session name (default: DIR base name)
-o ONTOLOGY (default: scholarly_paper)
Available ontologies:
* cenelec_50128
* mathex
* scholarly_paper
-t TEMPLATE (default: scrartcl)
Available document templates:
* lncs
* scrartcl
* scrreprt
* scrreprt-modern
-I init Mercurial repository and add generated files
-n NAME alternative session name (default: directory base name)
-o ONTOLOGY ontology (default: scholarly_paper)
-t TEMPLATE tempalte (default: scrartcl)
Prepare session root DIR (default: current directory).
Prepare session root directory (default: current directory).
```
## Releases
For releases, signed archives including a PDF version of the Isabelle/DOF manual are
For releases, signed archives including a PDF version of the Isabelle/DOF manual
are available:
* Isabelle/DOF 1.2.0/Isabelle2021
@ -153,7 +145,7 @@ Main contacts:
* Idir Ait-Sadoune
* Paolo Crisafulli
* Chantal Keller
* Nicolas Méric
* Nicolas Méric
## License
@ -176,11 +168,11 @@ SPDX-License-Identifier: BSD-2-Clause
Computer Science (11724), Springer-Verlag, 2019.
[doi:10.1007/978-3-030-30446-1_15](https://doi.org/10.1007/978-3-030-30446-1_15).
* Achim D. Brucker, Burkhart Wolff. [Using Ontologies in Formal Developments Targeting Certification](https://www.brucker.ch/bibliography/download/2019/brucker.ea-ontologies-certification-2019.pdf). In
* Achim D. Brucker, Burkhart Wolff. [Using Ontologies in Formal Developments Targeting Certification](https://www.brucker.ch/bibliography/download/2019/brucker.ea-ontologies-certification-2019.pdf). In
Integrated Formal Methods (IFM). Lecture Notes in Computer Science (11918). Springer-Verlag 2019.
[doi:10.1007/978-3-030-34968-4_4](http://dx.doi.org/10.1007/978-3-030-34968-4_4)
* Sergio Bezzecchi, Paolo Crisafulli, Charlotte Pichot, and Burkhart Wolff. [Making Agile Development
* Sergio Bezzecchi, Paolo Crisafulli, Charlotte Pichot, and Burkhart Wolff. [Making Agile Development
Processes fit for V-style Certification Procedures.](https://hal.archives-ouvertes.fr/hal-01702815/document)
In ERTS 2018. <https://hal.archives-ouvertes.fr/hal-01702815>

10
etc/options
View File

@ -2,18 +2,18 @@
section "Isabelle/DOF"
public option dof_document_class : string = "scrreprt-modern"
-- "Default document class for Isabelle/DOF documents"
public option dof_presentation_ontologies : string = "technical_report scholarly_paper"
-- "ontologies (separated by blanks)"
public option dof_template : string = "scrreprt-modern"
-- "Default document template for Isabelle/DOF documents"
public option dof_ontologies : string = "Isabelle_DOF.technical_report Isabelle_DOF.scholarly_paper"
-- "Isabelle/DOF ontologies (separated by blanks)"
option dof_version : string = "Unreleased"
-- "Isabelle/DOF version"
(* "Unreleased" for development, semantic version for releases *)
option dof_isabelle : string = "2021-1"
option dof_afp : string = "afp-2021-12-28"
option dof_latest_version : string = "1.2.0"
option dof_latest_isabelle : string = "Isabelle2021"

20
etc/settings
View File

@ -1,25 +1,5 @@
# -*- shell-script -*- :mode=shellscript:
ISABELLE_DOF_HOME="$COMPONENT"
ISABELLE_TOOLS="$ISABELLE_TOOLS":"$ISABELLE_DOF_HOME/src/Tools"
ISABELLE_DOCS="$ISABELLE_DOF_HOME/doc":"$ISABELLE_DOCS"
# Isabelle/DOF Version Information
DOF_VERSION="Unreleased" # "Unreleased" for development, semantic version for releases
DOF_DATE="00/00/00"
DOF_LATEST_VERSION="1.2.0"
DOF_LATEST_ISABELLE="Isabelle2021"
DOF_LATEST_DOI="10.5281/zenodo.6385695"
DOF_GENERIC_DOI="10.5281/zenodo.3370482"
#
# Isabelle and AFP Configuration
ISABELLE_VERSION="Isabelle2021-1"
ISABELLE_URL="https://isabelle.in.tum.de/website-Isabelle2021-1/"
AFP_DATE="afp-2021-12-28"
AFP_URL="https://www.isa-afp.org/release/"$AFP_DATE".tar.gz"
#
# Isabelle/DOF Repository Configuration
DOF_URL="https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF"
DOF_ARTIFACT_DIR="releases/Isabelle_DOF/Isabelle_DOF"
DOF_ARTIFACT_HOST="artifacts.logicalhacking.com"
#

5
examples/CENELEC_50128/mini_odo/ROOT
View File

@ -1,9 +1,9 @@
session "mini_odo" = "Isabelle_DOF" +
options [document = pdf, document_output = "output", document_build = dof]
options [document = pdf, document_output = "output", document_build = dof,
dof_ontologies = "technical_report cenelec_50128", dof_template = "scrreprt-modern"]
theories
"mini_odo"
document_files
"isadof.cfg"
"preamble.tex"
"root.bib"
"root.mst"
@ -12,3 +12,4 @@ session "mini_odo" = "Isabelle_DOF" +
"figures/odometer.jpeg"
"figures/three-phase-odo.pdf"
"figures/wheel-df.png"

3
examples/CENELEC_50128/mini_odo/document/isadof.cfg
View File

@ -1,3 +0,0 @@
Template: scrreprt-modern
Ontology: technical_report
Ontology: cenelec_50128

2
examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy
View File

@ -256,7 +256,7 @@ enforcing a sequence of text-elements that must belong to the corresponding clas
To start using \<^isadof>, one creates an Isabelle project (with the name
\inlinebash{IsaDofApplications}):
\begin{bash}
isabelle mkroot_DOF -o scholarly_paper -t lncs -d IsaDofApplications
isabelle dof_mkroot -o scholarly_paper -t lncs IsaDofApplications
\end{bash}
where the \inlinebash{-o scholarly_paper} specifies the ontology for writing scientific articles and
\inlinebash{-t lncs} specifies the use of Springer's \LaTeX-configuration for the Lecture Notes in

4
examples/scholarly_paper/2018-cicm-isabelle_dof-applications/ROOT
View File

@ -1,10 +1,10 @@
session "2018-cicm-isabelle_dof-applications" = "Isabelle_DOF" +
options [document = pdf, document_output = "output", document_build = dof,
quick_and_dirty = true]
dof_ontologies = "scholarly_paper", dof_template = lncs,
quick_and_dirty = true]
theories
IsaDofApplications
document_files
"isadof.cfg"
"root.bib"
"authorarchive.sty"
"preamble.tex"

2
examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/isadof.cfg
View File

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

4
examples/scholarly_paper/2020-iFM-CSP/ROOT
View File

@ -1,8 +1,8 @@
session "2020-iFM-csp" = "Isabelle_DOF" +
options [document = pdf, document_output = "output", document_build = dof]
options [document = pdf, document_output = "output", document_build = dof,
dof_ontologies = "scholarly_paper", dof_template = scrartcl]
theories
"paper"
document_files
"isadof.cfg"
"root.bib"
"preamble.tex"

2
examples/scholarly_paper/2020-iFM-CSP/document/isadof.cfg
View File

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

57
examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy
View File

@ -54,7 +54,7 @@ text\<open>
Depending on your operating system and depending if you put Isabelle's \<^boxed_bash>\<open>bin\<close> directory
in your \<^boxed_bash>\<open>PATH\<close>, you will need to invoke \<^boxed_bash>\<open>isabelle\<close> using its
full qualified path, \<^eg>:
@{boxed_bash [display]\<open>ë\prompt{}ë /usr/local/Isabelleë\isabelleversionë/bin/isabelle version
@{boxed_bash [display]\<open>ë\prompt{}ë /usr/local/Isabelleë\isabelleversion/bin/isabelleë version
ë\isabellefullversionë\<close>}
\<close>
@ -115,15 +115,17 @@ session and all example documents, execute:
subsection*[first_project::technical]\<open>Creating an \<^isadof> Project\<close>
text\<open>
\<^isadof> provides its own variant of Isabelle's
\<^boxed_bash>\<open>mkroot\<close> tool, called \<^boxed_bash>\<open>mkroot_DOF\<close>\index{mkroot\_DOF}:
@{boxed_bash [display]\<open>ë\prompt{}ë isabelle mkroot_DOF myproject
\<^boxed_bash>\<open>mkroot\<close> tool, called \<^boxed_bash>\<open>dof_mkroot\<close>\index{mkroot\_DOF}:
@{boxed_bash [display]\<open>ë\prompt{}ë isabelle dof_mkroot myproject
Preparing session "myproject" iëën "myproject"
creating "myproject/ROOT"
creating "myproject/document/root.tex"
creating "myproject/myproject.thy"
creating "myproject/document/preamble.tex"
Now use the following coëëmmand line to build the session:
isabelle build -D myproject \<close>}
Now use the following commanëëd line to build the session:
isabelle build -D myproject\<close>}
The created project uses the default configuration (the ontology for writing academic papers
(scholarly\_paper) using a report layout based on the article class (\<^boxed_latex>\<open>scrartcl\<close>) of
the KOMA-Script bundle~@{cite "kohm:koma-script:2019"}). The directory \<^boxed_bash>\<open>myproject\<close>
@ -139,21 +141,24 @@ The directory \<^boxed_bash>\<open>myproject\<close> contains the following fil
.1 .
.2 myproject.
.3 document.
.4 isadof.cfg\DTcomment{\<^isadof> configuration}.
.4 preamble.tex\DTcomment{Manual \<^LaTeX>-configuration}.
.3 myproject.thy\DTcomment{Example theory file}.
.3 ROOT\DTcomment{Isabelle build-configuration}.
}
\end{minipage}
\end{center}
The \<^isadof> configuration (\<^boxed_bash>\<open>isadof.cfg\<close>) specifies the required
ontologies and the document template using a YAML syntax.\<^footnote>\<open>Isabelle power users will recognize that
The main two configuration files\<^footnote>\<open>Isabelle power users will recognize that
\<^isadof>'s document setup does not make use of a file \<^boxed_bash>\<open>root.tex\<close>: this file is
replaced by built-in document templates.\<close> The main two configuration files for
users are:
replaced by built-in document templates.\<close> for users are:
\<^item> The file \<^boxed_bash>\<open>ROOT\<close>\<^index>\<open>ROOT\<close>, which defines the Isabelle session. New theory files as well as new
files required by the document generation (\<^eg>, images, bibliography database using \<^BibTeX>, local
\<^LaTeX>-styles) need to be registered in this file. For details of Isabelle's build system, please
consult the Isabelle System Manual~@{cite "wenzel:system-manual:2020"}.
consult the Isabelle System Manual~@{cite "wenzel:system-manual:2020"}. In addition to the
standard features of, this file also contains \<^isadof> specific configurations:
\<^item> \<^boxed_bash>\<open>dof_ontologies\<close> a list of (fully qualified) ontologies, separated by spaces, used
by the project.
\<^item> \<^boxed_bash>\<open>dof_template\<close> the document template.
\<^item> The file \<^boxed_bash>\<open>preamble.tex\<close>\<^index>\<open>preamble.tex\<close>, which allows users to add additional
\<^LaTeX>-packages or to add/modify \<^LaTeX>-commands.
\<close>
@ -166,31 +171,21 @@ text\<open>
obtains and adds the necessary \<^LaTeX> class file.
This is due to licensing restrictions).\<close>
text\<open>
This can be configured by using the command-line options of \<^boxed_bash>\<open>mkroot_DOF\<close>. In
This can be configured by using the command-line options of \<^boxed_bash>\<open>dof_mkroot\<close>. In
Particular, \<^boxed_bash>\<open>-o\<close> allows selecting the ontology and \<^boxed_bash>\<open>-t\<close> allows selecting
the document template. The built-in help (using \<^boxed_bash>\<open>-h\<close>) shows all available options
as well as a complete list of the available document templates and ontologies:
the document template. The built-in help (using \<^boxed_bash>\<open>-h\<close>) shows all available options:
@{boxed_bash [display]\<open>ë\prompt{}ë isabelle mkroot_DOF -h
@{boxed_bash [display]\<open>ë\prompt{}ë isabelle dof_mkroot -h
Usage: isabelle mkroot_DOF [OPTIONS] [DIR]
Usage: isabelle dof_mkroot [OPTIONS] [DIRECTORY]
Options are:
-h print this hëëelp text and exëëit
-n NAME alternative session name (default: DIR base name)
-o ONTOLOGY (default: scholarly_paper)
Available ontologies:
* CENELEC_50128
* scholarly_paper
* technical_report
-t TEMPLATE (default: scrartcl)
Available document templates:
* lncs
* scrartcl
* scrreprt-modern
* scrreprt
-I init Mercurial repository and add generated files
-n NAME alternative session name (default: directory base name)
-o ONTOLOGY ontology (default: scholarly_paper)
-t TEMPLATE tempalte (default: scrartcl)
Prepare session root DIR (default: current directory). \<close>}
Prepare session root directory (default: current directory).\<close>}
\<close>

13
examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy
View File

@ -1236,7 +1236,7 @@ section*[infrastructure::technical]\<open>Technical Infrastructure\<close>
text\<open>
The list of fully supported (\<^ie>, supporting both interactive ontological modeling and
document generation) ontologies and the list of supported document templates can be
obtained by calling \<^boxed_bash>\<open>isabelle mkroot_DOF -h\<close> (see \<^technical>\<open>first_project\<close>).
obtained by calling \<^boxed_bash>\<open>isabelle dof_mkroot -h\<close> (see \<^technical>\<open>first_project\<close>).
Note that the postfix \<^boxed_bash>\<open>-UNSUPPORTED\<close> denotes experimental ontologies or templates
for which further manual setup steps might be required or that are not fully tested. Also note
that the \<^LaTeX>-class files required by the templates need to be already installed on your
@ -1360,14 +1360,7 @@ text\<open>
\usepackage{isabelle,isabellesym,amssymb} % Required (by Isabelle)
\usepackage{amsmath} % Used by some ontologies
\bibliographystyle{abbrv}
\IfFileExists{DOF-core.sty}{}{ % Required by Isabelle/DOF
\PackageError{DOF-core}{The doëëcument preparation
requires the Isabelle/DOF framework.}{For further help, see
ë\url{\dofurl}ë
}
\input{ontologies} % This will include the document specific
% ontologies from isadof.cfg
\IfFileExists{preamble.tex}{\input{preamble.tex}}{}
\input{dof-common} % setup shared between all Isabelle/DOF templates
\usepackage{graphicx} % Required for images.
\usepackage[caption]{subfig}
\usepackage[size=footnotesize]{caption}
@ -1393,7 +1386,7 @@ text\<open>
subsubsection\<open>Getting Started\<close>
text\<open>
In general, we recommend creating a test project (\<^eg>, using \<^boxed_bash>\<open>isabelle mkroot_DOF\<close>)
In general, we recommend creating a test project (\<^eg>, using \<^boxed_bash>\<open>isabelle dof_mkroot\<close>)
to develop new document templates or ontology representations. The default setup of the \<^isadof>
build system generated a \<^path>\<open>output/document\<close> directory with a self-contained \<^LaTeX>-setup. In
this directory, you can directly use \<^LaTeX> on the main file, called \<^path>\<open>root.tex\<close>:

2
examples/technical_report/Isabelle_DOF-Manual/ROOT
View File

@ -1,10 +1,10 @@
session "Isabelle_DOF-Manual" = "Isabelle_DOF" +
options [document = pdf, document_output = "output", document_build = dof,
dof_ontologies = "technical_report cenelec_50128", dof_template = "scrreprt-modern",
quick_and_dirty = true]
theories
"Isabelle_DOF-Manual"
document_files
"isadof.cfg"
"root.bib"
"root.mst"
"preamble.tex"

4
examples/technical_report/Isabelle_DOF-Manual/document/isadof.cfg
View File

@ -1,4 +0,0 @@
Template: scrreprt-modern
Ontology: technical_report
Ontology: cenelec_50128

2
examples/technical_report/TR_my_commented_isabelle/ROOT
View File

@ -1,11 +1,11 @@
session "TR_MyCommentedIsabelle" = "Isabelle_DOF" +
options [document = pdf, document_output = "output", document_build = dof,
dof_ontologies = "technical_report", dof_template = scrreprt,
quick_and_dirty = true]
theories
"TR_MyCommentedIsabelle"
document_files
"root.bib"
"isadof.cfg"
"preamble.tex"
"prooftree.sty"
"figures/markup-demo.png"

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

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

15
install-afp
View File

@ -30,6 +30,7 @@
#set -e
shopt -s nocasematch
print_help()
{
echo "Usage: isabelle env ./install-afp [OPTION] "
@ -58,8 +59,8 @@ check_isabelle_version() {
echo " version of Isabelle and rerun the install script, providing the"
echo " the \"isabelle\" command as argument."
echo " Isabelle ($ISABELLE_VERSION) can be obtained from:"
echo " $ISABELLE_URL"
echo
echo " https://isabelle.in.tum.de/website-$ISABELLE_VERSION/"
echo ""
read -p " Still continue (y/N)? " -n 1 -r
echo
if [[ $REPLY =~ ^[Yy]$ ]];
@ -128,8 +129,18 @@ do
shift
done
if [ -z ${ISABELLE_TOOL+x} ];
then
print_help
exit 1
fi
ACTUAL_ISABELLE_VERSION=`$ISABELLE_TOOL version`
ISABELLE_VERSION="Isabelle$($ISABELLE_TOOL options -g dof_isabelle)"
AFP_DATE="$($ISABELLE_TOOL options -g dof_afp)"
AFP_URL="https://www.isa-afp.org/release/"$AFP_DATE".tar.gz"
echo ""
echo "Isabelle/DOF Installer"
echo "======================"

3
src/DOF/latex/DOF-COL.sty
View File

@ -14,8 +14,7 @@
\NeedsTeXFormat{LaTeX2e}\relax
\ProvidesPackage{DOF-COL}
[<isadofltxversion>%
Document-Type Support Framework for Isabelle.]
[00/00/0000 Document-Type Support Framework for Isabelle.]
\RequirePackage{DOF-core}

3
src/DOF/latex/DOF-amssymb.sty
View File

@ -14,8 +14,7 @@
\NeedsTeXFormat{LaTeX2e}\relax
\ProvidesPackage{DOF-amssymb}
[<isadofltxversion>%
Document-Type Support Framework for Isabelle (amssymb wrapper for lualatex/pdflatex).]
[00/00/0000 Document-Type Support Framework for Isabelle (amssymb wrapper for lualatex/pdflatex).]
\usepackage{ifxetex,ifluatex}
\ifnum 0\ifxetex 1\fi\ifluatex 1\fi=0 % if pdftex

17
src/DOF/latex/DOF-core.sty
View File

@ -14,8 +14,7 @@
\NeedsTeXFormat{LaTeX2e}\relax
\ProvidesPackage{DOF-core}
[<isadofltxversion>%
Document-Type Support Framework for Isabelle.]
[00/00/0000 Document-Type Support Framework for Isabelle.]
\RequirePackage{keycommand}
\RequirePackage{environ}
@ -24,19 +23,7 @@
\RequirePackage{etoolbox}
\RequirePackage{fp}
\newcommand{\isabelleurl}{UNDEFINED}
\newcommand{\dofurl}{UNDEFINED}
\newcommand{\dof@isabelleversion}{UNDEFINED}
\newcommand{\isabellefullversion}{UNDEFINED\xspace}
\newcommand{\dof@version}{UNDEFINED}
\newcommand{\dof@artifacturl}{UNDEFINED}
\newcommand{\doflatestversion}{UNDEFINED}
\newcommand{\isadoflatestdoi}{UNDEFINED}
\newcommand{\isadofgenericdoi}{UNDEFINED}
\newcommand{\isabellelatestversion}{Isabelle2019}
%%% CONFIG %%%
\RequirePackage{dof-config}
\newcommand{\isabelleversion}{\dof@isabelleversion\xspace}
\newcommand{\dofversion}{\dof@version\xspace}
\newcommand{\isadofversion}{\dofversion/\isabelleversion}

150
src/Tools/mkroot_DOF
View File

@ -1,150 +0,0 @@
#/usr/bin/env bash
# Copyright (c) 2019 University of Exeter
# 2018-2019 University of Paris-Saclay
# 2018-2019 The University of Sheffield
#
# 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
#
# DESCRIPTION: prepare session root directory with DOF setup
## diagnostics
PRG="$(basename "$0")"
function usage()
{
echo
echo "Usage: isabelle $PRG [OPTIONS] [DIR]"
echo
echo " Options are:"
echo " -h print this help text and exit"
echo " -n NAME alternative session name (default: DIR base name)"
echo " -o ONTOLOGY (default: $DEFAULT_ONTOLOGY)"
echo " Available ontologies:"
for t in "$ISABELLE_DOF_HOME/src/ontologies"/*/*.sty; do
if [[ $t =~ DOF-(.*).sty$ ]]; then
echo " * ${BASH_REMATCH[1]}"
fi
done
echo " -t TEMPLATE (default: $DEFAULT_TEMPLATE)"
echo " Available document templates:"
for t in "$ISABELLE_DOF_HOME/src/document-templates/"*.tex; do
if [[ $t =~ root-(.*).tex$ ]]; then
echo " * ${BASH_REMATCH[1]}"
fi
done
echo
echo " Prepare session root DIR (default: current directory)."
echo
exit 1
}
function fail()
{
echo "$1" >&2
exit 2
}
## process command line
# options
NAME=""
DEFAULT_TEMPLATE="scrartcl"
DEFAULT_ONTOLOGY="scholarly_paper"
TEMPLATE="$DEFAULT_TEMPLATE"
ONTOLOGY=""
while getopts "t:o:n:dh" OPT
do
case "$OPT" in
h)
usage
exit 1
;;
n)
NAME="$OPTARG"
;;
o)
if [ ! -f "$ISABELLE_DOF_HOME/src/ontologies"/*/DOF-$OPTARG.sty ]; then
echo "ERROR: Ontology $OPTARG not available!"
exit 1
fi
ONTOLOGY="$ONTOLOGY $OPTARG"
;;
t)
TEMPLATE="$OPTARG"
if [ ! -f "$ISABELLE_DOF_HOME/src/document-templates/root-$TEMPLATE.tex" ]; then
echo "ERROR: Template $TEMPLATE not available!"
exit 1
fi
;;
\?)
usage
exit 0
;;
esac
done
shift $(($OPTIND - 1))
ONTOLOGY="${ONTOLOGY:-$DEFAULT_ONTOLOGY}"
# args
if [ "$#" -eq 0 ]; then
DIR="."
elif [ "$#" -eq 1 ]; then
DIR="$1"
shift
else
usage
fi
if [ -z "$NAME" ]; then
NAME="$DIR"
fi
$ISABELLE_TOOL mkroot -n "$NAME" "$DIR"
echo " \"preamble.tex\"" >> "$DIR"/ROOT
sed -i -e "s/root.tex/isadof.cfg/" "$DIR"/ROOT
sed -i -e "s/HOL/Isabelle_DOF/" "$DIR"/ROOT
sed -i -e "s/\"output\"\]/\"output\", document_build = dof\]/" "$DIR"/ROOT
rm -f "$DIR"/document/root.tex
# Creating isadof.cfg
echo "Template: $TEMPLATE" > "$DIR"/document/isadof.cfg
for o in $ONTOLOGY; do
echo "Ontology: $o" >> "$DIR"/document/isadof.cfg;
done
# Creating praemble.tex
TITLE=$(echo "$NAME" | tr _ - | tr -d '\\')
AUTHOR=$(echo "By $USER" | tr _ - | tr -d '\\')
echo "%% This is a placeholder for user-specific configuration and packages." >> "$DIR"/document/preamble.tex
echo "\\title{$TITLE}{}{}{}{}{}{}" >> "$DIR"/document/preamble.tex
echo "\\author{$AUTHOR}{}{}{}{}{}" >> "$DIR"/document/preamble.tex

34
src/document-templates/dof-common.tex Normal file
View File

@ -0,0 +1,34 @@
%% Copyright (c) 2019-2022 University of Exeter
%% 2018-2022 University of Paris-Saclay
%% 2018-2019 The University of Sheffield
%%
%% 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.3c of the License, or (at your option) any later version.
%% OR
%% The 2-clause BSD-style license.
%%
%% SPDX-License-Identifier: LPPL-1.3c+ OR BSD-2-Clause
%% Warning: Do Not Edit!
%% =====================
%% This is the root file for the Isabelle/DOF using the lncs class.
%%
%% All customization and/or additional packages should be added to the file
%% preamble.tex.
\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 component for Isabelle.
}{For further help, see the Isabelle/DOF manual.}
}
\title{No Title Given}
\title{No Author Given}
\input{ontologies}
\IfFileExists{preamble.tex}{\input{preamble.tex}}{}%
\isabellestyle{it}

29
src/document-templates/root-eptcs-UNSUPPORTED.tex
View File

@ -12,8 +12,6 @@
%%
%% SPDX-License-Identifier: LPPL-1.3c+ OR BSD-2-Clause
%% <isadofltxversion>
%% Warning: Do Not Edit!
%% =====================
%% This is the root file for the Isabelle/DOF using the eptcs class.
@ -26,25 +24,17 @@
\documentclass[submission,copyright,creativecommons]{eptcs}
\bibliographystyle{eptcs}% the mandatory bibstyle
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage[USenglish]{babel}
\usepackage{isabelle}
%\usepackage{underscore}
\usepackage{xcolor}
\usepackage{isabellesym}
\input{dof-common}
\usepackage{amsmath}
\usepackage{DOF-amssymb}
\usepackage[numbers, sort&compress, sectionbib]{natbib}
\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 component from:
<isadofurl>
}{For further help, see <isadofurl>}
}
\usepackage{xcolor}
\newcommand{\subtitle}[1]{%
\PackageError{DOF-eptcs-UNSUPPORTED}
{The LaTeX class eptcs does not support subtitles.}
@ -54,7 +44,6 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% provide an alternative definition of
% begin: scholarly_paper.author
\RequirePackage{DOF-core}
\newcommand{\dofeptcsinstitute}[1]{\mbox{}\\\protect\scriptsize%
\protect\begin{tabular}[t]{@{\protect\footnotesize}c@{}}%
#1%
@ -80,15 +69,15 @@
\makeatother
% end: scholarly_paper.author
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\input{ontologies}
\IfFileExists{preamble.tex}{\input{preamble.tex}}{}%
\begin{document}
\maketitle
\input{session}
% optional bibliography
\IfFileExists{root.bib}{{\bibliography{root}}}{}
\IfFileExists{root.bib}{%
\bibliography{root}
}{}
\end{document}
%%% Local Variables:

25
src/document-templates/root-lipics-v2021.tex
View File

@ -12,8 +12,6 @@
%%
%% SPDX-License-Identifier: LPPL-1.3c+ OR BSD-2-Clause
%% <isadofltxversion>
%% Warning: Do Not Edit!
%% =====================
%% This is the root file for the Isabelle/DOF using the lipics class.
@ -29,20 +27,9 @@
\documentclass[a4paper,UKenglish,cleveref, autoref,thm-restate]{lipics-v2021}
\bibliographystyle{plainurl}% the mandatory bibstyle
\usepackage{isabelle}
\usepackage{isabellesym}
% \usepackage{amsmath}
% \usepackage{DOF-amssymb}
\usepackage[numbers, sort&compress, sectionbib]{natbib}
\IfFileExists{DOF-core.sty}{}{%
\PackageError{DOF-core}{Isabelle/DOF not installed.
This is a Isabelle_DOF project. The document preparation requires
the Isabelle_DOF component from:
<isadofurl>
}{For further help, see <isadofurl>}
}
\input{dof-common}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% provide an alternative definition of
@ -68,21 +55,21 @@
\makeatother
% end: scholarly_paper.author
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\input{ontologies}
\renewcommand{\DOFauthor}{}
\renewcommand{\DOFinstitute}{}
\expandafter\newcommand\csname 2authand\endcsname{}
\expandafter\newcommand\csname 3authand\endcsname{}
\expandafter\newcommand\csname 4authand\endcsname{}
\IfFileExists{preamble.tex}{\input{preamble.tex}}{}%
\begin{document}
\maketitle
\input{session}
% optional bibliography
\IfFileExists{root.bib}{{\small\bibliography{root}}}{}
\IfFileExists{root.bib}{%
\small
\bibliography{root}
}{}
\end{document}
%%% Local Variables:

22
src/document-templates/root-lncs.tex
View File

@ -12,8 +12,6 @@
%%
%% SPDX-License-Identifier: LPPL-1.3c+ OR BSD-2-Clause
%% <isadofltxversion>
%% Warning: Do Not Edit!
%% =====================
%% This is the root file for the Isabelle/DOF using the lncs class.
@ -26,21 +24,12 @@
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage[USenglish]{babel}
\input{dof-common}
\bibliographystyle{splncs04}
\usepackage{isabelle}
\usepackage{xcolor}
\usepackage{isabellesym}
\usepackage{amsmath}
\usepackage{DOF-amssymb}
\IfFileExists{DOF-core.sty}{}{%
\PackageError{DOF-core}{Isabelle/DOF not installed.
This is a Isabelle_DOF project. The document preparation requires
the Isabelle_DOF component from:
<isadofurl>
}{For further help, see <isadofurl>}
}
\input{ontologies}
\IfFileExists{preamble.tex}{\input{preamble.tex}}{}%
\usepackage{xcolor}
\usepackage{graphicx}
\usepackage{hyperref}
\setcounter{tocdepth}{3}
@ -53,8 +42,7 @@
} % more detailed digital TOC (aka bookmarks)
\sloppy
\allowdisplaybreaks[4]
\urlstyle{rm}
\isabellestyle{it}
\usepackage[caption]{subfig}
\usepackage[size=footnotesize]{caption}
@ -84,7 +72,7 @@
\maketitle
\maketitle
\input{session}
% optional bibliography
\IfFileExists{root.bib}{{\small\bibliography{root}}}{}

24
src/document-templates/root-scrartcl.tex
View File

@ -12,8 +12,6 @@
%%
%% SPDX-License-Identifier: LPPL-1.3c+ OR BSD-2-Clause
%% <isadofltxversion>
%% Warning: Do Not Edit!
%% =====================
%% This is the root file for the Isabelle/DOF using the scrartcl class.
@ -23,26 +21,21 @@
\RequirePackage{ifvtex}
\documentclass[abstract=true,fontsize=11pt,DIV=12,paper=a4]{scrartcl}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage[english]{babel}
\usepackage{textcomp}
\bibliographystyle{abbrvnat}
\usepackage[english]{babel}
\RequirePackage[caption]{subfig}
\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 component from:
<isadofurl>
}{For further help, see <isadofurl>}
}
\input{ontologies}
\IfFileExists{preamble.tex}{\input{preamble.tex}}{}%
\input{dof-common}
\usepackage{amsmath}
\usepackage{DOF-amssymb}
\usepackage[numbers, sort&compress, sectionbib]{natbib}
\usepackage{xcolor}
\usepackage{graphicx}
\usepackage{hyperref}
\setcounter{tocdepth}{3}
@ -55,15 +48,12 @@
} % more detailed digital TOC (aka bookmarks)
\sloppy
\allowdisplaybreaks[4]
\urlstyle{rm}
\isabellestyle{it}
\newenvironment{frontmatter}{}{}
\begin{document}
\begin{frontmatter}
\maketitle
% \tableofcontents
\end{frontmatter}
\input{session}
% optional bibliography

29
src/document-templates/root-scrreprt-modern.tex
View File

@ -12,8 +12,6 @@
%%
%% SPDX-License-Identifier: LPPL-1.3c+ OR BSD-2-Clause
%% <isadofltxversion>
%% Warning: Do Not Edit!
%% =====================
%% This is the root file for the Isabelle/DOF using the scrreprt class with
@ -27,13 +25,18 @@
\documentclass[fontsize=11pt,paper=a4,open=right,twoside,abstract=true]{scrreprt}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage[english]{babel}
\usepackage{textcomp}
\bibliographystyle{abbrvnat}
\usepackage[varqu,varl]{zi4}% inconsolata typewriter
\usepackage{amsmath,amsthm}
\usepackage{amsthm}
\usepackage{newtxsf}
\input{dof-common}
\usepackage{amsmath}
\usepackage{DOF-amssymb}
\renewcommand\familydefault{\sfdefault}
\usepackage{xcolor}
\colorlet{DOFsectioncolor}{blue!60!black}
\addtokomafont{chapterentrypagenumber}{\color{DOFsectioncolor}}
\addtokomafont{chapterentry}{\color{DOFsectioncolor}}
@ -45,25 +48,15 @@
\addtokomafont{paragraph}{\color{DOFsectioncolor}}
\addtokomafont{subparagraph}{\color{DOFsectioncolor}}
\usepackage[english]{babel}
\RequirePackage[caption]{subfig}
\usepackage{isabelle}
\usepackage{isabellesym}
\renewcommand{\isastyletext}{\normalsize\normalfont\sffamily}
\renewcommand{\isastyletxt}{\normalfont\sffamily}
\renewcommand{\isastylecmt}{\normalfont\sffamily}
\IfFileExists{DOF-core.sty}{}{%
\PackageError{DOF-core}{Isabelle/DOF not installed.
This is a Isabelle_DOF project. The document preparation requires
the Isabelle_DOF component from:
<isadofurl>
}{For further help, see <isadofurl>}
}
\input{ontologies}
\IfFileExists{preamble.tex}{\input{preamble.tex}}{}%
\usepackage{amsmath}
\usepackage{DOF-amssymb}
\usepackage[numbers, sort&compress, sectionbib]{natbib}
\usepackage{xcolor}
\usepackage{graphicx}
\usepackage{hyperref}
\setcounter{tocdepth}{2}
@ -76,8 +69,6 @@
} % more detailed digital TOC (aka bookmarks)
\sloppy
\allowdisplaybreaks[4]
\urlstyle{sf}
\isabellestyle{it}
\newenvironment{frontmatter}{}{}

26
src/document-templates/root-scrreprt.tex
View File

@ -12,8 +12,6 @@
%%
%% SPDX-License-Identifier: LPPL-1.3c+ OR BSD-2-Clause
%% <isadofltxversion>
%% Warning: Do Not Edit!
%% =====================
%% This is the root file for the Isabelle/DOF using the scrreprt class.
@ -25,24 +23,18 @@
\documentclass[fontsize=11pt,paper=a4,open=right,twoside,abstract=true]{scrreprt}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage[english]{babel}
\usepackage{textcomp}
\bibliographystyle{abbrvnat}
\usepackage[english]{babel}
\RequirePackage[caption]{subfig}
\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 component from:
<isadofurl>
}{For further help, see <isadofurl>}
}
\input{ontologies}
\IfFileExists{preamble.tex}{\input{preamble.tex}}{}%
\input{dof-common}
\usepackage{amsmath}
\usepackage{DOF-amssymb}
\usepackage[numbers, sort&compress, sectionbib]{natbib}
\usepackage{xcolor}
\usepackage{graphicx}
\usepackage{hyperref}
\setcounter{tocdepth}{2}
@ -55,10 +47,6 @@
} % more detailed digital TOC (aka bookmarks)
\sloppy
\allowdisplaybreaks[4]
\urlstyle{rm}
\isabellestyle{it}
\newenvironment{frontmatter}{}{}
\begin{document}
\renewcommand{\chapterautorefname}{Chapter}
@ -67,10 +55,8 @@
\renewcommand{\subsubsectionautorefname}{Section}
\newcommand{\subtableautorefname}{\tableautorefname}
\newcommand{\subfigureautorefname}{\figureautorefname}
\begin{frontmatter}
\maketitle
\tableofcontents
\end{frontmatter}
\input{session}
% optional bibliography
\IfFileExists{root.bib}{{\bibliography{root}}}{}

22
src/document-templates/root-svjour3-UNSUPPORTED.tex
View File

@ -12,8 +12,6 @@
%%
%% SPDX-License-Identifier: LPPL-1.3c+ OR BSD-2-Clause
%% <isadofltxversion>
%% Warning: Do Not Edit!
%% =====================
%% This is the root file for the Isabelle/DOF using the scrartcl class.
@ -26,24 +24,16 @@
\documentclass[]{svjour3}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage[english]{babel}
\usepackage{mathptmx}
\bibliographystyle{abbrvnat}
\usepackage[USenglish]{babel}
\usepackage{isabelle}
\usepackage{xcolor}
\usepackage{isabellesym}
\input{dof-common}
\usepackage{amsmath}
\usepackage{DOF-amssymb}
\usepackage[numbers, sort&compress, sectionbib]{natbib}
\IfFileExists{DOF-core.sty}{}{%
\PackageError{DOF-core}{Isabelle/DOF not installed.
This is a Isabelle_DOF project. The document preparation requires
the Isabelle_DOF component from:
<isadofurl>
}{For further help, see <isadofurl>}
}
\input{ontologies}
\IfFileExists{preamble.tex}{\input{preamble.tex}}{}%
\usepackage{xcolor}
\usepackage{graphicx}
\usepackage{hyperref}
\setcounter{tocdepth}{3}
@ -56,8 +46,6 @@
} % more detailed digital TOC (aka bookmarks)
\sloppy
\allowdisplaybreaks[4]
\urlstyle{rm}
\isabellestyle{it}
\usepackage[caption]{subfig}
\usepackage[size=footnotesize]{caption}

3
src/ontologies/CENELEC_50128/DOF-CENELEC_50128.sty
View File

@ -14,8 +14,7 @@
\NeedsTeXFormat{LaTeX2e}\relax
\ProvidesPackage{DOF-cenelec_50128}
[<isadofltxversion>%
Document-Type Support Framework for Isabelle (CENELEC 50128).]
[00/00/0000 Document-Type Support Framework for Isabelle (CENELEC 50128).]
\RequirePackage{DOF-COL}
\usepackage{etex}

3
src/ontologies/scholarly_paper/DOF-scholarly_paper-thm.sty
View File

@ -13,8 +13,7 @@
\NeedsTeXFormat{LaTeX2e}\relax
\ProvidesPackage{DOF-scholarly_paper-thm}
[<isadofltxversion>%
Document-Type Support Framework for Isabelle (LNCS).]
[00/00/0000 Document-Type Support Framework for Isabelle (LNCS).]
\RequirePackage{amsthm}

3
src/ontologies/technical_report/DOF-technical_report.sty
View File

@ -13,8 +13,7 @@
\NeedsTeXFormat{LaTeX2e}\relax
\ProvidesPackage{DOF-technical_report}
[<isadofltxversion>%
Document-Type Support Framework for Isabelle (LNCS).]
[00/00/0000 Document-Type Support Framework for Isabelle (LNCS).]
\RequirePackage[force]{DOF-scholarly_paper}
\RequirePackage{ifthen}

47
src/scala/dof_document_build.scala
View File

@ -31,13 +31,14 @@
package isabelle_dof
import isabelle._
import java.io.{File => JFile}
object DOF_Document_Build
{
class Engine extends Document_Build.Bash_Engine("dof")
{
override def use_build_script: Boolean = true
// override def use_build_script: Boolean = true
override def prepare_directory(
context: Document_Build.Context,
@ -59,7 +60,49 @@ object DOF_Document_Build
}
val dof_home= Path.explode(Isabelle_System.getenv_strict("ISABELLE_DOF_HOME"));
// print(context.options.string("dof_url"));
Isabelle_System.copy_file(dof_home + Path.explode("src/scripts/build"), directory.doc_dir);
// copy Isabelle/DOF LaTeX templates
val template_dir = dof_home + Path.explode("src/document-templates/")
// TODO: error handling in case 1) template does not exist or 2) root.tex does already exist
Isabelle_System.copy_file(template_dir + Path.explode("root-"+context.options.string("dof_template")+".tex"),
directory.doc_dir+Path.explode("root.tex"))
Isabelle_System.copy_file(template_dir + Path.explode("dof-common.tex"),
directory.doc_dir)
// copy Isabelle/DOF LaTeX styles
val doc_jdir = new JFile(directory.doc_dir.implode)
val styles = File.find_files(new JFile(dof_home.implode),((f:JFile) => f.getName().endsWith(".sty")), true)
for (sty <- styles) {
Isabelle_System.copy_file(sty, doc_jdir)
}
// create ontology.sty
val regex = """^.*\.""".r
val ltx_styles = context.options.string("dof_ontologies").split(" +").map(s => regex.replaceAllIn(s,""))
File.write(directory.doc_dir+Path.explode("ontologies.tex"),
ltx_styles.mkString("\\usepackage{DOF-","}\n\\usepackage{DOF-","}\n"))
// create dof-config.sty
File.write(directory.doc_dir+Path.explode("dof-config.sty"), """
\newcommand{\isabelleurl}{https://isabelle.in.tum.de/website-Isabelle2021-1/""" + context.options.string("dof_isabelle") + """}
\newcommand{\dofurl}{""" + context.options.string("dof_url") + """}
\newcommand{\dof@isabelleversion}{""" + context.options.string("dof_isabelle") + """}
\newcommand{\isabellefullversion}{""" + context.options.string("dof_isabelle") + """\xspace}
\newcommand{\dof@version}{""" + context.options.string("dof_version") + """}
\newcommand{\dof@artifacturl}{""" + context.options.string("dof_artifact_dir") + """}
\newcommand{\doflatestversion}{""" + context.options.string("dof_latest_version") + """}
\newcommand{\isadoflatestdoi}{""" + context.options.string("dof_latest_doi") + """}
\newcommand{\isadofgenericdoi}{""" + context.options.string("dof_generic_doi") + """}
\newcommand{\isabellelatestversion}{""" + context.options.string("dof_latest_isabelle") + """}
""")
/*
sed -i -e "s|<isadofurl>|$DOF_URL|" *.sty
sed -i -e "s|<isadofurl>|$DOF_URL|" *.tex
LTX_VERSION="$DOF_DATE $DOF_VERSION/$ISABELLE_SHORT_VERSION"
sed -i -e "s|<isadofltxversion>|$LTX_VERSION|" *.tex
sed -i -e "s|<isadofltxversion>|$LTX_VERSION|" *.sty
*/
// Isabelle_System.copy_file(dof_home + Path.explode("src/scripts/build"), directory.doc_dir);
directory
}

152
src/scala/dof_mkroot.scala
View File

@ -1,3 +1,34 @@
/*
* Copyright (c)
* 2021-2022 The University of Exeter.
* 2021-2022 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
*/
/* Author: Makarius
Prepare session root directory for Isabelle/DOF.
@ -7,7 +38,6 @@ package isabelle_dof
import isabelle._
object DOF_Mkroot
{
/** mkroot **/
@ -17,15 +47,96 @@ object DOF_Mkroot
session_dir: Path = Path.current,
session_parent: String = "",
init_repos: Boolean = false,
title: String = "",
author: String = "",
template: String = "",
ontologies: List[String] = List(),
progress: Progress = new Progress): Unit =
{
Mkroot.mkroot(session_name = session_name, session_dir = session_dir,
session_parent = session_parent, init_repos = init_repos,
title = title, author = author, progress = progress)
}
Isabelle_System.make_directory(session_dir)
val name = proper_string(session_name) getOrElse session_dir.absolute_file.getName
val parent = proper_string(session_parent) getOrElse Isabelle_System.getenv("ISABELLE_LOGIC")
val root_path = session_dir + Sessions.ROOT
if (root_path.file.exists) error("Cannot overwrite existing " + root_path)
val document_path = session_dir + Path.explode("document")
if (document_path.file.exists) error("Cannot overwrite existing " + document_path)
progress.echo("\nPreparing session " + quote(name) + " in " + session_dir)
/* ROOT */
progress.echo(" creating " + root_path)
File.write(root_path,
"session " + Mkroot.root_name(name) + " = " + Mkroot.root_name(parent) + """ +
options [document = pdf, document_output = "output", document_build = dof, dof_ontologies = """"
+ ontologies.mkString(" ") + """", dof_template = """ + Mkroot.root_name(template)
+ """, document_comment_latex=true]
(*theories [document = false]
A
B*)
theories
""" + Mkroot.root_name(name) + """
document_files
"preamble.tex"
""")
val thy = session_dir + Path.explode(name+".thy")
progress.echo(" creating " + thy)
File.write(thy,
"theory\n " + name + "\nimports\n " + ontologies.mkString("\n ") + """
begin
end
""")
val preamble_tex = session_dir + Path.explode("document/preamble.tex")
progress.echo(" creating " + preamble_tex)
Isabelle_System.make_directory(preamble_tex.dir)
File.write(preamble_tex,"""%% This is a placeholder for user-specific configuration and packages.""")
/* Mercurial repository */
if (init_repos) {
progress.echo(" \nInitializing Mercurial repository " + session_dir)
val hg = Mercurial.init_repository(session_dir)
val hg_ignore = session_dir + Path.explode(".hgignore")
File.write(hg_ignore,
"""syntax: glob
*~
*.marks
*.orig
*.rej
.DS_Store
.swp
syntax: regexp
^output/
""")
hg.add(List(root_path, preamble_tex, hg_ignore))
}
/* notes */
{
val print_dir = session_dir.implode
progress.echo("""
Now use the following command line to build the session:
isabelle build -D """ +
(if (Bash.string(print_dir) == print_dir) print_dir else quote(print_dir)) + "\n")
}
}
/** Isabelle tool wrapper **/
@ -33,29 +144,36 @@ object DOF_Mkroot
val isabelle_tool = Isabelle_Tool("dof_mkroot", "prepare session root directory for Isabelle/DOF",
Scala_Project.here, args =>
{
var author = ""
var init_repos = false
var title = ""
var help = false
var session_name = ""
var session_parent = "Isabelle_DOF"
var ontologies:List[String] = List()
var template = "scrartcl"
val getopts = Getopts("""
Usage: isabelle dof_mkroot [OPTIONS] [DIRECTORY]
Options are:
-A LATEX provide author in LaTeX notation (default: user name)
-I init Mercurial repository and add generated files
-T LATEX provide title in LaTeX notation (default: session name)
-n NAME alternative session name (default: directory base name)
-o ONTOLOGY ontology (default: scholarly_paper)
-t TEMPLATE tempalte (default: scrartcl)
Prepare session root directory (default: current directory).
""",
"A:" -> (arg => author = arg),
"I" -> (arg => init_repos = true),
"T:" -> (arg => title = arg),
"n:" -> (arg => session_name = arg))
"I" -> (arg => init_repos = true),
"n:" -> (arg => session_name = arg),
"o:" -> (arg => ontologies = ontologies :+ arg),
"t:" -> (arg => template = arg),
"h" -> (arg => help = true)
)
val more_args = getopts(args)
ontologies = if (ontologies.isEmpty) List("scholarly_paper") else ontologies
if (help) {getopts.usage()} else {()}
val session_dir =
more_args match {
case Nil => Path.current
@ -63,7 +181,7 @@ Usage: isabelle dof_mkroot [OPTIONS] [DIRECTORY]
case _ => getopts.usage()
}
mkroot(session_name = session_name, session_dir = session_dir, init_repos = init_repos,
author = author, title = title, progress = new Console_Progress)
mkroot(session_parent=session_parent, session_name = session_name, session_dir = session_dir, init_repos = init_repos,
ontologies = ontologies, template = template, progress = new Console_Progress)
})
}

34
src/scala/dof_tools.scala
View File

@ -1,8 +1,34 @@
/* Author: Makarius
Isabelle/DOF command-line tools.
*/
/*
* Copyright (c)
* 2021-2022 The University of Exeter.
* 2021-2022 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
*/
package isabelle_dof
import isabelle._

160
src/scripts/build
View File

@ -1,160 +0,0 @@
#!/usr/bin/env bash
# Copyright (c) 2019 University of Exeter
# 2018-2019 University of Paris-Saclay
# 2018-2019 The University of Sheffield
#
# 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
OUTFORMAT=${1:-pdf}
NAME=${2:-root}
ROOT_NAME="root_$NAME"
install_dof_tex(){
cp $ISABELLE_DOF_HOME/src/document-templates/* .
cp $ISABELLE_DOF_HOME/src/DOF/*/*.sty .
cp $ISABELLE_DOF_HOME/src/ontologies/*/*.sty .
ISABELLE_SHORT_VERSION=`echo $ISABELLE_VERSION | sed -e 's/:.*$//'`
sed -i -e "s|%%% CONFIG %%%| \
\\\\renewcommand{\\\\dof@isabelleversion}{$ISABELLE_SHORT_VERSION} \
\\\\renewcommand{\\\\isabellelatestversion}{$DOF_LATEST_ISABELLE} \
\\\\renewcommand{\\\\isabellefullversion}{$ISABELLE_VERSION\\\\xspace} \
\\\\renewcommand{\\\\dof@version}{$DOF_VERSION} \
\\\\renewcommand{\\\\doflatestversion}{$DOF_LATEST_VERSION} \
\\\\renewcommand{\\\\isadoflatestdoi}{$DOF_LATEST_DOI} \
\\\\renewcommand{\\\\isadofgenericdoi}{$DOF_GENERIC_DOI} \
\\\\renewcommand{\\\\isabelleurl}{$ISABELLE_URL} \
\\\\renewcommand{\\\\dofurl}{$DOF_URL} \
\\\\renewcommand{\\\\dof@artifacturl}{https://$DOF_ARTIFACT_HOST/$DOF_ARTIFACT_DIR}|" \
"DOF-core.sty"
sed -i -e "s|<isadofurl>|$DOF_URL|" *.sty
sed -i -e "s|<isadofurl>|$DOF_URL|" *.tex
LTX_VERSION="$DOF_DATE $DOF_VERSION/$ISABELLE_SHORT_VERSION"
sed -i -e "s|<isadofltxversion>|$LTX_VERSION|" *.tex
sed -i -e "s|<isadofltxversion>|$LTX_VERSION|" *.sty
}
[ ! -f "$DIR/$ROOT_NAME.tex" ] && ROOT_NAME="root"
if [ -f "$DIR/$ROOT_NAME.tex" ]; then
>&2 echo ""
>&2 echo "Error: Found root file ($DIR/$ROOT_NAME.tex)"
>&2 echo "====="
>&2 echo "Isabelle/DOF does not use the Isabelle root file setup. Please check"
>&2 echo "your project setup. Your $DIR/isadof.cfg should define a Isabelle/DOF"
>&2 echo "template and your project should not include a root file."
>&2 echo ""
exit 1
fi
if [ ! -f isadof.cfg ]; then
>&2 echo ""
>&2 echo "Error: Isabelle/DOF document setup not correct"
>&2 echo "====="
>&2 echo "Could not find isadof.cfg. Please upgrade your Isabelle/DOF document"
>&2 echo "setup manually."
exit 1
fi
TEMPLATE=""
ONTOLOGY="core"
CONFIG="isadof.cfg"
while IFS= read -r line;do
fields=($(printf "%s" "$line"|cut -d':' -f1- | tr ':' ' '))
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
>&2 echo "\usepackage{DOF-$o}" >> ontologies.tex;
done
install_dof_tex
ROOT="root-$TEMPLATE.tex"
if [ ! -f $ROOT ]; then
>&2 echo ""
>&2 echo "Error: Isabelle/DOF document setup not correct"
>&2 echo "====="
>&2 echo "Could not find root file ($ROOT)."
>&2 echo "Please upgrade your Isabelle/DOF document setup manually."
exit 1
fi
cp $ROOT root.tex
# delete outdated aux files from previous runs
rm -f *.aux
sed -i -e 's/<@>/@/g' *.tex
$ISABELLE_PDFLATEX root && \
{ [ ! -f "$ROOT_NAME.bib" ] || $ISABELLE_BIBTEX root; } && \
{ [ ! -f "$ROOT_NAME.idx" ] || $ISABELLE_MAKEINDEX root; } && \
$ISABELLE_PDFLATEX root && \
$ISABELLE_PDFLATEX root
MISSING_CITATIONS=`grep 'Warning.*Citation' root.log | awk '{print $5}' | sort -u`
if [ "$MISSING_CITATIONS" != "" ]; then
>&2 echo ""
>&2 echo "ERROR (Isabelle/DOF): document referencing inconsistent due to missing citations: "
>&2 echo "$MISSING_CITATIONS"
exit 1
fi
DANGLING_REFS=`grep 'Warning.*Refer' root.log | awk '{print $4}' | sort -u`
if [ "$DANGLING_REFS" != "" ]; then
>&2 echo ""
>&2 echo "ERROR (Isabelle/DOF): document referencing inconsistent due to dangling references:"
>&2 echo "$DANGLING_REFS"
>&2 echo ""
exit 1
fi
if [ -f "root.blg" ]; then
>&2 echo "BibTeX Warnings:"
>&2 echo "================"
>&2 grep Warning root.blg | sed -e 's/Warning--//'
>&2 echo ""
fi
>&2 echo "Layout Glitches:"
>&2 echo "================"
>&2 echo -n "Number of overfull hboxes: "
>&2 grep 'Overfull .hbox' root.log | wc -l
>&2 echo -n "Number of underfull hboxes: "
>&2 grep 'Underfull .hbox' root.log | wc -l
>&2 echo -n "Number of overfull vboxes: "
grep 'Overfull .vbox' root.log | wc -l
>&2 echo -n "Number of underfull vboxes: "
grep 'Underfull .vbox' root.log | wc -l
>&2 echo ""
exit 0