Compare commits
173 Commits
v1.2.0/Isa
...
v1.3.0/Isa
Author | SHA1 | Date |
---|---|---|
Achim D. Brucker | b93ff8f65c | |
Achim D. Brucker | adf87dfde4 | |
Achim D. Brucker | df5d037942 | |
Achim D. Brucker | f2f48f2340 | |
Achim D. Brucker | 6839f63129 | |
Achim D. Brucker | 3febf83b3c | |
Achim D. Brucker | fb8dbfac49 | |
Achim D. Brucker | 45e4a11a74 | |
Burkhart Wolff | c8a3c58f7f | |
Achim D. Brucker | 1939ffeea4 | |
Achim D. Brucker | 74093dfaae | |
Achim D. Brucker | d2b6cb81aa | |
Achim D. Brucker | b24ede4400 | |
Achim D. Brucker | 205aa5a6b1 | |
Achim D. Brucker | c8f3bfc65d | |
Achim D. Brucker | 44f9317b35 | |
Achim D. Brucker | 6c2a0d6876 | |
Achim D. Brucker | 909dda1ea2 | |
Achim D. Brucker | 367d8f28ad | |
Achim D. Brucker | d3f41dca9e | |
Achim D. Brucker | ae3d35e363 | |
Achim D. Brucker | 41a6c22822 | |
Achim D. Brucker | 4ac7c84403 | |
Achim D. Brucker | 38f6516ad9 | |
Achim D. Brucker | 03b721f014 | |
Achim D. Brucker | c5752ba4a2 | |
Achim D. Brucker | 5721398340 | |
Achim D. Brucker | 6c0d325673 | |
Achim D. Brucker | b40069bedd | |
Achim D. Brucker | 70b2647e7c | |
Achim D. Brucker | c1efddf252 | |
Achim D. Brucker | 9ded308371 | |
Achim D. Brucker | f63d922096 | |
Achim D. Brucker | 11b309da02 | |
Achim D. Brucker | 1444f8f48b | |
Achim D. Brucker | e6ca682114 | |
Achim D. Brucker | 15fb6fdc2d | |
Achim D. Brucker | 9d5c71d4e1 | |
Burkhart Wolff | 013296f25e | |
Achim D. Brucker | d10b277c60 | |
Achim D. Brucker | 7c50ffb3af | |
Achim D. Brucker | 3a9826901a | |
Achim D. Brucker | a54373ad2f | |
Achim D. Brucker | aa7d0aec09 | |
Achim D. Brucker | 31778374ed | |
Achim D. Brucker | 0d55da68de | |
Achim D. Brucker | a973707a73 | |
Achim D. Brucker | b83f7a8abb | |
Achim D. Brucker | e138855623 | |
Achim D. Brucker | 5582644068 | |
Achim D. Brucker | 5278608b89 | |
Achim D. Brucker | 59658cea6f | |
Achim D. Brucker | ef674b5ae2 | |
Achim D. Brucker | ac8c939179 | |
Burkhart Wolff | c16ec333f1 | |
Burkhart Wolff | d1e4fd173b | |
Burkhart Wolff | 43c857af2c | |
Burkhart Wolff | 0cc010cecc | |
Burkhart Wolff | ba7bd6dc03 | |
Burkhart Wolff | 43b0a3049f | |
Nicolas Méric | 03fd491d5d | |
Nicolas Méric | 9673359688 | |
Nicolas Méric | 5d1b271336 | |
Nicolas Méric | 83c790d66a | |
Nicolas Méric | 9981c31966 | |
Nicolas Méric | 319b39905f | |
Nicolas Méric | c00c6ed31d | |
Nicolas Méric | ae3300ac2c | |
Achim D. Brucker | 61f167c29c | |
Achim D. Brucker | 2833deff90 | |
Achim D. Brucker | a8424979eb | |
Achim D. Brucker | f6f6f32b50 | |
Achim D. Brucker | 15e71fe189 | |
Achim D. Brucker | 45c23b4330 | |
Achim D. Brucker | 995feb6685 | |
Nicolas Méric | d8fde4b4f4 | |
Achim D. Brucker | 41e6c9ed02 | |
Achim D. Brucker | cbad96aba5 | |
Achim D. Brucker | 82c9a07c1a | |
Achim D. Brucker | ae8b91ac4e | |
Achim D. Brucker | 0f3f5d4b56 | |
Achim D. Brucker | fee83a2a29 | |
Achim D. Brucker | a0993b6eea | |
Achim D. Brucker | 64b4eca5ea | |
Achim D. Brucker | 2e4fb5d174 | |
Achim D. Brucker | 317c5a7759 | |
Achim D. Brucker | 12f1b230e6 | |
Achim D. Brucker | 530783c23b | |
Nicolas Méric | 1457c1cb85 | |
Nicolas Méric | e3caad804b | |
Nicolas Méric | 17df6a271b | |
Nicolas Méric | a331b80095 | |
Nicolas Méric | 74420a932f | |
Nicolas Méric | 8e1702d2da | |
Achim D. Brucker | 609f09e919 | |
Achim D. Brucker | 0f5e5bf6f6 | |
Achim D. Brucker | 5c886d49b4 | |
Nicolas Méric | b1f73e9235 | |
Nicolas Méric | 9603311a9a | |
Burkhart Wolff | 2351e00be6 | |
Burkhart Wolff | 3e99e9e013 | |
Burkhart Wolff | d2e1d77b01 | |
Burkhart Wolff | 96726fc507 | |
Burkhart Wolff | a68ecb4f11 | |
Achim D. Brucker | 1ea897e660 | |
Achim D. Brucker | 1b25a08da8 | |
Burkhart Wolff | 6a7b5c6afb | |
Burkhart Wolff | 9403afd86f | |
Burkhart Wolff | 894166a630 | |
Burkhart Wolff | 34df9f6fcd | |
Nicolas Méric | c5a3239d2b | |
Nicolas Méric | e4e4a708a5 | |
Nicolas Méric | 9cd5323063 | |
Nicolas Méric | 444d6d077c | |
Nicolas Méric | ec33e70bbf | |
Achim D. Brucker | f655d2a784 | |
Achim D. Brucker | d80d5b0538 | |
Achim D. Brucker | e5874396c4 | |
Achim D. Brucker | 60b7216daa | |
Achim D. Brucker | 4a7605b43e | |
Achim D. Brucker | 8a2828f3bf | |
Achim D. Brucker | 9522597733 | |
Achim D. Brucker | 9f773ca129 | |
Achim D. Brucker | 7b8ae0a93d | |
Achim D. Brucker | 700855411e | |
Achim D. Brucker | 5348a609be | |
Achim D. Brucker | 46c46af880 | |
Achim D. Brucker | 7b4450450d | |
Achim D. Brucker | 1d48fb810f | |
Achim D. Brucker | c2fbd57f12 | |
Achim D. Brucker | 1f1a504bf0 | |
Achim D. Brucker | 05e85edd91 | |
Achim D. Brucker | 57b9720d99 | |
Achim D. Brucker | 846237b515 | |
Achim D. Brucker | 74368af56c | |
Achim D. Brucker | 21ab0ff6b9 | |
Achim D. Brucker | b7948659ad | |
Achim D. Brucker | 95cda1aaea | |
Achim D. Brucker | 0f6ec7dcd1 | |
Achim D. Brucker | 250755e7f1 | |
Achim D. Brucker | 68e8d0be4a | |
Achim D. Brucker | aff78b0625 | |
Achim D. Brucker | 9f5d20a586 | |
Achim D. Brucker | 3c49a9aaba | |
Achim D. Brucker | f4286404fb | |
Achim D. Brucker | a1d83e33ef | |
Achim D. Brucker | 5ae72e1103 | |
Achim D. Brucker | de67a05160 | |
Achim D. Brucker | 16bd3b3a94 | |
Achim D. Brucker | f3f24c0d2e | |
Achim D. Brucker | 76582f75fd | |
Achim D. Brucker | 442835442f | |
Achim D. Brucker | c69b11a312 | |
Achim D. Brucker | 0c9dcfb6e1 | |
Achim D. Brucker | f51ee34681 | |
Achim D. Brucker | ef89a95307 | |
Achim D. Brucker | 62726920a7 | |
Achim D. Brucker | 7bb4ab58e9 | |
Achim D. Brucker | 010202e34a | |
Achim D. Brucker | 62eefcee5d | |
Achim D. Brucker | abe7713f1e | |
Achim D. Brucker | 2314b2191f | |
Makarius Wenzel | 4352691e95 | |
Makarius Wenzel | 2547b2324e | |
Makarius Wenzel | 99264edc02 | |
Makarius Wenzel | 70617f59fe | |
Makarius Wenzel | fadd982285 | |
Makarius Wenzel | 4e4995bde5 | |
Makarius Wenzel | 2e4d37e3ca | |
Makarius Wenzel | ff32bac3fc | |
Makarius Wenzel | bcf7849083 | |
Makarius Wenzel | 86b555b56e | |
Makarius Wenzel | ec49f45966 |
18
.config
|
@ -1,18 +0,0 @@
|
||||||
# Isabelle/DOF Version Information
|
|
||||||
DOF_VERSION="1.2.0" # "Unreleased" for development, semantic version for releases
|
|
||||||
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"
|
|
||||||
AFP_URL="https://www.isa-afp.org/release/"$AFP_DATE".tar.gz"
|
|
||||||
#
|
|
||||||
# Isabelle/DOF Repository Configuration
|
|
||||||
DOF_URL="https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF"
|
|
||||||
DOF_ARTIFACT_DIR="releases/Isabelle_DOF/Isabelle_DOF"
|
|
||||||
DOF_ARTIFACT_HOST="artifacts.logicalhacking.com"
|
|
||||||
#
|
|
|
@ -1,3 +1,2 @@
|
||||||
install -crlf
|
core.autocrlf false
|
||||||
document-generator/Tools/DOF_mkroot -crlf
|
core.eol lf
|
||||||
document-generator/document-template/build -crlf
|
|
||||||
|
|
|
@ -1,3 +1,4 @@
|
||||||
output
|
output
|
||||||
.afp
|
.afp
|
||||||
*~
|
*~
|
||||||
|
*#
|
||||||
|
|
|
@ -9,6 +9,10 @@ It may also contain additional tools and script that are useful for preparing a
|
||||||
|
|
||||||
### Latest Build
|
### Latest Build
|
||||||
|
|
||||||
* [document.pdf](https://artifacts.logicalhacking.com/ci-confidential/Isabelle_DOF/Isabelle_DOF/main/latest/document.pdf)
|
* lualatex
|
||||||
* [browser_info](https://artifacts.logicalhacking.com/ci-confidential/Isabelle_DOF/Isabelle_DOF/main/latest/browser_info/Unsorted/Isabelle_DOF/)
|
* [browser_info](https://artifacts.logicalhacking.com/ci/Isabelle_DOF/Isabelle_DOF/main/latest/lualatex/browser_info/Unsorted/)
|
||||||
* [aux files](https://artifacts.logicalhacking.com/ci-confidential/Isabelle_DOF/Isabelle_DOF/main/latest/)
|
* [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/)
|
||||||
|
* [Isabelle_DOF-Unreleased_Isabelle2021-1.tar.xz](https://artifacts.logicalhacking.com/ci/Isabelle_DOF/Isabelle_DOF/main/latest/Isabelle_DOF-Unreleased_Isabelle2021-1.tar.xz)
|
||||||
|
|
|
@ -1,17 +1,31 @@
|
||||||
pipeline:
|
pipeline:
|
||||||
build:
|
build:
|
||||||
image: docker.io/logicalhacking/isabelle2021
|
image: docker.io/logicalhacking/isabelle2021-1
|
||||||
commands:
|
commands:
|
||||||
- export ARTIFACT_DIR=$CI_WORKSPACE/.artifacts/$CI_REPO/$CI_BRANCH/$CI_BUILD_NUMBER/
|
- export ARTIFACT_DIR=$CI_WORKSPACE/.artifacts/$CI_REPO/$CI_BRANCH/$CI_BUILD_NUMBER/$LATEX
|
||||||
- mkdir -p $ARTIFACT_DIR
|
- mkdir -p $ARTIFACT_DIR
|
||||||
- export `isabelle getenv ISABELLE_HOME_USER`
|
- export `isabelle getenv ISABELLE_HOME_USER`
|
||||||
- ./install
|
- 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 build -D . -o browser_info
|
||||||
|
- isabelle dof_mkroot DOF_test
|
||||||
|
- isabelle build -D DOF_test
|
||||||
- cp -r $ISABELLE_HOME_USER/browser_info $ARTIFACT_DIR
|
- cp -r $ISABELLE_HOME_USER/browser_info $ARTIFACT_DIR
|
||||||
- cp output/document.pdf $ARTIFACT_DIR
|
|
||||||
- cd $ARTIFACT_DIR
|
- cd $ARTIFACT_DIR
|
||||||
- cd ..
|
- cd ../..
|
||||||
- ln -s * latest
|
- ln -s * latest
|
||||||
|
archive:
|
||||||
|
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_VERSION=`isabelle version`
|
||||||
|
- ./.woodpecker/mk_release -d
|
||||||
|
- cp Isabelle_DOF-Unreleased_$ISABELLE_VERSION.tar.xz $ARTIFACT_DIR/../
|
||||||
|
when:
|
||||||
|
matrix:
|
||||||
|
LATEX: lualatex
|
||||||
deploy:
|
deploy:
|
||||||
image: docker.io/drillster/drone-rsync
|
image: docker.io/drillster/drone-rsync
|
||||||
settings:
|
settings:
|
||||||
|
@ -23,5 +37,18 @@ pipeline:
|
||||||
key:
|
key:
|
||||||
from_secret: artifacts_ssh
|
from_secret: artifacts_ssh
|
||||||
user: artifacts
|
user: artifacts
|
||||||
|
notify:
|
||||||
|
image: drillster/drone-email
|
||||||
|
settings:
|
||||||
|
host: smtp.0x5f.org
|
||||||
|
username: woodpecker
|
||||||
|
password:
|
||||||
|
from_secret: email
|
||||||
|
from: ci@logicalhacking.com
|
||||||
|
when:
|
||||||
|
status: [ failure ]
|
||||||
|
|
||||||
|
matrix:
|
||||||
|
LATEX:
|
||||||
|
- lualatex
|
||||||
|
- pdflatex
|
||||||
|
|
|
@ -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
|
|
||||||
|
|
|
@ -39,26 +39,18 @@ print_help()
|
||||||
echo "Run ..."
|
echo "Run ..."
|
||||||
echo ""
|
echo ""
|
||||||
echo " --help, -h display this help message"
|
echo " --help, -h display this help message"
|
||||||
echo " --sign -s sign release archive"
|
echo " --sign, -s sign release archive"
|
||||||
echo " (default: $SIGN)"
|
echo " (default: $SIGN)"
|
||||||
echo " --isabelle, -i isabelle isabelle command used for installation"
|
echo " --isabelle, -i isabelle isabelle command used for installation"
|
||||||
echo " (default: $ISABELLE)"
|
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 " (default: use master branch)"
|
||||||
echo " --p --publish publish generated artefact"
|
echo " --publish, -p publish generated artefact"
|
||||||
echo " (use master: $PUBLISH)"
|
echo " (default: $PUBLISH)"
|
||||||
|
echo " --quick-and-dirty, -d only build required artifacts, no complete test"
|
||||||
|
echo " (default: $DIRTY)"
|
||||||
}
|
}
|
||||||
|
|
||||||
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() {
|
check_isabelle_version() {
|
||||||
ACTUAL_ISABELLE_VERSION=`$ISABELLE version`
|
ACTUAL_ISABELLE_VERSION=`$ISABELLE version`
|
||||||
echo "* Checking Isabelle version:"
|
echo "* Checking Isabelle version:"
|
||||||
|
@ -80,21 +72,38 @@ clone_repo()
|
||||||
else
|
else
|
||||||
echo " * Not tag specified, using master branch"
|
echo " * Not tag specified, using master branch"
|
||||||
fi
|
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()
|
build_and_install_manuals()
|
||||||
{
|
{
|
||||||
echo "* Building manual"
|
echo "* Building manual"
|
||||||
ROOTS=$ISABELLE_HOME_USER/ROOTS
|
|
||||||
if [ -f $ROOTS ]; then
|
if [ "$DIRTY" = "true" ]; then
|
||||||
mv $ROOTS $ROOTS.backup
|
if [ -z ${ARTIFACT_DIR+x} ]; then
|
||||||
|
echo " * Quick and Dirty Mode (local build)"
|
||||||
|
$ISABELLE build -d . Isabelle_DOF-Manual 2018-cicm-isabelle_dof-applications
|
||||||
|
mkdir -p $ISADOF_WORK_DIR/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/output/
|
||||||
|
cp examples/scholarly_paper/2018-cicm-isabelle_dof-applications/output/document.pdf \
|
||||||
|
$ISADOF_WORK_DIR/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/output/
|
||||||
|
mkdir -p $ISADOF_WORK_DIR/examples/technical_report/Isabelle_DOF-Manual/output/
|
||||||
|
cp examples/technical_report/Isabelle_DOF-Manual/output/document.pdf \
|
||||||
|
$ISADOF_WORK_DIR/examples/technical_report/Isabelle_DOF-Manual/output/;
|
||||||
|
else
|
||||||
|
echo " * Quick and Dirty Mode (running on CI)"
|
||||||
|
mkdir -p $ISADOF_WORK_DIR/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/output/
|
||||||
|
cp $ARTIFACT_DIR/browser_info/Unsorted/2018-cicm-isabelle_dof-applications/document.pdf \
|
||||||
|
$ISADOF_WORK_DIR/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/output/
|
||||||
|
|
||||||
|
mkdir -p $ISADOF_WORK_DIR/examples/technical_report/Isabelle_DOF-Manual/output/
|
||||||
|
cp $ARTIFACT_DIR/browser_info/Unsorted/Isabelle_DOF-Manual/document.pdf \
|
||||||
|
$ISADOF_WORK_DIR/examples/technical_report/Isabelle_DOF-Manual/output/;
|
||||||
|
fi
|
||||||
|
else
|
||||||
|
(cd $ISADOF_WORK_DIR && $ISABELLE env ./install-afp)
|
||||||
|
(cd $ISADOF_WORK_DIR && $ISABELLE build -c -D . )
|
||||||
fi
|
fi
|
||||||
|
|
||||||
(cd $ISADOF_WORK_DIR && ./install)
|
|
||||||
(cd $ISADOF_WORK_DIR && $ISABELLE build -c -D . )
|
|
||||||
|
|
||||||
mkdir -p $ISADOF_WORK_DIR/doc
|
mkdir -p $ISADOF_WORK_DIR/doc
|
||||||
echo "Isabelle/DOF Manuals!" > $ISADOF_WORK_DIR/doc/Contents
|
echo "Isabelle/DOF Manuals!" > $ISADOF_WORK_DIR/doc/Contents
|
||||||
|
|
||||||
|
@ -108,9 +117,7 @@ build_and_install_manuals()
|
||||||
|
|
||||||
find $ISADOF_WORK_DIR -type d -name "output" -exec rm -rf {} \; &> /dev/null || true
|
find $ISADOF_WORK_DIR -type d -name "output" -exec rm -rf {} \; &> /dev/null || true
|
||||||
rm -rf $ISADOF_WORK_DIR/.git* $ISADOF_WORK_DIR/.woodpecker $ISADOF_WORK_DIR/.afp
|
rm -rf $ISADOF_WORK_DIR/.git* $ISADOF_WORK_DIR/.woodpecker $ISADOF_WORK_DIR/.afp
|
||||||
if [ -f $ROOTS.backup ]; then
|
|
||||||
mv $ROOTS.backup $ROOTS
|
|
||||||
fi
|
|
||||||
}
|
}
|
||||||
|
|
||||||
create_archive()
|
create_archive()
|
||||||
|
@ -120,7 +127,6 @@ create_archive()
|
||||||
(mv $ISADOF_WORK_DIR $ISADOF_DIR)
|
(mv $ISADOF_WORK_DIR $ISADOF_DIR)
|
||||||
(cd $BUILD_DIR && tar cf $ISADOF_TAR.tar $ISADOF_TAR && xz $ISADOF_DIR.tar)
|
(cd $BUILD_DIR && tar cf $ISADOF_TAR.tar $ISADOF_TAR && xz $ISADOF_DIR.tar)
|
||||||
mv $BUILD_DIR/$ISADOF_TAR.tar.xz .
|
mv $BUILD_DIR/$ISADOF_TAR.tar.xz .
|
||||||
rm -rf $BUILD_DIR
|
|
||||||
}
|
}
|
||||||
|
|
||||||
sign_archive()
|
sign_archive()
|
||||||
|
@ -138,11 +144,11 @@ publish_archive()
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
read_config
|
|
||||||
ISABELLE=`which isabelle`
|
ISABELLE=`which isabelle`
|
||||||
USE_TAG="false"
|
USE_TAG="false"
|
||||||
SIGN="false"
|
SIGN="false"
|
||||||
PUBLISH="false"
|
PUBLISH="false"
|
||||||
|
DIRTY="false"
|
||||||
BUILD_DIR=`mktemp -d`
|
BUILD_DIR=`mktemp -d`
|
||||||
ISADOF_WORK_DIR="$BUILD_DIR/Isabelle_DOF"
|
ISADOF_WORK_DIR="$BUILD_DIR/Isabelle_DOF"
|
||||||
while [ $# -gt 0 ]
|
while [ $# -gt 0 ]
|
||||||
|
@ -159,6 +165,8 @@ do
|
||||||
SIGN="true";;
|
SIGN="true";;
|
||||||
--publish|-p)
|
--publish|-p)
|
||||||
PUBLISH="true";;
|
PUBLISH="true";;
|
||||||
|
--quick-and-dirty|-d)
|
||||||
|
DIRTY="true";;
|
||||||
--help|-h)
|
--help|-h)
|
||||||
print_help
|
print_help
|
||||||
exit 0;;
|
exit 0;;
|
||||||
|
@ -171,19 +179,36 @@ done
|
||||||
|
|
||||||
clone_repo
|
clone_repo
|
||||||
|
|
||||||
source $ISADOF_WORK_DIR/.config
|
ISADOF_MAIN_DIR=`pwd`
|
||||||
|
|
||||||
|
if [ "$DIRTY" = "true" ]; then
|
||||||
|
echo "Running in Quick and Dirty mode!"
|
||||||
|
$ISABELLE components -u $ISADOF_MAIN_DIR
|
||||||
|
else
|
||||||
|
$ISABELLE components -x $ISADOF_MAIN_DIR
|
||||||
|
$ISABELLE components -u $ISADOF_WORK_DIR
|
||||||
|
fi
|
||||||
|
|
||||||
|
VARS=`$ISABELLE getenv ISABELLE_TOOL`
|
||||||
|
for i in $VARS; do
|
||||||
|
export "$i"
|
||||||
|
done
|
||||||
|
|
||||||
|
ISABELLE_VERSION="Isabelle$($ISABELLE_TOOL options -g dof_isabelle)"
|
||||||
|
DOF_VERSION="$($ISABELLE_TOOL options -g dof_version)"
|
||||||
|
|
||||||
ISABELLE_SHORT_VERSION=`echo $ISABELLE_VERSION | sed -e 's/:.*$//'`
|
ISABELLE_SHORT_VERSION=`echo $ISABELLE_VERSION | sed -e 's/:.*$//'`
|
||||||
ISADOF_TAR="Isabelle_DOF-"$DOF_VERSION"_"$ISABELLE_SHORT_VERSION
|
ISADOF_TAR="Isabelle_DOF-"$DOF_VERSION"_"$ISABELLE_SHORT_VERSION
|
||||||
ISADOF_DIR="$BUILD_DIR/$ISADOF_TAR"
|
ISADOF_DIR="$BUILD_DIR/$ISADOF_TAR"
|
||||||
|
|
||||||
check_isabelle_version
|
check_isabelle_version
|
||||||
VARS=`$ISABELLE getenv ISABELLE_HOME_USER`
|
|
||||||
for i in $VARS; do
|
|
||||||
export "$i"
|
|
||||||
done
|
|
||||||
|
|
||||||
build_and_install_manuals
|
build_and_install_manuals
|
||||||
|
|
||||||
|
if [ "$DIRTY" != "true" ]; then
|
||||||
|
$ISABELLE components -x $ISADOF_WORK_DIR
|
||||||
|
$ISABELLE components -u $ISADOF_MAIN_DIR
|
||||||
|
fi
|
||||||
|
|
||||||
create_archive
|
create_archive
|
||||||
|
|
||||||
if [ "$SIGN" = "true" ]; then
|
if [ "$SIGN" = "true" ]; then
|
||||||
|
@ -194,4 +219,6 @@ if [ "$PUBLISH" = "true" ]; then
|
||||||
publish_archive
|
publish_archive
|
||||||
fi
|
fi
|
||||||
|
|
||||||
|
rm -rf $BUILD_DIR
|
||||||
|
|
||||||
exit 0
|
exit 0
|
||||||
|
|
22
CHANGELOG.md
|
@ -5,9 +5,22 @@ 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/)
|
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).
|
and this project adheres to [Semantic Versioning](http://semver.org/spec/v2.0.0.html).
|
||||||
|
|
||||||
## 1.2.0 - 2022-03-26
|
## [1.3.0] - 2022-07-08
|
||||||
|
|
||||||
## 1.1.0 - 2021-03-20
|
### Changed
|
||||||
|
|
||||||
|
- The project-specific configuration is not part of the `ROOT` file, the formerly
|
||||||
|
used `isadof.cfg` is obsolete and no longer supported.
|
||||||
|
- Removed explicit use of `document/build` script. Requires removing the `build` script
|
||||||
|
entry from ROOT files.
|
||||||
|
- Isabelle/DOF is now a proper Isabelle component that should be installed using the
|
||||||
|
`isabelle components` command. The installation script is now only a convenient way
|
||||||
|
of installing the required AFP entries.
|
||||||
|
- `mkroot_DOF` has been renamed to `dof_mkroot` (and reimplemented in Scala).
|
||||||
|
|
||||||
|
## [1.2.0] - 2022-03-26
|
||||||
|
|
||||||
|
## [1.1.0] - 2021-03-20
|
||||||
|
|
||||||
### Added
|
### Added
|
||||||
|
|
||||||
|
@ -24,4 +37,7 @@ and this project adheres to [Semantic Versioning](http://semver.org/spec/v2.0.0.
|
||||||
|
|
||||||
- First public release
|
- 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.3.0/Isabelle2021...HEAD
|
||||||
|
[v1.3.0]: https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF/compare/v1.2.0/Isabelle2021...v1.3.0/Isabelle2021-1
|
||||||
|
[v1.2.0]: https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF/compare/v1.1.0/Isabelle2021...v1.2.0/Isabelle2021
|
||||||
|
[v1.1.0]: https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF/compare/v1.0.0/Isabelle2019...v1.1.0/Isabelle2021
|
||||||
|
|
|
@ -1,5 +1,4 @@
|
||||||
To cite Isabelle/DOF in publications, please use
|
To cite Isabelle/DOF in publications, please use
|
||||||
|
|
||||||
|
|
||||||
Achim D. Brucker, Idir Ait-Sadoune, Paolo Crisafulli, and Burkhart
|
Achim D. Brucker, Idir Ait-Sadoune, Paolo Crisafulli, and Burkhart
|
||||||
Wolff. Using The Isabelle Ontology Framework: Linking the Formal
|
Wolff. Using The Isabelle Ontology Framework: Linking the Formal
|
||||||
|
|
|
@ -2,54 +2,51 @@
|
||||||
|
|
||||||
Isabelle/DOF is a novel Document Ontology Framework on top of Isabelle.
|
Isabelle/DOF is a novel Document Ontology Framework on top of Isabelle.
|
||||||
Isabelle/DOF allows for both conventional typesetting as well as formal
|
Isabelle/DOF allows for both conventional typesetting as well as formal
|
||||||
development. The manual for [Isabelle/DOF 1.2.0/Isabelle2021 is available
|
development. The manual for [Isabelle/DOF 1.2.0/Isabelle2021 is available
|
||||||
online.](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.2.0_Isabelle2021.pdf)
|
online.](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.2.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.2.0_isabelle2021 isabelle jedit
|
|
||||||
```
|
|
||||||
|
|
||||||
## Pre-requisites
|
## Pre-requisites
|
||||||
|
|
||||||
Isabelle/DOF has two major pre-requisites:
|
Isabelle/DOF has three major prerequisites:
|
||||||
|
|
||||||
* **Isabelle:** Isabelle/DOF requires [Isabelle 2021](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 distribution for your operating
|
Please download the Isabelle 2021-1 distribution for your operating
|
||||||
system from the [Isabelle website](http://isabelle.in.tum.de/website-Isabelle2021/).
|
system from the [Isabelle
|
||||||
* **LaTeX:** Isabelle/DOF requires a modern LaTeX installation, i.e., at least
|
website](http://isabelle.in.tum.de/website-Isabelle2021-1/).
|
||||||
[TeX Live 2021](https://www.tug.org/texlive/) with all available updates applied.
|
* **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. First, Isabelle/DOF
|
||||||
|
needs to be registered as an Isabelle component:
|
||||||
|
|
||||||
|
```console
|
||||||
|
foo@bar:~$ isabelle components -u `pwd`
|
||||||
|
```
|
||||||
|
|
||||||
|
Thereafter, the AFP entries can be installed as follows:
|
||||||
|
|
||||||
|
```console
|
||||||
|
foo@bar:~$ isabelle env ./install-afp
|
||||||
|
```
|
||||||
|
|
||||||
|
* **LaTeX:** Isabelle/DOF requires a modern LaTeX installation, i.e., at least
|
||||||
|
[TeX Live 2022](https://www.tug.org/texlive/) with all available updates applied.
|
||||||
|
|
||||||
## Installation
|
## Installation
|
||||||
|
|
||||||
In most case, the DOF-plugin can be installed as follows:
|
Isabelle/DOF is provided as an Isabelle component. After installing the
|
||||||
|
prerequisites, change into the directory containing Isabelle/DOF (this should be
|
||||||
|
the directory containing this `README.md` file) and execute (if you executed
|
||||||
|
this command already during the installation of the pre-requisites, you
|
||||||
|
can skip it now):
|
||||||
|
|
||||||
```console
|
```console
|
||||||
foo@bar:~$ ./install
|
foo@bar:~$ isabelle components -u `pwd`
|
||||||
```
|
```
|
||||||
|
|
||||||
If a specific Isabelle version should be used (i.e., not the default
|
The final step for the installation is:
|
||||||
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:
|
|
||||||
|
|
||||||
```console
|
```console
|
||||||
foo@bar:~$ isabelle build -D .
|
foo@bar:~$ isabelle build -D .
|
||||||
|
@ -87,19 +84,19 @@ The DOF-plugin provides an alternative to Isabelle's ``mkroot`` command.
|
||||||
Isabelle projects that use DOF need to be created using
|
Isabelle projects that use DOF need to be created using
|
||||||
|
|
||||||
```console
|
```console
|
||||||
foo@bar:~$ isabelle mkroot_DOF
|
foo@bar:~$ isabelle dof_mkroot
|
||||||
```
|
```
|
||||||
|
|
||||||
The ``mkroot_DOF`` command takes the same parameter as the standard
|
The ``dof_mkroot`` command takes the same parameter as the standard
|
||||||
``mkroot`` command of Isabelle. Thereafter, the normal Isabelle
|
``mkroot`` command of Isabelle. Thereafter, the normal Isabelle
|
||||||
command for building documents can be used.
|
command for building documents can be used.
|
||||||
|
|
||||||
Using the ``-o`` option, different ontology setups can be
|
Using the ``-o`` option, different ontology setups can be
|
||||||
selected and using the ``-t`` option, different LaTeX setups
|
selected and using the ``-t`` option, different LaTeX setups
|
||||||
can be selected. For example,
|
can be selected. For example,
|
||||||
|
|
||||||
```console
|
```console
|
||||||
foo@bar:~$ isabelle mkroot_DOF -o scholarly_paper -t scrartcl
|
foo@bar:~$ isabelle dof_mkroot -o scholarly_paper -t scrartcl
|
||||||
```
|
```
|
||||||
|
|
||||||
creates a setup using the scholarly_paper ontology and the article
|
creates a setup using the scholarly_paper ontology and the article
|
||||||
|
@ -109,33 +106,30 @@ The help (option ``-h``) show a list of all supported ontologies and
|
||||||
document templates:
|
document templates:
|
||||||
|
|
||||||
```console
|
```console
|
||||||
foo@bar:~$ isabelle mkroot_DOF -h
|
foo@bar:~$ isabelle dof_mkroot -h
|
||||||
|
Usage: isabelle dof_mkroot [OPTIONS] [DIRECTORY]
|
||||||
Usage: isabelle mkroot_DOF [OPTIONS] [DIR]
|
|
||||||
|
|
||||||
Options are:
|
Options are:
|
||||||
-h print this help text and exit
|
-I init Mercurial repository and add generated files
|
||||||
-n NAME alternative session name (default: DIR base name)
|
-n NAME alternative session name (default: directory base name)
|
||||||
-o ONTOLOGY (default: scholarly_paper)
|
-o ONTOLOGY ontology (default: scholarly_paper)
|
||||||
Available ontologies:
|
-t TEMPLATE tempalte (default: scrartcl)
|
||||||
* cenelec_50128
|
|
||||||
* mathex
|
|
||||||
* scholarly_paper
|
|
||||||
-t TEMPLATE (default: scrartcl)
|
|
||||||
Available document templates:
|
|
||||||
* lncs
|
|
||||||
* scrartcl
|
|
||||||
* scrreprt
|
|
||||||
* scrreprt-modern
|
|
||||||
|
|
||||||
Prepare session root DIR (default: current directory).
|
Prepare session root directory (default: current directory).
|
||||||
```
|
```
|
||||||
|
|
||||||
## Releases
|
## Releases
|
||||||
|
|
||||||
For releases, signed archives including a PDF version of the Isabelle/DOF manual are
|
For releases, signed archives including a PDF version of the Isabelle/DOF manual
|
||||||
are available:
|
are available:
|
||||||
|
|
||||||
|
* Isabelle/DOF 1.3.0/Isabelle2021-1
|
||||||
|
* [Isabelle_DOF-1.3.0_Isabelle2021-1.pdf](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.3.0_Isabelle2021-1.pdf)
|
||||||
|
* [Isabelle_DOF-1.3.0_Isabelle2021-1.tar.xz](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.3.0_Isabelle2021-1.tar.xz)
|
||||||
|
* [Isabelle_DOF-1.3.0_Isabelle2021-1.tar.xz.asc](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.3.0_Isabelle2021-1.tar.xz.asc)
|
||||||
|
|
||||||
|
### Older Releases
|
||||||
|
|
||||||
* Isabelle/DOF 1.2.0/Isabelle2021
|
* 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.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](https://artifacts.logicalhacking.com/releases/Isabelle_DOF/Isabelle_DOF/Isabelle_DOF-1.2.0_Isabelle2021.tar.xz)
|
||||||
|
@ -165,7 +159,7 @@ Main contacts:
|
||||||
* Idir Ait-Sadoune
|
* Idir Ait-Sadoune
|
||||||
* Paolo Crisafulli
|
* Paolo Crisafulli
|
||||||
* Chantal Keller
|
* Chantal Keller
|
||||||
* Nicolas Méric
|
* Nicolas Méric
|
||||||
|
|
||||||
## License
|
## License
|
||||||
|
|
||||||
|
@ -188,11 +182,11 @@ SPDX-License-Identifier: BSD-2-Clause
|
||||||
Computer Science (11724), Springer-Verlag, 2019.
|
Computer Science (11724), Springer-Verlag, 2019.
|
||||||
[doi:10.1007/978-3-030-30446-1_15](https://doi.org/10.1007/978-3-030-30446-1_15).
|
[doi:10.1007/978-3-030-30446-1_15](https://doi.org/10.1007/978-3-030-30446-1_15).
|
||||||
|
|
||||||
* Achim D. Brucker, Burkhart Wolff. [Using Ontologies in Formal Developments Targeting Certification](https://www.brucker.ch/bibliography/download/2019/brucker.ea-ontologies-certification-2019.pdf). In
|
* Achim D. Brucker, Burkhart Wolff. [Using Ontologies in Formal Developments Targeting Certification](https://www.brucker.ch/bibliography/download/2019/brucker.ea-ontologies-certification-2019.pdf). In
|
||||||
Integrated Formal Methods (IFM). Lecture Notes in Computer Science (11918). Springer-Verlag 2019.
|
Integrated Formal Methods (IFM). Lecture Notes in Computer Science (11918). Springer-Verlag 2019.
|
||||||
[doi:10.1007/978-3-030-34968-4_4](http://dx.doi.org/10.1007/978-3-030-34968-4_4)
|
[doi:10.1007/978-3-030-34968-4_4](http://dx.doi.org/10.1007/978-3-030-34968-4_4)
|
||||||
|
|
||||||
* Sergio Bezzecchi, Paolo Crisafulli, Charlotte Pichot, and Burkhart Wolff. [Making Agile Development
|
* Sergio Bezzecchi, Paolo Crisafulli, Charlotte Pichot, and Burkhart Wolff. [Making Agile Development
|
||||||
Processes fit for V-style Certification Procedures.](https://hal.archives-ouvertes.fr/hal-01702815/document)
|
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>
|
In ERTS 2018. <https://hal.archives-ouvertes.fr/hal-01702815>
|
||||||
|
|
||||||
|
|
|
@ -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
|
|
@ -0,0 +1,30 @@
|
||||||
|
(* :mode=isabelle-options: *)
|
||||||
|
|
||||||
|
section "Isabelle/DOF"
|
||||||
|
|
||||||
|
public option dof_template : string = "scrreprt-modern"
|
||||||
|
-- "Default document template for Isabelle/DOF documents"
|
||||||
|
|
||||||
|
public option dof_ontologies : string = "Isabelle_DOF.technical_report Isabelle_DOF.scholarly_paper"
|
||||||
|
-- "Isabelle/DOF ontologies (separated by blanks)"
|
||||||
|
|
||||||
|
option dof_version : string = "1.3.0"
|
||||||
|
-- "Isabelle/DOF version"
|
||||||
|
(* "Unreleased" for development, semantic version for releases *)
|
||||||
|
|
||||||
|
option dof_isabelle : string = "2021-1"
|
||||||
|
option dof_afp : string = "afp-2021-12-28"
|
||||||
|
|
||||||
|
option dof_latest_version : string = "1.3.0"
|
||||||
|
option dof_latest_isabelle : string = "Isabelle2021-1"
|
||||||
|
option dof_latest_doi : string = "10.5281/zenodo.6810799"
|
||||||
|
option dof_generic_doi : string = "10.5281/zenodo.3370482"
|
||||||
|
|
||||||
|
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"
|
||||||
|
|
|
@ -0,0 +1,5 @@
|
||||||
|
# -*- shell-script -*- :mode=shellscript:
|
||||||
|
|
||||||
|
ISABELLE_DOF_HOME="$COMPONENT"
|
||||||
|
ISABELLE_DOCS="$ISABELLE_DOF_HOME/doc":"$ISABELLE_DOCS"
|
||||||
|
|
|
@ -1,11 +1,10 @@
|
||||||
session "mini_odo" = "Isabelle_DOF" +
|
session "mini_odo" = "Isabelle_DOF" +
|
||||||
options [document = pdf, document_output = "output"]
|
options [document = pdf, document_output = "output", document_build = dof,
|
||||||
|
dof_ontologies = "Isabelle_DOF.technical_report Isabelle_DOF.cenelec_50128", dof_template = "Isabelle_DOF.scrreprt-modern"]
|
||||||
theories
|
theories
|
||||||
"mini_odo"
|
"mini_odo"
|
||||||
document_files
|
document_files
|
||||||
"isadof.cfg"
|
|
||||||
"preamble.tex"
|
"preamble.tex"
|
||||||
"build"
|
|
||||||
"root.bib"
|
"root.bib"
|
||||||
"root.mst"
|
"root.mst"
|
||||||
"lstisadof.sty"
|
"lstisadof.sty"
|
||||||
|
@ -13,3 +12,4 @@ session "mini_odo" = "Isabelle_DOF" +
|
||||||
"figures/odometer.jpeg"
|
"figures/odometer.jpeg"
|
||||||
"figures/three-phase-odo.pdf"
|
"figures/three-phase-odo.pdf"
|
||||||
"figures/wheel-df.png"
|
"figures/wheel-df.png"
|
||||||
|
|
||||||
|
|
|
@ -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
|
|
0
examples/CENELEC_50128/mini_odo/document/figures/df-numerics-encshaft.png
Executable file → Normal file
Before Width: | Height: | Size: 27 KiB After Width: | Height: | Size: 27 KiB |
Before Width: | Height: | Size: 407 KiB After Width: | Height: | Size: 407 KiB |
0
examples/CENELEC_50128/mini_odo/document/figures/three-phase-odo.pdf
Executable file → Normal file
Before Width: | Height: | Size: 23 KiB After Width: | Height: | Size: 23 KiB |
|
@ -1,3 +0,0 @@
|
||||||
Template: scrreprt-modern
|
|
||||||
Ontology: technical_report
|
|
||||||
Ontology: cenelec_50128
|
|
2
examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy
Executable file → Normal file
|
@ -256,7 +256,7 @@ enforcing a sequence of text-elements that must belong to the corresponding clas
|
||||||
To start using \<^isadof>, one creates an Isabelle project (with the name
|
To start using \<^isadof>, one creates an Isabelle project (with the name
|
||||||
\inlinebash{IsaDofApplications}):
|
\inlinebash{IsaDofApplications}):
|
||||||
\begin{bash}
|
\begin{bash}
|
||||||
isabelle mkroot_DOF -o scholarly_paper -t lncs -d IsaDofApplications
|
isabelle dof_mkroot -o scholarly_paper -t lncs IsaDofApplications
|
||||||
\end{bash}
|
\end{bash}
|
||||||
where the \inlinebash{-o scholarly_paper} specifies the ontology for writing scientific articles and
|
where the \inlinebash{-o scholarly_paper} specifies the ontology for writing scientific articles and
|
||||||
\inlinebash{-t lncs} specifies the use of Springer's \LaTeX-configuration for the Lecture Notes in
|
\inlinebash{-t lncs} specifies the use of Springer's \LaTeX-configuration for the Lecture Notes in
|
||||||
|
|
|
@ -1,13 +1,15 @@
|
||||||
session "2018-cicm-isabelle_dof-applications" = "Isabelle_DOF" +
|
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,
|
||||||
|
dof_ontologies = "Isabelle_DOF.scholarly_paper", dof_template = Isabelle_DOF.lncs,
|
||||||
|
quick_and_dirty = true]
|
||||||
theories
|
theories
|
||||||
IsaDofApplications
|
IsaDofApplications
|
||||||
document_files
|
document_files
|
||||||
"isadof.cfg"
|
|
||||||
"root.bib"
|
"root.bib"
|
||||||
|
"authorarchive.sty"
|
||||||
"preamble.tex"
|
"preamble.tex"
|
||||||
"build"
|
|
||||||
"lstisadof.sty"
|
"lstisadof.sty"
|
||||||
|
"vector_iD_icon.pdf"
|
||||||
"figures/isabelle-architecture.pdf"
|
"figures/isabelle-architecture.pdf"
|
||||||
"figures/Dogfood-Intro.png"
|
"figures/Dogfood-Intro.png"
|
||||||
"figures/InteractiveMathSheet.png"
|
"figures/InteractiveMathSheet.png"
|
||||||
|
|
|
@ -0,0 +1,339 @@
|
||||||
|
%% Copyright (C) 2008-2019 Achim D. Brucker, https://www.brucker.ch
|
||||||
|
%%
|
||||||
|
%% 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
|
||||||
|
\NeedsTeXFormat{LaTeX2e}\relax
|
||||||
|
\ProvidesPackage{authorarchive}
|
||||||
|
[0000/00/00 Unreleased v1.1.1+%
|
||||||
|
Self-archiving information for scientific publications.]
|
||||||
|
%
|
||||||
|
\PassOptionsToPackage{hyphens}{url}
|
||||||
|
%
|
||||||
|
\RequirePackage{ifthen}
|
||||||
|
\RequirePackage[inline]{enumitem}
|
||||||
|
\RequirePackage{graphicx}
|
||||||
|
\RequirePackage{eso-pic}
|
||||||
|
\RequirePackage{intopdf}
|
||||||
|
\RequirePackage{kvoptions}
|
||||||
|
\RequirePackage{hyperref}
|
||||||
|
\RequirePackage{calc}
|
||||||
|
\RequirePackage{qrcode}
|
||||||
|
\RequirePackage{hvlogos}
|
||||||
|
%
|
||||||
|
%Better url breaking
|
||||||
|
\g@addto@macro{\UrlBreaks}{\UrlOrds}
|
||||||
|
%
|
||||||
|
% Option declarations
|
||||||
|
% -------------------
|
||||||
|
\SetupKeyvalOptions{
|
||||||
|
family=AA,
|
||||||
|
prefix=AA@
|
||||||
|
}
|
||||||
|
%
|
||||||
|
\DeclareStringOption[.]{bibtexdir}
|
||||||
|
\DeclareStringOption[https://duckduckgo.com/?q=]{baseurl}
|
||||||
|
\DeclareStringOption[.pdf]{suffix}
|
||||||
|
\DeclareStringOption[UNKNOWN PUBLISHER]{publisher}[]
|
||||||
|
\DeclareStringOption[UNKNOWN YEAR]{year}[]
|
||||||
|
\DeclareStringOption[]{key}[]
|
||||||
|
\DeclareStringOption[]{doi}[]
|
||||||
|
\DeclareStringOption[]{doiText}[]
|
||||||
|
\DeclareStringOption[]{publisherurl}[]
|
||||||
|
\DeclareStringOption[UNKNOWN START PAGE]{startpage}[]
|
||||||
|
\DeclareStringOption[UNKNOWN PUBLICATION]{publication}[]
|
||||||
|
|
||||||
|
\DeclareBoolOption{ACM}
|
||||||
|
\DeclareBoolOption{acmart}
|
||||||
|
\DeclareBoolOption{ENTCS}
|
||||||
|
\DeclareBoolOption{IEEE}
|
||||||
|
\DeclareBoolOption{LNCS}
|
||||||
|
\DeclareBoolOption{LNI}
|
||||||
|
\DeclareBoolOption{nocopyright}
|
||||||
|
\DeclareBoolOption{nourl}
|
||||||
|
\DeclareBoolOption{nobib}
|
||||||
|
\DeclareBoolOption{orcidicon}
|
||||||
|
%\ProcessOptions\relax
|
||||||
|
|
||||||
|
|
||||||
|
% Default option rule
|
||||||
|
\DeclareDefaultOption{%
|
||||||
|
\ifx\CurrentOptionValue\relax
|
||||||
|
\PackageWarningNoLine{\@currname}{%
|
||||||
|
Unknown option `\CurrentOption'\MessageBreak
|
||||||
|
is passed to package `authorarchive'%
|
||||||
|
}%
|
||||||
|
% Pass the option to package color.
|
||||||
|
% Again it is better to expand \CurrentOption.
|
||||||
|
\expandafter\PassOptionsToPackage\expandafter{\CurrentOption}{color}%
|
||||||
|
\else
|
||||||
|
% Package color does not take options with values.
|
||||||
|
% We provide the standard LaTeX error.
|
||||||
|
\@unknownoptionerror
|
||||||
|
\fi
|
||||||
|
}
|
||||||
|
\ProcessKeyvalOptions*
|
||||||
|
|
||||||
|
% Provide command for dynamic configuration seutp
|
||||||
|
\def\authorsetup{\kvsetkeys{AA}}
|
||||||
|
|
||||||
|
% Load local configuration
|
||||||
|
\InputIfFileExists{authorarchive.config}{}{}
|
||||||
|
|
||||||
|
|
||||||
|
\newlength\AA@x
|
||||||
|
\newlength\AA@y
|
||||||
|
\newlength\AA@width
|
||||||
|
|
||||||
|
\def\AA@bibBibTeX{\AA@bibtexdir/\AA@key.bib}
|
||||||
|
\def\AA@bibBibTeXLong{\AA@bibtexdir/\AA@key.bibtex}
|
||||||
|
\def\AA@bibWord{\AA@bibtexdir/\AA@key.word.xml}
|
||||||
|
\def\AA@bibEndnote{\AA@bibtexdir/\AA@key.enw}
|
||||||
|
\def\AA@bibRIS{\AA@bibtexdir/\AA@key.ris}
|
||||||
|
|
||||||
|
\newboolean{AA@bibExists}
|
||||||
|
\setboolean{AA@bibExists}{false}
|
||||||
|
\IfFileExists{\AA@bibBibTeX}{\setboolean{AA@bibExists}{true}}{}
|
||||||
|
\IfFileExists{\AA@bibBibTeXLong}{\setboolean{AA@bibExists}{true}}{}
|
||||||
|
\IfFileExists{\AA@bibWord}{\setboolean{AA@bibExists}{true}}{}
|
||||||
|
\IfFileExists{\AA@bibEndnote}{\setboolean{AA@bibExists}{true}}{}
|
||||||
|
\IfFileExists{\AA@bibRIS}{\setboolean{AA@bibExists}{true}}{}
|
||||||
|
|
||||||
|
\setlength\AA@x{1in+\hoffset+\oddsidemargin}
|
||||||
|
|
||||||
|
\newcommand{\authorcrfont}{\footnotesize}
|
||||||
|
\newcommand{\authorat}[1]{\AtPageUpperLeft{\put(\LenToUnit{\AA@x},\LenToUnit{.2cm-\paperheight}){#1}}}
|
||||||
|
\newcommand{\authorwidth}[1]{\setlength{\AA@width}{#1}}
|
||||||
|
\setlength{\AA@width}{\textwidth}
|
||||||
|
|
||||||
|
\def\AA@pageinfo{}
|
||||||
|
\ifthenelse{\equal{\AA@startpage}{UNKNOWN START PAGE}}{%
|
||||||
|
}{%
|
||||||
|
\setcounter{page}{\AA@startpage}%
|
||||||
|
\def\AA@pageinfo{pp. \thepage--\pageref{\aa@lastpage}, }
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
%%%% sig-alternate.cls
|
||||||
|
\ifAA@ACM%
|
||||||
|
\ifthenelse{\equal{\AA@publisher}{UNKNOWN PUBLISHER}}{%
|
||||||
|
\setkeys{AA}{publisher=ACM}
|
||||||
|
}{}
|
||||||
|
\global\boilerplate={}
|
||||||
|
\global\copyrightetc={}
|
||||||
|
\renewcommand{\conferenceinfo}[2]{}
|
||||||
|
\renewcommand{\authorcrfont}{\scriptsize}
|
||||||
|
\setlength\AA@x{1in+\hoffset+\oddsidemargin}
|
||||||
|
\setlength\AA@y{-\textheight+\topmargin+\headheight-\footskip} % -\voffset-\topmargin-\headheight-\footskip}
|
||||||
|
\renewcommand{\authorat}[1]{\put(\LenToUnit{\AA@x},\LenToUnit{\AA@y}){#1}}
|
||||||
|
\setlength{\AA@width}{\columnwidth}
|
||||||
|
\fi
|
||||||
|
%
|
||||||
|
%%%% acmart.cls
|
||||||
|
\ifAA@acmart%
|
||||||
|
\ifthenelse{\equal{\AA@publisher}{UNKNOWN PUBLISHER}}{%
|
||||||
|
\setkeys{AA}{publisher=ACM}
|
||||||
|
}{}
|
||||||
|
\renewcommand{\authorat}[1]{\AtPageUpperLeft{\put(\LenToUnit{\AA@x},\LenToUnit{0.2cm-\paperheight}){#1}}}
|
||||||
|
\setlength{\AA@width}{\textwidth}
|
||||||
|
\fi
|
||||||
|
%
|
||||||
|
%%%% LNCS
|
||||||
|
\ifAA@LNCS%
|
||||||
|
\ifAA@orcidicon%
|
||||||
|
\renewcommand{\orcidID}[1]{\href{https://orcid.org/#1}{%
|
||||||
|
\textsuperscript{\,\includegraphics[height=2\fontcharht\font`A]{vector_iD_icon}}}}
|
||||||
|
\else\relax\fi%
|
||||||
|
%
|
||||||
|
\ifthenelse{\equal{\AA@publisher}{UNKNOWN PUBLISHER}}{%
|
||||||
|
\setkeys{AA}{publisher=Springer-Verlag}
|
||||||
|
}{}
|
||||||
|
\renewcommand{\authorcrfont}{\scriptsize}
|
||||||
|
\@ifclasswith{llncs}{a4paper}{%
|
||||||
|
\ExplSyntaxOn
|
||||||
|
\@ifundefined{pdfmanagement_add:nnn}{%
|
||||||
|
\pdfpagesattr{/CropBox [92 114 523 780]}%
|
||||||
|
}{%
|
||||||
|
\pdfmanagement_add:nnn {Pages}{CropBox}{[92~114~523~780]}
|
||||||
|
}%
|
||||||
|
\ExplSyntaxOff
|
||||||
|
\renewcommand{\authorat}[1]{\put(\LenToUnit{\AA@x},40){#1}}%
|
||||||
|
}{%
|
||||||
|
\ExplSyntaxOn
|
||||||
|
\@ifundefined{pdfmanagement_add:nnn}{%
|
||||||
|
\pdfpagesattr{/CropBox [92 65 523 731]}% LNCS page: 152x235 mm
|
||||||
|
}{%
|
||||||
|
\pdfmanagement_add:nnn {Pages}{CropBox}{[92~62~523~731]}
|
||||||
|
}%
|
||||||
|
\ExplSyntaxOff
|
||||||
|
\renewcommand{\authorat}[1]{\put(\LenToUnit{\AA@x},23){#1}}
|
||||||
|
}
|
||||||
|
\setlength{\AA@width}{\textwidth}
|
||||||
|
\setcounter{tocdepth}{2}
|
||||||
|
\fi
|
||||||
|
%
|
||||||
|
%%%% LNI
|
||||||
|
\ifAA@LNI%
|
||||||
|
\ifthenelse{\equal{\AA@publisher}{UNKNOWN PUBLISHER}}{%
|
||||||
|
\setkeys{AA}{publisher=GI}
|
||||||
|
}{}
|
||||||
|
\renewcommand{\authorat}[1]{\put(\LenToUnit{\AA@x},35){#1}}
|
||||||
|
\renewcommand{\authorcrfont}{\scriptsize}
|
||||||
|
\pdfpagesattr{/CropBox [70 65 526.378 748.15]} % TODO
|
||||||
|
\setlength{\AA@width}{\textwidth}
|
||||||
|
\setcounter{tocdepth}{2}
|
||||||
|
\fi
|
||||||
|
%
|
||||||
|
%%%% ENTCS
|
||||||
|
\ifAA@ENTCS%
|
||||||
|
\addtolength{\voffset}{1cm}
|
||||||
|
\ifthenelse{\equal{\AA@publisher}{UNKNOWN PUBLISHER}}{%
|
||||||
|
\setkeys{AA}{publisher=Elsevier Science B.~V.}
|
||||||
|
}{}
|
||||||
|
\renewcommand{\authorat}[1]{\put(\LenToUnit{\AA@x},\LenToUnit{-.5cm-\the\ht\AA@authoratBox}){#1}}
|
||||||
|
\renewcommand{\authorcrfont}{\scriptsize}
|
||||||
|
\setlength{\AA@width}{\textwidth}
|
||||||
|
\fi
|
||||||
|
%
|
||||||
|
%%%% IEEE
|
||||||
|
\ifAA@IEEE%
|
||||||
|
\ifthenelse{\equal{\AA@publisher}{UNKNOWN PUBLISHER}}{%
|
||||||
|
\setkeys{AA}{publisher=IEEE}
|
||||||
|
}{}
|
||||||
|
\renewcommand{\authorat}[1]{\put(\LenToUnit{\AA@x},6){#1}}
|
||||||
|
\renewcommand{\authorcrfont}{\scriptsize}
|
||||||
|
\setlength{\AA@width}{\textwidth}
|
||||||
|
\setcounter{tocdepth}{2}
|
||||||
|
\fi
|
||||||
|
%
|
||||||
|
|
||||||
|
\hypersetup{%
|
||||||
|
draft = false,
|
||||||
|
bookmarksopen = true,
|
||||||
|
bookmarksnumbered= true,
|
||||||
|
pdfauthor = {\@author},
|
||||||
|
pdftitle = {\@title},
|
||||||
|
}
|
||||||
|
|
||||||
|
\@ifpackageloaded{totpages}{%
|
||||||
|
\def\aa@lastpage{TotPages}
|
||||||
|
}{%
|
||||||
|
\RequirePackage{lastpage}
|
||||||
|
\def\aa@lastpage{LastPage}
|
||||||
|
}
|
||||||
|
\newsavebox{\AA@authoratBox}
|
||||||
|
|
||||||
|
\AddToShipoutPicture*{%
|
||||||
|
\setlength{\unitlength}{1mm}%
|
||||||
|
\savebox{\AA@authoratBox}{%
|
||||||
|
\parbox{1.4cm}{%
|
||||||
|
\bgroup%
|
||||||
|
\normallineskiplimit=0pt%
|
||||||
|
\ifAA@nourl%
|
||||||
|
\ifx\AA@doi\@empty\relax%
|
||||||
|
\else%
|
||||||
|
\qrcode[hyperlink,height=1.17cm,padding]{https://doi.org/\AA@doi}%
|
||||||
|
\fi%
|
||||||
|
\else%
|
||||||
|
\qrcode[hyperlink,height=1.17cm,padding]{\AA@baseurl/\AA@key\AA@suffix}%
|
||||||
|
\fi%
|
||||||
|
\egroup%
|
||||||
|
}%
|
||||||
|
\ifAA@nourl\ifx\AA@doi\@empty\addtolength{\AA@width}{1.4cm}\fi\fi
|
||||||
|
\parbox{\AA@width-1.4cm}{\authorcrfont%
|
||||||
|
\ifAA@LNCS%
|
||||||
|
\AA@publication, \AA@pageinfo \AA@year. %
|
||||||
|
\ifAA@nocopyright\else
|
||||||
|
\textcopyright~\AA@year~\AA@publisher.
|
||||||
|
\fi
|
||||||
|
This is the author's
|
||||||
|
version of the work. It is posted
|
||||||
|
\ifAA@nourl\relax\else%
|
||||||
|
at \url{\AA@baseurl/\AA@key\AA@suffix} %
|
||||||
|
\fi
|
||||||
|
\ifAA@nocopyright\relax\else
|
||||||
|
by permission of \AA@publisher{}
|
||||||
|
\fi
|
||||||
|
for your personal use.
|
||||||
|
\ifx\AA@doi\@empty%
|
||||||
|
\relax
|
||||||
|
\else
|
||||||
|
The final publication is available at Springer via
|
||||||
|
\ifx\AA@doiText\@empty%
|
||||||
|
\url{https://doi.org/\AA@doi}.
|
||||||
|
\else
|
||||||
|
\href{https://doi.org/\AA@doi}{\AA@doiText}.
|
||||||
|
\fi
|
||||||
|
\fi
|
||||||
|
\else
|
||||||
|
\ifAA@nocopyright\relax\else
|
||||||
|
\textcopyright~\AA@year~\AA@publisher. %
|
||||||
|
\fi%
|
||||||
|
This is the author's
|
||||||
|
version of the work. It is posted
|
||||||
|
\ifAA@nourl\relax\else%
|
||||||
|
at \url{\AA@baseurl/\AA@key\AA@suffix} %
|
||||||
|
\fi
|
||||||
|
\ifAA@nocopyright\relax\else
|
||||||
|
by permission of \AA@publisher{} %
|
||||||
|
\fi
|
||||||
|
for your personal use. Not for redistribution. The definitive
|
||||||
|
version was published in \emph{\AA@publication}, \AA@pageinfo \AA@year%
|
||||||
|
\ifx\AA@doi\@empty%
|
||||||
|
\ifx\AA@publisherurl\@empty%
|
||||||
|
.%
|
||||||
|
\else
|
||||||
|
\url{\AA@publisherurl}.%
|
||||||
|
\fi
|
||||||
|
\else
|
||||||
|
\ifx\AA@doiText\@empty%
|
||||||
|
, doi: \href{https://doi.org/\AA@doi}{\AA@doi}.%
|
||||||
|
\else
|
||||||
|
, doi: \href{https://doi.org/\AA@doi}{\AA@doiText}.%
|
||||||
|
\fi
|
||||||
|
\fi
|
||||||
|
\fi
|
||||||
|
\ifAA@nobib\relax\else%
|
||||||
|
\ifthenelse{\boolean{AA@bibExists}}{%
|
||||||
|
\hfill
|
||||||
|
\begin{itemize*}[label={}, itemjoin={,}]
|
||||||
|
\IfFileExists{\AA@bibBibTeX}{%
|
||||||
|
\item \attachandlink{\AA@bibBibTeX}[application/x-bibtex]{BibTeX entry of this paper}{\BibTeX}%
|
||||||
|
}{%
|
||||||
|
\IfFileExists{\AA@bibBibTeXLong}{%
|
||||||
|
\item \attachandlink[\AA@key.bib]{\AA@bibBibTeXLong}[application/x-bibtex]{BibTeX entry of this paper}{\BibTeX}%
|
||||||
|
}{%
|
||||||
|
\typeout{No file \AA@bibBibTeX{} (and no \AA@bibBibTeXLong) found. Not embedded reference in BibTeX format.}%
|
||||||
|
}%
|
||||||
|
}%
|
||||||
|
\IfFileExists{\AA@bibWord}{%
|
||||||
|
\item \attachandlink{\AA@bibWord}[application/xml]{XML entry of this paper (e.g., for Word 2007 and later)}{Word}%
|
||||||
|
}{%
|
||||||
|
\typeout{No file \AA@bibWord{} found. Not embedded reference for Word 2007 and later.}%
|
||||||
|
}%
|
||||||
|
\IfFileExists{\AA@bibEndnote}{%
|
||||||
|
\item \attachandlink{\AA@bibEndnote}[application/x-endnote-refer]{Endnote entry of this paper}{EndNote}%
|
||||||
|
}{%
|
||||||
|
\typeout{No file \AA@bibEndnote{} found. Not embedded reference in Endnote format.}%
|
||||||
|
}%
|
||||||
|
\IfFileExists{\AA@bibRIS}{%
|
||||||
|
\item \attachandlink{\AA@bibRIS}[application/x-research-info-systems]{RIS entry of this paper}{RIS}%
|
||||||
|
}{%
|
||||||
|
\typeout{No file \AA@bibRIS{} found. Not embedded reference in RIS format.}%
|
||||||
|
}%
|
||||||
|
\end{itemize*}\\
|
||||||
|
}{%
|
||||||
|
\PackageError{authorarchive}{No bibliographic files found. Specify option 'nobib' if this is intended.}
|
||||||
|
}
|
||||||
|
\fi
|
||||||
|
}
|
||||||
|
}
|
||||||
|
\authorat{\raisebox{\the\ht\AA@authoratBox}{\usebox{\AA@authoratBox}}}
|
||||||
|
}
|
|
@ -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
|
|
0
examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-II-bgnd1.png
Executable file → Normal file
Before Width: | Height: | Size: 14 KiB After Width: | Height: | Size: 14 KiB |
0
examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-III-bgnd-text_section.png
Executable file → Normal file
Before Width: | Height: | Size: 18 KiB After Width: | Height: | Size: 18 KiB |
0
examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-IV-jumpInDocCLass.png
Executable file → Normal file
Before Width: | Height: | Size: 23 KiB After Width: | Height: | Size: 23 KiB |
0
examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-Intro.png
Executable file → Normal file
Before Width: | Height: | Size: 85 KiB After Width: | Height: | Size: 85 KiB |
0
examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-V-attribute.png
Executable file → Normal file
Before Width: | Height: | Size: 16 KiB After Width: | Height: | Size: 16 KiB |
0
examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-figures.png
Executable file → Normal file
Before Width: | Height: | Size: 18 KiB After Width: | Height: | Size: 18 KiB |
0
examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/InteractiveMathSheet.png
Executable file → Normal file
Before Width: | Height: | Size: 75 KiB After Width: | Height: | Size: 75 KiB |
0
examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/antiquotations-PIDE.png
Executable file → Normal file
Before Width: | Height: | Size: 96 KiB After Width: | Height: | Size: 96 KiB |
0
examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/isabelle-architecture.pdf
Executable file → Normal file
0
examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/isabelle-architecture.svg
Executable file → Normal file
Before Width: | Height: | Size: 57 KiB After Width: | Height: | Size: 57 KiB |
0
examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/srac-as-es-application.png
Executable file → Normal file
Before Width: | Height: | Size: 67 KiB After Width: | Height: | Size: 67 KiB |
0
examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/srac-definition.png
Executable file → Normal file
Before Width: | Height: | Size: 50 KiB After Width: | Height: | Size: 50 KiB |
|
@ -1,2 +0,0 @@
|
||||||
Template: scrartcl
|
|
||||||
Ontology: scholarly_paper
|
|
0
examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/lstisadof.sty
Executable file → Normal file
29
examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/preamble.tex
Executable file → Normal file
|
@ -53,23 +53,18 @@
|
||||||
\usepackage[size=footnotesize]{caption}
|
\usepackage[size=footnotesize]{caption}
|
||||||
|
|
||||||
|
|
||||||
\subject{Example of an Academic Paper\footnote{%
|
\usepackage[LNCS,
|
||||||
This document is an example setup for writing an academic paper. While
|
orcidicon,
|
||||||
it is optimized for the Springer's LNCS class, it uses a Koma Script
|
key=brucker.ea-isabelle-ontologies-2018,
|
||||||
LaTeX class to avoid the re-distribution of \texttt{llncs.cls},
|
year=2018,
|
||||||
which would violate Springer's copyright. This example has been
|
publication={F. Rabe et al. (Eds.): CICM 2018, LNAI 11006},
|
||||||
published at CICM 2018:
|
nobib,
|
||||||
\protect\begin{quote}
|
startpage={1},
|
||||||
Achim D. Brucker, Idir Ait-Sadoune, Paolo Crisafulli, and
|
doi={10.1007/978-3-319-96812-4_3},
|
||||||
Burkhart Wolff. Using The Isabelle Ontology Framework: Linking
|
doiText={10.1007/978-3-319-96812-4\_3},
|
||||||
the Formal with the Informal. In Conference on Intelligent
|
]{authorarchive}
|
||||||
Computer Mathematics (CICM). Lecture Notes in Computer Science
|
\authorrunning{A. D. Brucker et al.}
|
||||||
(11006), Springer-Verlag, 2018.
|
\pagestyle{headings}
|
||||||
\protect\end{quote}
|
|
||||||
Note that the content of this example is not updated and, hence,
|
|
||||||
might not be correct with respect to the latest version of
|
|
||||||
\isadof{}.
|
|
||||||
}}
|
|
||||||
|
|
||||||
|
|
||||||
\title{<TITLE>}
|
\title{<TITLE>}
|
||||||
|
|
0
examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/root.bib
Executable file → Normal file
|
@ -1,9 +1,8 @@
|
||||||
session "2020-iFM-csp" = "Isabelle_DOF" +
|
session "2020-iFM-csp" = "Isabelle_DOF" +
|
||||||
options [document = pdf, document_output = "output"]
|
options [document = pdf, document_output = "output", document_build = dof,
|
||||||
|
dof_ontologies = "Isabelle_DOF.scholarly_paper", dof_template = Isabelle_DOF.scrartcl]
|
||||||
theories
|
theories
|
||||||
"paper"
|
"paper"
|
||||||
document_files
|
document_files
|
||||||
"isadof.cfg"
|
|
||||||
"root.bib"
|
"root.bib"
|
||||||
"preamble.tex"
|
"preamble.tex"
|
||||||
"build"
|
|
||||||
|
|
|
@ -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
|
|
|
@ -1,2 +0,0 @@
|
||||||
Template: scrartcl
|
|
||||||
Ontology: scholarly_paper
|
|
|
@ -29,20 +29,6 @@ text\<open>
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
section*[getting_started::technical]\<open>Getting Started\<close>
|
section*[getting_started::technical]\<open>Getting Started\<close>
|
||||||
text\<open>
|
|
||||||
As an alternative to installing \<^isadof>{} locally, the latest official release of \<^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>}
|
|
||||||
|
|
||||||
Further configuration of the X11 permissions to authorize docker to start \<^isadof> might be required,
|
|
||||||
depending on the user system configuration.
|
|
||||||
\<close>
|
|
||||||
|
|
||||||
subsection*[installation::technical]\<open>Installation\<close>
|
subsection*[installation::technical]\<open>Installation\<close>
|
||||||
text\<open>
|
text\<open>
|
||||||
|
@ -50,8 +36,8 @@ text\<open>
|
||||||
\<^LaTeX>. We assume a basic familiarity with a Linux/Unix-like command line (i.e., a shell).
|
\<^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
|
\<^isadof> requires Isabelle\<^bindex>\<open>Isabelle\<close> (\isabellefullversion) with a recent \<^LaTeX>-distribution
|
||||||
(e.g., Tex Live 2021 or later).
|
(e.g., Tex Live 2022 or later).
|
||||||
\<^isadof> uses a two-part version system (e.g., 1.1.0/Isabelle2021), where the first part is the version
|
\<^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.
|
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.
|
Thus, the same version of \<^isadof> might be available for different versions of Isabelle.
|
||||||
\<close>
|
\<close>
|
||||||
|
@ -68,7 +54,7 @@ text\<open>
|
||||||
Depending on your operating system and depending if you put Isabelle's \<^boxed_bash>\<open>bin\<close> directory
|
Depending on your operating system and depending if you put Isabelle's \<^boxed_bash>\<open>bin\<close> directory
|
||||||
in your \<^boxed_bash>\<open>PATH\<close>, you will need to invoke \<^boxed_bash>\<open>isabelle\<close> using its
|
in your \<^boxed_bash>\<open>PATH\<close>, you will need to invoke \<^boxed_bash>\<open>isabelle\<close> using its
|
||||||
full qualified path, \<^eg>:
|
full qualified path, \<^eg>:
|
||||||
@{boxed_bash [display]\<open>ë\prompt{}ë /usr/local/Isabelleë\isabelleversionë/bin/isabelle version
|
@{boxed_bash [display]\<open>ë\prompt{}ë /usr/local/Isabelleë\isabelleversion/bin/isabelleë version
|
||||||
ë\isabellefullversionë\<close>}
|
ë\isabellefullversionë\<close>}
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
|
@ -83,36 +69,30 @@ text\<open>
|
||||||
subsubsection*[isadof::technical]\<open>Installing \<^isadof>\<close>
|
subsubsection*[isadof::technical]\<open>Installing \<^isadof>\<close>
|
||||||
text\<open>
|
text\<open>
|
||||||
In the following, we assume that you already downloaded the \<^isadof> distribution
|
In the following, we assume that you already downloaded the \<^isadof> distribution
|
||||||
(\href{\isadofarchiveurl}{\isadofarchiven}) from the \<^isadof> web site. The main steps for
|
(\href{\isadofarchiveurl}{\isadofarchiven}) from the \<^isadof> web site.
|
||||||
installing are extracting the \<^isadof> distribution and calling its \<^boxed_bash>\<open>install\<close> script.
|
|
||||||
We start by extracting the \<^isadof> archive:
|
We start by extracting the \<^isadof> archive:
|
||||||
@{boxed_bash [display]\<open>ë\prompt{}ë tar xf ë\href{\isadofarchiveurl}{\isadofarchiven}ë\<close>}
|
@{boxed_bash [display]\<open>ë\prompt{}ë tar xf ë\href{\isadofarchiveurl}{\isadofarchiven}ë\<close>}
|
||||||
This will create a directory \texttt{\isadofdirn} containing \<^isadof> distribution.
|
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 installation
|
|
||||||
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
|
Next, we need to register \<^isadof> as an Isabelle component:
|
||||||
\<^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
|
@{boxed_bash [display]\<open>ë\prompt{}ë isabelle components -u ë\mbox{\isadofdirn}ë\<close>}
|
||||||
you an overview of all available configuration options):
|
|
||||||
|
Moreover, \<^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 eëënv\<close> command:
|
||||||
|
|
||||||
@{boxed_bash [display]\<open>ë\prompt{}ë cd ë\isadofdirnë
|
@{boxed_bash [display]\<open>ë\prompt{}ë cd ë\isadofdirnë
|
||||||
ë\prompt{\isadofdirn}ë ./install --isabelle /usr/local/Isabelleë\isabelleversion/bin/isabelleë
|
ë\prompt{\isadofdirn}ë isabelle eëënv ë\mbox{./install-afp}ë
|
||||||
|
|
||||||
Isabelle/DOF Installer
|
Isabelle/DOF Installer
|
||||||
======================
|
======================
|
||||||
* Checking Isabelle version:
|
* Checking Isabelle version:
|
||||||
Success: found supported Isabelle version ë(\isabellefullversion)ë
|
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>}
|
* Checking availability of AFP entries:\<close>}
|
||||||
|
|
||||||
@{boxed_bash [display]
|
@{boxed_bash [display]
|
||||||
|
@ -124,18 +104,6 @@ Isabelle/DOF Installer
|
||||||
Registering Functional-Automata iëën
|
Registering Functional-Automata iëën
|
||||||
/home/achim/.isabelle/Isabelleë\isabelleversion/ROOTSë
|
/home/achim/.isabelle/Isabelleë\isabelleversion/ROOTSë
|
||||||
AFP installation successful.
|
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
|
* Installation successful. Enjoy Isabelle/DOF, you can build the session
|
||||||
Isabelle/DOF and all example documents by executing:
|
Isabelle/DOF and all example documents by executing:
|
||||||
/usr/local/Isabelleë\isabelleversion/bin/isabelleë build -D . \<close>}
|
/usr/local/Isabelleë\isabelleversion/bin/isabelleë build -D . \<close>}
|
||||||
|
@ -150,15 +118,17 @@ session and all example documents, execute:
|
||||||
subsection*[first_project::technical]\<open>Creating an \<^isadof> Project\<close>
|
subsection*[first_project::technical]\<open>Creating an \<^isadof> Project\<close>
|
||||||
text\<open>
|
text\<open>
|
||||||
\<^isadof> provides its own variant of Isabelle's
|
\<^isadof> provides its own variant of Isabelle's
|
||||||
\<^boxed_bash>\<open>mkroot\<close> tool, called \<^boxed_bash>\<open>mkroot_DOF\<close>\index{mkroot\_DOF}:
|
\<^boxed_bash>\<open>mkroot\<close> tool, called \<^boxed_bash>\<open>dof_mkroot\<close>\index{mkroot\_DOF}:
|
||||||
@{boxed_bash [display]\<open>ë\prompt{}ë isabelle mkroot_DOF myproject
|
@{boxed_bash [display]\<open>ë\prompt{}ë isabelle dof_mkroot myproject
|
||||||
|
|
||||||
Preparing session "myproject" iëën "myproject"
|
Preparing session "myproject" iëën "myproject"
|
||||||
creating "myproject/ROOT"
|
creating "myproject/ROOT"
|
||||||
creating "myproject/document/root.tex"
|
creating "myproject/myproject.thy"
|
||||||
|
creating "myproject/document/preamble.tex"
|
||||||
|
|
||||||
Now use the following coëëmmand line to build the session:
|
Now use the following commanëëd line to build the session:
|
||||||
isabelle build -D myproject \<close>}
|
|
||||||
|
isabelle build -D myproject\<close>}
|
||||||
The created project uses the default configuration (the ontology for writing academic papers
|
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
|
(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>
|
||||||
|
@ -174,22 +144,26 @@ The directory \<^boxed_bash>\<open>myproject\<close> contains the following fil
|
||||||
.1 .
|
.1 .
|
||||||
.2 myproject.
|
.2 myproject.
|
||||||
.3 document.
|
.3 document.
|
||||||
.4 build\DTcomment{Build Script}.
|
|
||||||
.4 isadof.cfg\DTcomment{\<^isadof> configuration}.
|
|
||||||
.4 preamble.tex\DTcomment{Manual \<^LaTeX>-configuration}.
|
.4 preamble.tex\DTcomment{Manual \<^LaTeX>-configuration}.
|
||||||
|
.3 myproject.thy\DTcomment{Example theory file}.
|
||||||
.3 ROOT\DTcomment{Isabelle build-configuration}.
|
.3 ROOT\DTcomment{Isabelle build-configuration}.
|
||||||
}
|
}
|
||||||
\end{minipage}
|
\end{minipage}
|
||||||
\end{center}
|
\end{center}
|
||||||
The \<^isadof> configuration (\<^boxed_bash>\<open>isadof.cfg\<close>) specifies the required
|
|
||||||
ontologies and the document template using a YAML syntax.\<^footnote>\<open>Isabelle power users will recognize that
|
The main two configuration files\<^footnote>\<open>Isabelle power users will recognize that
|
||||||
\<^isadof>'s document setup does not make use of a file \<^boxed_bash>\<open>root.tex\<close>: this file is
|
\<^isadof>'s document setup does not make use of a file \<^boxed_bash>\<open>root.tex\<close>: this file is
|
||||||
replaced by built-in document templates.\<close> The main two configuration files for
|
replaced by built-in document templates.\<close> for users are:
|
||||||
users are:
|
|
||||||
\<^item> The file \<^boxed_bash>\<open>ROOT\<close>\<^index>\<open>ROOT\<close>, which defines the Isabelle session. New theory files as well as new
|
\<^item> The file \<^boxed_bash>\<open>ROOT\<close>\<^index>\<open>ROOT\<close>, which defines the Isabelle session. New theory files as well as new
|
||||||
files required by the document generation (\<^eg>, images, bibliography database using \<^BibTeX>, local
|
files required by the document generation (\<^eg>, images, bibliography database using \<^BibTeX>, local
|
||||||
\<^LaTeX>-styles) need to be registered in this file. For details of Isabelle's build system, please
|
\<^LaTeX>-styles) need to be registered in this file. For details of Isabelle's build system, please
|
||||||
consult the Isabelle System Manual~@{cite "wenzel:system-manual:2020"}.
|
consult the Isabelle System Manual~@{cite "wenzel:system-manual:2020"}. In addition to the
|
||||||
|
standard features of, this file also contains \<^isadof> specific configurations:
|
||||||
|
\<^item> \<^boxed_bash>\<open>dof_ontologies\<close> a list of (fully qualified) ontologies, separated by spaces, used
|
||||||
|
by the project.
|
||||||
|
\<^item> \<^boxed_bash>\<open>dof_template\<close> the (fully qualified) document template.
|
||||||
|
\<^item> \<^boxed_bash>\<open>document_build=dof\<close> needs to be present, to tell Isabelle, to use the
|
||||||
|
Isabelle/DOF backend for the document generation.
|
||||||
\<^item> The file \<^boxed_bash>\<open>preamble.tex\<close>\<^index>\<open>preamble.tex\<close>, which allows users to add additional
|
\<^item> The file \<^boxed_bash>\<open>preamble.tex\<close>\<^index>\<open>preamble.tex\<close>, which allows users to add additional
|
||||||
\<^LaTeX>-packages or to add/modify \<^LaTeX>-commands.
|
\<^LaTeX>-packages or to add/modify \<^LaTeX>-commands.
|
||||||
\<close>
|
\<close>
|
||||||
|
@ -202,32 +176,21 @@ text\<open>
|
||||||
obtains and adds the necessary \<^LaTeX> class file.
|
obtains and adds the necessary \<^LaTeX> class file.
|
||||||
This is due to licensing restrictions).\<close>
|
This is due to licensing restrictions).\<close>
|
||||||
text\<open>
|
text\<open>
|
||||||
This can be configured by using the command-line options of \<^boxed_bash>\<open>mkroot_DOF\<close>. In
|
This can be configured by using the command-line options of \<^boxed_bash>\<open>dof_mkroot\<close>. In
|
||||||
Particular, \<^boxed_bash>\<open>-o\<close> allows selecting the ontology and \<^boxed_bash>\<open>-t\<close> allows selecting
|
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
|
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:
|
|
||||||
|
|
||||||
@{boxed_bash [display]\<open>ë\prompt{}ë isabelle mkroot_DOF -h
|
@{boxed_bash [display]\<open>ë\prompt{}ë isabelle dof_mkroot -h
|
||||||
|
|
||||||
Usage: isabelle mkroot_DOF [OPTIONS] [DIR]
|
Usage: isabelle dof_mkroot [OPTIONS] [DIRECTORY]
|
||||||
|
|
||||||
Options are:
|
Options are:
|
||||||
-h print this hëëelp text and exëëit
|
-I init Mercurial repository and add generated files
|
||||||
-n NAME alternative session name (default: DIR base name)
|
-n NAME alternative session name (default: directory base name)
|
||||||
-o ONTOLOGY (default: scholarly_paper)
|
-o ONTOLOGY ontology (default: scholarly_paper)
|
||||||
Available ontologies:
|
-t TEMPLATE tempalte (default: scrartcl)
|
||||||
* CENELEC_50128
|
|
||||||
* math_exam
|
|
||||||
* scholarly_paper
|
|
||||||
* technical_report
|
|
||||||
-t TEMPLATE (default: scrartcl)
|
|
||||||
Available document templates:
|
|
||||||
* lncs
|
|
||||||
* scrartcl
|
|
||||||
* scrreprt-modern
|
|
||||||
* scrreprt
|
|
||||||
|
|
||||||
Prepare session root DIR (default: current directory). \<close>}
|
Prepare session root directory (default: current directory).\<close>}
|
||||||
|
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
|
@ -541,9 +504,6 @@ side_by_side_figure*["hyperlinks"::side_by_side_figure,anchor="''fig:Dogfood-IV-
|
||||||
caption2="''Exploring an attribute (hyperlinked to the class).''",
|
caption2="''Exploring an attribute (hyperlinked to the class).''",
|
||||||
relative_width2="47",
|
relative_width2="47",
|
||||||
src2="''figures/Dogfood-V-attribute''"]\<open>Navigation via generated hyperlinks.\<close>
|
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>
|
text\<open>
|
||||||
From these class definitions, \<^isadof> also automatically generated editing
|
From these class definitions, \<^isadof> also automatically generated editing
|
||||||
|
|
|
@ -324,21 +324,28 @@ is currently only available in the SML API's of the kernel.
|
||||||
as specified in @{technical \<open>odl-manual0\<close>}.
|
as specified in @{technical \<open>odl-manual0\<close>}.
|
||||||
\<^item> \<open>meta_args\<close> :
|
\<^item> \<open>meta_args\<close> :
|
||||||
\<^rail>\<open>obj_id ('::' class_id) ((',' attribute '=' HOL_term) *) \<close>
|
\<^rail>\<open>obj_id ('::' class_id) ((',' attribute '=' HOL_term) *) \<close>
|
||||||
|
\<^item> \<^emph>\<open>evaluator\<close>: from @{cite "wenzel:isabelle-isar:2020"}, evaluation is tried first using ML,
|
||||||
|
falling back to normalization by evaluation if this fails. Alternatively a specific
|
||||||
|
evaluator can be selected using square brackets; typical evaluators use the
|
||||||
|
current set of code equations to normalize and include \<open>simp\<close> for fully
|
||||||
|
symbolic evaluation using the simplifier, \<open>nbe\<close> for \<^emph>\<open>normalization by
|
||||||
|
evaluation\<close> and \<^emph>\<open>code\<close> for code generation in SML.
|
||||||
\<^item> \<open>upd_meta_args\<close> :
|
\<^item> \<open>upd_meta_args\<close> :
|
||||||
\<^rail>\<open> (obj_id ('::' class_id) ((',' attribute ('=' | '+=') HOL_term) * ))\<close>
|
\<^rail>\<open> (obj_id ('::' class_id) ((',' attribute (':=' | '+=') HOL_term) * ))\<close>
|
||||||
\<^item> \<open>annotated_text_element\<close> :
|
\<^item> \<open>annotated_text_element\<close> :
|
||||||
\<^rail>\<open>
|
\<^rail>\<open>
|
||||||
( ( @@{command "text*"} '[' meta_args ']' '\<open>' formal_text '\<close>'
|
( @@{command "text*"} '[' meta_args ']' '\<open>' formal_text '\<close>'
|
||||||
| @@{command "ML*"} ('[' meta_args ']')? '\<open>' SML_code '\<close>'
|
| @@{command "ML*"} ('[' meta_args ']')? '\<open>' SML_code '\<close>'
|
||||||
| @@{command "term*"} ('[' meta_args ']')? '\<open>' HOL_term '\<close>'
|
| @@{command "term*"} ('[' meta_args ']')? '\<open>' HOL_term '\<close>'
|
||||||
| @@{command "value*"} ('[' meta_args ']')? '\<open>' HOL_term '\<close>'
|
| @@{command "value*"} \<newline> ('[' meta_args ']' ('[' evaluator ']')?)? '\<open>' HOL_term '\<close>'
|
||||||
)
|
| @@{command "assert*"} \<newline> ('[' meta_args ']' ('[' evaluator ']')?)? '\<open>' HOL_term '\<close>'
|
||||||
|
|
)
|
||||||
( @@{command "open_monitor*"}
|
\<close>
|
||||||
|
\<^rail>\<open>
|
||||||
|
( @@{command "open_monitor*"}
|
||||||
| @@{command "close_monitor*"}
|
| @@{command "close_monitor*"}
|
||||||
| @@{command "declare_reference*"}
|
| @@{command "declare_reference*"}
|
||||||
) '[' meta_args ']'
|
) '[' meta_args ']'
|
||||||
)
|
|
||||||
| change_status_command
|
| change_status_command
|
||||||
| inspection_command
|
| inspection_command
|
||||||
| macro_command
|
| macro_command
|
||||||
|
@ -399,23 +406,35 @@ in the context of the SML toplevel of the Isabelle system as in the correspondin
|
||||||
\<^theory_text>\<open>ML\<open> \<dots> SML-code \<dots> \<close>\<close>-command.
|
\<^theory_text>\<open>ML\<open> \<dots> SML-code \<dots> \<close>\<close>-command.
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
|
(*<*)
|
||||||
|
declare_reference*["text-elements-expls"::technical]
|
||||||
|
(*>*)
|
||||||
|
|
||||||
subsection\<open>Ontological Term-Contexts and their Management\<close>
|
subsection\<open>Ontological Term-Contexts and their Management\<close>
|
||||||
text\<open>The major commands providing term-contexts are
|
text\<open>The major commands providing term-contexts are
|
||||||
\<^theory_text>\<open>term*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close> and
|
\<^theory_text>\<open>term*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close>,
|
||||||
\<^theory_text>\<open>value*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close>\<^footnote>\<open>The meta-argument list is optional.\<close>.
|
\<^theory_text>\<open>value*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close> and
|
||||||
|
\<^theory_text>\<open>assert*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close>\<^footnote>\<open>The meta-argument list is optional.\<close>.
|
||||||
Wrt. creation, track-ability and checking they are analogous to the ontological text and
|
Wrt. creation, track-ability and checking they are analogous to the ontological text and
|
||||||
code-commands. However the argument terms may contain term-antiquotations stemming from an
|
code-commands. However the argument terms may contain term-antiquotations stemming from an
|
||||||
ontology definition. Both term-contexts were type-checked and \<^emph>\<open>validated\<close> against
|
ontology definition. Both term-contexts were type-checked and \<^emph>\<open>validated\<close> against
|
||||||
the global context (so: in the term \<open>@{A \<open>oid\<close>}\<close>, \<open>oid\<close> is indeed a string which refers
|
the global context (so: in the term \<open>@{A \<open>oid\<close>}\<close>, \<open>oid\<close> is indeed a string which refers
|
||||||
to a meta-object belonging to the document class \<open>A\<close>, for example).
|
to a meta-object belonging to the document class \<open>A\<close>, for example).
|
||||||
The term-context in the \<open>value*\<close>-command is additionally expanded (\<^eg> replaced) by a term
|
The term-context in the \<open>value*\<close>-command and \<^emph>\<open>assert*\<close>-command is additionally expanded
|
||||||
denoting the meta-object. This expansion happens \<^emph>\<open>before\<close> evaluation of the term, thus permitting
|
(\<^eg> replaced) by a term denoting the meta-object.
|
||||||
|
This expansion happens \<^emph>\<open>before\<close> evaluation of the term, thus permitting
|
||||||
executable HOL-functions to interact with meta-objects.
|
executable HOL-functions to interact with meta-objects.
|
||||||
|
The \<^emph>\<open>assert*\<close>-command allows for logical statements to be checked in the global context
|
||||||
|
(see @{technical (unchecked) \<open>text-elements-expls\<close>}).
|
||||||
|
% TODO:
|
||||||
|
% Section reference @{docitem (unchecked) \<open>text-elements-expls\<close>} has not the right number
|
||||||
|
This is particularly useful to explore formal definitions wrt. their border cases.
|
||||||
|
|
||||||
Note unspecified attribute values were represented by free fresh variables which constrains \<^dof>
|
Note unspecified attribute values were represented by free fresh variables which constrains \<^dof>
|
||||||
to choose either the normalization-by-evaluation strategy \<^theory_text>\<open>nbe\<close> or a proof attempt via
|
to choose either the normalization-by-evaluation strategy \<^theory_text>\<open>nbe\<close> or a proof attempt via
|
||||||
the \<^theory_text>\<open>auto\<close> method. A failure of these strategies will be reported and regarded as non-validation
|
the \<^theory_text>\<open>auto\<close> method. A failure of these strategies will be reported and regarded as non-validation
|
||||||
of this meta-object. The latter leads to a failure of the entire command.
|
of this meta-object. The latter leads to a failure of the entire command.
|
||||||
|
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
(*<*)
|
(*<*)
|
||||||
|
@ -619,9 +638,6 @@ during the editing process but is only visible in the integrated source but usua
|
||||||
a \<^typ>\<open>text_element\<close> to a specific \<^typ>\<open>author\<close>. Note that this is possible since \<^isadof> assigns to each
|
a \<^typ>\<open>text_element\<close> to a specific \<^typ>\<open>author\<close>. Note that this is possible since \<^isadof> assigns to each
|
||||||
document class also a class-type which is declared in the HOL environment.\<close>
|
document class also a class-type which is declared in the HOL environment.\<close>
|
||||||
|
|
||||||
(*<*)
|
|
||||||
declare_reference*["text-elements-expls"::example]
|
|
||||||
(*>*)
|
|
||||||
text*[s23::example, main_author = "Some(@{author \<open>bu\<close>})"]\<open>
|
text*[s23::example, main_author = "Some(@{author \<open>bu\<close>})"]\<open>
|
||||||
Recall that concrete authors can be denoted by term-antiquotations generated by \<^isadof>; for example,
|
Recall that concrete authors can be denoted by term-antiquotations generated by \<^isadof>; for example,
|
||||||
this may be for a text fragment like
|
this may be for a text fragment like
|
||||||
|
@ -649,7 +665,7 @@ of the \<^isadof> language:
|
||||||
\<newline>
|
\<newline>
|
||||||
'[' meta_args ']' '\<open>' text '\<close>'
|
'[' meta_args ']' '\<open>' text '\<close>'
|
||||||
)
|
)
|
||||||
| @@{command "assert*"} '[' meta_args ']' '\<open>' term '\<close>'
|
|
||||||
\<close>
|
\<close>
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
|
@ -680,29 +696,28 @@ text\<open>
|
||||||
\<^boxed_theory_text>\<open>title*\<open> ... \<close>\<close> or \<^boxed_theory_text>\<open>section*\<open> ... \<close>\<close>, \<^eg>:
|
\<^boxed_theory_text>\<open>title*\<open> ... \<close>\<close> or \<^boxed_theory_text>\<open>section*\<open> ... \<close>\<close>, \<^eg>:
|
||||||
|
|
||||||
@{boxed_theory_text [display]\<open>
|
@{boxed_theory_text [display]\<open>
|
||||||
title*[title::title]\<open>Isabelle/DOF\<close>
|
title*[title::title]\<open>Isabelle/DOF\<close>
|
||||||
subtitle*[subtitle::subtitle]\<open>User and Implementation Manual\<close>
|
subtitle*[subtitle::subtitle]\<open>User and Implementation Manual\<close>
|
||||||
author*[adb::author, email="\<open>a.brucker@exeter.ac.uk\<close>",
|
author*[adb::author, email="\<open>a.brucker@exeter.ac.uk\<close>",
|
||||||
orcid="\<open>0000-0002-6355-1200\<close>", http_site="\<open>https://brucker.ch/\<close>",
|
orcid="\<open>0000-0002-6355-1200\<close>", http_site="\<open>https://brucker.ch/\<close>",
|
||||||
affiliation="\<open>University of Exeter, Exeter, UK\<close>"] \<open>Achim D. Brucker\<close>
|
affiliation="\<open>University of Exeter, Exeter, UK\<close>"] \<open>Achim D. Brucker\<close>
|
||||||
author*[bu::author, email = "\<open>wolff@lri.fr\<close>",
|
author*[bu::author, email = "\<open>wolff@lri.fr\<close>",
|
||||||
affiliation = "\<open>Université Paris-Saclay, LRI, Paris, France\<close>"]\<open>Burkhart Wolff\<close>
|
affiliation = "\<open>Université Paris-Saclay, LRI, Paris, France\<close>"]\<open>Burkhart Wolff\<close>\<close>}
|
||||||
\<close>}
|
|
||||||
|
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
text\<open>Assertions allow for logical statements to be checked in the global context.
|
text\<open>Assertions allow for logical statements to be checked in the global context.
|
||||||
This is particularly useful to explore formal definitions wrt. their border cases. \<close>
|
This is particularly useful to explore formal definitions wrt. their border cases.
|
||||||
|
@{boxed_theory_text [display]\<open>
|
||||||
assert*[ass1::assertion, short_name = "\<open>This is an assertion\<close>"] \<open>last [3] < (4::int)\<close>
|
assert*[ass1::assertion, short_name = "\<open>This is an assertion\<close>"] \<open>last [3] < (4::int)\<close>\<close>}
|
||||||
|
\<close>
|
||||||
|
|
||||||
text\<open>We want to check the consequences of this definition and can add the following statements:
|
text\<open>We want to check the consequences of this definition and can add the following statements:
|
||||||
@{boxed_theory_text [display]\<open>
|
@{boxed_theory_text [display]\<open>
|
||||||
text*[claim::assertion]\<open>For non-empty lists, our definition yields indeed
|
text*[claim::assertion]\<open>For non-empty lists, our definition yields indeed
|
||||||
the last element of a list.\<close>
|
the last element of a list.\<close>
|
||||||
assert*[claim1::assertion] \<open>last[4::int] = 4\<close>
|
assert*[claim1::assertion] \<open>last[4::int] = 4\<close>
|
||||||
assert*[claim2::assertion] \<open>last[1,2,3,4::int] = 4\<close>
|
assert*[claim2::assertion] \<open>last[1,2,3,4::int] = 4\<close>\<close>}
|
||||||
\<close>}
|
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
text\<open>
|
text\<open>
|
||||||
|
@ -714,14 +729,12 @@ However, in order to avoid the somewhat tedious consequence:
|
||||||
|
|
||||||
the choice of the default class can be influenced by setting globally an attribute such as
|
the choice of the default class can be influenced by setting globally an attribute such as
|
||||||
@{boxed_theory_text [display]
|
@{boxed_theory_text [display]
|
||||||
\<open>declare[[ Definition_default_class = "definition"]]
|
\<open>declare[[Definition_default_class = "definition"]]
|
||||||
declare[[ Theorem_default_class = "theorem"]]
|
declare[[Theorem_default_class = "theorem"]]\<close>}
|
||||||
\<close>}
|
|
||||||
|
|
||||||
which allows the above example be shortened to:
|
which allows the above example be shortened to:
|
||||||
@{boxed_theory_text [display]
|
@{boxed_theory_text [display]
|
||||||
\<open>Theorem*[T1, short_name="\<open>DF definition captures deadlock-freeness\<close>"] \<open> \<dots> \<close>
|
\<open>Theorem*[T1, short_name="\<open>DF definition captures deadlock-freeness\<close>"] \<open> \<dots> \<close>\<close>}
|
||||||
\<close>}
|
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
subsection\<open>The Ontology \<^verbatim>\<open>technical_report\<close>\<close>
|
subsection\<open>The Ontology \<^verbatim>\<open>technical_report\<close>\<close>
|
||||||
|
@ -993,12 +1006,9 @@ text\<open>
|
||||||
entities, \<^eg>, \<^ML_type>\<open>term\<close> (\<open>\<lambda>\<close>-term), \<^ML_type>\<open>typ\<close>, or
|
entities, \<^eg>, \<^ML_type>\<open>term\<close> (\<open>\<lambda>\<close>-term), \<^ML_type>\<open>typ\<close>, or
|
||||||
\<^ML_type>\<open>thm\<close>, we represent the types of the implementation language
|
\<^ML_type>\<open>thm\<close>, we represent the types of the implementation language
|
||||||
\<^emph>\<open>inside\<close> the HOL type system. We do, however, not reflect the data of
|
\<^emph>\<open>inside\<close> the HOL type system. We do, however, not reflect the data of
|
||||||
these types. They are just declared abstract types,
|
these types. They are just types declared in HOL,
|
||||||
``inhabited'' by special constant symbols carrying strings, for
|
which are ``inhabited'' by special constant symbols carrying strings, for
|
||||||
example of the format \<^boxed_theory_text>\<open>@{thm <string>}\<close>.
|
example of the format \<^boxed_theory_text>\<open>@{thm <string>}\<close>.
|
||||||
% TODO:
|
|
||||||
% Update meta-types implementation explanation to the new implementation
|
|
||||||
% in repository commit 08c101c5440eee2a087068581952026e88c39f6a
|
|
||||||
When HOL
|
When HOL
|
||||||
expressions were used to denote values of \<^boxed_theory_text>\<open>doc_class\<close>
|
expressions were used to denote values of \<^boxed_theory_text>\<open>doc_class\<close>
|
||||||
instance attributes, this requires additional checks after
|
instance attributes, this requires additional checks after
|
||||||
|
@ -1226,12 +1236,11 @@ section*[infrastructure::technical]\<open>Technical Infrastructure\<close>
|
||||||
text\<open>
|
text\<open>
|
||||||
The list of fully supported (\<^ie>, supporting both interactive ontological modeling and
|
The list of fully supported (\<^ie>, supporting both interactive ontological modeling and
|
||||||
document generation) ontologies and the list of supported document templates can be
|
document generation) ontologies and the list of supported document templates can be
|
||||||
obtained by calling \<^boxed_bash>\<open>isabelle mkroot_DOF -h\<close> (see \<^technical>\<open>first_project\<close>).
|
obtained by calling \<^boxed_bash>\<open>isabelle dof_mkroot -h\<close> (see \<^technical>\<open>first_project\<close>).
|
||||||
Note that the postfix \<^boxed_bash>\<open>-UNSUPPORTED\<close> denotes experimental ontologies or templates
|
Note that the postfix \<^boxed_bash>\<open>-UNSUPPORTED\<close> denotes experimental ontologies or templates
|
||||||
for which further manual setup steps might be required or that are not fully tested. Also note
|
for which further manual setup steps might be required or that are not fully tested. Also note
|
||||||
that the \<^LaTeX>-class files required by the templates need to be already installed on your
|
that the \<^LaTeX>-class files required by the templates need to be already installed on your
|
||||||
system. This is mostly a problem for publisher specific templates (\<^eg>, Springer's
|
system. This is mostly a problem for publisher specific templates, which cannot be re-distributed due to copyright restrictions.
|
||||||
\<^path>\<open>llncs.cls\<close>), which cannot be re-distributed due to copyright restrictions.
|
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
subsection\<open>Developing Ontologies and their Representation Mappings\<close>
|
subsection\<open>Developing Ontologies and their Representation Mappings\<close>
|
||||||
|
@ -1282,9 +1291,9 @@ text\<open>
|
||||||
file \<^path>\<open>src/ontologies/foo/DOF-foo.sty\<close>
|
file \<^path>\<open>src/ontologies/foo/DOF-foo.sty\<close>
|
||||||
\<^item> registration (as import) of the new ontology in the file \<^path>\<open>src/ontologies/ontologies.thy\<close>.
|
\<^item> registration (as import) of the new ontology in the file \<^path>\<open>src/ontologies/ontologies.thy\<close>.
|
||||||
\<^item> activation of the new document setup by executing the install script. You can skip the lengthy
|
\<^item> activation of the new document setup by executing the install script. You can skip the lengthy
|
||||||
checks for the AFP entries by using the
|
checks for the AFP entries and the installation of the Isabelle patch by using the
|
||||||
\<^boxed_bash>\<open>--skip-patch-and-afp\<close> option:
|
\<^boxed_bash>\<open>--skip-afp\<close> option:
|
||||||
@{boxed_bash [display] \<open>ë\prompt{\isadofdirn}ë ./install --skip-patch-and-afp\<close>}
|
@{boxed_bash [display] \<open>ë\prompt{\isadofdirn}ë ./install --skip-afp\<close>}
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
subsection\<open>Document Templates\<close>
|
subsection\<open>Document Templates\<close>
|
||||||
|
@ -1313,8 +1322,8 @@ text\<open>
|
||||||
\<^item> develop a new \<^LaTeX>-template \<^boxed_bash>\<open>src/document-templates/root-bar.tex\<close>
|
\<^item> develop a new \<^LaTeX>-template \<^boxed_bash>\<open>src/document-templates/root-bar.tex\<close>
|
||||||
\<^item> activation of the new document template by executing the \<^boxed_bash>\<open>install\<close> script. You can skip the lengthy
|
\<^item> activation of the new document template by executing the \<^boxed_bash>\<open>install\<close> script. You can skip the lengthy
|
||||||
checks for the AFP entries and the installation of the Isabelle patch by using the
|
checks for the AFP entries and the installation of the Isabelle patch by using the
|
||||||
\<^boxed_bash>\<open>--skip-patch-and-afp\<close> option:
|
\<^boxed_bash>\<open>--skip-afp\<close> option:
|
||||||
@{boxed_bash [display] \<open>ë\prompt{\isadofdirn}ë ./install --skip-patch-and-afp\<close>}
|
@{boxed_bash [display] \<open>ë\prompt{\isadofdirn}ë ./install --skip-afp\<close>}
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
|
|
||||||
|
@ -1351,14 +1360,7 @@ text\<open>
|
||||||
\usepackage{isabelle,isabellesym,amssymb} % Required (by Isabelle)
|
\usepackage{isabelle,isabellesym,amssymb} % Required (by Isabelle)
|
||||||
\usepackage{amsmath} % Used by some ontologies
|
\usepackage{amsmath} % Used by some ontologies
|
||||||
\bibliographystyle{abbrv}
|
\bibliographystyle{abbrv}
|
||||||
\IfFileExists{DOF-core.sty}{}{ % Required by Isabelle/DOF
|
\input{dof-common} % setup shared between all Isabelle/DOF templates
|
||||||
\PackageError{DOF-core}{The doëëcument preparation
|
|
||||||
requires the Isabelle/DOF framework.}{For further help, see
|
|
||||||
ë\url{\dofurl}ë
|
|
||||||
}
|
|
||||||
\input{ontologies} % This will include the document specific
|
|
||||||
% ontologies from isadof.cfg
|
|
||||||
\IfFileExists{preamble.tex}{\input{preamble.tex}}{}
|
|
||||||
\usepackage{graphicx} % Required for images.
|
\usepackage{graphicx} % Required for images.
|
||||||
\usepackage[caption]{subfig}
|
\usepackage[caption]{subfig}
|
||||||
\usepackage[size=footnotesize]{caption}
|
\usepackage[size=footnotesize]{caption}
|
||||||
|
@ -1384,7 +1386,7 @@ text\<open>
|
||||||
|
|
||||||
subsubsection\<open>Getting Started\<close>
|
subsubsection\<open>Getting Started\<close>
|
||||||
text\<open>
|
text\<open>
|
||||||
In general, we recommend creating a test project (\<^eg>, using \<^boxed_bash>\<open>isabelle mkroot_DOF\<close>)
|
In general, we recommend creating a test project (\<^eg>, using \<^boxed_bash>\<open>isabelle dof_mkroot\<close>)
|
||||||
to develop new document templates or ontology representations. The default setup of the \<^isadof>
|
to develop new document templates or ontology representations. The default setup of the \<^isadof>
|
||||||
build system generated a \<^path>\<open>output/document\<close> directory with a self-contained \<^LaTeX>-setup. In
|
build system generated a \<^path>\<open>output/document\<close> directory with a self-contained \<^LaTeX>-setup. In
|
||||||
this directory, you can directly use \<^LaTeX> on the main file, called \<^path>\<open>root.tex\<close>:
|
this directory, you can directly use \<^LaTeX> on the main file, called \<^path>\<open>root.tex\<close>:
|
||||||
|
|
0
examples/technical_report/Isabelle_DOF-Manual/Isabelle_DOF-Manual.thy
Executable file → Normal file
|
@ -1,13 +1,13 @@
|
||||||
session "Isabelle_DOF-Manual" = "Isabelle_DOF" +
|
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,
|
||||||
|
dof_ontologies = "Isabelle_DOF.technical_report Isabelle_DOF.cenelec_50128", dof_template = "Isabelle_DOF.scrreprt-modern",
|
||||||
|
quick_and_dirty = true]
|
||||||
theories
|
theories
|
||||||
"Isabelle_DOF-Manual"
|
"Isabelle_DOF-Manual"
|
||||||
document_files
|
document_files
|
||||||
"isadof.cfg"
|
|
||||||
"root.bib"
|
"root.bib"
|
||||||
"root.mst"
|
"root.mst"
|
||||||
"preamble.tex"
|
"preamble.tex"
|
||||||
"build"
|
|
||||||
"lstisadof-manual.sty"
|
"lstisadof-manual.sty"
|
||||||
"figures/antiquotations-PIDE.png"
|
"figures/antiquotations-PIDE.png"
|
||||||
"figures/cicm2018-combined.png"
|
"figures/cicm2018-combined.png"
|
||||||
|
|
|
@ -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-II-bgnd1.png
Executable file → Normal file
Before Width: | Height: | Size: 14 KiB After Width: | Height: | Size: 10 KiB |
BIN
examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-III-bgnd-text_section.png
Executable file → Normal file
Before Width: | Height: | Size: 18 KiB After Width: | Height: | Size: 10 KiB |
BIN
examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-IV-jumpInDocCLass.png
Executable file → Normal file
Before Width: | Height: | Size: 23 KiB After Width: | Height: | Size: 17 KiB |
0
examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-Intro.png
Executable file → Normal file
Before Width: | Height: | Size: 85 KiB After Width: | Height: | Size: 85 KiB |
BIN
examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-V-attribute.png
Executable file → Normal file
Before Width: | Height: | Size: 16 KiB After Width: | Height: | Size: 13 KiB |
0
examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-figures.png
Executable file → Normal file
Before Width: | Height: | Size: 18 KiB After Width: | Height: | Size: 18 KiB |
0
examples/technical_report/Isabelle_DOF-Manual/document/figures/Isabelle_DOF-logo.pdf
Executable file → Normal file
0
examples/technical_report/Isabelle_DOF-Manual/document/figures/MyCommentedIsabelle.png
Executable file → Normal file
Before Width: | Height: | Size: 162 KiB After Width: | Height: | Size: 162 KiB |
0
examples/technical_report/Isabelle_DOF-Manual/document/figures/antiquotations-PIDE.png
Executable file → Normal file
Before Width: | Height: | Size: 43 KiB After Width: | Height: | Size: 43 KiB |
0
examples/technical_report/Isabelle_DOF-Manual/document/figures/cicm2018-combined.png
Executable file → Normal file
Before Width: | Height: | Size: 214 KiB After Width: | Height: | Size: 214 KiB |
0
examples/technical_report/Isabelle_DOF-Manual/document/figures/cicm2018-dof.png
Executable file → Normal file
Before Width: | Height: | Size: 135 KiB After Width: | Height: | Size: 135 KiB |
0
examples/technical_report/Isabelle_DOF-Manual/document/figures/cicm2018-pdf.png
Executable file → Normal file
Before Width: | Height: | Size: 73 KiB After Width: | Height: | Size: 73 KiB |
0
examples/technical_report/Isabelle_DOF-Manual/document/figures/definition-use-CSP-pdf.png
Executable file → Normal file
Before Width: | Height: | Size: 70 KiB After Width: | Height: | Size: 70 KiB |
0
examples/technical_report/Isabelle_DOF-Manual/document/figures/document-hierarchy.pdf
Executable file → Normal file
0
examples/technical_report/Isabelle_DOF-Manual/document/figures/document-hierarchy.svg
Executable file → Normal file
Before Width: | Height: | Size: 36 KiB After Width: | Height: | Size: 36 KiB |
0
examples/technical_report/Isabelle_DOF-Manual/document/figures/header_CSP_pdf.png
Executable file → Normal file
Before Width: | Height: | Size: 203 KiB After Width: | Height: | Size: 203 KiB |
0
examples/technical_report/Isabelle_DOF-Manual/document/figures/isabelle-architecture.pdf
Executable file → Normal file
0
examples/technical_report/Isabelle_DOF-Manual/document/figures/isabelle-architecture.svg
Executable file → Normal file
Before Width: | Height: | Size: 57 KiB After Width: | Height: | Size: 57 KiB |
0
examples/technical_report/Isabelle_DOF-Manual/document/figures/isadof.png
Executable file → Normal file
Before Width: | Height: | Size: 81 KiB After Width: | Height: | Size: 81 KiB |
0
examples/technical_report/Isabelle_DOF-Manual/document/figures/srac-as-es-application.png
Executable file → Normal file
Before Width: | Height: | Size: 37 KiB After Width: | Height: | Size: 37 KiB |
0
examples/technical_report/Isabelle_DOF-Manual/document/figures/srac-definition.png
Executable file → Normal file
Before Width: | Height: | Size: 26 KiB After Width: | Height: | Size: 26 KiB |
|
@ -1,4 +0,0 @@
|
||||||
Template: scrreprt-modern
|
|
||||||
Ontology: technical_report
|
|
||||||
Ontology: cenelec_50128
|
|
||||||
|
|
0
examples/technical_report/Isabelle_DOF-Manual/document/lstisadof-manual.sty
Executable file → Normal file
|
@ -1,13 +1,13 @@
|
||||||
session "TR_MyCommentedIsabelle" = "Isabelle_DOF" +
|
session "TR_MyCommentedIsabelle" = "Isabelle_DOF" +
|
||||||
options [document = pdf, document_output = "output",quick_and_dirty = true]
|
options [document = pdf, document_output = "output", document_build = dof,
|
||||||
|
dof_ontologies = "Isabelle_DOF.technical_report", dof_template = Isabelle_DOF.scrreprt,
|
||||||
|
quick_and_dirty = true]
|
||||||
theories
|
theories
|
||||||
"TR_MyCommentedIsabelle"
|
"TR_MyCommentedIsabelle"
|
||||||
document_files
|
document_files
|
||||||
"root.bib"
|
"root.bib"
|
||||||
"isadof.cfg"
|
|
||||||
"preamble.tex"
|
"preamble.tex"
|
||||||
"prooftree.sty"
|
"prooftree.sty"
|
||||||
"build"
|
|
||||||
"figures/markup-demo.png"
|
"figures/markup-demo.png"
|
||||||
"figures/text-element.pdf"
|
"figures/text-element.pdf"
|
||||||
"figures/isabelle-architecture.pdf"
|
"figures/isabelle-architecture.pdf"
|
||||||
|
|
182
examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy
Executable file → Normal file
|
@ -612,32 +612,36 @@ subsection\<open>More operations on types\<close>
|
||||||
text\<open>
|
text\<open>
|
||||||
\<^item> \<^ML>\<open>Term_Subst.map_types_same : (typ -> typ) -> term -> term\<close>
|
\<^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.map_aterms_same : (term -> term) -> term -> term\<close>
|
||||||
\<^item> \<^ML>\<open>Term_Subst.instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list
|
\<^item> \<^ML>\<open>Term_Subst.instantiate: typ TVars.table * term Vars.table -> term -> term\<close>
|
||||||
-> term -> term\<close>
|
\<^item> \<^ML>\<open>Term_Subst.instantiateT: typ TVars.table -> typ -> typ\<close>
|
||||||
\<^item> \<^ML>\<open>Term_Subst.instantiateT: ((indexname * sort) * typ) list -> typ -> typ\<close>
|
\<^item> \<^ML>\<open>Term_Subst.generalizeT: Names.set -> int -> typ -> typ\<close>
|
||||||
\<^item> \<^ML>\<open>Term_Subst.generalizeT: string list -> int -> typ -> typ\<close>
|
|
||||||
this is the standard type generalisation function !!!
|
this is the standard type generalisation function !!!
|
||||||
only type-frees in the string-list were taken into account.
|
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 !!!
|
this is the standard term generalisation function !!!
|
||||||
only type-frees and frees in the string-lists were taken
|
only type-frees and frees in the string-lists were taken
|
||||||
into account.
|
into account.
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
text \<open>Apparently, a bizarre conversion between the old-style interface and
|
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>
|
the new-style \<^ML>\<open>tyenv\<close> is necessary. See the following example.\<close>
|
||||||
ML\<open>
|
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;
|
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,
|
(* it took me quite some time to find out that these two type representations,
|
||||||
obscured by a number of type-synonyms, where actually identical. *)
|
obscured by a number of type-synonyms, where actually identical. *)
|
||||||
|
val S''= TVars.make S': typ TVars.table
|
||||||
val ty = t_schematic;
|
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 = (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 : *)
|
(* or alternatively : *)
|
||||||
val t'' = Term.map_types (Term_Subst.instantiateT S') (t)
|
val t'' = Term.map_types (Term_Subst.instantiateT S'') (t)
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
text\<open>A more abstract env for variable management in tactic proofs. A bit difficult to use
|
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_intr: cterm -> thm -> thm\<close>
|
||||||
\<^item> \<^ML>\<open> Thm.forall_elim: 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.transfer : theory -> thm -> thm\<close>
|
||||||
\<^item> \<^ML>\<open> Thm.generalize: string list * string list -> int -> thm -> thm\<close>
|
\<^item> \<^ML>\<open> Thm.generalize: Names.set * Names.set -> int -> thm -> thm\<close>
|
||||||
\<^item> \<^ML>\<open> Thm.instantiate: ((indexname*sort)*ctyp)list * ((indexname*typ)*cterm) list -> thm -> thm\<close>
|
\<^item> \<^ML>\<open> Thm.instantiate: ctyp TVars.table * cterm Vars.table -> thm -> thm\<close>
|
||||||
\<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.
|
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:
|
Notated as logical inference rules, these operations were presented as follows:
|
||||||
\<close>
|
\<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:
|
exist) for definitions and axiomatizations is here:
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
|
|
||||||
text\<open>
|
text\<open>
|
||||||
\<^item> \<^ML>\<open>Specification.definition: (binding * typ option * mixfix) option ->
|
\<^item> \<^ML>\<open>Specification.definition: (binding * typ option * mixfix) option ->
|
||||||
(binding * typ option * mixfix) list -> term list -> Attrib.binding * term ->
|
(binding * typ option * mixfix) list -> term list -> Attrib.binding * term ->
|
||||||
local_theory -> (term * (string * thm)) * local_theory\<close>
|
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 ->
|
\<^item> \<^ML>\<open>Specification.definition_cmd: (binding * string option * mixfix) option ->
|
||||||
(binding * string option * mixfix) list -> string list -> Attrib.binding * string ->
|
(binding * string option * mixfix) list -> string list -> Attrib.binding * string ->
|
||||||
bool -> local_theory -> (term * (string * thm)) * local_theory\<close>
|
bool -> local_theory -> (term * (string * thm)) * local_theory\<close>
|
||||||
|
@ -959,8 +959,8 @@ fun mk_def name p =
|
||||||
val ty_global = ty --> ty
|
val ty_global = ty --> ty
|
||||||
val args = (((SOME(nameb,SOME ty_global,NoSyn),(Binding.empty_atts,term_prop)),[]),[])
|
val args = (((SOME(nameb,SOME ty_global,NoSyn),(Binding.empty_atts,term_prop)),[]),[])
|
||||||
val cmd = (fn (((decl, spec), prems), params) =>
|
val cmd = (fn (((decl, spec), prems), params) =>
|
||||||
#2 oo Specification.definition' decl params prems spec)
|
#2 o Specification.definition decl params prems spec)
|
||||||
in cmd args true
|
in cmd args
|
||||||
end;
|
end;
|
||||||
in Named_Target.theory_map (mk_def "I" @{here} )
|
in Named_Target.theory_map (mk_def "I" @{here} )
|
||||||
end\<close>
|
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.theory': (bool -> theory -> theory) -> Toplevel.transition -> Toplevel.transition\<close>
|
||||||
\<^item> \<^ML>\<open>Toplevel.exit: 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.ignored: Position.T -> Toplevel.transition\<close>
|
||||||
\<^item> \<^ML>\<open>Toplevel.present_local_theory: (xstring * Position.T) option ->
|
\<^item> \<^ML>\<open>Toplevel.present_local_theory: (xstring * Position.T) option ->
|
||||||
(Toplevel.state -> unit) -> Toplevel.transition -> Toplevel.transition\<close>
|
(Toplevel.state -> Latex.text) -> Toplevel.transition -> Toplevel.transition\<close>
|
||||||
|
|
||||||
\<close>
|
\<close>
|
||||||
subsection*[cmdbinding::technical] \<open>Toplevel Transaction Management in the Isar-Engine\<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
|
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>
|
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>
|
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:
|
text\<open> The integration of the \<^theory_text>\<open>text\<close>-command is done as follows:
|
||||||
|
|
||||||
@{ML [display]\<open>
|
@{ML [display]\<open>
|
||||||
Outer_Syntax.command ("text", @{here}) "formal comment (primary style)"
|
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>}
|
\<close>}
|
||||||
|
|
||||||
where \<^ML>\<open>Pure_Syn.document_command\<close> is the defining operation for the
|
where \<^ML>\<open>Document_Output.document_output\<close> is the defining operation for the
|
||||||
"diagnostic" (=side-effect-free) toplevel operation. \<^ML>\<open>Pure_Syn.document_command\<close> looks as follows:
|
"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 =
|
@{ML [display]\<open>let fun document_reports txt =
|
||||||
Thy_Output.output_document (Toplevel.presentation_context state) markdown txt
|
let val pos = Input.pos_of txt in
|
||||||
fun document_command markdown (loc, txt) =
|
[(pos, Markup.language_document (Input.is_delimited txt)),
|
||||||
Toplevel.keep (fn state =>
|
(pos, Markup.plain_text)]
|
||||||
(case loc of
|
end;
|
||||||
NONE => ignore (output_document state markdown txt)
|
fun document_output {markdown, markup} (loc, txt) =
|
||||||
| SOME (_, pos) =>
|
let
|
||||||
error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o
|
fun output st =
|
||||||
Toplevel.present_local_theory loc (fn state =>
|
let
|
||||||
ignore (output_document state markdown txt)) in () end
|
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>}
|
||||||
|
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
subsubsection*[ex1138::example]\<open>Examples: \<^theory_text>\<open>ML\<close>\<close>
|
subsubsection*[ex1138::example]\<open>Examples: \<^theory_text>\<open>ML\<close>\<close>
|
||||||
|
|
||||||
text\<open>
|
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>
|
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>
|
ML\<open>
|
||||||
structure HLDefinitionSample =
|
structure HLDefinitionSample =
|
||||||
struct
|
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));
|
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 eq = push_eq binding (Binding.name_of name) rty sty lthy
|
||||||
val mty = MON_SE_T rty sty
|
val mty = MON_SE_T rty sty
|
||||||
val args = (SOME(name, SOME mty, NoSyn), (Binding.empty_atts,eq),[],[])
|
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"})
|
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
|
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
|
discussed earlier. Markup operations were used for hyperlinking applications to binding
|
||||||
occurrences, info for hovering, infos for type ... \<close>
|
occurrences, info for hovering, infos for type ... \<close>
|
||||||
|
|
||||||
ML\<open>
|
ML\<open>
|
||||||
(* Position.report is also a type consisting of a pair of a position and markup. *)
|
(* 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
|
(* 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
|
(* example for setting a link, the def flag controls if it is a defining or a binding
|
||||||
occurence of an item *)
|
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;
|
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,
|
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
|
be it on the level of thy-internal states or as reference in markup in
|
||||||
PIDE *)
|
PIDE *)
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
subsection\<open>A simple Example\<close>
|
subsection\<open>A simple Example\<close>
|
||||||
ML\<open>
|
ML\<open>
|
||||||
local
|
local
|
||||||
|
@ -1573,10 +1587,7 @@ val docclassN = "doc_class";
|
||||||
|
|
||||||
(* derived from: theory_markup; def for "defining occurrence" (true) in contrast to
|
(* derived from: theory_markup; def for "defining occurrence" (true) in contrast to
|
||||||
"referring occurence" (false). *)
|
"referring occurence" (false). *)
|
||||||
fun docclass_markup def name id pos =
|
val docclass_markup = theory_markup docclassN
|
||||||
if id = 0 then Markup.empty
|
|
||||||
else Markup.properties (Position.entity_properties_of def id pos)
|
|
||||||
(Markup.entity docclassN name);
|
|
||||||
|
|
||||||
in
|
in
|
||||||
|
|
||||||
|
@ -1602,14 +1613,16 @@ fun markup_tvar def_name ps (name, id) =
|
||||||
let
|
let
|
||||||
fun markup_elem name = (name, (name, []): Markup.T);
|
fun markup_elem name = (name, (name, []): Markup.T);
|
||||||
val (tvarN, tvar) = markup_elem ((case def_name of SOME name => name | _ => "") ^ "'s nickname is");
|
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
|
val def = def_name = NONE
|
||||||
in
|
in
|
||||||
tvar ::
|
tvar ::
|
||||||
(if def then I else cons (Markup.keyword_properties Markup.ML_keyword3))
|
(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
|
end
|
||||||
|
|
||||||
|
(* Position.make_entity_markup {def = def} id refN (name, pos) *)
|
||||||
|
|
||||||
fun report [] _ _ = I
|
fun report [] _ _ = I
|
||||||
| report ps markup x =
|
| report ps markup x =
|
||||||
let val ms = markup x
|
let val ms = markup x
|
||||||
|
@ -1856,11 +1869,6 @@ Common Isar Syntax
|
||||||
|
|
||||||
|
|
||||||
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_input: Input.source parser\<close>
|
||||||
\<^item>\<^ML>\<open>Args.text : string parser\<close>
|
\<^item>\<^ML>\<open>Args.text : string parser\<close>
|
||||||
\<^item>\<^ML>\<open>Args.binding : Binding.binding 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>
|
subsection*[ex33::example] \<open>Example\<close>
|
||||||
|
|
||||||
ML\<open>
|
ML\<open>
|
||||||
|
@ -2070,10 +2082,10 @@ ML\<open>
|
||||||
|
|
||||||
(* Here is the code to register the above parsers as text antiquotations into the Isabelle
|
(* Here is the code to register the above parsers as text antiquotations into the Isabelle
|
||||||
Framework: *)
|
Framework: *)
|
||||||
Thy_Output.antiquotation_pretty_source \<^binding>\<open>theory\<close>
|
Document_Output.antiquotation_pretty_source \<^binding>\<open>theory\<close>
|
||||||
(Scan.lift (Parse.position Args.embedded));
|
(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)) ;
|
(Scan.lift (Parse.position Parse.path)) ;
|
||||||
|
|
||||||
\<close>
|
\<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> :
|
transaction that, of course, has the type \<^ML_type>\<open>theory -> theory\<close> :
|
||||||
|
|
||||||
@{ML [display] \<open>
|
@{ML [display] \<open>
|
||||||
(fn name => (Thy_Output.antiquotation_pretty_source
|
(fn name => (Document_Output.antiquotation_pretty_source
|
||||||
name
|
name
|
||||||
(Scan.lift (Parse.position Args.cartouche_input))))
|
(Scan.lift (Parse.position Args.cartouche_input))))
|
||||||
: binding ->
|
: 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>
|
text\<open>It provides a number of hooks that can be used for redirection hacks ...\<close>
|
||||||
|
|
||||||
section \<open> Output: LaTeX \<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
|
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:
|
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.string: string -> Latex.text\<close>
|
||||||
\<^item>\<^ML>\<open>Latex.text: string * Position.T -> 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_name: string -> string\<close>
|
||||||
\<^item>\<^ML>\<open>Latex.output_ascii: 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.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.environment: string -> Latex.text -> 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.block: Latex.text -> XML.tree\<close>
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
ML\<open> Latex.output_ascii;
|
ML\<open> Latex.output_ascii;
|
||||||
Latex.environment "isa" "bg";
|
Latex.environment "isa" (Latex.string "bg");
|
||||||
Latex.output_ascii "a_b:c'é";
|
Latex.output_ascii "a_b:c'é";
|
||||||
(* Note: *)
|
(* Note: *)
|
||||||
space_implode "sd &e sf dfg" ["qs","er","alpa"];
|
space_implode "sd &e sf dfg" ["qs","er","alpa"];
|
||||||
\<close>
|
\<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>
|
text\<open>
|
||||||
\<^item>\<^ML>\<open>Thy_Output.output_document: Proof.context -> {markdown: bool} -> Input.source -> Latex.text list\<close>
|
\<^item>\<^ML>\<open>Document_Output.output_document: Proof.context -> {markdown: bool} -> Input.source -> Latex.text \<close>
|
||||||
\<^item>\<^ML>\<open>Thy_Output.output_token: Proof.context -> Token.T -> Latex.text list\<close>
|
\<^item>\<^ML>\<open>Document_Output.output_token: Proof.context -> Token.T -> Latex.text \<close>
|
||||||
\<^item>\<^ML>\<open>Thy_Output.output_source: Proof.context -> string -> Latex.text list\<close>
|
\<^item>\<^ML>\<open>Document_Output.output_source: Proof.context -> string -> Latex.text \<close>
|
||||||
\<^item>\<^ML>\<open>Thy_Output.present_thy: Options.T -> theory -> Thy_Output.segment list -> Latex.text list\<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>Document_Output.isabelle: Proof.context -> Latex.text -> Latex.text\<close>
|
||||||
\<^item>\<^ML>\<open>Thy_Output.isabelle_typewriter: Proof.context -> Latex.text list -> Latex.text\<close>
|
\<^item>\<^ML>\<open>Document_Output.isabelle_typewriter: Proof.context -> Latex.text -> Latex.text\<close>
|
||||||
\<^item>\<^ML>\<open>Thy_Output.typewriter: Proof.context -> string -> Latex.text\<close>
|
\<^item>\<^ML>\<open>Document_Output.typewriter: Proof.context -> string -> Latex.text\<close>
|
||||||
\<^item>\<^ML>\<open>Thy_Output.verbatim: Proof.context -> string -> Latex.text\<close>
|
\<^item>\<^ML>\<open>Document_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>Document_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>Document_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>Document_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>Document_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.pretty_items_source: Proof.context -> {embedded: bool} -> Token.src -> Pretty.T list -> Latex.text\<close>
|
||||||
|
|
||||||
Finally a number of antiquotation registries :
|
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>
|
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>
|
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>
|
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>
|
binding -> 'a context_parser -> (Proof.context -> 'a -> string) -> theory -> theory\<close>
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
|
|
|
@ -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
|
|
0
examples/technical_report/TR_my_commented_isabelle/document/figures/document-model.pdf
Executable file → Normal file
0
examples/technical_report/TR_my_commented_isabelle/document/figures/isabelle-architecture.pdf
Executable file → Normal file
0
examples/technical_report/TR_my_commented_isabelle/document/figures/markup-demo.png
Executable file → Normal file
Before Width: | Height: | Size: 13 KiB After Width: | Height: | Size: 13 KiB |
0
examples/technical_report/TR_my_commented_isabelle/document/figures/pure-inferences-I.pdf
Executable file → Normal file
Before Width: | Height: | Size: 91 KiB After Width: | Height: | Size: 91 KiB |
0
examples/technical_report/TR_my_commented_isabelle/document/figures/pure-inferences-II.pdf
Executable file → Normal file
Before Width: | Height: | Size: 31 KiB After Width: | Height: | Size: 31 KiB |