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

Merge branch 'main' into test-merge

This commit is contained in:
Nicolas Méric 2022-04-01 09:59:22 +02:00
parent f96db62396 9603311a9a
commit d95a5aa2a8
80 changed files with 2128 additions and 4803 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

27
.ci/Jenkinsfile vendored
View File

@ -1,27 +0,0 @@
pipeline {
agent any
stages {
stage('Build Docker') {
steps {
sh 'cp src/patches/thy_output.ML .ci/isabelle4isadof/'
sh 'docker build -t logicalhacking:isabelle4dof .ci/isabelle4isadof'
sh 'rm -f .ci/isabelle4isadof/thy_output.ML'
}
}
stage('Check Docker') {
when { changeset "src/patches/*" }
steps {
sh 'cp src/patches/thy_output.ML .ci/isabelle4isadof/'
sh 'docker build --no-cache -t logicalhacking:isabelle4dof .ci/isabelle4isadof'
sh 'rm -f .ci/isabelle4isadof/thy_output.ML'
}
}
stage('Build Isabelle/DOF') {
steps {
sh 'find -type d -name "output" -exec rm -rf {} \\; || true'
sh 'docker run -v $PWD:/DOF logicalhacking:isabelle4dof sh -c "cd /DOF && ./install && isabelle build -D ."'
}
}
}
}

32
.ci/isabelle4isadof/Dockerfile
View File

@ -1,32 +0,0 @@
# Copyright (c) 2019 Achim D. Brucker
#
# All rights reserved.
#
# Redistribution and use in source and binary forms, with or without
# modification, are permitted provided that the following conditions are met:
#
# * Redistributions of source code must retain the above copyright notice, this
#
# * 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
FROM logicalhacking/lh-docker-isabelle:isabelle2021
WORKDIR /home/isabelle
COPY thy_output.ML /home/isabelle/Isabelle/src/Pure/Thy
RUN Isabelle/bin/isabelle build -b Functional-Automata

3
.gitattributes vendored
View File

@ -1,3 +0,0 @@
install -crlf
document-generator/Tools/DOF_mkroot -crlf
document-generator/document-template/build -crlf

1
.gitignore vendored
View File

@ -1,3 +1,4 @@
output
.afp
*~
*#

17
.woodpecker/README.md Normal file
View File

@ -0,0 +1,17 @@
# Continuous Build and Release Setup
[![status-badge](https://ci.logicalhacking.com/api/badges/Isabelle_DOF/Isabelle_DOF/status.svg)](https://ci.logicalhacking.com/Isabelle_DOF/Isabelle_DOF)
This directory contains the CI configuration for the [Woodpecker CI](https://woodpecker-ci.org/).
It may also contain additional tools and script that are useful for preparing a release.
## Generated Artifacts
### Latest Build
* lualatex
* [browser_info](https://artifacts.logicalhacking.com/ci/Isabelle_DOF/Isabelle_DOF/main/latest/lualatex/browser_info/Unsorted/)
* [aux files](https://artifacts.logicalhacking.com/ci/Isabelle_DOF/Isabelle_DOF/main/latest/lualatex/)
* pdflatex
* [browser_info](https://artifacts.logicalhacking.com/ci/Isabelle_DOF/Isabelle_DOF/main/latest/pdflatex/browser_info/Unsorted/)
* [aux files](https://artifacts.logicalhacking.com/ci/Isabelle_DOF/Isabelle_DOF/main/latest/pdflatex/)

43
.woodpecker/build.yml Normal file
View File

@ -0,0 +1,43 @@
pipeline:
build:
image: docker.io/logicalhacking/isabelle2021-1
commands:
- export ARTIFACT_DIR=$CI_WORKSPACE/.artifacts/$CI_REPO/$CI_BRANCH/$CI_BUILD_NUMBER/$LATEX
- mkdir -p $ARTIFACT_DIR
- export `isabelle getenv ISABELLE_HOME_USER`
- mkdir -p $ISABELLE_HOME_USER/etc
- echo "ISABELLE_PDFLATEX=\"$LATEX --file-line-error\"" >> $ISABELLE_HOME_USER/etc/settings
- isabelle components -u `pwd`
- isabelle build -D . -o browser_info
- isabelle mkroot_DOF DOF_test
- isabelle build -D DOF_test
- cp -r $ISABELLE_HOME_USER/browser_info $ARTIFACT_DIR
- cd $ARTIFACT_DIR
- cd ../..
- ln -s * latest
deploy:
image: docker.io/drillster/drone-rsync
settings:
hosts: [ "ci.logicalhacking.com"]
port: 22
source: .artifacts/$CI_REPO_OWNER/*
target: $CI_REPO_OWNER
include: [ "**.*"]
key:
from_secret: artifacts_ssh
user: artifacts
notify:
image: drillster/drone-email
settings:
host: smtp.0x5f.org
username: woodpecker
password:
from_secret: email
from: ci@logicalhacking.com
when:
status: [ changed, failure ]
matrix:
LATEX:
- pdflatex
- lualatex

57
.ci/mk_release → .woodpecker/mk_release
View File

@ -1,6 +1,6 @@
#!/usr/bin/env bash
# Copyright (c) 2019The University of Exeter.
# 2019 The University of Paris-Saclay.
# Copyright (c) 2019-2022 University of Exeter.
# 2019 University of Paris-Saclay.
#
# Redistribution and use in source and binary forms, with or without
# modification, are permitted provided that the following conditions
@ -39,26 +39,16 @@ print_help()
echo "Run ..."
echo ""
echo " --help, -h display this help message"
echo " --sign -s sign release archive"
echo " --sign, -s sign release archive"
echo " (default: $SIGN)"
echo " --isabelle, -i isabelle isabelle command used for installation"
echo " (default: $ISABELLE)"
echo " --tag -t tag use tag for release archive"
echo " --tag tag, -t tag use tag for release archive"
echo " (default: use master branch)"
echo " --p --publish publish generated artefact"
echo " --publish, -p publish generated artefact"
echo " (use master: $PUBLISH)"
}
read_config() {
if [ ! -f .config ]; then
echo "Error: .config not found (not started in the main directory?)!"
exit 1
else
source .config
fi
}
check_isabelle_version() {
ACTUAL_ISABELLE_VERSION=`$ISABELLE version`
echo "* Checking Isabelle version:"
@ -80,19 +70,15 @@ clone_repo()
else
echo " * Not tag specified, using master branch"
fi
(cd $ISADOF_WORK_DIR && git show -s --format="COMMIT=%H%nDATE=%cd" --date=short | sed -e 's|-|/|g') >> $ISADOF_WORK_DIR/.config
(cd $ISADOF_WORK_DIR && git show -s --format="COMMIT=%H%nDATE=%cd" --date=short | sed -e 's|-|/|g') >> $ISADOF_WORK_DIR/etc/settings
}
build_and_install_manuals()
{
echo "* Building manual"
ROOTS=$ISABELLE_HOME_USER/ROOTS
if [ -f $ROOTS ]; then
mv $ROOTS $ROOTS.backup
fi
(cd $ISADOF_WORK_DIR && ./install)
(cd $ISADOF_WORK_DIR && $ISABELLE env ./install-afp)
(cd $ISADOF_WORK_DIR && $ISABELLE build -c -D . )
mkdir -p $ISADOF_WORK_DIR/doc
@ -107,10 +93,8 @@ build_and_install_manuals()
echo " 2018-cicm-isabelle_dof-applications Example academic paper" >> $ISADOF_WORK_DIR/doc/Contents
find $ISADOF_WORK_DIR -type d -name "output" -exec rm -rf {} \; &> /dev/null || true
rm -rf $ISADOF_WORK_DIR/.git* $ISADOF_WORK_DIR/.ci $ISADOF_WORK_DIR/.afp
if [ -f $ROOTS.backup ]; then
mv $ROOTS.backup $ROOTS
fi
rm -rf $ISADOF_WORK_DIR/.git* $ISADOF_WORK_DIR/.woodpecker $ISADOF_WORK_DIR/.afp
}
create_archive()
@ -138,12 +122,13 @@ publish_archive()
}
read_config
ISABELLE=`which isabelle`
USE_TAG="false"
SIGN="false"
PUBLISH="false"
BUILD_DIR=`mktemp -d`
ISABELLE_HOME_USER=`mktemp -d`
export ISABELLE_HOME_USER
ISADOF_WORK_DIR="$BUILD_DIR/Isabelle_DOF"
while [ $# -gt 0 ]
do
@ -171,17 +156,19 @@ done
clone_repo
source $ISADOF_WORK_DIR/.config
$ISABELLE components -x `pwd`
$ISABELLE components -u $ISADOF_WORK_DIR
VARS=`$ISABELLE getenv ISABELLE_VERSION DOF_VERSION ISABELLE_HOME_USER`
for i in $VARS; do
export "$i"
done
ISABELLE_SHORT_VERSION=`echo $ISABELLE_VERSION | sed -e 's/:.*$//'`
ISADOF_TAR="Isabelle_DOF-"$DOF_VERSION"_"$ISABELLE_SHORT_VERSION
ISADOF_DIR="$BUILD_DIR/$ISADOF_TAR"
check_isabelle_version
VARS=`$ISABELLE getenv ISABELLE_HOME_USER`
for i in $VARS; do
export "$i"
done
build_and_install_manuals
create_archive
@ -194,4 +181,10 @@ if [ "$PUBLISH" = "true" ]; then
publish_archive
fi
$ISABELLE components -x $ISADOF_WORK_DIR
$ISABELLE components -u `pwd`
rm -rf ISABELLE_HOME_USER
rm -rf ISADOF_WORK_DIR
exit 0

14
CHANGELOG.md Executable file → Normal file
View File

@ -5,11 +5,21 @@ All notable changes to this project will be documented in this file.
The format is based on [Keep a Changelog](http://keepachangelog.com/en/1.0.0/)
and this project adheres to [Semantic Versioning](http://semver.org/spec/v2.0.0.html).
## [Unreleased]
## Unreleased
### Added
### Changed
- 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
means for installing the required AFP entries.
## 1.2.0 - 2022-03-26
## 1.1.0 - 2021-03-20
@ -28,4 +38,4 @@ and this project adheres to [Semantic Versioning](http://semver.org/spec/v2.0.0.
- First public release
[Unreleased]: https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF/compare/v1.0.0/Isabelle2019...HEAD
[Unreleased]: https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF/compare/v1.2.0/Isabelle2021...HEAD

1
CITATION
View File

@ -1,5 +1,4 @@
To cite Isabelle/DOF in publications, please use
Achim D. Brucker, Idir Ait-Sadoune, Paolo Crisafulli, and Burkhart
Wolff. Using The Isabelle Ontology Framework: Linking the Formal

4
LICENSE
View File

@ -1,6 +1,6 @@
Copyright (C) 2018-2019 The University of Sheffield
2019-2019 The University of Exeter
2018-2019 The University of Paris-Saclay
2019-2022 The University of Exeter
2018-2022 The University of Paris-Saclay
All rights reserved.
Redistribution and use in source and binary forms, with or without

70
README.md
View File

@ -2,54 +2,42 @@
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.1.0/Isabelle2021 is available
online.](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.1.0_Isabelle2021.pdf)
## Running Isabelle/DOF using Docker
As an alternative to installing Isabelle/DOF locally, the latest official release Isabelle/DOF
is also available on Docker Hub. Thus, if you have Docker installed and your installation of
Docker supports X11 application, you can start Isabelle/DOF as follows:
```console
foo@bar:~$ docker run -ti --rm -e DISPLAY=$DISPLAY -v /tmp/.X11-unix:/tmp/.X11-unix \
logicalhacking/isabelle_dof-1.1.0_isabelle2021 isabelle jedit
```
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 two major pre-requisites:
Isabelle/DOF has three major pre-requisites:
* **Isabelle:** Isabelle/DOF requires [Isabelle 2021](http://isabelle.in.tum.de/website-Isabelle2021/).
Please download the Isabelle 2021 distribution for your operating
system from the [Isabelle website](http://isabelle.in.tum.de/website-Isabelle2021/).
* **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
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
script as follows:
```console
foo@bar:~$ isabelle env ./install-afp
```
* **LaTeX:** Isabelle/DOF requires a modern LaTeX installation, i.e., at least
[TeX Live 2021](https://www.tug.org/texlive/) with all available updates applied.
[TeX Live 2022](https://www.tug.org/texlive/) with all available updates applied.
## Installation
In most case, the DOF-plugin can be installed as follows:
Isabelle/DOF is provided as a Isabelle component. After installing the
pre-requisites 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
```console
foo@bar:~$ ./install
foo@bar:~$ isabelle components -u `pwd`
```
If a specific Isabelle version should be used (i.e., not the default
one), the full path to the ``isabelle`` command needs to be passed as
using the ``--isabelle`` command line argument of the ``install`` script:
```console
foo@bar:~$ ./install --isabelle /usr/local/Isabelle2021/bin/isabelle
```
For further command line options of the installer, please use the
built-in help:
```console
foo@bar:~$ ./install --help
```
A final step for the installation is:
The final step for the installation is:
```console
foo@bar:~$ isabelle build -D .
@ -136,6 +124,10 @@ Usage: isabelle mkroot_DOF [OPTIONS] [DIR]
For releases, signed archives including a PDF version of the Isabelle/DOF manual are
are available:
* Isabelle/DOF 1.2.0/Isabelle2021
* [Isabelle_DOF-1.2.0_Isabelle2021.pdf](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.2.0_Isabelle2021.pdf)
* [Isabelle_DOF-1.2.0_Isabelle2021.tar.xz](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.2.0_Isabelle2021.tar.xz)
* [Isabelle_DOF-1.2.0_Isabelle2021.tar.xz.asc](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.2.0_Isabelle2021.tar.xz.asc)
* Isabelle/DOF 1.1.0/Isabelle2021
* [Isabelle_DOF-1.1.0_Isabelle2021.pdf](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.1.0_Isabelle2021.pdf)
* [Isabelle_DOF-1.1.0_Isabelle2021.tar.xz](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.1.0_Isabelle2021.tar.xz)
@ -192,7 +184,7 @@ SPDX-License-Identifier: BSD-2-Clause
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>
## Master Repository
## Upstream Repository
The master git repository for this project is hosted
<https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF>.
The upstream git repository, i.e., the single source of truth, for this project is hosted
at <https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF>.

12
etc/build.props Normal file
View File

@ -0,0 +1,12 @@
title = Isabelle/DOF
module = $ISABELLE_HOME_USER/DOF/isabelle_dof.jar
no_build = false
requirements = \
env:ISABELLE_SCALA_JAR
sources = \
src/scala/dof_document_build.scala \
src/scala/dof_mkroot.scala \
src/scala/dof_tools.scala
services = \
isabelle_dof.DOF_Tools \
isabelle_dof.DOF_Document_Build$Engine

12
etc/options Normal file
View File

@ -0,0 +1,12 @@
(* :mode=isabelle-options: *)
section "Isabelle/DOF"
public option dof_url : string = "https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF"
-- "Isabelle/DOF source repository"
option dof_artifact_dir : string = "releases/Isabelle_DOF/Isabelle_DOF"
-- "Isabelle/DOF release artifacts"
option dof_artifact_host : string = "artifacts.logicalhacking.com"

19
.config → etc/settings Executable file → Normal file
View File

@ -1,14 +1,21 @@
# -*- 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_LATEST_VERSION="1.1.0"
DOF_LATEST_ISABELLE="Isabelle2021"
DOF_LATEST_DOI="10.5281/zenodo.4625176"
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: February 2021"
ISABELLE_URL="https://isabelle.in.tum.de/website-Isabelle2021/"
AFP_DATE="afp-2021-03-09"
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

0
examples/CC_ISO15408/README
View File

3
examples/CENELEC_50128/mini_odo/ROOT
View File

@ -1,11 +1,10 @@
session "mini_odo" = "Isabelle_DOF" +
options [document = pdf, document_output = "output"]
options [document = pdf, document_output = "output", document_build = dof]
theories
"mini_odo"
document_files
"isadof.cfg"
"preamble.tex"
"build"
"root.bib"
"root.mst"
"lstisadof.sty"

46
examples/CENELEC_50128/mini_odo/document/build
View File

@ -1,46 +0,0 @@
#!/usr/bin/env bash
# Copyright (c) 2018-2019 The University of Sheffield. All rights reserved.
# 2018 The University of Paris-Saclay. All rights reserved.
#
# Redistribution and use in source and binary forms, with or without
# modification, are permitted provided that the following conditions
# are met:
# 1. Redistributions of source code must retain the above copyright
# notice, this list of conditions and the following disclaimer.
# 2. Redistributions in binary form must reproduce the above copyright
# notice, this list of conditions and the following disclaimer in
# the documentation and/or other materials provided with the
# distribution.
# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
# FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
# COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
# INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
# BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
# LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
# CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
# LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
# ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
# POSSIBILITY OF SUCH DAMAGE.
#
# SPDX-License-Identifier: BSD-2-Clause
set -e
if [ ! -f $ISABELLE_HOME_USER/DOF/document-template/build_lib.sh ]; then
echo ""
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/Isabelle_DOF/Isabelle_DOF"
echo "You can install the framework as follows:"
echo " cd Isabelle_DOF/document-generator"
echo " ./install"
echo ""
exit 1
fi
cp $ISABELLE_HOME_USER/DOF/document-template/build_lib.sh .
source build_lib.sh

1
examples/ROOTS
View File

@ -1,4 +1,3 @@
scholarly_paper
technical_report
math_exam
CENELEC_50128

2
examples/cytology/Cytology.thy
View File

@ -69,7 +69,7 @@ onto_class procaryotic_cells = cell +
onto_class eucaryotic_cells = cell +
organelles :: "organelles' list"
invariant has_nucleus :: "\<lambda>\<sigma>::eucaryotic_cells. \<exists> org \<in> set (organelles \<sigma>). is\<^sub>n\<^sub>u\<^sub>c\<^sub>l\<^sub>e\<^sub>u\<^sub>s org"
\<comment>\<open>Cells must have at least one nucleus. However, this should be executable.\<close>
\<comment> \<open>Cells must have at least one nucleus. However, this should be executable.\<close>
find_theorems (70)name:"eucaryotic_cells"
find_theorems name:has_nucleus

111
examples/math_exam/MathExam/MathExam.thy
View File

@ -1,111 +0,0 @@
(*************************************************************************
* Copyright (C)
* 2019 The University of Exeter
* 2018-2019 The University of Paris-Saclay
* 2018 The University of Sheffield
*
* License:
* This program can be redistributed and/or modified under the terms
* of the 2-clause BSD-style license.
*
* SPDX-License-Identifier: BSD-2-Clause
*************************************************************************)
(*<*)
theory MathExam
imports "Isabelle_DOF.math_exam"
HOL.Real
begin
(*>*)
(* open_monitor*[exam::MathExam] *)
section*[header::Header,examSubject= "[algebra]",
date="''02-05-2018''", timeAllowed="90::int"] \<open>Exam number 1\<close>
text\<open>
\begin{itemize}
\item Use black ink or black ball-point pen.
\item Draw diagrams in pencil.
\item Answer all questions in the spaces provided.
\end{itemize}
\<close>
text*[idir::Author, affiliation="''CentraleSupelec''",
email="''idir.aitsadoune@centralesupelec.fr''"]
\<open>Idir AIT SADOUNE\<close>
figure*[figure::figure, spawn_columns=False,
relative_width="80",
src="''figures/Polynomialdeg5''"]
\<open>A Polynome.\<close>
subsubsection*[exo1 :: Exercise, content="[q1::Task,q2::Task]"]\<open>Exercise 1\<close>
text\<open>
Here are the first four lines of a number pattern.
\begin{itemize}
\item Line 1 : @{term "1*6 + 2*4 = 2*7"}
\item Line 2 : @{term "2*7 + 2*5 = 3*8"}
\item Line 3 : @{term "3*8 + 2*6 = 4*9"}
\item Line 4 : @{term "4*9 + 2*7 = 5*10"}
\end{itemize}
\<close>
declare [[show_sorts=false]]
subsubsection*[exo2 :: Exercise, content="[q1::Task,q2::Task]"]\<open>Exercise 2\<close>
text\<open>Find the roots of the polynome:
@{term "(x^3) - 6 * x^2 + 5 * x + 12"}.
Note the intermediate steps in the following fields and submit the solution.\<close>
text\<open>
\begin{Form}[action={http://your-web-server.com/path/receiveform.cgi}]
\begin{tabular}{l}
From @{term "(x^3) - 6 * x^2 + 5 * x + 12"} \\\\
\TextField{have 1} \\\\
\TextField{have 2} \\\\
\TextField{have 3} \\\\
\TextField{finally show} \\\\
\CheckBox[width=1em]{Has the polynomial as many solutions as its degree ? } \\\\
\Submit{Submit}\\
\end{tabular}
\end{Form}
\<close>
(* a bit brutal, as long as lemma* does not yet work *)
(*<*)
lemma check_polynome :
fixes x::real
shows "(x^3) - 6 * x^2 + 5 * x + 12 = (x-4) * (x+1) * (x - 3)"
proof -
have * : "(x-4) * (x+1) * (x - 3) = (x-4) * ((x+1) * (x-3))"
by simp
have ** : "... = (x-4) * (x^2 - 2*x - 3)"
apply(auto simp: right_diff_distrib add.commute semiring_normalization_rules(1)[symmetric])
by (simp add: semiring_normalization_rules(29))
have *** : "... = x^3 - 6 * x^2 + 5 * x + 12"
apply(auto simp: right_diff_distrib left_diff_distrib add.commute semiring_normalization_rules(1)[symmetric])
by (simp add: numeral_3_eq_3 semiring_normalization_rules(29))
show ?thesis
by(simp only: * ** ***)
qed
(*>*)
text*[a1::Answer_Formal_Step]\<open>First Step: Fill in term and justification\<close>
text*[a2::Answer_Formal_Step]\<open>Next Step: Fill in term and justification\<close>
text*[a3::Answer_Formal_Step]\<open>Next Step: Fill in term and justification\<close>
text*[a4::Answer_Formal_Step]\<open>Next Step: Fill in term and justification\<close>
text*[q1::Task, local_grade="oneStar", mark="1::int", type="formal"]
\<open>Complete Line 10 : @{term "10*x + 2*y = 11*16"}\<close>
subsubsection*[exo3 :: Exercise, content="[q1::Task,q2::Task]"]\<open>Exercise 3\<close>
text*[q2::Task, local_grade="threeStars", mark="3::int", type="formal"]
\<open>Prove that @{term "n*(n+5) + 2*(n+3) "} is always the product of two numbers
with a difference of 5.
\<close>
(* this does not work on the level of the LaTeX output for known restrictions of the Toplevel. *)
(* close_monitor*[exam :: MathExam] *)
end

10
examples/math_exam/MathExam/ROOT
View File

@ -1,10 +0,0 @@
session "MathExam" = "Isabelle_DOF" +
options [document = pdf, document_output = "output"]
theories
MathExam
document_files
"preamble.tex"
"isadof.cfg"
"preamble.tex"
"build"
"figures/Polynomialdeg5.png"

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

@ -1,46 +0,0 @@
#!/usr/bin/env bash
# Copyright (c) 2018-2019 The University of Sheffield. All rights reserved.
# 2018 The University of Paris-Saclay. All rights reserved.
#
# Redistribution and use in source and binary forms, with or without
# modification, are permitted provided that the following conditions
# are met:
# 1. Redistributions of source code must retain the above copyright
# notice, this list of conditions and the following disclaimer.
# 2. Redistributions in binary form must reproduce the above copyright
# notice, this list of conditions and the following disclaimer in
# the documentation and/or other materials provided with the
# distribution.
# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
# FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
# COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
# INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
# BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
# LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
# CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
# LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
# ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
# POSSIBILITY OF SUCH DAMAGE.
#
# SPDX-License-Identifier: BSD-2-Clause
set -e
if [ ! -f $ISABELLE_HOME_USER/DOF/document-template/build_lib.sh ]; then
echo ""
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/Isabelle_DOF/Isabelle_DOF"
echo "You can install the framework as follows:"
echo " cd Isabelle_DOF/document-generator"
echo " ./install"
echo ""
exit 1
fi
cp $ISABELLE_HOME_USER/DOF/document-template/build_lib.sh .
source build_lib.sh

BIN
examples/math_exam/MathExam/document/figures/Polynomialdeg5.png
View File

Binary file not shown.
Side by Side

Before

Width:  |  Height:  |  Size: 4.9 KiB

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

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

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

@ -1,23 +0,0 @@
%% Copyright (C) 2018 The University of Sheffield
%% 2018 The University of Paris-Saclay
%% 2019 The University of Exeter
%%
%% 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
%% Copyright (C) 2018 The University of Sheffield
%% 2018 The University of Paris-Saclay
%%
%% This is a placeholder for user-specific configuration and packages.
\title{<TITLE>}
\author{<AUTHOR>}

1
examples/math_exam/ROOTS
View File

@ -1 +0,0 @@
MathExam

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

@ -1,12 +1,12 @@
session "2018-cicm-isabelle_dof-applications" = "Isabelle_DOF" +
options [document = pdf, document_output = "output", quick_and_dirty = true]
options [document = pdf, document_output = "output", document_build = dof,
quick_and_dirty = true]
theories
IsaDofApplications
document_files
"isadof.cfg"
"root.bib"
"preamble.tex"
"build"
"lstisadof.sty"
"figures/isabelle-architecture.pdf"
"figures/Dogfood-Intro.png"

46
examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/build
View File

@ -1,46 +0,0 @@
#!/usr/bin/env bash
# Copyright (c) 2018-2019 The University of Sheffield. All rights reserved.
# 2018 The University of Paris-Saclay. All rights reserved.
#
# Redistribution and use in source and binary forms, with or without
# modification, are permitted provided that the following conditions
# are met:
# 1. Redistributions of source code must retain the above copyright
# notice, this list of conditions and the following disclaimer.
# 2. Redistributions in binary form must reproduce the above copyright
# notice, this list of conditions and the following disclaimer in
# the documentation and/or other materials provided with the
# distribution.
# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
# FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
# COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
# INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
# BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
# LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
# CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
# LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
# ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
# POSSIBILITY OF SUCH DAMAGE.
#
# SPDX-License-Identifier: BSD-2-Clause
set -e
if [ ! -f $ISABELLE_HOME_USER/DOF/document-template/build_lib.sh ]; then
echo ""
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/Isabelle_DOF/Isabelle_DOF"
echo "You can install the framework as follows:"
echo " cd Isabelle_DOF/document-generator"
echo " ./install"
echo ""
exit 1
fi
cp $ISABELLE_HOME_USER/DOF/document-template/build_lib.sh .
source build_lib.sh

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

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

47
examples/scholarly_paper/2020-iFM-CSP/document/build
View File

@ -1,47 +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
if [ ! -f $ISABELLE_HOME_USER/DOF/document-template/build_lib.sh ]; then
>&2 echo ""
>&2 echo "Error: Isabelle/DOF not installed"
>&2 echo "====="
>&2 echo "This is a Isabelle/DOF project. The document preparation requires"
>&2 echo "the Isabelle/DOF framework. Please obtain the framework by cloning"
>&2 echo "the Isabelle/DOF git repository, i.e.: "
>&2 echo " git clone https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF"
>&2 echo "You can install the framework as follows:"
>&2 echo " cd Isabelle_DOF/document-generator"
>&2 echo " ./install"
>&2 echo ""
exit 1
fi
cp $ISABELLE_HOME_USER/DOF/document-template/build_lib.sh .
source build_lib.sh

12
examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy
View File

@ -1,7 +1,7 @@
(*************************************************************************
* Copyright (C)
* 2019-2021 The University of Exeter
* 2018-2021 The University of Paris-Saclay
* 2019-2022 The University of Exeter
* 2018-2022 The University of Paris-Saclay
* 2018 The University of Sheffield
*
* License:
@ -21,7 +21,7 @@ section\<open>Local Document Setup.\<close>
text\<open>Introducing document specific abbreviations and macros:\<close>
define_shortcut* dof \<rightleftharpoons> \<open>\dof\<close>
isadof \<rightleftharpoons> \<open>\isadof\<close>
isadof \<rightleftharpoons> \<open>\isadof{}\<close>
define_shortcut* TeXLive \<rightleftharpoons> \<open>\TeXLive\<close>
BibTeX \<rightleftharpoons> \<open>\BibTeX{}\<close>
@ -134,9 +134,9 @@ abstract*[abs, keywordlist="[\<open>Ontology\<close>, \<open>Ontological Modelin
It is an unique feature of \<^isadof> that ontologies may be used to control
the link between formal and informal content in documents in a machine
checked way. These links can connect both text elements as well as formal
modelling elements such as terms, definitions, code and logical formulas,
alltogether \<^emph>\<open>integrated\<close> in a state-of-the-art interactive theorem prover.
checked way. These links can connect both text elements and formal
modeling elements such as terms, definitions, code and logical formulas,
altogether \<^emph>\<open>integrated\<close> in a state-of-the-art interactive theorem prover.
\<close>

24
examples/technical_report/Isabelle_DOF-Manual/02_Background.thy
View File

@ -1,7 +1,7 @@
(*************************************************************************
* Copyright (C)
* 2019-2021 The University of Exeter
* 2018-2021 The University of Paris-Saclay
* 2019-2022 The University of Exeter
* 2018-2022 The University of Paris-Saclay
* 2018 The University of Sheffield
*
* License:
@ -26,7 +26,7 @@ figure*[architecture::figure,relative_width="95",src="''figures/isabelle-archite
the IDE (right-hand side). \<close>
text*[bg::introduction]\<open>
While Isabelle @{cite "nipkow.ea:isabelle:2002"} is widely perceived as an interactive theorem
While Isabelle is widely perceived as an interactive theorem
prover for HOL (Higher-order Logic)~@{cite "nipkow.ea:isabelle:2002"}, we would like to emphasize
the view that Isabelle is far more than that: it is the \<^emph>\<open>Eclipse of Formal Methods Tools\<close>. This
refers to the ``\<^emph>\<open>generic system framework of Isabelle/Isar underlying recent versions of Isabelle.
@ -37,7 +37,7 @@ with explicit infrastructure for building derivative systems.\<close>''~@{cite "
The current system framework offers moreover the following features:
\<^item> a build management grouping components into to pre-compiled sessions,
\<^item> a prover IDE (PIDE) framework~@{cite "wenzel:asynchronous:2014"} with various front-ends
\<^item> a prover IDE (PIDE) framework~@{cite "wenzel:asynchronous:2014"} with various front-ends,
\<^item> documentation-generation,
\<^item> code generators for various target languages,
\<^item> an extensible front-end language Isabelle/Isar, and,
@ -50,7 +50,7 @@ with Standard ML (SML) at the bottom layer as implementation language. The arch
foresees a \<^emph>\<open>Nano-Kernel\<close> (our terminology) which resides in the SML structure \<^boxed_sml>\<open>Context\<close>.
This structure provides a kind of container called \<^emph>\<open>context\<close> providing an identity, an
ancestor-list as well as typed, user-defined state for components (plugins) such as \<^isadof>.
On top of the latter, the LCF-Kernel, tactics, automated proof procedures as well as specific
On top of the latter, the LCF-Kernel, tactics, automated proof procedures as well as specific
support for higher specification constructs were built.\<close>
section*[dof::introduction]\<open>The Document Model Required by \<^dof>\<close>
@ -70,13 +70,13 @@ declare_reference*["fig:dependency"::text_section]
text\<open>
The Isabelle Framework is based on a \<^emph>\<open>document-centric view\<close> bindex>\<open>document-centric view\<close> of
The Isabelle Framework is based on a \<^emph>\<open>document-centric view\<close>\<^bindex>\<open>document-centric view\<close> of
a document, treating the input in its integrality as set of (user-programmable) \<^emph>\<open>document element\<close>
that may mutually depend and link to each other; A \<^emph>\<open>document\<close> in our sense is what is configured in a set of
that may mutually depend on and link to each other; A \<^emph>\<open>document\<close> in our sense is what is configured in a set of
\<^verbatim>\<open>ROOT\<close>- and \<^verbatim>\<open>ROOTS\<close>-files.
Isabelle assumes a hierarchical document model\<^index>\<open>document model\<close>, \<^ie>, an \<^emph>\<open>integrated\<close> document
consist of a hierarchy \<^emph>\<open>sub-documents\<close> (files); dependencies are restricted to be
consist of a hierarchy of \<^emph>\<open>sub-documents\<close> (files); dependencies are restricted to be
acyclic at this level.
Sub-documents can have different document types in order to capture documentations consisting of
documentation, models, proofs, code of various forms and other technical artifacts. We call the
@ -103,8 +103,8 @@ text\<open> A text-element \<^index>\<open>text-element\<close> may look like th
@{boxed_theory_text [display]\<open>
text\<open> According to the \<^emph>\<open>reflexivity\<close> axiom @{thm refl},
we obtain in \<Gamma> for @{term "fac 5"} the result @{value "fac 5"}.\<close>\<close>}
... so it is a command \<^theory_text>\<open>text\<close> followed by an argument (here in \<open>\<open> ... \<close>\<close> paranthesis) which
contains characters and and a special notation for semantic macros \<^bindex>\<open>semantic macros\<close>
... so it is a command \<^theory_text>\<open>text\<close> followed by an argument (here in \<open>\<open> ... \<close>\<close> parenthesis) which
contains characters and a special notation for semantic macros \<^bindex>\<open>semantic macros\<close>
(here \<^theory_text>\<open>@{term "fac 5"}).\<close>
\<close>
@ -122,7 +122,7 @@ value*[label::classid, attr\<^sub>1=E\<^sub>1, ... attr\<^sub>n=E\<^sub>n]\<open
Depending on the family, we will speak about \<^emph>\<open>(formal) text-contexts\<close>,\<^index>\<open>formal text-contexts\<close>
\<^emph>\<open>(ML) code-contexts\<close>\<^index>\<open>code-contexts\<close> and \<^emph>\<open>term-contexts\<close>\<^index>\<open>term-contexts\<close> if we refer
to sub-elements inside the \<open>\<open>...\<close>\<close> cartouches of these command families. Note that the Isabelle
framework allows for nesting cartouches that permits to support to switch into a different
framework allows for nesting cartouches that permits to support switching into a different
context. In general, this has also the effect that the evaluation of antiquotations changes.
\<^footnote>\<open>In the literature, this concept has been referred to \<open>Cascade-Syntax\<close> and was used in the
Centaur-system and is existing in some limited form in some Emacs-implementations these days. \<close>
@ -188,7 +188,7 @@ text\<open>
Isabelle provides, beyond the features required for \<^dof>, a lot of additional benefits.
Besides UTF8-support for characters used in text-elements, Isabelle offers built-in already a
mechanism user-programmable antiquotations \<^index>\<open>antiquotations\<close> which we use to implement
mechanism for user-programmable antiquotations \<^index>\<open>antiquotations\<close> which we use to implement
semantic macros \<^index>\<open>semantic macros\<close> in \<^isadof> (We will actually use these two terms
as synonym in the context of \<^isadof>). Moreover, \<^isadof> allows for the asynchronous
evaluation and checking of the document content~@{cite "wenzel:asynchronous:2014" and

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

@ -1,7 +1,7 @@
(*************************************************************************
* Copyright (C)
* 2019-2021 The University of Exeter
* 2018-2021 The University of Paris-Saclay
* 2019-2022 The University of Exeter
* 2018-2022 The University of Paris-Saclay
* 2018 The University of Sheffield
*
* License:
@ -24,22 +24,11 @@ begin
chapter*[isadof_tour::text_section]\<open>\<^isadof>: A Guided Tour\<close>
text\<open>
In this chapter, we will give a introduction into using \<^isadof> for users that want to create and
In this chapter, we will give an introduction into using \<^isadof> for users that want to create and
maintain documents following an existing document ontology.
\<close>
section*[getting_started::technical]\<open>Getting Started\<close>
text\<open>
As an alternative to installing \<^isadof>{} locally, the latest official release \<^isadof> is also
available on \href{https://cloud.docker.com/u/logicalhacking/}{Docker Hub}. Thus, if you have
\href{https://www.docker.com}{Docker} installed and
your installation of Docker supports X11 application, you can start \<^isadof> as follows:
@{boxed_bash [display] \<open>ë\prompt{}ë docker run -ti --rm -e DISPLAY=$DISPLAY \
-v /tmp/.X11-unix:/tmp/.X11-unix \
logicalhacking/isabelle_dof-ë\doflatestversionë_ë\MakeLowercase{\isabellelatestversion}ë \
isabelle jedit\<close>}
\<close>
subsection*[installation::technical]\<open>Installation\<close>
text\<open>
@ -47,8 +36,8 @@ text\<open>
\<^LaTeX>. We assume a basic familiarity with a Linux/Unix-like command line (i.e., a shell).
\<^isadof> requires Isabelle\<^bindex>\<open>Isabelle\<close> (\isabellefullversion) with a recent \<^LaTeX>-distribution
(e.g., Tex Live 2021 or later).
\<^isadof> uses a two-part version system (e.g., 1.1.0/Isabelle2021), where the first part is the version
(e.g., Tex Live 2022 or later).
\<^isadof> uses a two-part version system (e.g., 1.2.0/Isabelle2021), where the first part is the version
of \<^isadof> (using semantic versioning) and the second part is the supported version of Isabelle.
Thus, the same version of \<^isadof> might be available for different versions of Isabelle.
\<close>
@ -74,42 +63,33 @@ text\<open>
Modern Linux distribution will allow you to install \<^TeXLive> using their respective package
managers. On a modern Debian system or a Debian derivative (\<^eg>, Ubuntu), the following command
should install all required \<^LaTeX> packages:
@{boxed_bash [display]\<open>ë\prompt{}ë sudo aptitude install texlive-latex-extra texlive-fonts-extra\<close>}
@{boxed_bash [display]\<open>ë\prompt{}ë sudo aptitude install texlive-full\<close>}
\<close>
subsubsection*[isadof::technical]\<open>Installing \<^isadof>\<close>
text\<open>
In the following, we assume that you already downloaded the \<^isadof> distribution
(\href{\isadofarchiveurl}{\isadofarchiven}) from the \<^isadof> web site. The main steps for
installing are extracting the \<^isadof> distribution and calling its \<^boxed_bash>\<open>install\<close> script.
installing are extracting the \<^isadof> distribution and calling its \<^boxed_bash>\<open>install-afp\<close> script.
We start by extracting the \<^isadof> archive:
@{boxed_bash [display]\<open>ë\prompt{}ë tar xf ë\href{\isadofarchiveurl}{\isadofarchiven}ë\<close>}
This will create a directory \texttt{\isadofdirn} containing \<^isadof> distribution.
Next, we need to invoke the \<^boxed_bash>\<open>install\<close> script. If necessary, the installations
automatically downloads additional dependencies from the AFP (\<^url>\<open>https://www.isa-afp.org\<close>),
namely the AFP entries ``Functional Automata''~@{cite "nipkow.ea:functional-Automata-afp:2004"}
and ``Regular Sets and Expressions''~@{cite "kraus.ea:regular-sets-afp:2010"}. This might take a
few minutes to complete. Moreover, the installation script applies a patch to the Isabelle system,
which requires \<^emph>\<open>write permissions for the Isabelle system directory\<close> and registers \<^isadof> as
Isabelle component.
If the \<^boxed_bash>\<open>isabelle\<close> tool is not in your \<^boxed_bash>\<open>PATH\<close>, you need to call the
\<^boxed_bash>\<open>install\<close> script with the \<^boxed_bash>\<open>--isabelle\<close> option, passing the full-qualified
path of the \<^boxed_bash>\<open>isabelle\<close> tool ( \<^boxed_bash>\<open>install --help\<close> gives
you an overview of all available configuration options):
\<^isadof> depends on the the AFP (\<^url>\<open>https://www.isa-afp.org\<close>), namely the AFP
entries ``Functional Automata''~@{cite "nipkow.ea:functional-Automata-afp:2004"} and
``Regular Sets and Expressions''~@{cite "kraus.ea:regular-sets-afp:2010"}. You can either
install the complete AFP, following the instructions given at \<^url>\<open>https://www.isa-afp.org/using.html\<close>),
or use the provided \<^boxed_bash>\<open>install\<close> script to install a minimal AFP
setup into the local \<^isadof> directory. The script needs to be prefixed with the
\<^boxed_bash>\<open>isabelle env\<close> command:
@{boxed_bash [display]\<open>ë\prompt{}ë cd ë\isadofdirnë
ë\prompt{\isadofdirn}ë ./install --isabelle /usr/local/Isabelleë\isabelleversion/bin/isabelleë
ë\prompt{\isadofdirn}ë isabelle env ./install-afp
Isabelle/DOF Installer
======================
* Checking Isabelle version:
Success: found supported Isabelle version ë(\isabellefullversion)ë
* Check availability of Isabelle/DOF patch:
Warning: Isabelle/DOF patch is not available or outdated.
Trying to patch system ....
Applied patch successfully, Isabelle/HOL will be rebuilt during
the next start of Isabelle.
* Checking availability of AFP entries:\<close>}
@{boxed_bash [display]
@ -121,24 +101,12 @@ Isabelle/DOF Installer
Registering Functional-Automata iëën
/home/achim/.isabelle/Isabelleë\isabelleversion/ROOTSë
AFP installation successful.
* Searching fëëor existing installation:
No old installation found.
* Installing Isabelle/DOF
- Installing Tools iëën
/home/achim/.isabelle/Isabelleë\isabelleversion/DOF/Toolsë
- Installing document templates iëën
/home/achim/.isabelle/Isabelleë\isabelleversion/DOF/document-templateë
- Installing LaTeX styles iëën
/home/achim/.isabelle/Isabelleë\isabelleversion/DOF/latexë
- Registering Isabelle/DOF
* Registering tools iëën
/home/achim/.isabelle/Isabelleë\isabelleversion/etc/settingsë
* Installation successful. Enjoy Isabelle/DOF, you can build the session
Isabelle/DOF and all example documents by executing:
/usr/local/Isabelleë\isabelleversion/bin/isabelleë build -D . \<close>}
After the successful installation, you can explore the examples (in the sub-directory
\<^boxed_bash>\<open>examples\<close> or create your own project. On the first start, the session
\<^boxed_bash>\<open>examples\<close>) or create your own project. On the first start, the session
\<^boxed_bash>\<open>Isabelle_DOF\<close> will be built automatically. If you want to pre-build this
session and all example documents, execute:
@{boxed_bash [display]\<open>ë\prompt{\isadofdirn}ë isabelle build -D . \<close>}
@ -158,21 +126,20 @@ Now use the following coëëmmand 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>
the KOMA-Script bundle~@{cite "kohm:koma-script:2019"}). The directory \<^boxed_bash>\<open>myproject\<close>
contains the \<^isadof>-setup for your new document. To check the document formally, including the
generation of the document in PDF, you only need to execute
generation of the document in \<^pdf>, you only need to execute
@{boxed_bash [display]\<open>ë\prompt{}ë isabelle build -d . myproject \<close>}
@{boxed_bash [display]\<open>ë\prompt{myproject}ë isabelle build -d . myproject \<close>}
The dictory \<^boxed_bash>\<open>myproject\<close> contains the following files and directories:
The directory \<^boxed_bash>\<open>myproject\<close> contains the following files and directories:
\begin{center}
\begin{minipage}{.9\textwidth}
\dirtree{%
.1 .
.2 myproject.
.3 document.
.4 build\DTcomment{Build Script}.
.4 isadof.cfg\DTcomment{\<^isadof> configuraiton}.
.4 isadof.cfg\DTcomment{\<^isadof> configuration}.
.4 preamble.tex\DTcomment{Manual \<^LaTeX>-configuration}.
.3 ROOT\DTcomment{Isabelle build-configuration}.
}
@ -193,14 +160,14 @@ users are:
text\<open>
Creating a new document setup requires two decisions:
\<^item> which ontologies (\<^eg>, scholarly\_paper) are required and
\<^item> which ontologies (\<^eg>, scholarly\_paper) are required, and
\<^item> which document template (layout)\index{document template} should be used
(\<^eg>, scrartcl\index{scrartcl}). Some templates (\<^eg>, lncs) require that the users manually
obtains and adds the necessary \<^LaTeX> class file (\<^eg>, \<^boxed_bash>\<open>llncs.cls\<close>.
(\<^eg>, scrartcl\index{scrartcl}). Some templates require that the users manually
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 of \<^boxed_bash>\<open>mkroot_DOF\<close>. In
Particular, \<^boxed_bash>\<open>-o\<close> allows selecting the ontology and \<^boxed_bash>\<open>-t\<close> allows to selecting
This can be configured by using the command-line options of \<^boxed_bash>\<open>mkroot_DOF\<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:
@ -228,49 +195,96 @@ Usage: isabelle mkroot_DOF [OPTIONS] [DIR]
\<close>
section*[writing_doc::technical]\<open>Writing Documents: General Remarks\<close>
subsection*[naming::example]\<open>Name-Spaces, Long- and Short-Names\<close>
text\<open>\<^isadof> is built upon the name space and lexical conventions of Isabelle. Long-names were
composed of a name of the session, the name of the theory, and a sequence of local names referring
to, \<^eg>, nested specification constructs that were used to identify types, constant symbols,
definitions, \<^etc>. The general format of a long-name is
\<^boxed_theory_text>\<open> session_name.theory_name.local_name. ... .local_name\<close>
By lexical conventions, theory-names must be unique inside a session
(and session names must be unique too), such that long-names are unique by construction.
There are actually different name categories that form a proper name space, \<^eg>, the name space for
constant symbols and type symbols are distinguished.
Isabelle identifies names already with the shortest suffix that is unique in the global
context and in the appropriate name category. This also holds for pretty-printing, which can
at times be confusing since names stemming from the same specification construct may
be printed with different prefixes according to their uniqueness.
\<close>
subsection*[cartouches::example]\<open>Caveat: Lexical Conventions of Cartouches, Strings, Names, ... \<close>
text\<open>WARNING: The embedding of strings, terms, names \<^etc>, as parts of commands, anti-quotations,
terms, \<^etc>, is unfortunately not always so consistent as one might expect, when it comes
to variants that should be lexically equivalent in principle. This can be a nuisance for
users, but is again a consequence that we build on existing technology that has been developed
over decades.
\<close>
text\<open>At times, this causes idiosyncrasies like the ones cited in the following incomplete list:
\<^item> text-antiquotations
\<^theory_text>\<open>text\<close>\<^latex>\<open>\isasymopen\textbf{thm} "normally\_behaved\_def"\isasymclose\ \<close>
versus \<^theory_text>\<open>text\<close>\<^latex>\<open>\isasymopen @\{\textbf{thm} "srac$_1$\_def"\}\isasymclose\ \<close>
(while
\<^theory_text>\<open>text\<close>\<^latex>\<open>\isasymopen @\{\textbf{thm} \isasymopen srac$_1$\_def \isasymclose\}\isasymclose\ \<close>
fails)
\<^item> commands \<^theory_text>\<open>thm fundamental_theorem_of_calculus\<close> and
\<^theory_text>\<open>thm\<close>\<^latex>\<open> "fundamental\_theorem\_of\_calculus"\<close>
or \<^theory_text>\<open>lemma\<close> \<^latex>\<open>"H"\<close> and \<^theory_text>\<open>lemma \<open>H\<close>\<close> and \<^theory_text>\<open>lemma H\<close>
\<^item> string expressions \<^theory_text>\<open>term\<close>\<^latex>\<open>\isasymopen ''abc'' @ ''cd''\isasymclose\ \<close> and equivalent
\<^theory_text>\<open>term\<close>\<^latex>\<open>\isasymopen \isasymopen abc\isasymclose\ @ \isasymopen cd\isasymclose\isasymclose\<close>;
but
\<^theory_text>\<open>term\<close>\<^latex>\<open>\isasymopen\isasymopen A \isasymlongrightarrow\ B\isasymclose\isasymclose\ \<close>
not equivalent to \<^theory_text>\<open>term\<close>\<^latex>\<open>\isasymopen''A \isasymlongrightarrow\ B''\isasymclose\ \<close>
which fails.
\<close>
section*[scholar_onto::example]\<open>Writing Academic Publications in \<^boxed_theory_text>\<open>scholarly_paper\<close>\<close>
subsection\<open>Writing Academic Papers\<close>
text\<open>
The ontology \<^boxed_theory_text>\<open>scholarly_paper\<close>
The ontology \<^verbatim>\<open>scholarly_paper\<close>
\<^index>\<open>ontology!scholarly\_paper\<close> is an ontology modeling
academic/scientific papers, with a slight bias to texts in the domain of mathematics and engineering.
We explain first the principles of its underlying ontology, and then we present two ''real''
academic/scientific papers, with a slight bias towards texts in the domain of mathematics and engineering.
We explain first the principles of its underlying ontology, and then we present two ``real''
examples from our own publication practice.
\<close>
text\<open>
\<^enum> The iFM 2020 paper~@{cite "taha.ea:philosophers:2020"} is a typical mathematical text,
heavy in definitions with complex mathematical notation and a lot of non-trivial cross-referencing
between statements, definitions and proofs which is ontologically tracked. However, wrt.
between statements, definitions and proofs which are ontologically tracked. However, wrt.
the possible linking between the underlying formal theory and this mathematical presentation,
it follows a pragmatic path without any ``deep'' linking to types, terms and theorems,
deliberately not exploiting \<^isadof> 's full potential with this regard.
\<^enum> In the CICM 2018 paper~@{cite "brucker.ea:isabelle-ontologies:2018"}, we deliberately
refrain from integrating references to formal content in order demonstrate that \<^isadof> is not
refrain from integrating references to formal content in order to demonstrate that \<^isadof> is not
a framework from Isabelle users to Isabelle users only, but people just avoiding as much as
possible \<^LaTeX> notation.
The \<^isadof> distribution contains both examples using the ontology \<^verbatim>\<open>scholarly_paper\<close> in
the directory \nolinkurl{examples/scholarly_paper/2018-cicm-isabelle_dof-applications/} or
\nolinkurl{examples/scholarly_paper/2020-ifm-csp-applications/}.
\nolinkurl{examples/scholarly_paper/2020-iFM-CSP}.
You can inspect/edit the example in Isabelle's IDE, by either
\<^item> starting Isabelle/jedit using your graphical user interface (\<^eg>, by clicking on the
\<^item> starting Isabelle/jEdit using your graphical user interface (\<^eg>, by clicking on the
Isabelle-Icon provided by the Isabelle installation) and loading the file
\nolinkurl{examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy}.
\<^item> starting Isabelle/jedit from the command line by,\<^eg>, calling:
\nolinkurl{examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy},
\<^item> starting Isabelle/jEdit from the command line by, \<^eg>, calling:
@{boxed_bash [display]\<open>ë\prompt{\isadofdirn}ë
isabelle jedit -d . examples/scholarly_paper/2020-iFM-CSP/paper.thy \<close>}
\<close>
text\<open> You can build the PDF-document at the command line by calling:
text\<open> You can build the \<^pdf>-document at the command line by calling:
@{boxed_bash [display] \<open>ë\prompt{}ë isabelle build -d . 2020-iFM-csp \<close>}
\<close>
subsection*[sss::technical]\<open>A Bluffers Guide to the \<^verbatim>\<open>scholarly_paper\<close> Ontology\<close>
text\<open> In this section we give a minimal overview of the ontology formalized in
@{theory \<open>Isabelle_DOF.scholarly_paper\<close>}.\<close>
\<^theory>\<open>Isabelle_DOF.scholarly_paper\<close>.\<close>
text\<open> We start by modeling the usual text-elements of an academic paper: the title and author
information, abstract, and text section:
@ -292,18 +306,18 @@ doc_class abstract =
principal_theorems :: "thm list"\<close>}
\<close>
text\<open>Note \<open>short_title\<close> and \<open>abbrev\<close> are optional and have the default \<open>None\<close> (no value).
Note further, that abstracts may have a \<open>principal_theorems\<close> list, where the built-in \<^isadof> type
\<open>thm list\<close> which contain references to formally proven theorems that must exist in the logical
context of this document; this is a decisive feature of \<^isadof> that conventional ontological
languages lack.\<close>
text\<open>Note \<^const>\<open>short_title\<close> and \<^const>\<open>abbrev\<close> are optional and have the default \<^const>\<open>None\<close>
(no value). Note further, that \<^typ>\<open>abstract\<close>s may have a \<^const>\<open>principal_theorems\<close> list, where
the built-in \<^isadof> type \<^typ>\<open>thm list\<close> contains references to formally proven theorems that must
exist in the logical context of this document; this is a decisive feature of \<^isadof> that
conventional ontological languages lack.\<close>
text\<open>We continue by the introduction of a main class: the text-element \<open>text_section\<close> (in contrast
to \<open>figure\<close> or \<open>table\<close> or similar). Note that
the \<open>main_author\<close> is typed with the class \<open>author\<close>, a HOL type that is automatically derived from
the document class definition \<open>author\<close> shown above. It is used to express which author currently
``owns'' this \<open>text_section\<close>, an information that can give rise to presentational or even
access-control features in a suitably adapted front-end.
text\<open>We continue by the introduction of a main class: the text-element \<^typ>\<open>text_section\<close>
(in contrast to \<^typ>\<open>figure\<close> or \<open>table\<close> or similar). Note that
the \<^const>\<open>main_author\<close> is typed with the class \<^typ>\<open>author\<close>, a HOL type that is automatically
derived from the document class definition \<^typ>\<open>author\<close> shown above. It is used to express which
author currently ``owns'' this \<^typ>\<open>text_section\<close>, an information that can give rise to
presentational or even access-control features in a suitably adapted front-end.
@{boxed_theory_text [display] \<open>
doc_class text_section = text_element +
@ -312,16 +326,16 @@ doc_class text_section = text_element +
level :: "int option" <= "None"
\<close>}
The \<open>level\<close>-attibute \<^index>\<open>level\<close> enables doc-notation support for headers, chapters, sections, and
subsections; we follow here the \<^LaTeX> terminology on levels to which \<^isadof> is currently targeting at.
The values are interpreted accordingly to the \<^LaTeX> standard. The correspondance between the levels
The \<^const>\<open>Isa_COL.text_element.level\<close>-attibute \<^index>\<open>level\<close> enables doc-notation support for
headers, chapters, sections, and subsections; we follow here the \<^LaTeX> terminology on levels to which \<^isadof> is currently targeting at.
The values are interpreted accordingly to the \<^LaTeX> standard. The correspondence between the levels
and the structural entities is summarized as follows:
\<^item> part \<^index>\<open>part\<close> \<^bigskip>\<^bigskip> \<open>Some -1\<close> \vspace{-1cm}
\<^item> chapter \<^index>\<open>chapter\<close> \<^bigskip>\<^bigskip> \<open>Some 0\<close> \vspace{-1cm}
\<^item> section \<^index>\<open>section\<close> \<^bigskip>\<^bigskip> \<open>Some 1\<close> \vspace{-1cm}
\<^item> subsection \<^index>\<open>subsection\<close> \<^bigskip>\<^bigskip> \<open>Some 2\<close> \vspace{-1cm}
\<^item> subsubsection \<^index>\<open>subsubsection\<close> \<^bigskip>\<^bigskip> \<open>Some 3\<close> \vspace{-0.1cm}
\<^item> part \<^index>\<open>part\<close> \<open>Some -1\<close> \vspace{-0.3cm}
\<^item> chapter \<^index>\<open>chapter\<close> \<open>Some 0\<close> \vspace{-0.3cm}
\<^item> section \<^index>\<open>section\<close> \<open>Some 1\<close> \vspace{-0.3cm}
\<^item> subsection \<^index>\<open>subsection\<close> \<open>Some 2\<close> \vspace{-0.3cm}
\<^item> subsubsection \<^index>\<open>subsubsection\<close> \<open>Some 3\<close> \vspace{-0.1cm}
Additional means assure that the following invariant is maintained in a document
conforming to \<^verbatim>\<open>scholarly_paper\<close>:
@ -329,45 +343,47 @@ conforming to \<^verbatim>\<open>scholarly_paper\<close>:
\center {\<open>level > 0\<close>}
\<close>
text\<open> The rest of the ontology introduces concepts for \<open>introductions\<close>, \<open>conclusion\<close>, \<open>related_work\<close>,
\<open>bibliography\<close> etc. More details can be found in \<^verbatim>\<open>scholarly_paper\<close> contained ion the
theory @{theory \<open>Isabelle_DOF.scholarly_paper\<close>}. \<close>
text\<open> The rest of the ontology introduces concepts for \<^typ>\<open>introduction\<close>, \<^typ>\<open>conclusion\<close>,
\<^typ>\<open>related_work\<close>, \<^typ>\<open>bibliography\<close> etc. More details can be found in \<^verbatim>\<open>scholarly_paper\<close>
contained in the theory \<^theory>\<open>Isabelle_DOF.scholarly_paper\<close>. \<close>
subsection\<open>Writing Academic Publications I : A Freeform Mathematics Text \<close>
subsection\<open>Writing Academic Publications: A Freeform Mathematics Text \<close>
text*[csp_paper_synthesis::technical, main_author = "Some bu"]\<open>We present a typical mathematical
paper focussing on its form, not refering in any sense to its content which is out of scope here.
paper focusing on its form, not referring in any sense to its content which is out of scope here.
As mentioned before, we chose the paper~@{cite "taha.ea:philosophers:2020"} for this purpose,
which is written in the so-called free-form style: Formulas are superficially parsed and
type-setted, but no deeper type-checking and checking with the underlying logical context
type-set, but no deeper type-checking and checking with the underlying logical context
is undertaken. \<close>
figure*[fig0::figure,spawn_columns=False,relative_width="90",src="''figures/header_CSP_source.png''"]
\<open> A mathematics paper as integrated document source ... \<close>
figure*[fig0B::figure,spawn_columns=False,relative_width="90",src="''figures/header_CSP_pdf.png''"]
\<open> \ldots and as corresponding \<^pdf>-output. \<close>
\<open> ... and as corresponding \<^pdf>-output. \<close>
text\<open>The integrated source of this paper-except is shown in \<^figure>\<open>fig0\<close>, while the
text\<open>The integrated source of this paper-excerpt is shown in \<^figure>\<open>fig0\<close>, while the
document build process converts this to the corresponding \<^pdf>-output shown in \<^figure>\<open>fig0B\<close>.\<close>
text\<open>Recall that the standard syntax for a text-element in \<^isadof> is
\<^theory_text>\<open>text*[<id>::<class_id>,<attrs>]\<open> ... text ...\<close>\<close>, but there are a few built-in abbreviations like
\<^theory_text>\<open>title*[<id>,<attrs>]\<open> ... text ...\<close>\<close> that provide special command-level syntax for text-elements.
The other text-elements provide the authors and the abstract as specified by their class-id referring
to the \<^theory_text>\<open>doc_class\<close>es of \<^verbatim>\<open>scholarly_paper\<close>; we say that these text elements are \<^emph>\<open>instances\<close>
The other text-elements provide the authors and the abstract as specified by their
\<^emph>\<open>class\_id\<close>\<^index>\<open>class\_id@\<open>class_id\<close>\<close>
referring to the \<^theory_text>\<open>doc_class\<close>es of \<^verbatim>\<open>scholarly_paper\<close>;
we say that these text elements are \<^emph>\<open>instances\<close>
\<^bindex>\<open>instance\<close> of the \<^theory_text>\<open>doc_class\<close>es \<^bindex>\<open>doc\_class\<close> of the underlying ontology. \<close>
text\<open>\vspace{1,5cm} The paper proceeds by providing instances for introduction, technical sections,
text\<open>The paper proceeds by providing instances for introduction, technical sections,
examples, \<^etc>. We would like to concentrate on one --- mathematical paper oriented --- detail in the
ontology \<^verbatim>\<open>scholarly_paper\<close>:
@{boxed_theory_text [display]
\<open>doc_class technical = text_section + . . .
\<open>doc_class technical = text_section + ...
type_synonym tc = technical (* technical content *)
datatype math_content_class = "defn" | "axm" | "thm" | "lem" | "cor" | "prop" | ...
datatype math_content_class = "defn" | "axm" | "thm" | "lem" | "cor" | "prop" | ...
doc_class math_content = tc + ...
@ -379,53 +395,49 @@ doc_class "theorem" = math_content +
\<close>}\<close>
text\<open>The class \<^verbatim>\<open>technical\<close> regroups a number of text-elements that contain typical
"technical content" in mathematical or engineering papers: code, definitions, theorems,
lemmas, examples. From this class, the more stricter class of @{typ \<open>math_content\<close>} is derived,
text\<open>The class \<^typ>\<open>technical\<close> regroups a number of text-elements that contain typical
technical content in mathematical or engineering papers: code, definitions, theorems,
lemmas, examples. From this class, the stricter class of @{typ \<open>math_content\<close>} is derived,
which is grouped into @{typ "definition"}s and @{typ "theorem"}s (the details of these
class definitions are omitted here). Note, however, that class identifiers can be abbreviated by
standard \<^theory_text>\<open>type_synonym\<close>s for convenience and enumeration types can be defined by the
standard inductive \<^theory_text>\<open>datatype\<close> definition mechanism in Isabelle, since any HOL type is admitted
for attibute declarations. Vice-versa, document class definitions imply a corresponding HOL type
for attribute declarations. Vice-versa, document class definitions imply a corresponding HOL type
definition. \<close>
figure*[fig01::figure,spawn_columns=False,relative_width="95",src="''figures/definition-use-CSP.png''"]
\<open> A screenshot of the integrated source with definitions ...\<close>
text\<open>An example for a sequence of (Isabelle-formula-) texts, their ontological declarations as
\<open>"definition"\<close>s in terms of the \<^verbatim>\<open>scholarly_paper\<close>-ontology and their type-conform referencing
text\<open>An example for a sequence of (Isabelle-formula-)texts, their ontological declarations as
\<^typ>\<open>definition\<close>s in terms of the \<^verbatim>\<open>scholarly_paper\<close>-ontology and their type-conform referencing
later is shown in \<^figure>\<open>fig01\<close> in its presentation as the integrated source.
Note that the use in the ontology-generated antiquotation \<^theory_text>\<open>@{definition X4}\<close>
is type-checked; referencing \<^verbatim>\<open>X4\<close> as \<^theory_text>\<open>theorem\<close> would be a type-error and be reported directly
by \<^isadof> in Isabelle/jEdit. Note further, that if referenced correctly wrt. the sub-typing
hierarchy makes \<^verbatim>\<open>X4\<close> \<^emph>\<open>navigable\<close> in Isabelle/jedit; a click will cause the IDE to present the
hierarchy makes \<^verbatim>\<open>X4\<close> \<^emph>\<open>navigable\<close> in Isabelle/jEdit; a click will cause the IDE to present the
defining occurrence of this text-element in the integrated source.
% TODO:
% The definition \<^theory_text>\<open>@{definition X4}\<close> is not present in the screenshot,
% it might be better to use \<^theory_text>\<open>@{definition X22}\<close>.
Note, further, how \<^isadof>-commands like \<^theory_text>\<open>text*\<close> interact with standard Isabelle document
antiquotations described in the Isabelle Isar Reference Manual in Chapter 4.2 in great detail.
We refrain ourselves here to briefly describe three freeform antiquotations used her in this text:
We refrain ourselves here to briefly describe three freeform antiquotations used in this text:
\<^item> the freeform term antiquotation, also called \<^emph>\<open>cartouche\<close>, written by
\<open>@{cartouche [style-parms] \<open>. . .\<close>\<close> or just by \<open>\<open>...\<close>\<close> if the list of style parameters
\<open>@{cartouche [style-parms] \<open>...\<close>}\<close> or just by \<open>\<open>...\<close>\<close> if the list of style parameters
is empty,
\<^item> the freeform antiquotation for theory fragments written \<open>@{theory_text [style-parms] \<open>...\<close>\<close>
or just \<^verbatim>\<open>\<^theory_text> \<open>...\<close>\<close> if the list of style parameters
is empty,
\<^item> the freeform antiquotation for theory fragments written \<open>@{theory_text [style-parms] \<open>...\<close>}\<close>
or just \<^verbatim>\<open>\<^theory_text>\<close>\<open>\<open>...\<close>\<close> if the list of style parameters is empty,
\<^item> the freeform antiquotations for verbatim, emphasized, bold, or footnote text elements.
\<close>
figure*[fig02::figure,spawn_columns=False,relative_width="95",src="''figures/definition-use-CSP-pdf.png''"]
\<open> ... and the corresponding pdf-oputput.\<close>
\<open> ... and the corresponding \<^pdf>-output.\<close>
text\<open>
\<^isadof> text-elements such as \<^theory_text>\<open>text*\<close> allow to have such standard term-antiquotations inside their
text, permitting to give the whole text entity a formal, referentiable status with typed meta-
information attached to it that may be used for presentation issues, search, or other technical
purposes. The corresponding output of this snippet in the integrated source is shown in \<^figure>\<open>fig02\<close>.
text, permitting to give the whole text entity a formal, referentiable status with typed
meta-information attached to it that may be used for presentation issues, search,
or other technical purposes.
The corresponding output of this snippet in the integrated source is shown in \<^figure>\<open>fig02\<close>.
\<close>
@ -443,10 +455,10 @@ doc_class figure = text_section +
\<close>}
\<close>
figure*[fig_figures::figure,spawn_columns=False,relative_width="85",src="''figures/Dogfood-figures''"]
\<open> Declaring figures in the integrated source \ldots \<close>
\<open> Declaring figures in the integrated source.\<close>
text\<open>
The document class \<^boxed_theory_text>\<open>figure\<close> (supported by the \<^isadof> command abbreviation
The document class \<^typ>\<open>figure\<close> (supported by the \<^isadof> command abbreviation
\<^boxed_theory_text>\<open>figure*\<close>) makes it possible to express the pictures and diagrams
as shown in \<^figure>\<open>fig_figures\<close>, which presents its own representation in the
integrated source as screenshot.\<close>
@ -459,14 +471,11 @@ text\<open>
doc_class article =
style_id :: string <= "''LNCS''"
version :: "(int \<times> int \<times> int)" <= "(0,0,0)"
where "(title ~~ \<lbrakk>subtitle\<rbrakk> ~~ \<lbrace>author\<rbrace>$^+$+ ~~ abstract ~~
introduction ~~ \<lbrace>technical || example\<rbrace>$^+$ ~~ conclusion ~~
bibliography)"
accepts "(title ~~ \<lbrakk>subtitle\<rbrakk> ~~ \<lbrace>author\<rbrace>\<^sup>+ ~~ abstract ~~ \<lbrace>introduction\<rbrace>\<^sup>+
~~ \<lbrace>background\<rbrace>\<^sup>* ~~ \<lbrace>technical || example \<rbrace>\<^sup>+ ~~ \<lbrace>conclusion\<rbrace>\<^sup>+
~~ bibliography ~~ \<lbrace>annex\<rbrace>\<^sup>* )"
\<close>}\<close>
(* % TODO:
% Update to the new implementation.
% where is deprecated and the new implementation uses accepts and rejects. *)
text\<open>
In a integrated document source, the body of the content can be paranthesized into:
@ -478,7 +487,7 @@ text\<open>
which signals to \<^isadof> begin and end of the part of the integrated source
in which the text-elements instances are expected to appear in the textual ordering
defined by \<^theory_text>\<open>article\<close>.
defined by \<^typ>\<open>article\<close>.
\<close>
@ -491,12 +500,18 @@ side_by_side_figure*[exploring::side_by_side_figure,anchor="''fig-Dogfood-II-bgn
side_by_side_figure*["hyperlinks"::side_by_side_figure,anchor="''fig:Dogfood-IV-jumpInDocCLass''",
caption="''Hyperlink to class-definition.''",relative_width="48",
src="''figures/Dogfood-IV-jumpInDocCLass''",anchor2="''fig:Dogfood-V-attribute''",
caption2="''Exploring an attribute.''",relative_width2="47",
src2="''figures/Dogfood-III-bgnd-text_section''"]\<open>Navigation via generated hyperlinks.\<close>
src="''figures/Dogfood-IV-jumpInDocCLass''",
anchor2="''fig:Dogfood-V-attribute''",
caption2="''Exploring an attribute (hyperlinked to the class).''",
relative_width2="47",
src2="''figures/Dogfood-V-attribute''"]\<open>Navigation via generated hyperlinks.\<close>
(* TODO: Update the images in fig:Dogfood-IV-jumpInDocCLass side_by_side_figure
to align them. This has to wait that the exploration of an attribute is again possible.
See: https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF/issues/10 *)
text\<open>
From these class definitions, \<^isadof> also automatically generated editing
support for Isabelle/jedit. In \autoref{fig-Dogfood-II-bgnd1} and
support for Isabelle/jEdit. In \autoref{fig-Dogfood-II-bgnd1} and
\autoref{fig-bgnd-text_section} we show how hovering over links permits to explore its
meta-information. Clicking on a document class identifier permits to hyperlink into the
corresponding class definition (\autoref{fig:Dogfood-IV-jumpInDocCLass}); hovering over an
@ -504,45 +519,53 @@ text\<open>
\autoref{fig:Dogfood-V-attribute}) shows its type.
\<close>
figure*[figDogfoodVIlinkappl::figure,relative_width="80",src="''figures/Dogfood-V-attribute''"]
\<open> Exploring an attribute (hyperlinked to the class). \<close>
figure*[figDogfoodVIlinkappl::figure,relative_width="80",src="''figures/Dogfood-VI-linkappl.png''"]
\<open>Exploring an ontological reference.\<close>
text\<open>
An ontological reference application in @{figure "figDogfoodVIlinkappl"}: the
ontology-dependant antiquotation \<^boxed_theory_text>\<open>@ {example ...}\<close> refers to the corresponding
text-elements. Hovering allows for inspection, clicking for jumping to the definition. If the
link does not exist or has a non-compatible type, the text is not validated,\<^ie>, Isabelle/jEdit
will respond with an error.\<close>
ontology-dependant antiquotation \<^boxed_theory_text>\<open>@{example \<open>ex1\<close>}\<close> refers to the corresponding
text-element \<^boxed_theory_text>\<open>ex1\<close>.
Hovering allows for inspection, clicking for jumping to the definition.
If the link does not exist or has a non-compatible type, the text is not validated, \<^ie>,
Isabelle/jEdit will respond with an error.\<close>
section*[cenelec_onto::example]\<open>Writing Certification Documents (CENELEC\_50128)\<close>
text\<open>We advise users to experiment with different notation variants.
Note, further, that the Isabelle \<^latex>\<open>@\{cite ...\}\<close>-text-anti-quotation makes its checking
on the level of generated \<^verbatim>\<open>.aux\<close>-files, which are not necessarily up-to-date. Ignoring the PIDE
error-message and compiling a with a consistent bibtex usually makes disappear this behavior.
\<close>
section*[cenelec_onto::example]\<open>Writing Certification Documents \<^boxed_theory_text>\<open>CENELEC_50128\<close>\<close>
subsection\<open>The CENELEC 50128 Example\<close>
text\<open>
The ontology ``CENELEC\_50128''\index{ontology!CENELEC\_50128} is a small ontology modeling
The ontology \<^verbatim>\<open>CENELEC_50128\<close>\index{ontology!CENELEC\_50128} is a small ontology modeling
documents for a certification following CENELEC 50128~@{cite "boulanger:cenelec-50128:2015"}.
The \<^isadof> distribution contains a small example using the ontology ``CENELEC\_50128'' in
the directory \nolinkurl{examples/CENELEC_50128/mini_odo/}. You can inspect/edit the
integrated source example by either
\<^item> starting Isabelle/jedit using your graphical user interface (\<^eg>, by clicking on the
\<^item> starting Isabelle/jEdit using your graphical user interface (\<^eg>, by clicking on the
Isabelle-Icon provided by the Isabelle installation) and loading the file
\nolinkurl{examples/CENELEC_50128/mini_odo/mini_odo.thy}.
\<^item> starting Isabelle/jedit from the command line by calling:
\<^item> starting Isabelle/jEdit from the command line by calling:
@{boxed_bash [display]\<open>ë\prompt{\isadofdirn}ë
isabelle jedit examples/CENELEC_50128/mini_odo/mini_odo.thy \<close>}
\<close>
text\<open>\<^noindent> Finally, you
\<^item> can build the PDF-document by calling:
@{boxed_bash [display]\<open>ë\prompt{}ë isabelle build mini_odo \<close>}
\<^item> can build the \<^pdf>-document by calling:
@{boxed_bash [display]\<open>ë\prompt{\isadofdirn}ë isabelle build mini_odo \<close>}
\<close>
subsection\<open>Modeling CENELEC 50128\<close>
text\<open>
Documents to be provided in formal certifications (such as CENELEC
50128~@{cite "boulanger:cenelec-50128:2015"} or Common Criteria~@{cite "cc:cc-part3:2006"}) can
much profit from the control of ontological consistency: a substantial amount of the work
of evaluators in formal certification processes consists in tracing down the links from
requirements over assumptions down to elements of evidence, be it in form of semi-formal
documentation, models, code, or tests. In a certification process, traceability becomes a major
documentation, models, code, or tests. In a certification process, traceability becomes a major
concern; and providing mechanisms to ensure complete traceability already at the development of
the integrated source can in our view increase the speed and reduce the risk certification
processes. Making the link-structure machine-checkable, be it between requirements, assumptions,
@ -561,13 +584,6 @@ text\<open>
@{boxed_theory_text [display]\<open>
doc_class requirement = long_name :: "string option"
doc_class requirement_analysis = no :: "nat"
where "requirement_item +"
(*
% TODO:
% Update to the new implementation.
% where is deprecated and the new implementation uses accepts and rejects.
*)
doc_class hypothesis = requirement +
hyp_type :: hyp_type <= physical (* default *)
@ -579,31 +595,31 @@ doc_class assumption = requirement +
Such ontologies can be enriched by larger explanations and examples, which may help
the team of engineers substantially when developing the central document for a certification,
like an explication of what is precisely the difference between an \<^emph>\<open>hypothesis\<close> and an
\<^emph>\<open>assumption\<close> in the context of the evaluation standard. Since the PIDE makes for each
like an explication of what is precisely the difference between an \<^typ>\<open>hypothesis\<close> and an
\<^typ>\<open>assumption\<close> in the context of the evaluation standard. Since the PIDE makes for each
document class its definition available by a simple mouse-click, this kind on meta-knowledge
can be made far more accessible during the document evolution.
For example, the term of category \<^emph>\<open>assumption\<close> is used for domain-specific assumptions.
It has formal, semi-formal and informal sub-categories. They have to be
For example, the term of category \<^typ>\<open>assumption\<close> is used for domain-specific assumptions.
It has \<^const>\<open>formal\<close>, \<^const>\<open>semiformal\<close> and \<^const>\<open>informal\<close> sub-categories. They have to be
tracked and discharged by appropriate validation procedures within a
certification process, be it by test or proof. It is different from a hypothesis, which is
certification process, be it by test or proof. It is different from a \<^typ>\<open>hypothesis\<close>, which is
globally assumed and accepted.
In the sequel, the category \<^emph>\<open>exported constraint\<close> (or \<^emph>\<open>ec\<close> for short)
In the sequel, the category \<^typ>\<open>exported_constraint\<close> (or \<^typ>\<open>EC\<close> for short)
is used for formal assumptions, that arise during the analysis,
design or implementation and have to be tracked till the final
evaluation target, and discharged by appropriate validation procedures
within the certification process, be it by test or proof. A particular class of interest
is the category \<^emph>\<open>safety related application condition\<close> (or \<^emph>\<open>SRAC\<close>
for short) which is used for \<^emph>\<open>ec\<close>'s that establish safety properties
is the category \<^typ>\<open>safety_related_application_condition\<close> (or \<^typ>\<open>SRAC\<close>
for short) which is used for \<^typ>\<open>EC\<close>'s that establish safety properties
of the evaluation target. Their traceability throughout the certification
is therefore particularly critical. This is naturally modeled as follows:
@{boxed_theory_text [display]\<open>
doc_class ec = assumption +
doc_class EC = assumption +
assumption_kind :: ass_kind <= (*default *) formal
doc_class SRAC = ec +
doc_class SRAC = EC +
assumption_kind :: ass_kind <= (*default *) formal
\<close>}
@ -617,45 +633,40 @@ text*[ass123::SRAC]\<open>
\<close>
\<close>}
This will be shown in the PDF as follows:
This will be shown in the \<^pdf> as follows:
\<close>
text*[ass123::SRAC] \<open> The overall sampling frequence of the odometer
text*[ass123::SRAC] \<open> The overall sampling frequency of the odometer
subsystem is therefore 14 khz, which includes sampling, computing and
result communication times \ldots \<close>
text\<open>Note that this pdf-output is the result of a specific setup for "SRAC"s.\<close>
text\<open>Note that this \<^pdf>-output is the result of a specific setup for \<^typ>\<open>SRAC\<close>s.\<close>
subsection*[ontopide::technical]\<open>Editing Support for CENELEC 50128\<close>
figure*[figfig3::figure,relative_width="95",src="''figures/antiquotations-PIDE''"]
\<open> Standard antiquotations referring to theory elements.\<close>
text\<open> The corresponding view in @{docitem \<open>figfig3\<close>} shows core part of a document
conforming to the CENELEC 50128 ontology. The first sample shows standard Isabelle antiquotations
conforming to the \<^verbatim>\<open>CENELEC_50128\<close> ontology. The first sample shows standard Isabelle antiquotations
@{cite "wenzel:isabelle-isar:2020"} into formal entities of a theory. This way, the informal parts
of a document get ``formal content'' and become more robust under change.\<close>
figure*[figfig5::figure, relative_width="95", src="''figures/srac-definition''"]
\<open> Defining a "SRAC" in the integrated source \ldots \<close>
text\<open>
TODO:
The screenshot (figures/srac-definition) of the figure figfig5 should be updated
to have a SRAC type in uppercase.
\<close>
\<open> Defining a \<^typ>\<open>SRAC\<close> in the integrated source ... \<close>
figure*[figfig7::figure, relative_width="95", src="''figures/srac-as-es-application''"]
\<open> Using a "SRAC" as "EC" document element. \<close>
text\<open> The subsequent sample in @{figure \<open>figfig5\<close>} shows the definition of an
\<open> Using a \<^typ>\<open>SRAC\<close> as \<^typ>\<open>EC\<close> document element. \<close>
text\<open> The subsequent sample in @{figure \<open>figfig5\<close>} shows the definition of a
\<^emph>\<open>safety-related application condition\<close>, a side-condition of a theorem which
has the consequence that a certain calculation must be executed sufficiently fast on an embedded
device. This condition can not be established inside the formal theory but has to be
checked by system integration tests. Now we reference in @{figure \<open>figfig7\<close>} this
safety-related condition; however, this happens in a context where general \<^emph>\<open>exported constraints\<close>
are listed. \<^isadof>'s checks establish that this is legal in the given ontology.
are listed. \<^isadof>'s checks and establishes that this is legal in the given ontology.
\<close>
section*[tech_onto::example]\<open>Writing Technical Reports in \<^boxed_theory_text>\<open>technical_report\<close>\<close>
text\<open>While it is perfectly possible to write documents in the
\<^boxed_theory_text>\<open>technical_report\<close> ontology in freeform-style (the present manual is mostly an
\<^verbatim>\<open>technical_report\<close> ontology in freeform-style (the present manual is mostly an
example for this category), we will briefly explain here the tight-checking-style in which
most Isabelle reference manuals themselves are written.
@ -663,15 +674,15 @@ The idea has already been put forward by Isabelle itself; besides the general in
which this work is also based, current Isabelle versions provide around 20 built-in
document and code antiquotations described in the Reference Manual pp.75 ff. in great detail.
Most of them provide strict-checking, \<^ie> the argument strings where parsed and machine-checked in the
Most of them provide strict-checking, \<^ie> the argument strings were parsed and machine-checked in the
underlying logical context, which turns the arguments into \<^emph>\<open>formal content\<close> in the integrated
source, in contrast to the free-form antiquotations which basically influence the presentation.
We still mention a few of these document antiquotations here:
\<^item> \<^theory_text>\<open>@{thm \<open>refl\<close>}\<close> or \<^theory_text>\<open>@{thm [display] \<open>refl\<close>}\<close> check that \<^theory_text>\<open>refl\<close> is indeed a reference
to a theorem; the additional "style" argument changes the presentation by printing the
to a theorem; the additional ``style" argument changes the presentation by printing the
formula into the output instead of the reference itself,
\<^item> \<^theory_text>\<open>@{lemma \<open>prop\<close> } by \<open>method\<close>\<close> allows to derive \<open>prop\<close> on the fly, thus garantee
\<^item> \<^theory_text>\<open>@{lemma \<open>prop\<close> } by \<open>method\<close>\<close> allows deriving \<open>prop\<close> on the fly, thus guarantee
that it is a corrollary of the current context,
\<^item> \<^theory_text>\<open>@{term \<open>term\<close> }\<close> parses and type-checks \<open>term\<close>,
\<^item> \<^theory_text>\<open>@{value \<open>term\<close> }\<close> performs the evaluation of \<open>term\<close>,
@ -702,12 +713,13 @@ figure*[strict_SS::figure, relative_width="95", src="''figures/MyCommentedIsabel
\<open>A table with a number of SML functions, together with their type.\<close>
text\<open>
\<open>TR_MyCommentedIsabelle\<close> is written according to the @{theory "Isabelle_DOF.technical_report"}
ontology. \<^figure>\<open>strict_SS\<close> shows a snippet from this integrated source and gives an idea why
\<open>TR_MyCommentedIsabelle\<close> is written according to the \<^verbatim>\<open>technical_report\<close> ontology in
\<^theory>\<open>Isabelle_DOF.technical_report\<close>.
\<^figure>\<open>strict_SS\<close> shows a snippet from this integrated source and gives an idea why
its tight-checking allows for keeping track of underlying Isabelle changes:
Any reference to an SML operation in some library module is type-checked, and the displayed
SML-type really corresponds to the type of the operations in the underlying SML environment.
In the pdf output, these text-fragments were displayed verbatim.
In the \<^pdf> output, these text-fragments were displayed verbatim.
\<close>
@ -732,21 +744,21 @@ text\<open> This is *\<open>emphasized\<close> and this is a
\<close>}
Clearly, this is not always possible and, in fact, often \<^isadof> documents will contain
\<^LaTeX>-commands, this should be restricted to layout improvements that otherwise are (currently)
\<^LaTeX>-commands, but this should be restricted to layout improvements that otherwise are (currently)
not possible. As far as possible, the use of \<^LaTeX>-commands should be restricted to the definition
of ontologies and document templates (see @{docitem (unchecked) \<open>isadof_ontologies\<close>}).
Restricting the use of \<^LaTeX> has two advantages: first, \<^LaTeX> commands can circumvent the
consistency checks of \<^isadof> and, hence, only if no \<^LaTeX> commands are used, \<^isadof> can
ensure that a document that does not generate any error messages in Isabelle/jedit also generated
a PDF document. Second, future version of \<^isadof> might support different targets for the
ensure that a document that does not generate any error messages in Isabelle/jEdit also generated
a \<^pdf> document. Second, future version of \<^isadof> might support different targets for the
document generation (\<^eg>, HTML) which, naturally, are only available to documents not using
too complex native \<^LaTeX>-commands.
Similarly, (unchecked) forward references should, if possible, be avoided, as they also might
create dangling references during the document generation that break the document generation.
Finally, we recommend to use the @{command "check_doc_global"} command at the end of your
Finally, we recommend using the @{command "check_doc_global"} command at the end of your
document to check the global reference structure.
\<close>

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

File diff suppressed because it is too large Load Diff

67
examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy
View File

@ -1,7 +1,7 @@
(*************************************************************************
* Copyright (C)
* 2019-2021 University of Exeter
* 2018-2021 University of Paris-Saclay
* 2019-2022 University of Exeter
* 2018-2022 University of Paris-Saclay
* 2018 The University of Sheffield
*
* License:
@ -22,12 +22,12 @@ chapter*[isadof_developers::text_section]\<open>Extending \<^isadof>\<close>
text\<open>
In this chapter, we describe the basic implementation aspects of \<^isadof>, which is based on
the following design-decisions:
\<^item> the entire \<^isadof> is a ``pure add-on,'' \<^ie>, we deliberately resign on the possibility to
modify Isabelle itself.
\<^item> the entire \<^isadof> is a ``pure add-on,'' \<^ie>, we deliberately resign the possibility to
modify Isabelle itself,
\<^item> we made a small exception to this rule: the \<^isadof> package modifies in its installation
about 10 lines in the \LaTeX-generator (\path{src/patches/thy_output.ML}).
about 10 lines in the \LaTeX-generator (\path{src/patches/thy_output.ML}),
\<^item> we decided to make the markup-generation by itself to adapt it as well as possible to the
needs of tracking the linking in documents.
needs of tracking the linking in documents,
\<^item> \<^isadof> is deeply integrated into the Isabelle's IDE (PIDE) to give immediate feedback during
editing and other forms of document evolution.
\<close>
@ -57,8 +57,9 @@ text\<open>
fun merge((d1,c1,...),(d2,c2,...)) = (merge_docobj_tab (d1,d2,...),
merge_docclass_tab(c1,c2,...))
);\<close>}
where the table \<^boxed_sml>\<open>docobj_tab\<close> manages document classes and \<^boxed_sml>\<open>docclass_tab\<close> the
environment for class definitions (inducing the inheritance relation). Other tables capture, \eg,
where the table \<^boxed_sml>\<open>docobj_tab\<close> manages document class instances
and \<^boxed_sml>\<open>docclass_tab\<close> the environment for class definitions
(inducing the inheritance relation). Other tables capture, \eg,
the class invariants, inner-syntax antiquotations. Operations follow the MVC-pattern, where
Isabelle/Isar provides the controller part. A typical model operation has the type:
@ -75,7 +76,7 @@ in (Data.map(apfst decl)(ctxt)
handle Symtab.DUP _ =>
error("multiple declaration of document reference"))
end\<close>}
where \<^boxed_theory_text>\<open>Data.map\<close> is the update function resulting from the instantiation of the
where \<^boxed_sml>\<open>Data.map\<close> is the update function resulting from the instantiation of the
functor \<^boxed_sml>\<open>Generic_Data\<close>. This code fragment uses operations from a library structure
\<^boxed_sml>\<open>Symtab\<close> that were used to update the appropriate table for document objects in
the plugin-local state. Possible exceptions to the update operation were mapped to a system-global
@ -91,7 +92,7 @@ op >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c
op option : ('a -> 'b * 'a) -> 'a -> 'b option * 'a
op repeat : ('a -> 'b * 'a) -> 'a -> 'b list * 'a \<close>}
for alternative, sequence, and piping, as well as combinators for option and repeat. Parsing
combinators have the advantage that they can be smoothlessly integrated into standard programs,
combinators have the advantage that they can be integrated into standard programs,
and they enable the dynamic extension of the grammar. There is a more high-level structure
\inlinesml{Parse} providing specific combinators for the command-language Isar:
@ -106,7 +107,7 @@ val attributes =(Parse.$$$ "[" |-- (reference
|--(Parse.enum ","attribute)))[]))--| Parse.$$$ "]"
\end{sml}
The ``model'' \<^boxed_theory_text>\<open>declare_reference_opn\<close> and ``new'' \<^boxed_theory_text>\<open>attributes\<close> parts were
The ``model'' \<^boxed_sml>\<open>declare_reference_opn\<close> and ``new'' \<^boxed_sml>\<open>attributes\<close> parts were
combined via the piping operator and registered in the Isar toplevel:
@{boxed_sml [display]
@ -141,30 +142,31 @@ text\<open>
(docitem_antiq_gen default_cid) #>
ML_Antiquotation.inline <@>{binding docitem_value}
ML_antiq_docitem_value)\<close>}
the text antiquotation \<^boxed_theory_text>\<open>docitem\<close> is declared and bounded to a parser for the argument
the text antiquotation \<^boxed_sml>\<open>docitem\<close> is declared and bounded to a parser for the argument
syntax and the overall semantics. This code defines a generic antiquotation to be used in text
elements such as
@{boxed_theory_text [display]\<open>
text\<open>as defined in <@>{docitem \<open>d1\<close>} ...\<close>
text\<open>as defined in @{docitem \<open>d1\<close>} ...\<close>
\<close>}
The subsequent registration \<^boxed_theory_text>\<open>docitem_value\<close> binds code to a ML-antiquotation usable
The subsequent registration \<^boxed_sml>\<open>docitem_value\<close> binds code to a ML-antiquotation usable
in an ML context for user-defined extensions; it permits the access to the current ``value''
of document element, \ie; a term with the entire update history.
of document element, \<^ie>, a term with the entire update history.
It is possible to generate antiquotations \emph{dynamically}, as a consequence of a class
definition in ODL. The processing of the ODL class \<^boxed_theory_text>\<open>definition\<close> also \emph{generates}
a text antiquotation \<^boxed_theory_text>\<open>@{definition \<open>d1\<close>}\<close>, which works similar to
definition in ODL. The processing of the ODL class \<^typ>\<open>definition\<close> also \emph{generates}
a text antiquotation \<^boxed_theory_text>\<open>@{"definition" \<open>d1\<close>}\<close>, which works similar to
\<^boxed_theory_text>\<open>@{docitem \<open>d1\<close>}\<close> except for an additional type-check that assures that
\<^boxed_theory_text>\<open>d1\<close> is a reference to a definition. These type-checks support the subclass hierarchy.
\<close>
section\<open>Implementing Second-level Type-Checking\<close>
text\<open>
On expressions for attribute values, for which we chose to use HOL syntax to avoid that users
need to learn another syntax, we implemented an own pass over type-checked terms. Stored in the
late-binding table \<^boxed_theory_text>\<open>ISA_transformer_tab\<close>, we register for each inner-syntax-annotation
late-binding table \<^boxed_sml>\<open>ISA_transformer_tab\<close>, we register for each inner-syntax-annotation
(ISA's), a function of type
@{boxed_sml [display]
@ -184,28 +186,31 @@ text\<open>
\<close>
section\<open>Implementing Monitors\<close>
text\<open>
Since monitor-clauses have a regular expression syntax, it is natural to implement them as
deterministic automata. These are stored in the \<^boxed_theory_text>\<open>docobj_tab\<close> for monitor-objects
deterministic automata. These are stored in the \<^boxed_sml>\<open>docobj_tab\<close> for monitor-objects
in the \<^isadof> component. We implemented the functions:
@{boxed_sml [display]
\<open> val enabled : automaton -> env -> cid list
val next : automaton -> env -> cid -> automaton\<close>}
where \<^boxed_theory_text>\<open>env\<close> is basically a map between internal automaton states and class-id's
(\<^boxed_theory_text>\<open>cid\<close>'s). An automaton is said to be \<^emph>\<open>enabled\<close> for a class-id,
where \<^boxed_sml>\<open>env\<close> is basically a map between internal automaton states and class-id's
(\<^boxed_sml>\<open>cid\<close>'s). An automaton is said to be \<^emph>\<open>enabled\<close> for a class-id,
iff it either occurs in its accept-set or its reject-set (see @{docitem "sec:monitors"}). During
top-down document validation, whenever a text-element is encountered, it is checked if a monitor
is \emph{enabled} for this class; in this case, the \<^boxed_theory_text>\<open>next\<close>-operation is executed. The
transformed automaton recognizing the rest-language is stored in \<^boxed_theory_text>\<open>docobj_tab\<close> if
possible; otherwise, if \<^boxed_theory_text>\<open>next\<close> fails, an error is reported. The automata implementation
is \emph{enabled} for this class; in this case, the \<^boxed_sml>\<open>next\<close>-operation is executed. The
transformed automaton recognizing the rest-language is stored in \<^boxed_sml>\<open>docobj_tab\<close> if
possible;
% TODO: clarify the notion of rest-language
otherwise, if \<^boxed_sml>\<open>next\<close> fails, an error is reported. The automata implementation
is, in large parts, generated from a formalization of functional automata~\cite{nipkow.ea:functional-Automata-afp:2004}.
\<close>
section\<open>The \LaTeX-Core of \<^isadof>\<close>
section\<open>The \<^LaTeX>-Core of \<^isadof>\<close>
text\<open>
The \LaTeX-implementation of \<^isadof> heavily relies on the
``keycommand''~@{cite "chervet:keycommand:2010"} package. In fact, the core \<^isadof> \LaTeX-commands
The \<^LaTeX>-implementation of \<^isadof> heavily relies on the
``keycommand''~@{cite "chervet:keycommand:2010"} package. In fact, the core \<^isadof> \<^LaTeX>-commands
are just wrappers for the corresponding commands from the keycommand package:
@{boxed_latex [display]
@ -216,9 +221,9 @@ text\<open>
\newcommand\provideisadof[1]{%
\expandafter\providekeycommand\csname isaDof.#1\endcsname}%\<close>}
The \LaTeX-generator of \<^isadof> maps each \<^boxed_theory_text>\<open>doc_item\<close> to an \LaTeX-environment (recall
@{docitem "text-elements"}). As generic \<^boxed_theory_text>\<open>doc_item\<close> are derived from the text element,
the enviornment \inlineltx|{isamarkuptext*}| builds the core of \<^isadof>'s \LaTeX{} implementation.
The \<^LaTeX>-generator of \<^isadof> maps each \<^boxed_theory_text>\<open>doc_item\<close> to an \<^LaTeX>-environment (recall
@{docitem "text-elements"}). As generic \<^boxed_theory_text>\<open>doc_item\<close>s are derived from the text element,
the environment \inlineltx|isamarkuptext*| builds the core of \<^isadof>'s \<^LaTeX> implementation.
For example, the @{docitem "ass123"} from page \pageref{ass123} is mapped to
@{boxed_latex [display]
@ -231,7 +236,7 @@ text\<open>
times ...
\end{isamarkuptext*}\<close>}
This environment is mapped to a plain \LaTeX command via (again, recall @{docitem "text-elements"}):
This environment is mapped to a plain \<^LaTeX> command via (again, recall @{docitem "text-elements"}):
@{boxed_latex [display]
\<open> \NewEnviron{isamarkuptext*}[1][]{\isaDof[env={text},#1]{\BODY}} \<close>}

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

@ -1,5 +1,6 @@
session "Isabelle_DOF-Manual" = "Isabelle_DOF" +
options [document = pdf, document_output = "output", quick_and_dirty = true]
options [document = pdf, document_output = "output", document_build = dof,
quick_and_dirty = true]
theories
"Isabelle_DOF-Manual"
document_files
@ -7,7 +8,6 @@ session "Isabelle_DOF-Manual" = "Isabelle_DOF" +
"root.bib"
"root.mst"
"preamble.tex"
"build"
"lstisadof-manual.sty"
"figures/antiquotations-PIDE.png"
"figures/cicm2018-combined.png"
@ -21,6 +21,7 @@ session "Isabelle_DOF-Manual" = "Isabelle_DOF" +
"figures/Dogfood-Intro.png"
"figures/Dogfood-IV-jumpInDocCLass.png"
"figures/Dogfood-V-attribute.png"
"figures/Dogfood-VI-linkappl.png"
"figures/isabelle-architecture.pdf"
"figures/isabelle-architecture.svg"
"figures/isadof.png"

46
examples/technical_report/Isabelle_DOF-Manual/document/build
View File

@ -1,46 +0,0 @@
#!/usr/bin/env bash
# Copyright (c) 2018-2019 The University of Sheffield. All rights reserved.
# 2018 The University of Paris-Saclay. All rights reserved.
#
# Redistribution and use in source and binary forms, with or without
# modification, are permitted provided that the following conditions
# are met:
# 1. Redistributions of source code must retain the above copyright
# notice, this list of conditions and the following disclaimer.
# 2. Redistributions in binary form must reproduce the above copyright
# notice, this list of conditions and the following disclaimer in
# the documentation and/or other materials provided with the
# distribution.
# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
# FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
# COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
# INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
# BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
# LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
# CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
# LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
# ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
# POSSIBILITY OF SUCH DAMAGE.
#
# SPDX-License-Identifier: BSD-2-Clause
set -e
if [ ! -f $ISABELLE_HOME_USER/DOF/document-template/build_lib.sh ]; then
echo ""
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/Isabelle_DOF/Isabelle_DOF"
echo "You can install the framework as follows:"
echo " cd Isabelle_DOF/document-generator"
echo " ./install"
echo ""
exit 1
fi
cp $ISABELLE_HOME_USER/DOF/document-template/build_lib.sh .
source build_lib.sh

BIN
examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-VI-linkappl.png Normal file
View File

Binary file not shown.
Side by Side

After

Width:  |  Height:  |  Size: 35 KiB

BIN
examples/technical_report/Isabelle_DOF-Manual/document/figures/antiquotations-PIDE.png
View File

Binary file not shown.
Side by Side Swipe Overlay

Before

Width:  |  Height:  |  Size: 96 KiB

After

Width:  |  Height:  |  Size: 43 KiB

BIN
examples/technical_report/Isabelle_DOF-Manual/document/figures/srac-as-es-application.png
View File

Binary file not shown.
Side by Side Swipe Overlay

Before

Width:  |  Height:  |  Size: 67 KiB

After

Width:  |  Height:  |  Size: 37 KiB

BIN
examples/technical_report/Isabelle_DOF-Manual/document/figures/srac-definition.png
View File

Binary file not shown.
Side by Side Swipe Overlay

Before

Width:  |  Height:  |  Size: 50 KiB

After

Width:  |  Height:  |  Size: 26 KiB

2
examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex
View File

@ -21,7 +21,7 @@
\usepackage{xcolor}
\usepackage{lstisadof-manual}
\usepackage{xspace}
\usepackage{dtk-logos}
\IfFileExists{hvlogos.sty}{\usepackage{hvlogos}}{\newcommand{\TeXLive}{\TeX Live}\newcommand{\BibTeX}{Bib\TeX}}
\usepackage{railsetup}
\setcounter{secnumdepth}{2}
\usepackage{index}

4
examples/technical_report/TR_my_commented_isabelle/ROOT
View File

@ -1,5 +1,6 @@
session "TR_MyCommentedIsabelle" = "Isabelle_DOF" +
options [document = pdf, document_output = "output",quick_and_dirty = true]
options [document = pdf, document_output = "output", document_build = dof,
quick_and_dirty = true]
theories
"TR_MyCommentedIsabelle"
document_files
@ -7,7 +8,6 @@ session "TR_MyCommentedIsabelle" = "Isabelle_DOF" +
"isadof.cfg"
"preamble.tex"
"prooftree.sty"
"build"
"figures/markup-demo.png"
"figures/text-element.pdf"
"figures/isabelle-architecture.pdf"

182
examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy
View File

@ -612,32 +612,36 @@ subsection\<open>More operations on types\<close>
text\<open>
\<^item> \<^ML>\<open>Term_Subst.map_types_same : (typ -> typ) -> term -> term\<close>
\<^item> \<^ML>\<open>Term_Subst.map_aterms_same : (term -> term) -> term -> term\<close>
\<^item> \<^ML>\<open>Term_Subst.instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list
-> term -> term\<close>
\<^item> \<^ML>\<open>Term_Subst.instantiateT: ((indexname * sort) * typ) list -> typ -> typ\<close>
\<^item> \<^ML>\<open>Term_Subst.generalizeT: string list -> int -> typ -> typ\<close>
\<^item> \<^ML>\<open>Term_Subst.instantiate: typ TVars.table * term Vars.table -> term -> term\<close>
\<^item> \<^ML>\<open>Term_Subst.instantiateT: typ TVars.table -> typ -> typ\<close>
\<^item> \<^ML>\<open>Term_Subst.generalizeT: Names.set -> int -> typ -> typ\<close>
this is the standard type generalisation function !!!
only type-frees in the string-list were taken into account.
\<^item> \<^ML>\<open>Term_Subst.generalize: string list * string list -> int -> term -> term\<close>
\<^item> \<^ML>\<open>Term_Subst.generalize: Names.set * Names.set -> int -> term -> term\<close>
this is the standard term generalisation function !!!
only type-frees and frees in the string-lists were taken
into account.
\<close>
text \<open>Apparently, a bizarre conversion between the old-style interface and
the new-style \<^ML>\<open>tyenv\<close> is necessary. See the following example.\<close>
ML\<open>
val S = Vartab.dest tyenv;
val S = Vartab.dest tyenv : (Vartab.key * (sort * typ)) list;
val S' = (map (fn (s,(t,u)) => ((s,t),u)) S) : ((indexname * sort) * typ) list;
(* it took me quite some time to find out that these two type representations,
obscured by a number of type-synonyms, where actually identical. *)
val S''= TVars.make S': typ TVars.table
val ty = t_schematic;
val ty' = Term_Subst.instantiateT S' t_schematic;
val ty' = Term_Subst.instantiateT S'' t_schematic;
(* Don't know how to build a typ TVars.table *)
val t = (generalize_term @{term "[]"});
val t' = Term_Subst.map_types_same (Term_Subst.instantiateT S') (t)
val t' = Term_Subst.map_types_same (Term_Subst.instantiateT (TVars.make S')) (t)
(* or alternatively : *)
val t'' = Term.map_types (Term_Subst.instantiateT S') (t)
val t'' = Term.map_types (Term_Subst.instantiateT S'') (t)
\<close>
text\<open>A more abstract env for variable management in tactic proofs. A bit difficult to use
@ -794,11 +798,11 @@ text\<open> We come now to the very heart of the LCF-Kernel of Isabelle, which
\<^item> \<^ML>\<open> Thm.forall_intr: cterm -> thm -> thm\<close>
\<^item> \<^ML>\<open> Thm.forall_elim: cterm -> thm -> thm\<close>
\<^item> \<^ML>\<open> Thm.transfer : theory -> thm -> thm\<close>
\<^item> \<^ML>\<open> Thm.generalize: string list * string list -> int -> thm -> thm\<close>
\<^item> \<^ML>\<open> Thm.instantiate: ((indexname*sort)*ctyp)list * ((indexname*typ)*cterm) list -> thm -> thm\<close>
\<^item> \<^ML>\<open> Thm.generalize: Names.set * Names.set -> int -> thm -> thm\<close>
\<^item> \<^ML>\<open> Thm.instantiate: ctyp TVars.table * cterm Vars.table -> thm -> thm\<close>
\<close>
text\<open> They reflect the Pure logic depicted in a number of presentations such as
text\<open> They reflect the Pure logic depicted in a number of presentations such as
M. Wenzel, \<^emph>\<open>Parallel Proof Checking in Isabelle/Isar\<close>, PLMMS 2009, or simiular papers.
Notated as logical inference rules, these operations were presented as follows:
\<close>
@ -909,14 +913,10 @@ high-level component (more low-level components such as \<^ML>\<open>Global_Theo
exist) for definitions and axiomatizations is here:
\<close>
text\<open>
\<^item> \<^ML>\<open>Specification.definition: (binding * typ option * mixfix) option ->
(binding * typ option * mixfix) list -> term list -> Attrib.binding * term ->
local_theory -> (term * (string * thm)) * local_theory\<close>
\<^item> \<^ML>\<open>Specification.definition': (binding * typ option * mixfix) option ->
(binding * typ option * mixfix) list -> term list -> Attrib.binding * term ->
bool -> local_theory -> (term * (string * thm)) * local_theory\<close>
\<^item> \<^ML>\<open>Specification.definition_cmd: (binding * string option * mixfix) option ->
(binding * string option * mixfix) list -> string list -> Attrib.binding * string ->
bool -> local_theory -> (term * (string * thm)) * local_theory\<close>
@ -959,8 +959,8 @@ fun mk_def name p =
val ty_global = ty --> ty
val args = (((SOME(nameb,SOME ty_global,NoSyn),(Binding.empty_atts,term_prop)),[]),[])
val cmd = (fn (((decl, spec), prems), params) =>
#2 oo Specification.definition' decl params prems spec)
in cmd args true
#2 o Specification.definition decl params prems spec)
in cmd args
end;
in Named_Target.theory_map (mk_def "I" @{here} )
end\<close>
@ -1186,8 +1186,8 @@ text\<open> The extensibility of Isabelle as a system framework depends on a num
\<^item> \<^ML>\<open>Toplevel.theory': (bool -> theory -> theory) -> Toplevel.transition -> Toplevel.transition\<close>
\<^item> \<^ML>\<open>Toplevel.exit: Toplevel.transition -> Toplevel.transition\<close>
\<^item> \<^ML>\<open>Toplevel.ignored: Position.T -> Toplevel.transition\<close>
\<^item> \<^ML>\<open>Toplevel.present_local_theory: (xstring * Position.T) option ->
(Toplevel.state -> unit) -> Toplevel.transition -> Toplevel.transition\<close>
\<^item> \<^ML>\<open>Toplevel.present_local_theory: (xstring * Position.T) option ->
(Toplevel.state -> Latex.text) -> Toplevel.transition -> Toplevel.transition\<close>
\<close>
subsection*[cmdbinding::technical] \<open>Toplevel Transaction Management in the Isar-Engine\<close>
@ -1216,32 +1216,45 @@ text\<open>
text\<open>The file \<^file>\<open>~~/src/HOL/Examples/Commands.thy\<close> shows some example Isar command definitions, with the
all-important theory header declarations for outer syntax keywords.\<close>
text\<open>@{ML_structure Pure_Syn}\<close>
subsubsection*[ex1137::example]\<open>Examples: \<^theory_text>\<open>text\<close>\<close>
text\<open> The integration of the \<^theory_text>\<open>text\<close>-command is done as follows:
@{ML [display]\<open>
Outer_Syntax.command ("text", @{here}) "formal comment (primary style)"
(Parse.opt_target -- Parse.document_source >> Pure_Syn.document_command {markdown = true})
(Parse.opt_target -- Parse.document_source >> Document_Output.document_output
{markdown = true, markup = I})
\<close>}
where \<^ML>\<open>Pure_Syn.document_command\<close> is the defining operation for the
"diagnostic" (=side-effect-free) toplevel operation. \<^ML>\<open>Pure_Syn.document_command\<close> looks as follows:
where \<^ML>\<open>Document_Output.document_output\<close> is the defining operation for the
"diagnostic" (=side-effect-free) toplevel operation.
\<^ML>\<open>Document_Output.document_output\<close> looks as follows:
@{ML [display]\<open> let fun output_document state markdown txt =
Thy_Output.output_document (Toplevel.presentation_context state) markdown txt
fun document_command markdown (loc, txt) =
Toplevel.keep (fn state =>
(case loc of
NONE => ignore (output_document state markdown txt)
| SOME (_, pos) =>
error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o
Toplevel.present_local_theory loc (fn state =>
ignore (output_document state markdown txt)) in () end
@{ML [display]\<open>let fun document_reports txt =
let val pos = Input.pos_of txt in
[(pos, Markup.language_document (Input.is_delimited txt)),
(pos, Markup.plain_text)]
end;
fun document_output {markdown, markup} (loc, txt) =
let
fun output st =
let
val ctxt = Toplevel.presentation_context st;
val _ = Context_Position.reports ctxt (document_reports txt);
in txt |> Document_Output.output_document ctxt {markdown = markdown} |> markup end;
in
Toplevel.present (fn st =>
(case loc of
NONE => output st
| SOME (_, pos) =>
error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o
Toplevel.present_local_theory loc output
end in () end
\<close>}
\<close>
subsubsection*[ex1138::example]\<open>Examples: \<^theory_text>\<open>ML\<close>\<close>
text\<open>
@ -1316,10 +1329,12 @@ subsection*[ex213::example]\<open>A Definition Command (High-level)\<close>
text\<open>A quite complex example is drawn from the Theory \<^verbatim>\<open>Clean\<close>; it generates \<close>
ML\<open>Specification.definition\<close>
ML\<open>
structure HLDefinitionSample =
struct
fun cmd (decl, spec, prems, params) = #2 oo Specification.definition' decl params prems spec
fun cmd (decl, spec, prems, params) = #2 o Specification.definition decl params prems spec
fun MON_SE_T res state = state --> optionT(HOLogic.mk_prodT(res,state));
@ -1340,7 +1355,7 @@ fun mk_push_def binding sty lthy =
val eq = push_eq binding (Binding.name_of name) rty sty lthy
val mty = MON_SE_T rty sty
val args = (SOME(name, SOME mty, NoSyn), (Binding.empty_atts,eq),[],[])
in cmd args true lthy end;
in cmd args lthy end;
val define_test = Named_Target.theory_map (mk_push_def (Binding.name "test") @{typ "'a"})
@ -1536,6 +1551,7 @@ text\<open>The structures @{ML_structure Markup} and @{ML_structure Properties}
from \<^theory_text>\<open>Isabelle_DOF\<close>. A markup must be tagged with an id; this is done by the @{ML serial}-function
discussed earlier. Markup operations were used for hyperlinking applications to binding
occurrences, info for hovering, infos for type ... \<close>
ML\<open>
(* Position.report is also a type consisting of a pair of a position and markup. *)
(* It would solve all my problems if I find a way to infer the defining Position.report
@ -1551,20 +1567,18 @@ Markup.enclose : Markup.T -> string -> string;
(* example for setting a link, the def flag controls if it is a defining or a binding
occurence of an item *)
fun theory_markup (def:bool) (name:string) (id:serial) (pos:Position.T) =
if id = 0 then Markup.empty
else
Markup.properties (Position.entity_properties_of def id pos)
(Markup.entity Markup.theoryN name);
Markup.theoryN : string;
fun theory_markup refN (def:bool) (name:string) (id:serial) (pos:Position.T) =
if id = 0 then Markup.empty
else Position.make_entity_markup {def = def} id refN (name, pos);
serial(); (* A global, lock-guarded serial counter used to produce unique identifiers,
be it on the level of thy-internal states or as reference in markup in
PIDE *)
\<close>
subsection\<open>A simple Example\<close>
ML\<open>
local
@ -1573,10 +1587,7 @@ val docclassN = "doc_class";
(* derived from: theory_markup; def for "defining occurrence" (true) in contrast to
"referring occurence" (false). *)
fun docclass_markup def name id pos =
if id = 0 then Markup.empty
else Markup.properties (Position.entity_properties_of def id pos)
(Markup.entity docclassN name);
val docclass_markup = theory_markup docclassN
in
@ -1602,14 +1613,16 @@ fun markup_tvar def_name ps (name, id) =
let
fun markup_elem name = (name, (name, []): Markup.T);
val (tvarN, tvar) = markup_elem ((case def_name of SOME name => name | _ => "") ^ "'s nickname is");
val entity = Markup.entity tvarN name
val entity = Markup.entity tvarN name (* ??? *)
val def = def_name = NONE
in
tvar ::
(if def then I else cons (Markup.keyword_properties Markup.ML_keyword3))
(map (fn pos => Markup.properties (Position.entity_properties_of def id pos) entity) ps)
(map (fn pos => Position.make_entity_markup {def = def} id tvarN (name, pos) ) ps)
end
(* Position.make_entity_markup {def = def} id refN (name, pos) *)
fun report [] _ _ = I
| report ps markup x =
let val ms = markup x
@ -1856,11 +1869,6 @@ Common Isar Syntax
Common Isar Syntax
\<^item>\<^ML>\<open>Args.embedded_token : Token.T parser\<close>
\<^item>\<^ML>\<open>Args.embedded_inner_syntax: string parser\<close>
\<^item>\<^ML>\<open>Args.embedded_input : Input.source parser\<close>
\<^item>\<^ML>\<open>Args.embedded : string parser\<close>
\<^item>\<^ML>\<open>Args.embedded_position: (string * Position.T) parser\<close>
\<^item>\<^ML>\<open>Args.text_input: Input.source parser\<close>
\<^item>\<^ML>\<open>Args.text : string parser\<close>
\<^item>\<^ML>\<open>Args.binding : Binding.binding parser\<close>
@ -2058,6 +2066,10 @@ text\<open>
(*
Document_Antiquotation
*)
subsection*[ex33::example] \<open>Example\<close>
ML\<open>
@ -2070,10 +2082,10 @@ ML\<open>
(* Here is the code to register the above parsers as text antiquotations into the Isabelle
Framework: *)
Thy_Output.antiquotation_pretty_source \<^binding>\<open>theory\<close>
(Scan.lift (Parse.position Args.embedded));
Document_Output.antiquotation_pretty_source \<^binding>\<open>theory\<close>
(Scan.lift (Parse.position Parse.embedded));
Thy_Output.antiquotation_raw \<^binding>\<open>file\<close>
Document_Output.antiquotation_raw \<^binding>\<open>file\<close>
(Scan.lift (Parse.position Parse.path)) ;
\<close>
@ -2084,7 +2096,7 @@ text\<open>where we have the registration of the action
transaction that, of course, has the type \<^ML_type>\<open>theory -> theory\<close> :
@{ML [display] \<open>
(fn name => (Thy_Output.antiquotation_pretty_source
(fn name => (Document_Output.antiquotation_pretty_source
name
(Scan.lift (Parse.position Args.cartouche_input))))
: binding ->
@ -2104,7 +2116,7 @@ ML\<open> Output.output "bla_1:" \<close>
text\<open>It provides a number of hooks that can be used for redirection hacks ...\<close>
section \<open> Output: LaTeX \<close>
text\<open>The heart of the LaTeX generator is to be found in the structure \<^ML_structure>\<open>Thy_Output\<close>.
text\<open>The heart of the LaTeX generator is to be found in the structure \<^ML_structure>\<open>Document_Output\<close>.
This is an own parsing and writing process, with the risc that a parsed file in the IDE parsing
process can not be parsed for the LaTeX Generator. The reason is twofold:
@ -2120,60 +2132,52 @@ Since Isabelle2018, an own AST is provided for the LaTeX syntax, analogously to
\<^item>\<^ML>\<open>Latex.string: string -> Latex.text\<close>
\<^item>\<^ML>\<open>Latex.text: string * Position.T -> Latex.text\<close>
\<^item>\<^ML>\<open>Latex.output_text: Latex.text list -> string\<close>
\<^item>\<^ML>\<open>Latex.output_positions: Position.T -> Latex.text list -> string\<close>
\<^item>\<^ML>\<open>Latex.output_name: string -> string\<close>
\<^item>\<^ML>\<open>Latex.output_ascii: string -> string\<close>
\<^item>\<^ML>\<open>Latex.output_symbols: Symbol.symbol list -> string\<close>
\<^item>\<^ML>\<open>Latex.begin_delim: string -> string\<close>
\<^item>\<^ML>\<open>Latex.end_delim: string -> string\<close>
\<^item>\<^ML>\<open>Latex.begin_tag: string -> string\<close>
\<^item>\<^ML>\<open>Latex.end_tag: string -> string\<close>
\<^item>\<^ML>\<open>Latex.environment_block: string -> Latex.text list -> Latex.text\<close>
\<^item>\<^ML>\<open>Latex.environment: string -> string -> string\<close>
\<^item>\<^ML>\<open>Latex.block: Latex.text list -> Latex.text\<close>
\<^item>\<^ML>\<open>Latex.enclose_body: string -> string -> Latex.text list -> Latex.text list\<close>
\<^item>\<^ML>\<open>Latex.enclose_block: string -> string -> Latex.text list -> Latex.text\<close>
\<^item>\<^ML>\<open>Latex.environment: string -> Latex.text -> Latex.text\<close>
\<^item>\<^ML>\<open>Latex.block: Latex.text -> XML.tree\<close>
\<close>
ML\<open> Latex.output_ascii;
Latex.environment "isa" "bg";
Latex.environment "isa" (Latex.string "bg");
Latex.output_ascii "a_b:c'é";
(* Note: *)
space_implode "sd &e sf dfg" ["qs","er","alpa"];
\<close>
text\<open>Here is an abstract of the main interface to @{ML_structure Thy_Output}:\<close>
text\<open>Here is an abstract of the main interface to @{ML_structure Document_Output}:\<close>
text\<open>
\<^item>\<^ML>\<open>Thy_Output.output_document: Proof.context -> {markdown: bool} -> Input.source -> Latex.text list\<close>
\<^item>\<^ML>\<open>Thy_Output.output_token: Proof.context -> Token.T -> Latex.text list\<close>
\<^item>\<^ML>\<open>Thy_Output.output_source: Proof.context -> string -> Latex.text list\<close>
\<^item>\<^ML>\<open>Thy_Output.present_thy: Options.T -> theory -> Thy_Output.segment list -> Latex.text list\<close>
\<^item>\<^ML>\<open>Document_Output.output_document: Proof.context -> {markdown: bool} -> Input.source -> Latex.text \<close>
\<^item>\<^ML>\<open>Document_Output.output_token: Proof.context -> Token.T -> Latex.text \<close>
\<^item>\<^ML>\<open>Document_Output.output_source: Proof.context -> string -> Latex.text \<close>
\<^item>\<^ML>\<open>Document_Output.present_thy: Options.T -> theory -> Document_Output.segment list -> Latex.text \<close>
\<^item>\<^ML>\<open>Thy_Output.isabelle: Proof.context -> Latex.text list -> Latex.text\<close>
\<^item>\<^ML>\<open>Thy_Output.isabelle_typewriter: Proof.context -> Latex.text list -> Latex.text\<close>
\<^item>\<^ML>\<open>Thy_Output.typewriter: Proof.context -> string -> Latex.text\<close>
\<^item>\<^ML>\<open>Thy_Output.verbatim: Proof.context -> string -> Latex.text\<close>
\<^item>\<^ML>\<open>Thy_Output.source: Proof.context -> {embedded: bool} -> Token.src -> Latex.text\<close>
\<^item>\<^ML>\<open>Thy_Output.pretty: Proof.context -> Pretty.T -> Latex.text\<close>
\<^item>\<^ML>\<open>Thy_Output.pretty_source: Proof.context -> {embedded: bool} -> Token.src -> Pretty.T -> Latex.text\<close>
\<^item>\<^ML>\<open>Thy_Output.pretty_items: Proof.context -> Pretty.T list -> Latex.text\<close>
\<^item>\<^ML>\<open>Thy_Output.pretty_items_source: Proof.context -> {embedded: bool} -> Token.src -> Pretty.T list -> Latex.text\<close>
\<^item>\<^ML>\<open>Document_Output.isabelle: Proof.context -> Latex.text -> Latex.text\<close>
\<^item>\<^ML>\<open>Document_Output.isabelle_typewriter: Proof.context -> Latex.text -> Latex.text\<close>
\<^item>\<^ML>\<open>Document_Output.typewriter: Proof.context -> string -> Latex.text\<close>
\<^item>\<^ML>\<open>Document_Output.verbatim: Proof.context -> string -> Latex.text\<close>
\<^item>\<^ML>\<open>Document_Output.source: Proof.context -> {embedded: bool} -> Token.src -> Latex.text\<close>
\<^item>\<^ML>\<open>Document_Output.pretty: Proof.context -> Pretty.T -> Latex.text\<close>
\<^item>\<^ML>\<open>Document_Output.pretty_source: Proof.context -> {embedded: bool} -> Token.src -> Pretty.T -> Latex.text\<close>
\<^item>\<^ML>\<open>Document_Output.pretty_items: Proof.context -> Pretty.T list -> Latex.text\<close>
\<^item>\<^ML>\<open>Document_Output.pretty_items_source: Proof.context -> {embedded: bool} -> Token.src -> Pretty.T list -> Latex.text\<close>
Finally a number of antiquotation registries :
\<^item>\<^ML>\<open>Thy_Output.antiquotation_pretty:
\<^item>\<^ML>\<open>Document_Output.antiquotation_pretty:
binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory\<close>
\<^item>\<^ML>\<open>Thy_Output.antiquotation_pretty_source:
\<^item>\<^ML>\<open>Document_Output.antiquotation_pretty_source:
binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory\<close>
\<^item>\<^ML>\<open>Thy_Output.antiquotation_raw:
\<^item>\<^ML>\<open>Document_Output.antiquotation_raw:
binding -> 'a context_parser -> (Proof.context -> 'a -> Latex.text) -> theory -> theory\<close>
\<^item>\<^ML>\<open>Thy_Output.antiquotation_verbatim:
\<^item>\<^ML>\<open>Document_Output.antiquotation_verbatim:
binding -> 'a context_parser -> (Proof.context -> 'a -> string) -> theory -> theory\<close>
\<close>

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

@ -1,46 +0,0 @@
#!/usr/bin/env bash
# Copyright (c) 2018-2019 The University of Sheffield. All rights reserved.
# 2018 The University of Paris-Saclay. All rights reserved.
#
# Redistribution and use in source and binary forms, with or without
# modification, are permitted provided that the following conditions
# are met:
# 1. Redistributions of source code must retain the above copyright
# notice, this list of conditions and the following disclaimer.
# 2. Redistributions in binary form must reproduce the above copyright
# notice, this list of conditions and the following disclaimer in
# the documentation and/or other materials provided with the
# distribution.
# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
# FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
# COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
# INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
# BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
# LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
# CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
# LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
# ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
# POSSIBILITY OF SUCH DAMAGE.
#
# SPDX-License-Identifier: BSD-2-Clause
set -e
if [ ! -f $ISABELLE_HOME_USER/DOF/document-template/build_lib.sh ]; then
echo ""
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/Isabelle_DOF/Isabelle_DOF"
echo "You can install the framework as follows:"
echo " cd Isabelle_DOF/document-generator"
echo " ./install"
echo ""
exit 1
fi
cp $ISABELLE_HOME_USER/DOF/document-template/build_lib.sh .
source build_lib.sh

273
install
View File

@ -1,273 +0,0 @@
#!/usr/bin/env bash
# Copyright (c) 2018-2019 The University of Sheffield.
# 2019-2020 The University of Exeter.
# 2018-2020 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
#set -e
shopt -s nocasematch
# get global configuration
if [ -d .git ]; then
export `git show -s --format="COMMIT=%H DATE=%cd" --date=short | sed -e 's|-|/|g'`
fi
source .config
print_help()
{
echo "Usage: install [OPTION] "
echo ""
echo "Run ..."
echo ""
echo " --help, -h display this help message"
echo " --isabelle, -i isabelle isabelle command used for installation"
echo " (default: $ISABELLE)"
echo " --skip-patch-and-afp, -s skip installation of Isabelle/DOF patch for"
echo " Isabelle and required AFP entries. "
echo " USE AT YOUR OWN RISK (default: $SKIP)"
}
exit_error() {
echo ""
echo " *** Isabelle/DOF installation FAILED, please check the README.md for help ***"
echo ""
exit 1
}
check_isabelle_version() {
echo "* Checking Isabelle version:"
if [ "$ISABELLE_VERSION" != "$ACTUAL_ISABELLE_VERSION" ]; then
echo " WARNING:"
echo " The version of Isabelle (i.e., $ACTUAL_ISABELLE_VERSION) you are using"
echo " IS NOT SUPPORTED"
echo " by the current version of Isabelle/DOF. Please install a supported"
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
read -p " Still continue (y/N)? " -n 1 -r
echo
if [[ $REPLY =~ ^[Yy]$ ]];
then
echo " Continuing installation on your OWN risk."
else
exit_error
fi
else
echo " Success: found supported Isabelle version ($ISABELLE_VERSION)"
fi
}
check_afp_entries() {
echo "* Checking availability of AFP entries:"
missing=""
required="Regular-Sets Functional-Automata"
for afp in $required; do
res=`$ISABELLE build -n $afp 2>/dev/null || true`
if [ "$res" != "" ]; then
echo " Success: found APF entry $afp."
else
echo " Warning: could not find AFP entry $afp."
missing="$missing $afp"
fi
done
if [ "$missing" != "" ]; then
echo " Trying to install AFP (this might take a few *minutes*) ...."
extract=""
for e in $missing; do
extract="$extract $AFP_DATE/thys/$e"
done
mkdir -p .afp
if curl -s -L $AFP_URL | tar zxf - -C .afp $extract; then
for e in $missing; do
echo " Registering $e in $ISABELLE_HOME_USER/ROOTS"
touch $ISABELLE_HOME_USER/ROOTS
grep -q $PWD/.afp/$AFP_DATE/thys/$e $ISABELLE_HOME_USER/ROOTS || echo "$PWD/.afp/$AFP_DATE/thys/$e" >> $ISABELLE_HOME_USER/ROOTS
done
echo " AFP installation successful."
else
echo " FAILURE: could not find AFP entries: $missing."
echo " Please obtain the AFP from"
echo " $AFP_URL"
echo " and follow the following instructions:"
echo " https://www.isa-afp.org/using.html"
exit_error
fi
fi
}
check_isa_dof_patch() {
echo "* Check availability of Isabelle/DOF patch:"
src="src/patches/thy_output.ML"
dst="$ISABELLE_HOME/src/Pure/Thy/thy_output.ML"
if command -v cmp > /dev/null 2>&1 && cmp -s "$src" "$dst" ; then
echo " Success: latest Isabelle/DOF patch already applied"
if isabelle process -e 'Thy_Output.set_meta_args_parser' &> /dev/null ; then
true
else
echo " Warning: Isabelle/HOL needs to be rebuild to activate patch."
fi
else
command -v cmp >/dev/null 2>&1 || echo " Warning: cmp not available, cannot check if patch is already applied."
echo " Warning: Isabelle/DOF patch is not available or outdated."
echo " Trying to patch system ...."
if [ ! -f "$dst.backup-by-isadof-installer" ]; then
cp -f "$dst" "$dst.backup-by-isadof-installer" || true;
fi
if (cp -f $src $dst) &> /dev/null; then
echo " Applied patch successfully, Isabelle/HOL will be rebuilt during"
echo " the next start of Isabelle."
else
echo " FAILURE: Could not apply Isabelle/DOF patch."
echo " Please copy $src to $dst, e.g.:"
echo " cp -f $src $dst"
echo " and rebuild Isabelle/HOL."
exit_error
fi
fi
}
check_old_installation(){
echo "* Searching for existing installation:"
if [[ -d "$ISABELLE_HOME_USER/DOF" ]]; then
echo " Found old installation, moving it to $ISABELLE_HOME_USER/DOF.bak."
rm -rf "$ISABELLE_HOME_USER/DOF.bak"
mv "$ISABELLE_HOME_USER/DOF" "$ISABELLE_HOME_USER/DOF.bak"
else
echo " No old installation found."
fi
}
install_and_register(){
echo "* Installing Isabelle/DOF"
DIR="$ISABELLE_HOME_USER/DOF/Tools"
echo " - Installing Tools in $DIR"
mkdir -p "$DIR"
cp $GEN_DIR/Tools/* "$DIR"
chmod 755 "$DIR"/*
DIR="$ISABELLE_HOME_USER/DOF/document-template"
echo " - Installing document templates in $DIR"
mkdir -p "$DIR"
cp $GEN_DIR/scripts/* "$DIR"
cp $GEN_DIR/document-templates/* "$DIR"
cp $GEN_DIR/DOF/*/*.sty "$DIR"
cp $GEN_DIR/DOF/*/*.cls "$DIR"
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}|" \
"$DIR/DOF-core.sty"
DIR="$ISABELLE_HOME_USER/DOF/latex"
echo " - Installing LaTeX styles in $DIR"
mkdir -p "$DIR"
cp $GEN_DIR/ontologies/*/*.sty "$DIR"
DIR="$ISABELLE_HOME_USER/etc"
echo " - Registering Isabelle/DOF"
mkdir -p "$DIR"
if [[ $ISABELLE_TOOLS = *DOF* ]]; then
echo " * Tools already registered in $DIR/settings"
else
echo " * Registering tools in $DIR/settings"
echo 'ISABELLE_TOOLS=$ISABELLE_TOOLS:$ISABELLE_HOME_USER/DOF/Tools' \
>> "$DIR/settings"
fi
if [[ $ISABELLE_DOCS = *DOF* ]]; then
echo " * Docs already registered in $DIR/settings"
else
echo " * Registering docs in $DIR/settings"
echo "ISABELLE_DOCS=$PWD/doc"':$ISABELLE_DOCS' \
>> "$DIR/settings"
fi
sed -i -e "s|<isadofurl>|$DOF_URL|" $ISABELLE_HOME_USER/DOF/*/*
LTX_VERSION="$DATE $DOF_VERSION/$ISABELLE_SHORT_VERSION"
sed -i -e "s|<isadofltxversion>|$LTX_VERSION|" $ISABELLE_HOME_USER/DOF/*/*
touch $ISABELLE_HOME_USER/ROOTS
grep -q $PWD'$' $ISABELLE_HOME_USER/ROOTS || echo "$PWD" >> $ISABELLE_HOME_USER/ROOTS
}
ISABELLE=`command -v isabelle`
SKIP="false"
while [ $# -gt 0 ]
do
case "$1" in
--isabelle|-i)
ISABELLE="$2";
shift;;
--skip-patch-and-afp|-s)
SKIP="true";;
--help|-h)
print_help
exit 0;;
*) print_help
exit 1;;
esac
shift
done
ACTUAL_ISABELLE_VERSION=`$ISABELLE version`
GEN_DIR=src
PROG=`echo $0 | sed 's|.*/||'`;
VARS=`$ISABELLE getenv ISABELLE_HOME_USER ISABELLE_HOME ISABELLE_TOOLS ISABELLE_DOCS`
for i in $VARS; do
export "$i"
done
echo ""
echo "Isabelle/DOF Installer"
echo "======================"
check_isabelle_version
if [ "$SKIP" = "true" ]; then
echo "* Warning: skipping installation of Isabelle patch and AFP entries."
else
check_isa_dof_patch
check_afp_entries
fi
check_old_installation
install_and_register
echo "* Installation successful. Enjoy Isabelle/DOF, you can build the session"
echo " Isabelle/DOF and all example documents by executing:"
echo " $ISABELLE build -D ."
exit 0

142
install-afp Executable file
View File

@ -0,0 +1,142 @@
#!/usr/bin/env bash
# Copyright (c) 2018-2019 The University of Sheffield.
# 2019-2020 The University of Exeter.
# 2018-2020 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
#set -e
shopt -s nocasematch
print_help()
{
echo "Usage: isabelle env ./install-afp [OPTION] "
echo ""
echo "Run ..."
echo ""
echo " --help, -h display this help message"
}
exit_error() {
echo ""
echo " *** Isabelle/DOF installation FAILED, please check the README.md for help ***"
echo ""
exit 1
}
check_isabelle_version() {
echo "* Checking Isabelle version:"
if [ "$ISABELLE_VERSION" != "$ACTUAL_ISABELLE_VERSION" ]; then
echo " WARNING:"
echo " The version of Isabelle (i.e., $ACTUAL_ISABELLE_VERSION) you are using"
echo " IS NOT SUPPORTED"
echo " by the current version of Isabelle/DOF. Please install a supported"
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
read -p " Still continue (y/N)? " -n 1 -r
echo
if [[ $REPLY =~ ^[Yy]$ ]];
then
echo " Continuing installation on your OWN risk."
else
exit_error
fi
else
echo " Success: found supported Isabelle version ($ISABELLE_VERSION)"
fi
}
check_afp_entries() {
echo "* Checking availability of AFP entries:"
missing=""
required="Regular-Sets Functional-Automata"
for afp in $required; do
res=`$ISABELLE_TOOL build -n $afp 2>/dev/null || true`
if [ "$res" != "" ]; then
echo " Success: found APF entry $afp."
else
echo " Warning: could not find AFP entry $afp."
missing="$missing $afp"
fi
done
if [ "$missing" != "" ]; then
echo " Trying to install AFP (this might take a few *minutes*) ...."
extract=""
for e in $missing; do
extract="$extract $AFP_DATE/thys/$e"
done
mkdir -p .afp
if curl -s -L $AFP_URL | tar zxf - -C .afp $extract; then
for e in $missing; do
echo " Registering $e"
$ISABELLE_TOOL components -u "$PWD/.afp/$AFP_DATE/thys/$e"
done
echo " AFP installation successful."
else
echo " FAILURE: could not find AFP entries: $missing."
echo " Please obtain the AFP from"
echo " $AFP_URL"
echo " and follow the following instructions:"
echo " https://www.isa-afp.org/using.html"
exit_error
fi
fi
}
register(){
echo " - Registering Isabelle/DOF"
$ISABELLE_TOOL components -u "$PWD"
}
while [ $# -gt 0 ]
do
case "$1" in
--help|-h)
print_help
exit 0;;
*) print_help
exit 1;;
esac
shift
done
ACTUAL_ISABELLE_VERSION=`$ISABELLE_TOOL version`
echo ""
echo "Isabelle/DOF Installer"
echo "======================"
check_isabelle_version
check_afp_entries
register
echo "* Installation successful. Enjoy Isabelle/DOF, you can build the session"
echo " Isabelle/DOF and all example documents by executing:"
echo " $ISABELLE_TOOL build -D ."
exit 0

BIN
src/DOF/.Isa_DOF.thy.marks Normal file
View File

Binary file not shown.

82
src/DOF/Assert.thy
View File

@ -1,82 +0,0 @@
(*************************************************************************
* Copyright (C)
* 2019 The University of Exeter
* 2018-2019 The University of Paris-Saclay
* 2018 The University of Sheffield
*
* License:
* This program can be redistributed and/or modified under the terms
* of the 2-clause BSD-style license.
*
* SPDX-License-Identifier: BSD-2-Clause
*************************************************************************)
section \<open> Little theory implementing the an assertion command in Isabelle/HOL. \<close>
text\<open>This command is useful for certification documents allowing to validate
corner-cases of (executable) definitions. \<close>
theory Assert
imports Main
keywords "assert" ::thy_decl
begin
subsection\<open>Core\<close>
ML\<open>
local
(* Reimplementation needed because not exported from ML structure Value_Command *)
fun value_maybe_select some_name =
case some_name
of NONE => Value_Command.value
| SOME name => Value_Command.value_select name;
in
(* Reimplementation needed because not exported from ML structure Value_Command *)
val opt_modes =
Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) [];
(* Reimplementation needed because not exported from ML structure Value_Command *)
val opt_evaluator =
Scan.option (@{keyword "["} |-- Parse.name --| @{keyword "]"})
(* Reimplementation structure Value_Command due to tiny modification of value_cmd. *)
fun assert_cmd some_name modes raw_t ctxt (* state*) =
let
(* val ctxt = Toplevel.context_of state; *)
val t = Syntax.read_term ctxt raw_t;
val t' = value_maybe_select some_name ctxt t;
val ty' = Term.type_of t';
val ty' = case ty' of @{typ "bool"} => ty' | _ => error "Assertion expressions must be boolean.";
val t' = case t' of @{term "True"} => t' | _ => error "Assertion failed.";
val ctxt' = Proof_Context.augment t' ctxt;
val p = Print_Mode.with_modes modes (fn () =>
Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
in Pretty.writeln p end;
val _ =
Outer_Syntax.command @{command_keyword assert} "evaluate and print term"
(opt_evaluator -- opt_modes -- Parse.term
>> (fn ((some_name, modes), t) =>
Toplevel.keep ( (assert_cmd some_name modes t) o Toplevel.context_of) ));
end
\<close>
subsection\<open> Test: \<close>
(*
assert ""
assert "3 = 4"
assert "False"
assert "5 * 5 = 25"
*)
subsection\<open>Example\<close>
assert "True \<and> True "
assert "(5::int) * 5 = 25 "
end

70
src/DOF/AssertLong.thy
View File

@ -1,70 +0,0 @@
(*************************************************************************
* Copyright (C)
* 2019 The University of Exeter
* 2018-2019 The University of Paris-Saclay
* 2018 The University of Sheffield
*
* License:
* This program can be redistributed and/or modified under the terms
* of the 2-clause BSD-style license.
*
* SPDX-License-Identifier: BSD-2-Clause
*************************************************************************)
theory AssertLong
imports Main
keywords "assert" ::thy_decl
begin
ML\<open>
fun value_maybe_select some_name =
case some_name
of NONE => Value_Command.value
| SOME name => Value_Command.value_select name;
val TT = Unsynchronized.ref (HOLogic.boolT);
fun value_cmd2 some_name modes raw_t state =
let
val ctxt = Toplevel.context_of state;
val t = Syntax.read_term ctxt raw_t;
val t' = value_maybe_select some_name ctxt t;
val ty' = Term.type_of t';
val t' = case ty' of @{typ "bool"} => t' | _ => error "Assertion expressions must be boolean.";
val t' = case t' of @{term "True"} => t' | _ => error "Assertion failed.";
val ctxt' = Variable.auto_fixes t' ctxt;
val p = Print_Mode.with_modes modes (fn () =>
Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
in Pretty.writeln p end;
\<close>
ML\<open>value_cmd2\<close>
definition ASSERT :: "bool \<Rightarrow> bool" where "ASSERT p == (p=True)"
ML\<open>val x = @{code "ASSERT"}\<close>
ML\<open>
val opt_modes =
Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) [];
val opt_evaluator =
Scan.option (@{keyword "["} |-- Parse.name --| @{keyword "]"})
val _ =
Outer_Syntax.command @{command_keyword assert} "evaluate and print term"
(opt_evaluator -- opt_modes -- Parse.term
>> (fn ((some_name, modes), t) =>
let val _ = writeln t in
(* Toplevel.keep (Value_Command.value_cmd some_name modes (enclose "ASSERT(" ")" t)) *)
Toplevel.keep (value_cmd2 some_name modes t)
end));
\<close>
assert "True"
assert "True \<and> True "
ML\<open>!TT ;
@{term "True"}\<close>

85
src/DOF/Isa_COL.thy
View File

@ -106,60 +106,32 @@ in
fun enriched_formal_statement_command ncid (S: (string * string) list) =
let fun transform_attr doc_attrs = (map (fn(cat,tag) => ((cat,@{here}),tag)) S) @
(("formal_results",@{here}),"([]::thm list)")::doc_attrs
in fn md => fn margs => fn thy =>
in fn margs => fn thy =>
gen_enriched_document_cmd {inline=true}
(transform_cid thy ncid) transform_attr md margs thy
(transform_cid thy ncid) transform_attr margs thy
end;
fun enriched_document_cmd_exp ncid (S: (string * string) list) =
(* expands ncid into supertype-check. *)
let fun transform_attr attrs = (map (fn(cat,tag) => ((cat,@{here}),tag)) S) @ attrs
in fn md => fn margs => fn thy =>
gen_enriched_document_cmd {inline=true} (transform_cid thy ncid) transform_attr md margs thy
in fn margs => fn thy =>
gen_enriched_document_cmd {inline=true} (transform_cid thy ncid) transform_attr margs thy
end;
end (* local *)
val _ =
Outer_Syntax.command ("title*", @{here}) "section heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (enriched_text_element_cmd NONE {markdown = false} ))) ;
fun heading_command (name, pos) descr level =
ODL_Command_Parser.document_command (name, pos) descr
{markdown = false, body = true} (enriched_text_element_cmd level);
val _ =
Outer_Syntax.command ("subtitle*", @{here}) "section heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (enriched_text_element_cmd NONE {markdown = false} )));
val _ =
Outer_Syntax.command ("chapter*", @{here}) "section heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (enriched_text_element_cmd (SOME(SOME 0)) {markdown = false} )));
val _ =
Outer_Syntax.command ("section*", @{here}) "section heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (enriched_text_element_cmd (SOME(SOME 1)) {markdown = false} )));
val _ =
Outer_Syntax.command ("subsection*", @{here}) "subsection heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (enriched_text_element_cmd (SOME(SOME 2)) {markdown = false} )));
val _ =
Outer_Syntax.command ("subsubsection*", @{here}) "subsubsection heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (enriched_text_element_cmd (SOME(SOME 3)) {markdown = false} )));
val _ =
Outer_Syntax.command ("paragraph*", @{here}) "paragraph heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (enriched_text_element_cmd (SOME(SOME 4)) {markdown = false} )));
val _ =
Outer_Syntax.command ("subparagraph*", @{here}) "subparagraph heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (enriched_text_element_cmd (SOME(SOME 5)) {markdown = false} )));
val _ = heading_command ("title*", @{here}) "section heading" NONE;
val _ = heading_command ("subtitle*", @{here}) "section heading" NONE;
val _ = heading_command ("chapter*", @{here}) "section heading" (SOME (SOME 0));
val _ = heading_command ("section*", @{here}) "section heading" (SOME (SOME 1));
val _ = heading_command ("subsection*", @{here}) "subsection heading" (SOME (SOME 2));
val _ = heading_command ("subsubsection*", @{here}) "subsubsection heading" (SOME (SOME 3));
val _ = heading_command ("paragraph*", @{here}) "paragraph heading" (SOME (SOME 4));
val _ = heading_command ("subparagraph*", @{here}) "subparagraph heading" (SOME (SOME 5));
end
end
@ -206,24 +178,13 @@ print_doc_classes
subsection\<open>Ontological Macros\<close>
ML\<open> local open ODL_Command_Parser in
ML\<open>
(* *********************************************************************** *)
(* Ontological Macro Command Support *)
(* *********************************************************************** *)
val _ =
Outer_Syntax.command ("figure*", @{here}) "figure"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (Onto_Macros.enriched_text_element_cmd NONE {markdown = false} )));
val _ =
Outer_Syntax.command ("side_by_side_figure*", @{here}) "multiple figures"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (Onto_Macros.enriched_text_element_cmd NONE {markdown = false} )));
end
val _ = Onto_Macros.heading_command ("figure*", @{here}) "figure" NONE;
val _ = Onto_Macros.heading_command ("side_by_side_figure*", @{here}) "multiple figures" NONE;
\<close>
(*<*)
@ -247,22 +208,22 @@ section\<open>Tables\<close>
ML\<open>
local
fun mk_line st1 st2 [a] = [a @ [Latex.string st2]]
|mk_line st1 st2 (a::S) = [a @ [Latex.string st1]] @ mk_line st1 st2 S;
fun mk_line st1 st2 [a] = [a @ Latex.string st2]
|mk_line st1 st2 (a::S) = [a @ Latex.string st1] @ mk_line st1 st2 S;
fun table_antiquotation name =
Thy_Output.antiquotation_raw_embedded name
Document_Output.antiquotation_raw_embedded name
(Scan.repeat1(Scan.repeat1(Scan.lift Args.cartouche_input)))
(fn ctxt =>
(fn content:Input.source list list =>
let fun check _ = () (* ToDo *)
val _ = check content
in content
|> (map(map (Thy_Output.output_document ctxt {markdown = false})
|> (map(map (Document_Output.output_document ctxt {markdown = false})
#> mk_line "&" "\\\\"
#> List.concat )
#> List.concat)
|> Latex.enclose_block "\\table[allerhandquatsch]{" "}"
|> XML.enclose "\\table[allerhandquatsch]{" "}"
end
)
);

784
src/DOF/Isa_DOF.thy
View File

File diff suppressed because it is too large Load Diff

1249
src/DOF/latex/lipics-v2021-dof.cls
View File

File diff suppressed because it is too large Load Diff

17
src/ROOT
View File

@ -1,5 +1,5 @@
session "Isabelle_DOF" = "Functional-Automata" +
options [document = pdf, document_output = "output"]
options [document = pdf, document_output = "output", document_build = dof]
sessions
"Regular-Sets"
directories
@ -16,18 +16,3 @@ session "Isabelle_DOF" = "Functional-Automata" +
"DOF/Isa_DOF"
"ontologies/ontologies"
(*
session "Isabelle_DOF-tests" = "Isabelle_DOF" +
options [document = false]
directories
tests
theories
"tests/AssnsLemmaThmEtc"
"tests/Concept_ExampleInvariant"
"tests/Concept_Example"
"tests/InnerSyntaxAntiquotations"
"tests/Attributes"
*)

11
src/Tools/mkroot_DOF
View File

@ -43,14 +43,14 @@ function usage()
echo " -n NAME alternative session name (default: DIR base name)"
echo " -o ONTOLOGY (default: $DEFAULT_ONTOLOGY)"
echo " Available ontologies:"
for t in "$ISABELLE_HOME_USER/DOF/latex/"*.sty; do
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_HOME_USER/DOF/document-template/"*.tex; do
for t in "$ISABELLE_DOF_HOME/src/document-templates/"*.tex; do
if [[ $t =~ root-(.*).tex$ ]]; then
echo " * ${BASH_REMATCH[1]}"
fi
@ -90,7 +90,7 @@ do
NAME="$OPTARG"
;;
o)
if [ ! -f "$ISABELLE_HOME_USER/DOF/latex/DOF-$OPTARG.sty" ]; then
if [ ! -f "$ISABELLE_DOF_HOME/src/ontologies/*//DOF-$OPTARG.sty" ]; then
echo "ERROR: Ontology $OPTARG not available!"
exit 1
fi
@ -98,7 +98,7 @@ do
;;
t)
TEMPLATE="$OPTARG"
if [ ! -f "$ISABELLE_HOME_USER/DOF/document-template/root-$TEMPLATE.tex" ]; then
if [ ! -f "$ISABELLE_DOF_HOME/src/document-templates/root-$TEMPLATE.tex" ]; then
echo "ERROR: Template $TEMPLATE not available!"
exit 1
fi
@ -131,14 +131,13 @@ fi
$ISABELLE_TOOL mkroot -n "$NAME" "$DIR"
echo " \"preamble.tex\"" >> "$DIR"/ROOT
echo " \"build\"" >> "$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
cp "$ISABELLE_HOME_USER/DOF/document-template/build" "$DIR"/document/
for o in $ONTOLOGY; do
echo "Ontology: $o" >> "$DIR"/document/isadof.cfg;
done

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

@ -40,11 +40,9 @@
\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 <isadofurl>"
You can install the framework as follows:
"cd Isabelle_DOF/document-generator && ./install"}{%
For further help, see <isadofurl>}
the Isabelle_DOF component from:
<isadofurl>
}{For further help, see <isadofurl>}
}
\newcommand{\subtitle}[1]{%

94
src/document-templates/root-lipics-v2019-UNSUPPORTED.tex
View File

@ -1,94 +0,0 @@
%% Copyright (c) 2019 University of Exeter
%% 2018-2019 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.
%%
%% <isadofltxversion>
%% Warning: Do Not Edit!
%% =====================
%% This is the root file for the Isabelle/DOF using the lipics class.
%% Note that lipics cannot be distributed as part of Isabelle/DOF; you need
%% to download lipics.cls from
%% https://www.dagstuhl.de/en/publications/lipics/instructions-for-authors/
%% and add it manually to the praemble.tex and the ROOT file.
%%
%% All customization and/or additional packages should be added to the file
%% preamble.tex.
\documentclass[a4paper,USenglish,cleveref, autoref]{lipics-v2019}
\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 framework. Please obtain the framework by cloning
the Isabelle_DOF git repository, i.e.:
"git clone <isadofurl>"
You can install the framework as follows:
"cd Isabelle_DOF/document-generator && ./install"}{%
For further help, see <isadofurl>}
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% provide an alternative definition of
% begin: scholarly_paper.author
\RequirePackage{keycommand}
\makeatletter
\newcommand{\DOFlipicsAuthor}[4]{\expandafter\author{#1}{#2}{#3}{#4}}
\expandafter\newkeycommand\csname isaDof.text.scholarly_paper.author\endcsname%
[label=,type=%
,scholarly_paper.author.email=%
,scholarly_paper.author.affiliation=%
,scholarly_paper.author.orcid=%
,scholarly_paper.author.http_site=%
][1]{%
\protected@write\@auxout{}{\string\protect\string\DOFlipicsAuthor{#1}%
{\commandkey{scholarly_paper.author.affiliation}}
{\commandkey{scholarly_paper.author.email}}
{\commandkey{scholarly_paper.author.orcid}}
{}
}
}
\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}
}}{}
\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:

17
src/document-templates/root-lipics-v2021-UNSUPPORTED.tex → src/document-templates/root-lipics-v2021.tex
View File

@ -16,15 +16,17 @@
%% Warning: Do Not Edit!
%% =====================
%% This is the root file for the Isabelle/DOF using the lipics class.
%% Note that lipics cannot be distributed as part of Isabelle/DOF; you need
%% to download lipics.cls from
%% Note that lipics cannot is *not* distributed as part of Isabelle/DOF;
%% you need to download lipics.cls from
%% https://www.dagstuhl.de/en/publications/lipics/instructions-for-authors/
%% and add it manually to the praemble.tex and the ROOT file.
%% Moreover, the option "document_comment_latex=true" needs to be set
%% in the ROOT file.
%%
%% All customization and/or additional packages should be added to the file
%% preamble.tex.
\documentclass[a4paper,UKenglish,cleveref, autoref,thm-restate]{lipics-v2021-dof}
\documentclass[a4paper,UKenglish,cleveref, autoref,thm-restate]{lipics-v2021}
\bibliographystyle{plainurl}% the mandatory bibstyle
\usepackage{isabelle}
\usepackage{isabellesym}
@ -34,12 +36,9 @@
\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/Isabelle_DOF/Isabelle_DOF"
You can install the framework as follows:
"cd Isabelle_DOF/document-generator && ./install"}{%
For further help, see https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF}
the Isabelle_DOF component from:
<isadofurl>
}{For further help, see <isadofurl>}
}

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

@ -17,10 +17,6 @@
%% Warning: Do Not Edit!
%% =====================
%% This is the root file for the Isabelle/DOF using the lncs class.
%% Note that lncs cannot be distributed as part of Isabelle/DOF; you need
%% to download lncs.cls from
%% https://www.springer.com/gp/computer-science/lncs/conference-proceedings-guidelines
%% and add it manually to the praemble.tex and the ROOT file.
%%
%% All customization and/or additional packages should be added to the file
%% preamble.tex.
@ -39,12 +35,9 @@
\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 <isadofurl>"
You can install the framework as follows:
"cd Isabelle_DOF/document-generator && ./install"}{%
For further help, see <isadofurl>}
the Isabelle_DOF component from:
<isadofurl>
}{For further help, see <isadofurl>}
}
\input{ontologies}
\IfFileExists{preamble.tex}{\input{preamble.tex}}{}%

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

@ -34,12 +34,9 @@
\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 <isadofurl>"
You can install the framework as follows:
"cd Isabelle_DOF/document-generator && ./install"}{%
For further help, see <isadofurl>}
the Isabelle_DOF component from:
<isadofurl>
}{For further help, see <isadofurl>}
}
\input{ontologies}
\IfFileExists{preamble.tex}{\input{preamble.tex}}{}%

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

@ -55,12 +55,9 @@
\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 <isadofurl>"
You can install the framework as follows:
"cd Isabelle_DOF/document-generator && ./install"}{%
For further help, see <isadofurl>}
the Isabelle_DOF component from:
<isadofurl>
}{For further help, see <isadofurl>}
}
\input{ontologies}
\IfFileExists{preamble.tex}{\input{preamble.tex}}{}%

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

@ -34,12 +34,9 @@
\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 <isadofurl>"
You can install the framework as follows:
"cd Isabelle_DOF/document-generator && ./install"}{%
For further help, see <isadofurl>}
the Isabelle_DOF component from:
<isadofurl>
}{For further help, see <isadofurl>}
}
\input{ontologies}
\IfFileExists{preamble.tex}{\input{preamble.tex}}{}%

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

@ -38,12 +38,9 @@
\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 <isadofurl>"
You can install the framework as follows:
"cd Isabelle_DOF/document-generator && ./install"}{%
For further help, see <isadofurl>}
the Isabelle_DOF component from:
<isadofurl>
}{For further help, see <isadofurl>}
}
\input{ontologies}
\IfFileExists{preamble.tex}{\input{preamble.tex}}{}%

10
src/ontologies/CENELEC_50128/CENELEC_50128.thy
View File

@ -373,10 +373,6 @@ doc_class FnI = requirement +
is_concerned :: "role set" <= "UNIV"
type_synonym functions_and_interfaces = FnI
doc_class AC = requirement +
is_concerned :: "role set" <= "UNIV"
type_synonym application_conditions = AC
text\<open>The category \<^emph>\<open>assumption\<close> is used for domain-specific assumptions. It has formal, semi-formal
and informal sub-categories. They have to be tracked and discharged by appropriate
@ -387,6 +383,12 @@ datatype ass_kind = informal | semiformal | formal
doc_class assumption = requirement +
assumption_kind :: ass_kind <= informal
doc_class AC = assumption +
is_concerned :: "role set" <= "UNIV"
type_synonym application_conditions = AC
text\<open> The category \<^emph>\<open>exported constraint\<close> (or \<^emph>\<open>EC\<close> for short) is used for formal application
conditions; They represent in particular \<^emph>\<open>derived constraints\<close>, i.e. constraints that arrive
as side-conditions during refinement proofs or implementation decisions and must be tracked.\<close>

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

@ -71,6 +71,7 @@
,CENELEC_50128.SRAC.formal_repr=%
,CENELEC_50128.SRAC.assumption_kind=%
,CENELEC_50128.EC.assumption_kind=%
,CENELEC_50128.assumption.assumption_kind=%
][1]{%
\begin{isamarkuptext}%
\ifthenelse{\equal{\commandkey{CENELEC_50128.requirement.long_name}}{}}{%
@ -123,6 +124,7 @@
,CENELEC_50128.SRAC.formal_repr=%
,CENELEC_50128.SRAC.assumption_kind=%
,CENELEC_50128.EC.assumption_kind=%
,CENELEC_50128.assumption.assumption_kind=%
][1]{%
\begin{isamarkuptext}%
\ifthenelse{\equal{\commandkey{CENELEC_50128.requirement.long_name}}{}}{%

4
src/ontologies/Conceptual/Conceptual.thy Executable file → Normal file
View File

@ -136,7 +136,7 @@ text\<open>Now, we can use these definitions in order to generate code for these
Note, however, that not everything that we can write in an invariant (basically: HOL) is executable,
or even compilable by the code generator setup:\<close>
ML\<open> val cr_inv_code = @{code "cr_inv"} \<close> \<comment>\<open>works albeit thm is abstract ...\<close>
ML\<open> val cr_inv_code = @{code "cr_inv"} \<close> \<comment> \<open>works albeit thm is abstract ...\<close>
text\<open>while in :\<close>
(* ML\<open> val br_inv_code = @{code "br_inv"} \<close> \<comment>\<open>this does not work ...\<close> *)
@ -144,7 +144,7 @@ text\<open>... the compilation fails due to the fact that nothing prevents the u
to define an infinite relation between \<^typ>\<open>A\<close> and \<^typ>\<open>C\<close>. However, the alternative
variant: \<close>
ML\<open> val br'_inv_code = @{code "br'_inv"} \<close> \<comment>\<open>does work ...\<close>
ML\<open> val br'_inv_code = @{code "br'_inv"} \<close> \<comment> \<open>does work ...\<close>
text\<open>... is compilable ...\<close>

9
src/ontologies/scholarly_paper/DOF-scholarly_paper.sty
View File

@ -40,7 +40,7 @@
\RequirePackage{DOF-scholarly_paper-thm}%
}%
{%
\@ifclassloaded{lipics-v2021-dof}%
\@ifclassloaded{lipics-v2021}%
{%
\newcommand{\institute}[1]{}%
\newcommand{\inst}[1]{}%
@ -48,13 +48,6 @@
\newcommand{\email}[1]{}%
}%
{%
\@ifclassloaded{lipics-v2019}%
{%
\newcommand{\institute}[1]{}%
\newcommand{\inst}[1]{}%
\newcommand{\orcidID}[1]{}%
\newcommand{\email}[1]{}%
}%
{%
\@ifclassloaded{eptcs}%
{%

128
src/ontologies/scholarly_paper/scholarly_paper.thy
View File

@ -17,8 +17,6 @@ theory scholarly_paper
imports "../../DOF/Isa_COL"
keywords "author*" "abstract*"
"Definition*" "Lemma*" "Theorem*" :: document_body
and "assert*" :: thy_decl
begin
@ -47,23 +45,15 @@ doc_class abstract =
ML\<open>
local open ODL_Command_Parser in
val _ = Outer_Syntax.command ("abstract*", @{here}) "Textual Definition"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (Onto_Macros.enriched_document_cmd_exp
(SOME "abstract")
[]
{markdown = true} )));
val _ =
ODL_Command_Parser.document_command ("abstract*", @{here}) "Textual Definition"
{markdown = true, body = true}
(Onto_Macros.enriched_document_cmd_exp (SOME "abstract") []);
val _ = Outer_Syntax.command ("author*", @{here}) "Textual Definition"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (Onto_Macros.enriched_document_cmd_exp
(SOME "author")
[]
{markdown = true} )));
end
val _ =
ODL_Command_Parser.document_command ("author*", @{here}) "Textual Definition"
{markdown = true, body = true}
(Onto_Macros.enriched_document_cmd_exp (SOME "author") []);
\<close>
text\<open>Scholarly Paper is oriented towards the classical domains in science:
@ -298,45 +288,41 @@ setup\<open>Theorem_default_class_setup\<close>
ML\<open> local open ODL_Command_Parser in
(* {markdown = true} sets the parsing process such that in the text-core
markdown elements are accepted. *)
val _ =
ODL_Command_Parser.document_command ("Definition*", @{here}) "Textual Definition"
{markdown = true, body = true}
(fn meta_args => fn thy =>
let
val ddc = Config.get_global thy Definition_default_class
val use_Definition_default = SOME(((ddc = "") ? (K "math_content")) ddc)
in
Onto_Macros.enriched_formal_statement_command
use_Definition_default [("mcc","defn")] meta_args thy
end);
val _ = let fun use_Definition_default thy =
let val ddc = Config.get_global thy Definition_default_class
in (SOME(((ddc = "") ? (K "math_content")) ddc)) end
in Outer_Syntax.command ("Definition*", @{here}) "Textual Definition"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (fn args => fn thy =>
Onto_Macros.enriched_formal_statement_command
(use_Definition_default thy)
[("mcc","defn")]
{markdown = true} args thy)))
end;
val _ =
ODL_Command_Parser.document_command ("Lemma*", @{here}) "Textual Lemma Outline"
{markdown = true, body = true}
(fn meta_args => fn thy =>
let
val ddc = Config.get_global thy Definition_default_class
val use_Lemma_default = SOME(((ddc = "") ? (K "math_content")) ddc)
in
Onto_Macros.enriched_formal_statement_command
use_Lemma_default [("mcc","lem")] meta_args thy
end);
val _ = let fun use_Lemma_default thy =
let val ddc = Config.get_global thy Definition_default_class
in (SOME(((ddc = "") ? (K "math_content")) ddc)) end
in Outer_Syntax.command ("Lemma*", @{here}) "Textual Lemma Outline"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (fn args => fn thy =>
Onto_Macros.enriched_formal_statement_command
(use_Lemma_default thy)
[("mcc","lem")]
{markdown = true} args thy)))
end;
val _ = let fun use_Theorem_default thy =
let val ddc = Config.get_global thy Definition_default_class
in (SOME(((ddc = "") ? (K "math_content")) ddc)) end
in Outer_Syntax.command ("Theorem*", @{here}) "Textual Theorem Outline"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (fn args => fn thy =>
Onto_Macros.enriched_formal_statement_command
(use_Theorem_default thy)
[("mcc","thm")]
{markdown = true} args thy)))
end;
val _ =
ODL_Command_Parser.document_command ("Theorem*", @{here}) "Textual Theorem Outline"
{markdown = true, body = true}
(fn meta_args => fn thy =>
let
val ddc = Config.get_global thy Definition_default_class
val use_Theorem_default = SOME(((ddc = "") ? (K "math_content")) ddc)
in
Onto_Macros.enriched_formal_statement_command
use_Theorem_default [("mcc","thm")] meta_args thy
end);
end
\<close>
@ -359,39 +345,7 @@ doc_class assertion = math_formal +
properties :: "term list"
ML\<open>
(* TODO : Rework this code and make it closer to Definition*. There is still
a rest of "abstract classes in it: any class possessing a properties attribute
is admissible to this command, not just ... *)
local open ODL_Command_Parser in
fun assertion_cmd'((((((oid,pos),cid_pos),doc_attrs),name_opt:string option),modes : string list),
prop) =
let fun conv_2_holstring thy = (bstring_to_holstring (Proof_Context.init_global thy))
fun conv_attrs thy = (("properties",pos),"[@{termrepr ''"^conv_2_holstring thy prop ^" ''}]")
::doc_attrs
fun conv_attrs' thy = map (fn ((lhs,pos),rhs) => (((lhs,pos),"+="),rhs)) (conv_attrs thy)
fun mks thy = case DOF_core.get_object_global_opt oid thy of
SOME NONE => (error("update of declared but not created doc_item:" ^ oid))
| SOME _ => (update_instance_command (((oid,pos),cid_pos),conv_attrs' thy) thy)
| NONE => (create_and_check_docitem
{is_monitor = false} {is_inline = false}
oid pos cid_pos (conv_attrs thy) thy)
val check = (assert_cmd name_opt modes prop) o Proof_Context.init_global
in
(* Toplevel.keep (check o Toplevel.context_of) *)
Toplevel.theory (fn thy => (check thy; mks thy))
end
val attributes = attributes (* re-export *)
end
val _ =
Outer_Syntax.command @{command_keyword "assert*"}
"evaluate and print term"
(attributes -- opt_evaluator -- opt_modes -- Parse.term >> assertion_cmd');
\<close>
subsubsection*[ex_ass::example]\<open>Example\<close>
text\<open>Assertions allow for logical statements to be checked in the global context). \<close>

566
src/patches/thy_output.Isabelle2021.ML
View File

@ -1,566 +0,0 @@
(* Title: Pure/Thy/thy_output.ML
Author: Makarius
Theory document output.
*)
signature THY_OUTPUT =
sig
val output_document: Proof.context -> {markdown: bool} -> Input.source -> Latex.text list
val check_comments: Proof.context -> Symbol_Pos.T list -> unit
val output_token: Proof.context -> Token.T -> Latex.text list
val output_source: Proof.context -> string -> Latex.text list
type segment = {span: Command_Span.span, command: Toplevel.transition, state: Toplevel.state}
val present_thy: Options.T -> theory -> segment list -> Latex.text list
val pretty_term: Proof.context -> term -> Pretty.T
val pretty_thm: Proof.context -> thm -> Pretty.T
val lines: Latex.text list -> Latex.text list
val items: Latex.text list -> Latex.text list
val isabelle: Proof.context -> Latex.text list -> Latex.text
val isabelle_typewriter: Proof.context -> Latex.text list -> Latex.text
val typewriter: Proof.context -> string -> Latex.text
val verbatim: Proof.context -> string -> Latex.text
val source: Proof.context -> {embedded: bool} -> Token.src -> Latex.text
val pretty: Proof.context -> Pretty.T -> Latex.text
val pretty_source: Proof.context -> {embedded: bool} -> Token.src -> Pretty.T -> Latex.text
val pretty_items: Proof.context -> Pretty.T list -> Latex.text
val pretty_items_source: Proof.context -> {embedded: bool} -> Token.src ->
Pretty.T list -> Latex.text
val antiquotation_pretty:
binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
val antiquotation_pretty_embedded:
binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
val antiquotation_pretty_source:
binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
val antiquotation_pretty_source_embedded:
binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
val antiquotation_raw:
binding -> 'a context_parser -> (Proof.context -> 'a -> Latex.text) -> theory -> theory
val antiquotation_raw_embedded:
binding -> 'a context_parser -> (Proof.context -> 'a -> Latex.text) -> theory -> theory
val antiquotation_verbatim:
binding -> 'a context_parser -> (Proof.context -> 'a -> string) -> theory -> theory
val antiquotation_verbatim_embedded:
binding -> 'a context_parser -> (Proof.context -> 'a -> string) -> theory -> theory
end;
structure Thy_Output: THY_OUTPUT =
struct
(* output document source *)
val output_symbols = single o Latex.symbols_output;
fun output_comment ctxt (kind, syms) =
(case kind of
Comment.Comment =>
Input.cartouche_content syms
|> output_document (ctxt |> Config.put Document_Antiquotation.thy_output_display false)
{markdown = false}
|> Latex.enclose_body "%\n\\isamarkupcmt{" "%\n}"
| Comment.Cancel =>
Symbol_Pos.cartouche_content syms
|> output_symbols
|> Latex.enclose_body "%\n\\isamarkupcancel{" "}"
| Comment.Latex => [Latex.symbols (Symbol_Pos.cartouche_content syms)]
| Comment.Marker => [])
and output_comment_document ctxt (comment, syms) =
(case comment of
SOME kind => output_comment ctxt (kind, syms)
| NONE => [Latex.symbols syms])
and output_document_text ctxt syms =
Comment.read_body syms |> maps (output_comment_document ctxt)
and output_document ctxt {markdown} source =
let
val pos = Input.pos_of source;
val syms = Input.source_explode source;
val output_antiquotes =
maps (Document_Antiquotation.evaluate (output_document_text ctxt) ctxt);
fun output_line line =
(if Markdown.line_is_item line then [Latex.string "\\item "] else []) @
output_antiquotes (Markdown.line_content line);
fun output_block (Markdown.Par lines) =
Latex.block (separate (Latex.string "\n") (map (Latex.block o output_line) lines))
| output_block (Markdown.List {kind, body, ...}) =
Latex.environment_block (Markdown.print_kind kind) (output_blocks body)
and output_blocks blocks = separate (Latex.string "\n\n") (map output_block blocks);
in
if Toplevel.is_skipped_proof (Toplevel.presentation_state ctxt) then []
else if markdown andalso exists (Markdown.is_control o Symbol_Pos.symbol) syms
then
let
val ants = Antiquote.parse_comments pos syms;
val reports = Antiquote.antiq_reports ants;
val blocks = Markdown.read_antiquotes ants;
val _ = Context_Position.reports ctxt (reports @ Markdown.reports blocks);
in output_blocks blocks end
else
let
val ants = Antiquote.parse_comments pos (trim (Symbol.is_blank o Symbol_Pos.symbol) syms);
val reports = Antiquote.antiq_reports ants;
val _ = Context_Position.reports ctxt (reports @ Markdown.text_reports ants);
in output_antiquotes ants end
end;
(* output tokens with formal comments *)
local
val output_symbols_antiq =
(fn Antiquote.Text syms => output_symbols syms
| Antiquote.Control {name = (name, _), body, ...} =>
Latex.string (Latex.output_symbols [Symbol.encode (Symbol.Control name)]) ::
output_symbols body
| Antiquote.Antiq {body, ...} =>
Latex.enclose_body "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n" (output_symbols body));
fun output_comment_symbols ctxt {antiq} (comment, syms) =
(case (comment, antiq) of
(NONE, false) => output_symbols syms
| (NONE, true) =>
Antiquote.parse_comments (#1 (Symbol_Pos.range syms)) syms
|> maps output_symbols_antiq
| (SOME comment, _) => output_comment ctxt (comment, syms));
fun output_body ctxt antiq bg en syms =
Comment.read_body syms
|> maps (output_comment_symbols ctxt {antiq = antiq})
|> Latex.enclose_body bg en;
in
fun output_token ctxt tok =
let
fun output antiq bg en =
output_body ctxt antiq bg en (Input.source_explode (Token.input_of tok));
in
(case Token.kind_of tok of
Token.Comment NONE => []
| Token.Comment (SOME Comment.Marker) => []
| Token.Command => output false "\\isacommand{" "}"
| Token.Keyword =>
if Symbol.is_ascii_identifier (Token.content_of tok)
then output false "\\isakeyword{" "}"
else output false "" ""
| Token.String => output false "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}"
| Token.Alt_String => output false "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}"
| Token.Verbatim => output true "{\\isacharverbatimopen}" "{\\isacharverbatimclose}"
| Token.Cartouche => output false "{\\isacartoucheopen}" "{\\isacartoucheclose}"
| _ => output false "" "")
end handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok));
fun output_source ctxt s =
output_body ctxt false "" "" (Symbol_Pos.explode (s, Position.none));
fun check_comments ctxt =
Comment.read_body #> List.app (fn (comment, syms) =>
let
val pos = #1 (Symbol_Pos.range syms);
val _ =
comment |> Option.app (fn kind =>
Context_Position.reports ctxt (map (pair pos) (Comment.kind_markups kind)));
val _ = output_comment_symbols ctxt {antiq = false} (comment, syms);
in if comment = SOME Comment.Comment then check_comments ctxt syms else () end);
end;
(** present theory source **)
(* presentation tokens *)
datatype token =
Ignore
| Token of Token.T
| Heading of string * Input.source
| Body of string * Input.source
| Raw of Input.source;
fun token_with pred (Token tok) = pred tok
| token_with _ _ = false;
val white_token = token_with Document_Source.is_white;
val white_comment_token = token_with Document_Source.is_white_comment;
val blank_token = token_with Token.is_blank;
val newline_token = token_with Token.is_newline;
fun present_token ctxt tok =
(case tok of
Ignore => []
| Token tok => output_token ctxt tok
| Heading (cmd, source) =>
Latex.enclose_body ("%\n\\isamarkup" ^ cmd ^ "{") "%\n}\n"
(output_document ctxt {markdown = false} source)
| Body (cmd, source) =>
[Latex.environment_block ("isamarkup" ^ cmd) (output_document ctxt {markdown = true} source)]
| Raw source =>
Latex.string "%\n" :: output_document ctxt {markdown = true} source @ [Latex.string "\n"]);
(* command spans *)
type command = string * Position.T; (*name, position*)
type source = (token * (string * int)) list; (*token, markup flag, meta-comment depth*)
datatype span = Span of command * (source * source * source * source) * bool;
fun make_span cmd src =
let
fun chop_newline (tok :: toks) =
if newline_token (fst tok) then ([tok], toks, true)
else ([], tok :: toks, false)
| chop_newline [] = ([], [], false);
val (((src_prefix, src_main), src_suffix1), (src_suffix2, src_appendix, newline)) =
src
|> chop_prefix (white_token o fst)
||>> chop_suffix (white_token o fst)
||>> chop_prefix (white_comment_token o fst)
||> chop_newline;
in Span (cmd, (src_prefix, src_main, src_suffix1 @ src_suffix2, src_appendix), newline) end;
(* present spans *)
local
fun err_bad_nesting here =
error ("Bad nesting of commands in presentation" ^ here);
fun edge which f (x: string option, y) =
if x = y then I
else (case which (x, y) of NONE => I | SOME txt => cons (Latex.string (f txt)));
val begin_tag = edge #2 Latex.begin_tag;
val end_tag = edge #1 Latex.end_tag;
fun open_delim delim e = edge #2 Latex.begin_delim e #> delim #> edge #2 Latex.end_delim e;
fun close_delim delim e = edge #1 Latex.begin_delim e #> delim #> edge #1 Latex.end_delim e;
fun document_tag cmd_pos state state' tagging_stack =
let
val ctxt' = Toplevel.presentation_context state';
val nesting = Toplevel.level state' - Toplevel.level state;
val (tagging, taggings) = tagging_stack;
val (tag', tagging') = Document_Source.update_tagging ctxt' tagging;
val tagging_stack' =
if nesting = 0 andalso not (Toplevel.is_proof state) then tagging_stack
else if nesting >= 0 then (tagging', replicate nesting tagging @ taggings)
else
(case drop (~ nesting - 1) taggings of
tg :: tgs => (tg, tgs)
| [] => err_bad_nesting (Position.here cmd_pos));
in (tag', tagging_stack') end;
fun read_tag s =
(case space_explode "%" s of
["", b] => (SOME b, NONE)
| [a, b] => (NONE, SOME (a, b))
| _ => error ("Bad document_tags specification: " ^ quote s));
in
fun make_command_tag options keywords =
let
val document_tags =
map read_tag (space_explode "," (Options.string options \<^system_option>\<open>document_tags\<close>));
val document_tags_default = map_filter #1 document_tags;
val document_tags_command = map_filter #2 document_tags;
in
fn cmd_name => fn state => fn state' => fn active_tag =>
let
val keyword_tags =
if cmd_name = "end" andalso Toplevel.is_end_theory state' then ["theory"]
else Keyword.command_tags keywords cmd_name;
val command_tags =
the_list (AList.lookup (op =) document_tags_command cmd_name) @
keyword_tags @ document_tags_default;
val active_tag' =
(case command_tags of
default_tag :: _ => SOME default_tag
| [] =>
if Keyword.is_vacuous keywords cmd_name andalso Toplevel.is_proof state
then active_tag
else NONE);
in active_tag' end
end;
fun present_span command_tag span state state'
(tagging_stack, active_tag, newline, latex, present_cont) =
let
val ctxt' = Toplevel.presentation_context state';
val present = fold (fn (tok, (flag, 0)) =>
fold cons (present_token ctxt' tok)
#> cons (Latex.string flag)
| _ => I);
val Span ((cmd_name, cmd_pos), srcs, span_newline) = span;
val (tag', tagging_stack') = document_tag cmd_pos state state' tagging_stack;
val active_tag' =
if is_some tag' then Option.map #1 tag'
else command_tag cmd_name state state' active_tag;
val edge = (active_tag, active_tag');
val newline' =
if is_none active_tag' then span_newline else newline;
val latex' =
latex
|> end_tag edge
|> close_delim (fst present_cont) edge
|> snd present_cont
|> open_delim (present (#1 srcs)) edge
|> begin_tag edge
|> present (#2 srcs);
val present_cont' =
if newline then (present (#3 srcs), present (#4 srcs))
else (I, present (#3 srcs) #> present (#4 srcs));
in (tagging_stack', active_tag', newline', latex', present_cont') end;
fun present_trailer ((_, tags), active_tag, _, latex, present_cont) =
if not (null tags) then err_bad_nesting " at end of theory"
else
latex
|> end_tag (active_tag, NONE)
|> close_delim (fst present_cont) (active_tag, NONE)
|> snd present_cont;
end;
(* present_thy *)
local
val markup_true = "\\isamarkuptrue%\n";
val markup_false = "\\isamarkupfalse%\n";
val opt_newline = Scan.option (Scan.one Token.is_newline);
val ignore =
Scan.depend (fn d => opt_newline |-- Scan.one Token.is_begin_ignore
>> pair (d + 1)) ||
Scan.depend (fn d => Scan.one Token.is_end_ignore --|
(if d = 0 then Scan.fail_with (K (fn () => "Bad nesting of meta-comments")) else opt_newline)
>> pair (d - 1));
val locale =
Scan.option ((Parse.$$$ "(" -- Document_Source.improper -- Parse.$$$ "in") |--
Parse.!!!
(Document_Source.improper |-- Parse.name --| (Document_Source.improper -- Parse.$$$ ")")));
in
type segment = {span: Command_Span.span, command: Toplevel.transition, state: Toplevel.state};
fun present_thy options thy (segments: segment list) =
let
val keywords = Thy_Header.get_keywords thy;
(* tokens *)
val ignored = Scan.state --| ignore
>> (fn d => (NONE, (Ignore, ("", d))));
fun markup pred mk flag = Scan.peek (fn d =>
Document_Source.improper |--
Parse.position (Scan.one (fn tok =>
Token.is_command tok andalso pred keywords (Token.content_of tok))) --
(Document_Source.annotation |--
Parse.!!!! ((Document_Source.improper -- locale -- Document_Source.improper) |--
Parse.document_source --| Document_Source.improper_end))
>> (fn ((tok, pos'), source) =>
let val name = Token.content_of tok
in (SOME (name, pos'), (mk (name, source), (flag, d))) end));
val command = Scan.peek (fn d =>
Scan.optional (Scan.one Token.is_command_modifier ::: Document_Source.improper) [] --
Scan.one Token.is_command --| Document_Source.annotation
>> (fn (cmd_mod, cmd) =>
map (fn tok => (NONE, (Token tok, ("", d)))) cmd_mod @
[(SOME (Token.content_of cmd, Token.pos_of cmd),
(Token cmd, (markup_false, d)))]));
val cmt = Scan.peek (fn d =>
Scan.one Document_Source.is_black_comment >> (fn tok => (NONE, (Token tok, ("", d)))));
val other = Scan.peek (fn d =>
Parse.not_eof >> (fn tok => (NONE, (Token tok, ("", d)))));
val tokens =
(ignored ||
markup Keyword.is_document_heading Heading markup_true ||
markup Keyword.is_document_body Body markup_true ||
markup Keyword.is_document_raw (Raw o #2) "") >> single ||
command ||
(cmt || other) >> single;
(* spans *)
val is_eof = fn (_, (Token x, _)) => Token.is_eof x | _ => false;
val stopper = Scan.stopper (K (NONE, (Token Token.eof, ("", 0)))) is_eof;
val cmd = Scan.one (is_some o fst);
val non_cmd = Scan.one (is_none o fst andf not o is_eof) >> #2;
val white_comments = Scan.many (white_comment_token o fst o snd);
val blank = Scan.one (blank_token o fst o snd);
val newline = Scan.one (newline_token o fst o snd);
val before_cmd =
Scan.option (newline -- white_comments) --
Scan.option (newline -- white_comments) --
Scan.option (blank -- white_comments) -- cmd;
val span =
Scan.repeat non_cmd -- cmd --
Scan.repeat (Scan.unless before_cmd non_cmd) --
Scan.option (newline >> (single o snd))
>> (fn (((toks1, (cmd, tok2)), toks3), tok4) =>
make_span (the cmd) (toks1 @ (tok2 :: (toks3 @ the_default [] tok4))));
val spans = segments
|> maps (Command_Span.content o #span)
|> drop_suffix Token.is_space
|> Source.of_list
|> Source.source' 0 Token.stopper (Scan.error (Scan.bulk tokens >> flat))
|> Source.source stopper (Scan.error (Scan.bulk span))
|> Source.exhaust;
val command_results =
segments |> map_filter (fn {command, state, ...} =>
if Toplevel.is_ignored command then NONE else SOME (command, state));
(* present commands *)
val command_tag = make_command_tag options keywords;
fun present_command tr span st st' =
Toplevel.setmp_thread_position tr (present_span command_tag span st st');
fun present _ [] = I
| present st ((span, (tr, st')) :: rest) = present_command tr span st st' #> present st' rest;
in
if length command_results = length spans then
(([], []), NONE, true, [], (I, I))
|> present (Toplevel.init_toplevel ()) (spans ~~ command_results)
|> present_trailer
|> rev
else error "Messed-up outer syntax for presentation"
end;
end;
(** standard output operations **)
(* pretty printing *)
fun pretty_term ctxt t =
Syntax.pretty_term (Proof_Context.augment t ctxt) t;
fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
(* default output *)
val lines = separate (Latex.string "\\isanewline%\n");
val items = separate (Latex.string "\\isasep\\isanewline%\n");
fun isabelle ctxt body =
if Config.get ctxt Document_Antiquotation.thy_output_display
then Latex.environment_block "isabelle" body
else Latex.block (Latex.enclose_body "\\isa{" "}" body);
fun isabelle_typewriter ctxt body =
if Config.get ctxt Document_Antiquotation.thy_output_display
then Latex.environment_block "isabellett" body
else Latex.block (Latex.enclose_body "\\isatt{" "}" body);
fun typewriter ctxt s =
isabelle_typewriter ctxt [Latex.string (Latex.output_ascii s)];
fun verbatim ctxt =
if Config.get ctxt Document_Antiquotation.thy_output_display
then Document_Antiquotation.indent_lines ctxt #> typewriter ctxt
else split_lines #> map (typewriter ctxt) #> lines #> Latex.block;
fun token_source ctxt {embedded} tok =
if Token.is_kind Token.Cartouche tok andalso embedded andalso
not (Config.get ctxt Document_Antiquotation.thy_output_source_cartouche)
then Token.content_of tok
else Token.unparse tok;
fun is_source ctxt =
Config.get ctxt Document_Antiquotation.thy_output_source orelse
Config.get ctxt Document_Antiquotation.thy_output_source_cartouche;
fun source ctxt embedded =
Token.args_of_src
#> map (token_source ctxt embedded #> Document_Antiquotation.prepare_lines ctxt)
#> space_implode " "
#> output_source ctxt
#> isabelle ctxt;
fun pretty ctxt =
Document_Antiquotation.output ctxt #> Latex.string #> single #> isabelle ctxt;
fun pretty_source ctxt embedded src prt =
if is_source ctxt then source ctxt embedded src else pretty ctxt prt;
fun pretty_items ctxt =
map (Document_Antiquotation.output ctxt #> Latex.string) #> items #> isabelle ctxt;
fun pretty_items_source ctxt embedded src prts =
if is_source ctxt then source ctxt embedded src else pretty_items ctxt prts;
(* antiquotation variants *)
local
fun gen_setup name embedded =
if embedded
then Document_Antiquotation.setup_embedded name
else Document_Antiquotation.setup name;
fun gen_antiquotation_pretty name embedded scan f =
gen_setup name embedded scan (fn {context = ctxt, argument = x, ...} => pretty ctxt (f ctxt x));
fun gen_antiquotation_pretty_source name embedded scan f =
gen_setup name embedded scan
(fn {context = ctxt, source = src, argument = x} =>
pretty_source ctxt {embedded = embedded} src (f ctxt x));
fun gen_antiquotation_raw name embedded scan f =
gen_setup name embedded scan (fn {context = ctxt, argument = x, ...} => f ctxt x);
fun gen_antiquotation_verbatim name embedded scan f =
gen_antiquotation_raw name embedded scan (fn ctxt => verbatim ctxt o f ctxt);
in
fun antiquotation_pretty name = gen_antiquotation_pretty name false;
fun antiquotation_pretty_embedded name = gen_antiquotation_pretty name true;
fun antiquotation_pretty_source name = gen_antiquotation_pretty_source name false;
fun antiquotation_pretty_source_embedded name = gen_antiquotation_pretty_source name true;
fun antiquotation_raw name = gen_antiquotation_raw name false;
fun antiquotation_raw_embedded name = gen_antiquotation_raw name true;
fun antiquotation_verbatim name = gen_antiquotation_verbatim name false;
fun antiquotation_verbatim_embedded name = gen_antiquotation_verbatim name true;
end;
end;

590
src/patches/thy_output.ML
View File

@ -1,590 +0,0 @@
(* Title: Pure/Thy/thy_output.ML
Author: Makarius
Theory document output.
This is a modified/patched version that supports Isabelle/DOF.
*)
signature THY_OUTPUT =
sig
val output_document: Proof.context -> {markdown: bool} -> Input.source -> Latex.text list
val check_comments: Proof.context -> Symbol_Pos.T list -> unit
val output_token: Proof.context -> Token.T -> Latex.text list
val output_source: Proof.context -> string -> Latex.text list
type segment = {span: Command_Span.span, command: Toplevel.transition, state: Toplevel.state}
val present_thy: Options.T -> theory -> segment list -> Latex.text list
val set_meta_args_parser : (theory -> string parser) -> unit
val pretty_term: Proof.context -> term -> Pretty.T
val pretty_thm: Proof.context -> thm -> Pretty.T
val lines: Latex.text list -> Latex.text list
val items: Latex.text list -> Latex.text list
val isabelle: Proof.context -> Latex.text list -> Latex.text
val isabelle_typewriter: Proof.context -> Latex.text list -> Latex.text
val typewriter: Proof.context -> string -> Latex.text
val verbatim: Proof.context -> string -> Latex.text
val source: Proof.context -> {embedded: bool} -> Token.src -> Latex.text
val pretty: Proof.context -> Pretty.T -> Latex.text
val pretty_source: Proof.context -> {embedded: bool} -> Token.src -> Pretty.T -> Latex.text
val pretty_items: Proof.context -> Pretty.T list -> Latex.text
val pretty_items_source: Proof.context -> {embedded: bool} -> Token.src ->
Pretty.T list -> Latex.text
val antiquotation_pretty:
binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
val antiquotation_pretty_embedded:
binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
val antiquotation_pretty_source:
binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
val antiquotation_pretty_source_embedded:
binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
val antiquotation_raw:
binding -> 'a context_parser -> (Proof.context -> 'a -> Latex.text) -> theory -> theory
val antiquotation_raw_embedded:
binding -> 'a context_parser -> (Proof.context -> 'a -> Latex.text) -> theory -> theory
val antiquotation_verbatim:
binding -> 'a context_parser -> (Proof.context -> 'a -> string) -> theory -> theory
val antiquotation_verbatim_embedded:
binding -> 'a context_parser -> (Proof.context -> 'a -> string) -> theory -> theory
end;
structure Thy_Output: THY_OUTPUT =
struct
(* output document source *)
val output_symbols = single o Latex.symbols_output;
fun output_comment ctxt (kind, syms) =
(case kind of
Comment.Comment =>
Input.cartouche_content syms
|> output_document (ctxt |> Config.put Document_Antiquotation.thy_output_display false)
{markdown = false}
|> Latex.enclose_body "%\n\\isamarkupcmt{" "%\n}"
| Comment.Cancel =>
Symbol_Pos.cartouche_content syms
|> output_symbols
|> Latex.enclose_body "%\n\\isamarkupcancel{" "}"
| Comment.Latex => [Latex.symbols (Symbol_Pos.cartouche_content syms)]
| Comment.Marker => [])
and output_comment_document ctxt (comment, syms) =
(case comment of
SOME kind => output_comment ctxt (kind, syms)
| NONE => [Latex.symbols syms])
and output_document_text ctxt syms =
Comment.read_body syms |> maps (output_comment_document ctxt)
and output_document ctxt {markdown} source =
let
val pos = Input.pos_of source;
val syms = Input.source_explode source;
val output_antiquotes =
maps (Document_Antiquotation.evaluate (output_document_text ctxt) ctxt);
fun output_line line =
(if Markdown.line_is_item line then [Latex.string "\\item "] else []) @
output_antiquotes (Markdown.line_content line);
fun output_block (Markdown.Par lines) =
Latex.block (separate (Latex.string "\n") (map (Latex.block o output_line) lines))
| output_block (Markdown.List {kind, body, ...}) =
Latex.environment_block (Markdown.print_kind kind) (output_blocks body)
and output_blocks blocks = separate (Latex.string "\n\n") (map output_block blocks);
in
if Toplevel.is_skipped_proof (Toplevel.presentation_state ctxt) then []
else if markdown andalso exists (Markdown.is_control o Symbol_Pos.symbol) syms
then
let
val ants = Antiquote.parse_comments pos syms;
val reports = Antiquote.antiq_reports ants;
val blocks = Markdown.read_antiquotes ants;
val _ = Context_Position.reports ctxt (reports @ Markdown.reports blocks);
in output_blocks blocks end
else
let
val ants = Antiquote.parse_comments pos (trim (Symbol.is_blank o Symbol_Pos.symbol) syms);
val reports = Antiquote.antiq_reports ants;
val _ = Context_Position.reports ctxt (reports @ Markdown.text_reports ants);
in output_antiquotes ants end
end;
(* output tokens with formal comments *)
local
val output_symbols_antiq =
(fn Antiquote.Text syms => output_symbols syms
| Antiquote.Control {name = (name, _), body, ...} =>
Latex.string (Latex.output_symbols [Symbol.encode (Symbol.Control name)]) ::
output_symbols body
| Antiquote.Antiq {body, ...} =>
Latex.enclose_body "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n" (output_symbols body));
fun output_comment_symbols ctxt {antiq} (comment, syms) =
(case (comment, antiq) of
(NONE, false) => output_symbols syms
| (NONE, true) =>
Antiquote.parse_comments (#1 (Symbol_Pos.range syms)) syms
|> maps output_symbols_antiq
| (SOME comment, _) => output_comment ctxt (comment, syms));
fun output_body ctxt antiq bg en syms =
Comment.read_body syms
|> maps (output_comment_symbols ctxt {antiq = antiq})
|> Latex.enclose_body bg en;
in
fun output_token ctxt tok =
let
fun output antiq bg en =
output_body ctxt antiq bg en (Input.source_explode (Token.input_of tok));
in
(case Token.kind_of tok of
Token.Comment NONE => []
| Token.Comment (SOME Comment.Marker) => []
| Token.Command => output false "\\isacommand{" "}"
| Token.Keyword =>
if Symbol.is_ascii_identifier (Token.content_of tok)
then output false "\\isakeyword{" "}"
else output false "" ""
| Token.String => output false "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}"
| Token.Alt_String => output false "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}"
| Token.Verbatim => output true "{\\isacharverbatimopen}" "{\\isacharverbatimclose}"
| Token.Cartouche => output false "{\\isacartoucheopen}" "{\\isacartoucheclose}"
| _ => output false "" "")
end handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok));
fun output_source ctxt s =
output_body ctxt false "" "" (Symbol_Pos.explode (s, Position.none));
fun check_comments ctxt =
Comment.read_body #> List.app (fn (comment, syms) =>
let
val pos = #1 (Symbol_Pos.range syms);
val _ =
comment |> Option.app (fn kind =>
Context_Position.reports ctxt (map (pair pos) (Markup.cartouche :: Comment.kind_markups kind)));
val _ = output_comment_symbols ctxt {antiq = false} (comment, syms);
in if comment = SOME Comment.Comment then check_comments ctxt syms else () end);
end;
(** present theory source **)
(* presentation tokens *)
datatype token =
Ignore
| Token of Token.T
| Heading of string * string * Input.source
| Body of string * string * Input.source
| Raw of Input.source;
fun token_with pred (Token tok) = pred tok
| token_with _ _ = false;
val white_token = token_with Document_Source.is_white;
val white_comment_token = token_with Document_Source.is_white_comment;
val blank_token = token_with Token.is_blank;
val newline_token = token_with Token.is_newline;
fun present_token ctxt tok =
(case tok of
Ignore => []
| Token tok => output_token ctxt tok
| Heading (cmd, meta_args, source) =>
Latex.enclose_body ("%\n\\isamarkup" ^ cmd (* ^ meta_args *) ^ "{") "%\n}\n"
(output_document ctxt {markdown = false} source)
| Body (cmd, meta_args, source) =>
[Latex.environment_block
("isamarkup" ^ cmd (* ^ meta_args*))
(Latex.string meta_args :: output_document ctxt {markdown = true} source)]
| Raw source =>
Latex.string "%\n" :: output_document ctxt {markdown = true} source @ [Latex.string "\n"]);
(* command spans *)
type command = string * Position.T; (*name, position*)
type source = (token * (string * int)) list; (*token, markup flag, meta-comment depth*)
datatype span = Span of command * (source * source * source * source) * bool;
fun make_span cmd src =
let
fun chop_newline (tok :: toks) =
if newline_token (fst tok) then ([tok], toks, true)
else ([], tok :: toks, false)
| chop_newline [] = ([], [], false);
val (((src_prefix, src_main), src_suffix1), (src_suffix2, src_appendix, newline)) =
src
|> chop_prefix (white_token o fst)
||>> chop_suffix (white_token o fst)
||>> chop_prefix (white_comment_token o fst)
||> chop_newline;
in Span (cmd, (src_prefix, src_main, src_suffix1 @ src_suffix2, src_appendix), newline) end;
(* present spans *)
local
fun err_bad_nesting here =
error ("Bad nesting of commands in presentation" ^ here);
fun edge which f (x: string option, y) =
if x = y then I
else (case which (x, y) of NONE => I | SOME txt => cons (Latex.string (f txt)));
val begin_tag = edge #2 Latex.begin_tag;
val end_tag = edge #1 Latex.end_tag;
fun open_delim delim e = edge #2 Latex.begin_delim e #> delim #> edge #2 Latex.end_delim e;
fun close_delim delim e = edge #1 Latex.begin_delim e #> delim #> edge #1 Latex.end_delim e;
fun document_tag cmd_pos state state' tagging_stack =
let
val ctxt' = Toplevel.presentation_context state';
val nesting = Toplevel.level state' - Toplevel.level state;
val (tagging, taggings) = tagging_stack;
val (tag', tagging') = Document_Source.update_tagging ctxt' tagging;
val tagging_stack' =
if nesting = 0 andalso not (Toplevel.is_proof state) then tagging_stack
else if nesting >= 0 then (tagging', replicate nesting tagging @ taggings)
else
(case drop (~ nesting - 1) taggings of
tg :: tgs => (tg, tgs)
| [] => err_bad_nesting (Position.here cmd_pos));
in (tag', tagging_stack') end;
fun read_tag s =
(case space_explode "%" s of
["", b] => (SOME b, NONE)
| [a, b] => (NONE, SOME (a, b))
| _ => error ("Bad document_tags specification: " ^ quote s));
in
fun make_command_tag options keywords =
let
val document_tags =
map read_tag (space_explode "," (Options.string options \<^system_option>\<open>document_tags\<close>));
val document_tags_default = map_filter #1 document_tags;
val document_tags_command = map_filter #2 document_tags;
in
fn cmd_name => fn state => fn state' => fn active_tag =>
let
val keyword_tags =
if cmd_name = "end" andalso Toplevel.is_end_theory state' then ["theory"]
else Keyword.command_tags keywords cmd_name;
val command_tags =
the_list (AList.lookup (op =) document_tags_command cmd_name) @
keyword_tags @ document_tags_default;
val active_tag' =
(case command_tags of
default_tag :: _ => SOME default_tag
| [] =>
if Keyword.is_vacuous keywords cmd_name andalso Toplevel.is_proof state
then active_tag
else NONE);
in active_tag' end
end;
fun present_span command_tag span state state'
(tagging_stack, active_tag, newline, latex, present_cont) =
let
val ctxt' = Toplevel.presentation_context state';
val present = fold (fn (tok, (flag, 0)) =>
fold cons (present_token ctxt' tok)
#> cons (Latex.string flag)
| _ => I);
val Span ((cmd_name, cmd_pos), srcs, span_newline) = span;
val (tag', tagging_stack') = document_tag cmd_pos state state' tagging_stack;
val active_tag' =
if is_some tag' then Option.map #1 tag'
else command_tag cmd_name state state' active_tag;
val edge = (active_tag, active_tag');
val newline' =
if is_none active_tag' then span_newline else newline;
val latex' =
latex
|> end_tag edge
|> close_delim (fst present_cont) edge
|> snd present_cont
|> open_delim (present (#1 srcs)) edge
|> begin_tag edge
|> present (#2 srcs);
val present_cont' =
if newline then (present (#3 srcs), present (#4 srcs))
else (I, present (#3 srcs) #> present (#4 srcs));
in (tagging_stack', active_tag', newline', latex', present_cont') end;
fun present_trailer ((_, tags), active_tag, _, latex, present_cont) =
if not (null tags) then err_bad_nesting " at end of theory"
else
latex
|> end_tag (active_tag, NONE)
|> close_delim (fst present_cont) (active_tag, NONE)
|> snd present_cont;
end;
(* present_thy *)
local
val markup_true = "\\isamarkuptrue%\n";
val markup_false = "\\isamarkupfalse%\n";
val opt_newline = Scan.option (Scan.one Token.is_newline);
val ignore =
Scan.depend (fn d => opt_newline |-- Scan.one Token.is_begin_ignore
>> pair (d + 1)) ||
Scan.depend (fn d => Scan.one Token.is_end_ignore --|
(if d = 0 then Scan.fail_with (K (fn () => "Bad nesting of meta-comments")) else opt_newline)
>> pair (d - 1));
val locale =
Scan.option ((Parse.$$$ "(" -- Document_Source.improper -- Parse.$$$ "in") |--
Parse.!!!
(Document_Source.improper |-- Parse.name --| (Document_Source.improper -- Parse.$$$ ")")));
(*
val meta_args_parser_hook = Synchronized.var "meta args parser hook"
((fn thy => fn s => ("",s)): theory -> string parser);
*)
val meta_args_parser_hook = Unsynchronized.ref ((fn _ => fn s => ("",s)): theory -> string parser);
in
type segment = {span: Command_Span.span, command: Toplevel.transition, state: Toplevel.state};
fun present_thy options thy (segments: segment list) =
let
val keywords = Thy_Header.get_keywords thy;
(* tokens *)
val ignored = Scan.state --| ignore
>> (fn d => (NONE, (Ignore, ("", d))));
fun markup pred mk flag = Scan.peek (fn d =>
Document_Source.improper
|-- Parse.position (Scan.one (fn tok => Token.is_command tok andalso
pred keywords (Token.content_of tok)))
-- (Document_Source.annotation |--
(Parse.!!!!
( ( (!meta_args_parser_hook thy))
-- ( (Document_Source.improper -- locale -- Document_Source.improper)
|-- Parse.document_source )
--| Document_Source.improper_end)
)
)
>> (fn ((tok, pos'), (meta_args, source)) =>
let val name = Token.content_of tok
in (SOME (name, pos'), (mk (name, meta_args , source), (flag, d))) end));
val command = Scan.peek (fn d =>
Scan.optional (Scan.one Token.is_command_modifier ::: Document_Source.improper) [] --
Scan.one Token.is_command --| Document_Source.annotation
>> (fn (cmd_mod, cmd) =>
map (fn tok => (NONE, (Token tok, ("", d)))) cmd_mod @
[(SOME (Token.content_of cmd, Token.pos_of cmd),
(Token cmd, (markup_false, d)))]));
val cmt = Scan.peek (fn d =>
Scan.one Document_Source.is_black_comment >> (fn tok => (NONE, (Token tok, ("", d)))));
val other = Scan.peek (fn d =>
Parse.not_eof >> (fn tok => (NONE, (Token tok, ("", d)))));
val tokens =
(ignored ||
markup Keyword.is_document_heading Heading markup_true ||
markup Keyword.is_document_body Body markup_true ||
markup Keyword.is_document_raw (Raw o #3) "") >> single ||
command ||
(cmt || other) >> single;
(* spans *)
val is_eof = fn (_, (Token x, _)) => Token.is_eof x | _ => false;
val stopper = Scan.stopper (K (NONE, (Token Token.eof, ("", 0)))) is_eof;
val cmd = Scan.one (is_some o fst);
val non_cmd = Scan.one (is_none o fst andf not o is_eof) >> #2;
val white_comments = Scan.many (white_comment_token o fst o snd);
val blank = Scan.one (blank_token o fst o snd);
val newline = Scan.one (newline_token o fst o snd);
val before_cmd =
Scan.option (newline -- white_comments) --
Scan.option (newline -- white_comments) --
Scan.option (blank -- white_comments) -- cmd;
val span =
Scan.repeat non_cmd -- cmd --
Scan.repeat (Scan.unless before_cmd non_cmd) --
Scan.option (newline >> (single o snd))
>> (fn (((toks1, (cmd, tok2)), toks3), tok4) =>
make_span (the cmd) (toks1 @ (tok2 :: (toks3 @ the_default [] tok4))));
val spans = segments
|> maps (Command_Span.content o #span)
|> drop_suffix Token.is_space
|> Source.of_list
|> Source.source' 0 Token.stopper (Scan.error (Scan.bulk tokens >> flat))
|> Source.source stopper (Scan.error (Scan.bulk span))
|> Source.exhaust;
val command_results =
segments |> map_filter (fn {command, state, ...} =>
if Toplevel.is_ignored command then NONE else SOME (command, state));
(* present commands *)
val command_tag = make_command_tag options keywords;
fun present_command tr span st st' =
Toplevel.setmp_thread_position tr (present_span command_tag span st st');
fun present _ [] = I
| present st ((span, (tr, st')) :: rest) = present_command tr span st st' #> present st' rest;
in
if length command_results = length spans then
(([], []), NONE, true, [], (I, I))
|> present (Toplevel.init_toplevel ()) (spans ~~ command_results)
|> present_trailer
|> rev
else error "Messed-up outer syntax for presentation"
end;
fun set_meta_args_parser f =
let
val _ = writeln "Meta-args parser set to new value"
in
(meta_args_parser_hook := f)
end
end;
(** standard output operations **)
(* pretty printing *)
fun pretty_term ctxt t =
Syntax.pretty_term (Proof_Context.augment t ctxt) t;
fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
(* default output *)
val lines = separate (Latex.string "\\isanewline%\n");
val items = separate (Latex.string "\\isasep\\isanewline%\n");
fun isabelle ctxt body =
if Config.get ctxt Document_Antiquotation.thy_output_display
then Latex.environment_block "isabelle" body
else Latex.block (Latex.enclose_body "\\isa{" "}" body);
fun isabelle_typewriter ctxt body =
if Config.get ctxt Document_Antiquotation.thy_output_display
then Latex.environment_block "isabellett" body
else Latex.block (Latex.enclose_body "\\isatt{" "}" body);
fun typewriter ctxt s =
isabelle_typewriter ctxt [Latex.string (Latex.output_ascii s)];
fun verbatim ctxt =
if Config.get ctxt Document_Antiquotation.thy_output_display
then Document_Antiquotation.indent_lines ctxt #> typewriter ctxt
else split_lines #> map (typewriter ctxt) #> lines #> Latex.block;
fun token_source ctxt {embedded} tok =
if Token.is_kind Token.Cartouche tok andalso embedded andalso
not (Config.get ctxt Document_Antiquotation.thy_output_source_cartouche)
then Token.content_of tok
else Token.unparse tok;
fun is_source ctxt =
Config.get ctxt Document_Antiquotation.thy_output_source orelse
Config.get ctxt Document_Antiquotation.thy_output_source_cartouche;
fun source ctxt embedded =
Token.args_of_src
#> map (token_source ctxt embedded #> Document_Antiquotation.prepare_lines ctxt)
#> space_implode " "
#> output_source ctxt
#> isabelle ctxt;
fun pretty ctxt =
Document_Antiquotation.output ctxt #> Latex.string #> single #> isabelle ctxt;
fun pretty_source ctxt embedded src prt =
if is_source ctxt then source ctxt embedded src else pretty ctxt prt;
fun pretty_items ctxt =
map (Document_Antiquotation.output ctxt #> Latex.string) #> items #> isabelle ctxt;
fun pretty_items_source ctxt embedded src prts =
if is_source ctxt then source ctxt embedded src else pretty_items ctxt prts;
(* antiquotation variants *)
local
fun gen_setup name embedded =
if embedded
then Document_Antiquotation.setup_embedded name
else Document_Antiquotation.setup name;
fun gen_antiquotation_pretty name embedded scan f =
gen_setup name embedded scan (fn {context = ctxt, argument = x, ...} => pretty ctxt (f ctxt x));
fun gen_antiquotation_pretty_source name embedded scan f =
gen_setup name embedded scan
(fn {context = ctxt, source = src, argument = x} =>
pretty_source ctxt {embedded = embedded} src (f ctxt x));
fun gen_antiquotation_raw name embedded scan f =
gen_setup name embedded scan (fn {context = ctxt, argument = x, ...} => f ctxt x);
fun gen_antiquotation_verbatim name embedded scan f =
gen_antiquotation_raw name embedded scan (fn ctxt => verbatim ctxt o f ctxt);
in
fun antiquotation_pretty name = gen_antiquotation_pretty name false;
fun antiquotation_pretty_embedded name = gen_antiquotation_pretty name true;
fun antiquotation_pretty_source name = gen_antiquotation_pretty_source name false;
fun antiquotation_pretty_source_embedded name = gen_antiquotation_pretty_source name true;
fun antiquotation_raw name = gen_antiquotation_raw name false;
fun antiquotation_raw_embedded name = gen_antiquotation_raw name true;
fun antiquotation_verbatim name = gen_antiquotation_verbatim name false;
fun antiquotation_verbatim_embedded name = gen_antiquotation_verbatim name true;
end;
end;

80
src/scala/dof_document_build.scala Normal file
View File

@ -0,0 +1,80 @@
/*
* 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._
object DOF_Document_Build
{
class Engine extends Document_Build.Bash_Engine("dof")
{
override def use_build_script: Boolean = true
override def prepare_directory(
context: Document_Build.Context,
dir: Path,
doc: Document_Build.Document_Variant): Document_Build.Directory =
{
val latex_output = new Latex_Output(context.options)
val directory = context.prepare_directory(dir, doc, latex_output)
// produced by alternative presentation hook (workaround for missing Toplevel.present_theory)
for (name <- context.document_theories) {
val path = Path.basic(Document_Build.tex_name(name))
val xml =
YXML.parse_body(context.get_export(name.theory, Export.DOCUMENT_LATEX + "_dof").text)
if (xml.nonEmpty) {
File.Content(path, xml).output(latex_output(_, file_pos = path.implode_symbolic))
.write(directory.doc_dir)
}
}
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);
directory
}
}
class Latex_Output(options: Options) extends Latex.Output(options)
{
override def latex_environment(
name: String,
body: Latex.Text,
optional_argument: String = ""): Latex.Text =
{
XML.enclose(
"\n\\begin{" + name + "}" + optional_argument + "\n",
"\n\\end{" + name + "}", body)
}
}
}

69
src/scala/dof_mkroot.scala Normal file
View File

@ -0,0 +1,69 @@
/* Author: Makarius
Prepare session root directory for Isabelle/DOF.
*/
package isabelle_dof
import isabelle._
object DOF_Mkroot
{
/** mkroot **/
def mkroot(
session_name: String = "",
session_dir: Path = Path.current,
session_parent: String = "",
init_repos: Boolean = false,
title: String = "",
author: String = "",
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 tool wrapper **/
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 session_name = ""
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)
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))
val more_args = getopts(args)
val session_dir =
more_args match {
case Nil => Path.current
case List(dir) => Path.explode(dir)
case _ => getopts.usage()
}
mkroot(session_name = session_name, session_dir = session_dir, init_repos = init_repos,
author = author, title = title, progress = new Console_Progress)
})
}

13
src/scala/dof_tools.scala Normal file
View File

@ -0,0 +1,13 @@
/* Author: Makarius
Isabelle/DOF command-line tools.
*/
package isabelle_dof
import isabelle._
class DOF_Tools extends Isabelle_Scala_Tools(
DOF_Mkroot.isabelle_tool
)

135
src/scripts/build
View File

@ -28,20 +28,133 @@
# SPDX-License-Identifier: BSD-2-Clause
set -e
if [ ! -f $ISABELLE_HOME_USER/DOF/document-template/build_lib.sh ]; then
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: Isabelle/DOF not installed"
>&2 echo "Error: Found root file ($DIR/$ROOT_NAME.tex)"
>&2 echo "====="
>&2 echo "This is a Isabelle/DOF project. The document preparation requires"
>&2 echo "the Isabelle/DOF framework. Please obtain the framework by cloning"
>&2 echo "the Isabelle/DOF git repository, i.e.: "
>&2 echo " git clone <isadofurl>"
>&2 echo "You can install the framework as follows:"
>&2 echo " cd Isabelle_DOF/document-generator"
>&2 echo " ./install"
>&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
cp $ISABELLE_HOME_USER/DOF/document-template/build_lib.sh .
source build_lib.sh
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

169
src/scripts/build_lib.sh
View File

@ -1,169 +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
OUTFORMAT=${1:-pdf}
NAME=${2:-root}
set -e
ROOT_NAME="root_$NAME"
[ ! -f "$DIR/$ROOT_NAME.tex" ] && ROOT_NAME="root"
if [ ! -f $ISABELLE_HOME_USER/DOF/document-template/DOF-core.sty ]; then
>&2 echo ""
>&2 echo "Error: Isabelle/DOF not installed"
>&2 echo "====="
>&2 echo "This is a Isabelle/DOF project. The document preparation requires"
>&2 echo "the Isabelle/DOF framework. Please obtain the framework by cloning"
>&2 echo "the Isabelle/DOF git repository, i.e.: "
>&2 echo " git clone <isadofurl>"
>&2 echo "You can install the framework as follows:"
>&2 echo " cd Isabelle_DOF/document-generator"
>&2 echo " ./install"
>&2 echo ""
exit 1
fi
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 "$DIR/ontologies.tex" ]; then
>&2 echo ""
>&2 echo "Error: Old project setup, found a ontologies file ($DIR/ontologies.tex)"
>&2 echo "====="
>&2 echo "Isabelle/DOF does no longer support the use of $DIR/ontologies.tex. The"
>&2 echo "required ontologies should be defined in $DIR/isadof.cfg."
>&2 echo ""
exit 1
fi
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 make use of the Isabelle root file mechanism."
>&2 echo "Please check your Isabelle/DOF setup."
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
ROOT="$ISABELLE_HOME_USER/DOF/document-template/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
cp $ISABELLE_HOME_USER/DOF/latex/*.sty .
cp $ISABELLE_HOME_USER/DOF/document-template/*.sty .
cp $ISABELLE_HOME_USER/DOF/document-template/*.cls .
# delete outdated aux files from previous runs
rm -f *.aux
sed -i -e 's/<@>/@/g' *.tex
$ISABELLE_TOOL latex -o sty "root.tex" && \
$ISABELLE_TOOL latex -o "$OUTFORMAT" "root.tex" && \
{ [ ! -f "$ROOT_NAME.bib" ] || $ISABELLE_TOOL latex -o bbl "root.tex"; } && \
{ [ ! -f "$ROOT_NAME.idx" ] || $ISABELLE_TOOL latex -o idx "root.tex"; } && \
$ISABELLE_TOOL latex -o "$OUTFORMAT" "root.tex" && \
$ISABELLE_TOOL latex -o "$OUTFORMAT" "root.tex"
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

11
src/tests/AssnsLemmaThmEtc.thy
View File

@ -29,10 +29,15 @@ print_doc_items
section\<open>Definitions, Lemmas, Theorems, Assertions\<close>
term\<open>True\<close>
text*[aa::F, properties = "[@{term ''True''}]"]
\<open>Our definition of the HOL-Logic has the following properties:\<close>
assert*[aa::F] "True"
assert*\<open>F.properties @{F \<open>aa\<close>} = [@{term ''True''}]\<close>
text\<open>For now, as the term annotation is not bound to a meta logic which will translate
\<^term>\<open>[@{term ''True''}]\<close> to \<^term>\<open>[True]\<close>, we can not use the HOL \<^const>\<open>True\<close> constant
in the assertion.
\<close>
(* does not work in batch mode ...
(* sample for accessing a property filled with previous assert's of "aa" *)
@ -70,7 +75,7 @@ different class. "F" and "assertion" have only in common that they posses the at
text\<open>Creation just like that: \<close>
assert*[ababa::assertion] "3 < (4::int)"
assert*[ababa::assertion] "0 < (4::int)"
assert*[ababab::assertion] "0 < (4::int)"
end

52
src/tests/Evaluation.thy
View File

@ -6,14 +6,19 @@ theory
Evaluation
imports
"Isabelle_DOF-tests.TermAntiquotations"
"Isabelle_DOF-tests.High_Level_Syntax_Invariants"
begin
section\<open>\<^theory_text>\<open>ML*\<close>-Annotated SML-commands\<close>
ML*[the_function::B,x=\<open>\<open>dfg\<close>\<close>]\<open>fun fac x = if x = 0 then 1 else x * fac(x-1);
val t = @{const_name "List.Nil"}\<close>
ML\<open>fac 5; t\<close> \<comment> \<open>this is a test that ML* is actually evaluated and the
resulting toplevel state is preserved.\<close>
ML*\<open>3+4\<close> \<comment> \<open>meta-args are optional\<close>
ML*[the_function::C,x=\<open>\<open>dfg\<close>\<close>]\<open>fun fac x = if x = 0 then 1 else x * fac(x-1)\<close>
ML*\<open>3+4\<close> (* meta-args are optional *)
text-macro*[the::C]\<open> @{B [display] "the_function"} \<close>
text\<open>... and here we reference @{B [display] "the_function"}.\<close>
text\<open>... and here we reference @{B [display] \<open>the_function\<close>}.\<close>
section\<open>\<^theory_text>\<open>value*\<close>-Annotated evaluation-commands\<close>
@ -49,15 +54,19 @@ of the current implementation.
section\<open>Term Annotation evaluation\<close>
text\<open>We can validate a term with TA:\<close>
term*\<open>@{thm \<open>HOL.refl\<close>}\<close>
term*[axx::A]\<open>@{thm \<open>HOL.refl\<close>}\<close>
text\<open>check : @{A [display] "axx"}\<close>
text\<open>Now we can evaluate a term with TA:
the current implementation return the term which references the object referenced by the TA.
Here the evualuation of the TA will return the HOL.String which references the theorem:
\<close>
value*\<open>@{thm \<open>HOL.refl\<close>}\<close>
value*\<open>@{thm \<open>HOL.refl\<close>}\<close> \<comment> \<open>syntax check\<close>
value*[a::A]\<open>@{thm \<open>HOL.refl\<close>}\<close> (* using the option *)
value*[axxx::A]\<open>@{thm \<open>HOL.refl\<close>}\<close> \<comment> \<open>defining a reference of class A\<close>
text\<open>check : @{A [display] "axxx"}\<close> \<comment> \<open>using it\<close>
text\<open>An instance class is an object which allows us to define the concepts we want in an ontology.
It is a concept which will be used to implement an ontology. It has roughly the same meaning as
@ -82,8 +91,8 @@ value*\<open>A.x @{A \<open>xcv1\<close>}\<close>
text\<open>If the attribute of the instance is not initialized, we get an undefined value,
whose type is the type of the attribute:\<close>
term*\<open>level @{C \<open>xcv2\<close>}\<close>
value*\<open>level @{C \<open>xcv2\<close>}\<close>
term*\<open>B.level @{C \<open>xcv2\<close>}\<close>
value*\<open>B.level @{C \<open>xcv2\<close>}\<close>
text\<open>The value of a TA is the term itself:\<close>
term*\<open>C.g @{C \<open>xcv2\<close>}\<close>
@ -168,4 +177,31 @@ to update the instance @{docitem \<open>xcv4\<close>}:
update_instance*[xcv4::F, b+="{(@{A ''xcv3''},@{G ''xcv5''})}"]*)
section\<open>\<^theory_text>\<open>assert*\<close>-Annotated assertion-commands\<close>
text\<open>The \<^emph>\<open>assert*\<close>-command allows for logical statements to be checked in the global context.
It uses the same implementation as the \<^emph>\<open>value*\<close>-command and has the same limitations.
\<close>
text\<open>Using the ontology defined in \<^theory>\<open>Isabelle_DOF-tests.High_Level_Syntax_Invariants\<close>
we can check logical statements:\<close>
term*\<open>authored_by @{introduction \<open>introduction2\<close>} = authored_by @{introduction \<open>introduction3\<close>}\<close>
assert*\<open>authored_by @{introduction \<open>introduction2\<close>} = authored_by @{introduction \<open>introduction3\<close>}\<close>
assert*\<open>\<not>(authored_by @{introduction \<open>introduction2\<close>}
= authored_by @{introduction \<open>introduction4\<close>})\<close>
text\<open>Assertions must be boolean expressions, so the following assertion triggers an error:\<close>
(* Error:
assert*\<open>@{introduction \<open>introduction2\<close>}\<close>*)
text\<open>Assertions must be true, hence the error:\<close>
(* Error:
assert*\<open>{@{author \<open>curry\<close>}} = {@{author \<open>church\<close>}}\<close>*)
term*\<open>property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>
assert*\<open>\<not> property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>
assert*\<open>evidence @{result \<open>resultProof\<close>} = evidence @{result \<open>resultProof2\<close>}\<close>
end

37
src/tests/High_Level_Syntax_Invariants.thy
View File

@ -66,6 +66,7 @@ doc_class introduction = text_section +
authored_by :: "author set" <= "UNIV"
uses :: "notion set"
invariant author_finite :: "finite (authored_by \<sigma>)"
and force_level :: "the (level \<sigma>) > 1"
doc_class claim = introduction +
based_on :: "notion list"
@ -83,32 +84,54 @@ doc_class result = technical +
evidence :: kind
property :: "thm list" <= "[]"
invariant has_property :: "evidence \<sigma> = proof \<longleftrightarrow> property \<sigma> \<noteq> []"
doc_class example = technical +
referring_to :: "(notion + definition) set" <= "{}"
doc_class conclusion = text_section +
establish :: "(claim \<times> result) set"
invariant total_rel :: "\<forall> x. x \<in> Domain (establish \<sigma>)
\<longrightarrow> (\<exists> y \<in> Range (establish \<sigma>). (x, y) \<in> establish \<sigma>)"
invariant establish_defined :: "\<forall> x. x \<in> Domain (establish \<sigma>)
\<longrightarrow> (\<exists> y \<in> Range (establish \<sigma>). (x, y) \<in> establish \<sigma>)"
text\<open>Next we define some instances (docitems): \<close>
declare[[invariants_checking_with_tactics = true]]
text*[church::author, email="\<open>church@lambda.org\<close>"]\<open>\<close>
(*text*[introduction1::introduction, authored_by = "{@{author \<open>church\<close>}}", level = "Some 0"]\<open>\<close>*)
text*[resultProof::result, evidence = "proof", property="[@{thm \<open>HOL.refl\<close>}]"]\<open>\<close>
text*[resultArgument::result, evidence = "argument"]\<open>\<close>
text\<open>The invariants \<open>author_finite\<close> and \<open>total_rel\<close> can not be checked directly
text\<open>The invariants \<^theory_text>\<open>author_finite\<close> and \<^theory_text>\<open>establish_defined\<close> can not be checked directly
and need a little help.
We can set the \<open>invariants_checking_with_tactics\<close> theory attribute to help the checking.
It will enable a basic tactic, using unfold and auto:\<close>
declare[[invariants_checking_with_tactics = true]]
text*[introductionTest::introduction, authored_by = "{@{author \<open>church\<close>}}"]\<open>\<close>
text*[curry::author, email="\<open>curry@lambda.org\<close>"]\<open>\<close>
text*[introduction2::introduction, authored_by = "{@{author \<open>church\<close>}}", level = "Some 2"]\<open>\<close>
text*[introduction3::introduction, authored_by = "{@{author \<open>church\<close>}}", level = "Some 2"]\<open>\<close>
text*[introduction4::introduction, authored_by = "{@{author \<open>curry\<close>}}", level = "Some 4"]\<open>\<close>
text*[claimNotion::claim, authored_by = "{@{author \<open>church\<close>}}", based_on= "[\<open>Notion1\<close>, \<open>Notion2\<close>]"]\<open>\<close>
text*[resultProof2::result, evidence = "proof", property="[@{thm \<open>HOL.sym\<close>}]"]\<open>\<close>
text*[conclusionProof::conclusion,
establish = "{(@{claim \<open>claimNotion\<close>}, @{result \<open>resultProof\<close>})}"]\<open>\<close>
text\<open>Then we can evaluate expressions with instances:\<close>
term*\<open>authored_by @{introduction \<open>introduction2\<close>} = authored_by @{introduction \<open>introduction3\<close>}\<close>
value*\<open>authored_by @{introduction \<open>introduction2\<close>} = authored_by @{introduction \<open>introduction3\<close>}\<close>
value*\<open>authored_by @{introduction \<open>introduction2\<close>} = authored_by @{introduction \<open>introduction4\<close>}\<close>
value*\<open>@{introduction \<open>introduction2\<close>}\<close>
value*\<open>{@{author \<open>curry\<close>}} = {@{author \<open>church\<close>}}\<close>
term*\<open>property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>
value*\<open>property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>
value*\<open>evidence @{result \<open>resultProof\<close>} = evidence @{result \<open>resultProof2\<close>}\<close>
declare[[invariants_checking_with_tactics = false]]
end

251
src/tests/Isabelle2021-1.thy Normal file
View File

@ -0,0 +1,251 @@
chapter \<open>Notes on Isabelle/DOF for Isabelle2021-1\<close>
theory "Isabelle2021-1"
imports Main
begin
section \<open>Isabelle/DOF component setup\<close>
subsection \<open>Terminology\<close>
text \<open>
\<^item> The concept of \<^emph>\<open>Isabelle system component\<close> is explained in \<^doc>\<open>system\<close>
section 1.1.1; see also \<^tool>\<open>components\<close> explained in section 7.3.
For example:
\<^verbatim>\<open>isabelle components -l\<close>
\<close>
subsection \<open>Isabelle/DOF as component\<close>
text \<open>
Formal Isabelle/DOF component setup happens here:
\<^item> \<^path>\<open>$ISABELLE_HOME_USER/etc/components\<close>
\<^item> A suitable directory entry in the file registers our component to
existing Isabelle installation; it also activates the session
directory tree starting at \<^file>\<open>$ISABELLE_DOF_HOME/ROOTS\<close>.
\<^item> Alternative: use \<^path>\<open>$ISABELLE_HOME/Admin/build_release\<close> with
option \<^verbatim>\<open>-c\<close> to produce a derived Isabelle distribution that bundles
our component for end-users (maybe even with AFP entries).
\<^item> \<^file>\<open>$ISABELLE_DOF_HOME/etc/settings\<close>
\<^item> This provides a pervasive Bash process environment (variables,
shell functions etc.). It may refer to \<^verbatim>\<open>$COMPONENT\<close> for the
component root, e.g. to retain it in variable \<^dir>\<open>$ISABELLE_DOF_HOME\<close>.
\<^item> Historically, it used to be the main configuration area, but today
we see more and more alternatives, e.g. system options or services in
Isabelle/Scala (see below).
\<^item> \<^file>\<open>$ISABELLE_DOF_HOME/etc/options\<close>
\<^item> options declared as \<^verbatim>\<open>public\<close> appear in the Isabelle/jEdit dialog
\<^action>\<open>plugin-options\<close> (according to their \<^verbatim>\<open>section\<close>)
\<^item> all options (public and non-public) are available for command-line
usage, e.g. \<^verbatim>\<open>isabelle build -o dof_url="..."\<close>
\<^item> access to options in Isabelle/ML:
\<^item> implicit (for the running ML session)
\<^ML>\<open>Options.default_string \<^system_option>\<open>dof_url\<close>\<close>
\<^item> explicit (e.g. for each theories section in
\<^file>\<open>$ISABELLE_HOME/src/Pure/Tools/build.ML\<close>):
\<^ML>\<open>fn options => Options.string options \<^system_option>\<open>dof_url\<close>\<close>
\<^item> access in Isabelle/Scala is always explicit; the initial options
should be created only once and passed around as explicit argument:
\<^scala>\<open>{
val options = isabelle.Options.init();
options.string("dof_url");
}\<close>
Note: there are no antiquotations in Isabelle/Scala, so the literal
string \<^scala>\<open>"dof_url"\<close> is unchecked.
\<close>
section \<open>Document preparation in Isabelle/ML\<close>
subsection \<open>Session presentation hook\<close>
text \<open>
\<^ML>\<open>Build.add_hook\<close> allows to install a global session presentation
hook. It is used e.g. in Isabelle/Mirabelle to analyze all loaded
theories via Sledgehammer and other tools. Isabelle/DOF could use it to
"wrap-up" the whole session, to check if all document constraints hold
(cf. "monitors").
\<close>
subsection \<open>Theory presentation hook\<close>
text \<open>
\<^ML>\<open>Thy_Info.add_presentation\<close> installs a hook to be invoked at the
end of successful loading of theories; the provided context
\<^ML_type>\<open>Thy_Info.presentation_context\<close> provides access to
\<^ML_type>\<open>Options.T\<close> and \<^ML_type>\<open>Document_Output.segment\<close> with
command-spans and semantic states.
An example is regular Latex output in
\<^file>\<open>$ISABELLE_HOME/src/Pure/Thy/thy_info.ML\<close> where \<^ML>\<open>Export.export\<close>
is used to produce export artifacts in the session build database, for
retrieval via Isabelle/Scala.
\<close>
subsection \<open>Document commands\<close>
text \<open>
Isar toplevel commands now support a uniform concept for
\<^ML_type>\<open>Toplevel.presentation\<close>, but the exported interfaces are
limited to commands that do not change the semantic state: see
\<^ML>\<open>Toplevel.present\<close> and \<^ML>\<open>Toplevel.present_local_theory\<close>.
Since \<^verbatim>\<open>Toplevel.present_theory\<close> is missing in Isabelle2021-1, we use a
workaround with an alternative presentation hook: it exports
\<^verbatim>\<open>document/latex_dof\<close> files instead of regular \<^verbatim>\<open>document/latex_dof\<close>.
\<close>
subsection \<open>Document content\<close>
text \<open>
XML is now used uniformly (sometimes as inlined YXML). The meaning of
markup elements and properties is defined in
\<^scala_type>\<open>isabelle.Latex.Output\<close> (or user-defined subclasses).
\<close>
section \<open>Isabelle/Scala services\<close>
subsection \<open>Isabelle/DOF/Scala module\<close>
text \<open>
\<^item> \<^file>\<open>$ISABELLE_DOF_HOME/etc/build.props\<close> is the main specification for
the Isabelle/DOF/Scala module. It is built on the spot as required, e.g.
for \<^verbatim>\<open>isabelle scala\<close> or \<^verbatim>\<open>isabelle jedit\<close>; an alternative is to invoke
\<^verbatim>\<open>isabelle scala_build\<close> manually. See also \<^doc>\<open>system\<close>, chapter 5,
especially section 5.2.
\<^item> \<^verbatim>\<open>isabelle scala_project\<close> helps to develop Isabelle/Scala tools with
proper IDE support, notably IntelliJ IDEA: the generated project uses
Maven. See also \<^doc>\<open>system\<close>, section 5.2.3.
\<^item> Command-line tools should be always implemented in Scala; old-fashioned
shell scripts are no longer required (and more difficult to implement
properly). Only a few low-level tools are outside the Scala environment,
e.g. \<^verbatim>\<open>isabelle getenv\<close>. Add-on components should always use a name
prefix for their tools, e.g. \<^verbatim>\<open>isabelle dof_mkroot\<close> as defined in
\<^file>\<open>$ISABELLE_DOF_HOME/src/scala/dof_mkroot.scala\<close>.
\<close>
subsection \<open>Document preparation\<close>
text \<open>
\<^item> \<^scala_type>\<open>isabelle.Document_Build.Engine\<close> is the main entry-point
for user-defined document preparation; existing templates and examples
are defined in the same module \<^file>\<open>~~/src/Pure/Thy/document_build.scala\<close>.
There are two stages:
\<^enum> \<^verbatim>\<open>prepare_directory\<close>: populate the document output directory (e.g.
copy static document files, collect generated document sources from the
session build database).
\<^enum> \<^verbatim>\<open>build_document\<close>: produce the final PDF within the document output
directory (e.g. via standard LaTeX tools).
See also \<^system_option>\<open>document_build\<close> as explained in \<^doc>\<open>system\<close>,
section 3.3.
\<close>
section \<open>Miscellaneous NEWS and Notes\<close>
text \<open>
\<^item> Document preparation: there are many new options etc. that might help
to fine-tune DOF output, e.g. \<^system_option>\<open>document_comment_latex\<close>.
\<^item> ML: Theory_Data / Generic_Data: "val extend = I" has been removed;
obsolete since Isabelle2021.
\<^item> ML: \<^ML>\<open>Thm.instantiate\<close> and related operations now use explicit
abstract types for the instantiate, see \<^file>\<open>~~/src/Pure/term_items.ML\<close>
\<^item> ML: new antiquotation "instantiate" allows to instantiate formal
entities (types, terms, theorems) with values given ML. For example:
\<^ML>\<open>fn (A, B) =>
\<^instantiate>\<open>'a = A and 'b = B in typ \<open>('a \<times> 'b) list\<close>\<close>\<close>
\<^ML>\<open>fn A =>
\<^instantiate>\<open>'a = A in
lemma (schematic) \<open>x = y \<Longrightarrow> y = x\<close> for x y :: 'a by simp\<close>\<close>
\<^item> ML: new antiquotations for type constructors and term constants. For
example:
\<^ML>\<open>\<^Type>\<open>nat\<close>\<close>
\<^ML>\<open>fn (A, B) => \<^Type>\<open>fun A B\<close>\<close>
\<^ML>\<open>\<^Type_fn>\<open>fun A B => \<open>(A, B)\<close>\<close>\<close>
\<^ML>\<open>fn (A, B) => \<^Const>\<open>conj for A B\<close>\<close>
\<^ML>\<open>\<^Const_fn>\<open>conj for A B => \<open>(A, B)\<close>\<close>\<close>
\<^ML>\<open>fn t =>
case t of
\<^Const_>\<open>plus T for x y\<close> => ("+", T, x, y)
| \<^Const_>\<open>minus T for x y\<close> => ("-", T, x, y)
| \<^Const_>\<open>times T for x y\<close> => ("*", T, x, y)\<close>
Note: do not use unchecked things like
\<^ML>\<open>Const ("List.list.Nil", Type ("Nat.nat", []))\<close>
\<^item> ML: antiquotations "try" and "can" operate directly on the given ML
expression, in contrast to functions "try" and "can" that modify
application of a function.
Note: instead of semantically ill-defined "handle _ => ...", use
something like this:
\<^ML>\<open>
fn (x, y) =>
(case \<^try>\<open>x div y\<close> of
SOME z => z
| NONE => 0)
\<close>
\<^ML>\<open>
fn (x, y) => \<^try>\<open>x div y\<close> |> the_default 0
\<close>
\<close>
text \<open>Adhoc examples:\<close>
ML \<open>
fun mk_plus x y = \<^Const>\<open>plus \<^Type>\<open>nat\<close> for x y\<close>;
fn \<^Const_>\<open>plus \<^Type>\<open>nat\<close> for \<^Const_>\<open>Groups.zero \<^Type>\<open>nat\<close>\<close> y\<close> => y;
\<close>
ML \<open>
fn (A, B) =>
\<^instantiate>\<open>A and B in term \<open>A \<and> B \<longrightarrow> B \<and> A\<close>\<close>;
fn (A, B) =>
\<^instantiate>\<open>A and B in lemma \<open>A \<and> B \<longrightarrow> B \<and> A\<close> by simp\<close>;
\<close>
end
(* :maxLineLen=75: *)

1
src/tests/ROOT
View File

@ -7,5 +7,6 @@ session "Isabelle_DOF-tests" = "Isabelle_DOF" +
"TermAntiquotations"
"Attributes"
"Evaluation"
"Isabelle2021-1"
"High_Level_Syntax_Invariants"
"Ontology_Matching_Example"