This commit is contained in:
parent
2e7a48f21f
commit
39c50c52de
51
CHANGELOG.md
51
CHANGELOG.md
@ -1,51 +0,0 @@
|
||||
# Changelog
|
||||
|
||||
All notable changes to this project will be documented in this file.
|
||||
|
||||
The format is based on [Keep a Changelog](http://keepachangelog.com/en/1.0.0/)
|
||||
and this project adheres to [Semantic Versioning](http://semver.org/spec/v2.0.0.html).
|
||||
|
||||
## [Unreleased]
|
||||
|
||||
### Added
|
||||
|
||||
### Changed
|
||||
|
||||
- Updated Isabelle version to Isabelle 2023
|
||||
|
||||
## [1.3.0] - 2022-07-08
|
||||
|
||||
### 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
|
||||
|
||||
- New antiquotations, consistency checks
|
||||
|
||||
### Changed
|
||||
|
||||
- Updated manual
|
||||
- Restructured setup for ontologies (Isabelle theories and LaTeX styles)
|
||||
|
||||
## 1.0.0 - 2018-08-18
|
||||
|
||||
### Added
|
||||
|
||||
- First public release
|
||||
|
||||
[Unreleased]: https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF/compare/v1.3.0/Isabelle2021...HEAD
|
||||
[1.3.0]: https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF/compare/v1.2.0/Isabelle2021...v1.3.0/Isabelle2021-1
|
||||
[1.2.0]: https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF/compare/v1.1.0/Isabelle2021...v1.2.0/Isabelle2021
|
||||
[1.1.0]: https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF/compare/v1.0.0/Isabelle2019...v1.1.0/Isabelle2021
|
||||
20
Isabelle_DOF-Scaffold/Isabelle_DOF-Scaffold.thy
Normal file
20
Isabelle_DOF-Scaffold/Isabelle_DOF-Scaffold.thy
Normal file
@ -0,0 +1,20 @@
|
||||
theory
|
||||
"Isabelle_DOF-Scaffold"
|
||||
imports
|
||||
Isabelle_DOF.scholarly_paper
|
||||
begin
|
||||
|
||||
list_templates
|
||||
use_template "scrartcl"
|
||||
list_ontologies
|
||||
use_ontology "scholarly_paper"
|
||||
|
||||
title* [tit::title]\<open>Formal Verification of Security Protocols\<close>
|
||||
author*[alice, email = "\<open>alice@example.com\<close>",
|
||||
http_site = "\<open>https://example.com/alice\<close>",
|
||||
affiliation = "\<open>Wonderland University\<close>"]\<open>Alice\<close>
|
||||
author*[bob, email = "\<open>bob@example.com\<close>",
|
||||
http_site = "\<open>https://example.com/bob\<close>",
|
||||
affiliation = "\<open>Wonderland University\<close>"]\<open>Bob\<close>
|
||||
|
||||
end
|
||||
9
Isabelle_DOF-Scaffold/ROOT
Normal file
9
Isabelle_DOF-Scaffold/ROOT
Normal file
@ -0,0 +1,9 @@
|
||||
session "Isabelle_DOF-Scaffold" = "Isabelle_DOF" +
|
||||
options [document = pdf, document_output = "output", document_build = dof]
|
||||
(*theories [document = false]
|
||||
A
|
||||
B*)
|
||||
theories
|
||||
"Isabelle_DOF-Scaffold"
|
||||
document_files
|
||||
"preamble.tex"
|
||||
1
Isabelle_DOF-Scaffold/document/preamble.tex
Normal file
1
Isabelle_DOF-Scaffold/document/preamble.tex
Normal file
@ -0,0 +1 @@
|
||||
%% This is a placeholder for user-specific configuration and packages.
|
||||
1
ROOTS
1
ROOTS
@ -6,3 +6,4 @@ Isabelle_DOF-Example-I
|
||||
Isabelle_DOF-Example-II
|
||||
Isabelle_DOF-Examples-Extra
|
||||
Isabelle_DOF-Examples-Templates
|
||||
Isabelle_DOF-Scaffold
|
||||
|
||||
187
install-afp
187
install-afp
@ -1,187 +0,0 @@
|
||||
#!/usr/bin/env bash
|
||||
# Copyright (c) 2018-2019 The University of Sheffield.
|
||||
# 2019-2020 The University of Exeter.
|
||||
# 2018-2020 The University of Paris-Saclay.
|
||||
#
|
||||
# Redistribution and use in source and binary forms, with or without
|
||||
# modification, are permitted provided that the following conditions
|
||||
# are met:
|
||||
# 1. Redistributions of source code must retain the above copyright
|
||||
# notice, this list of conditions and the following disclaimer.
|
||||
# 2. Redistributions in binary form must reproduce the above copyright
|
||||
# notice, this list of conditions and the following disclaimer in
|
||||
# the documentation and/or other materials provided with the
|
||||
# distribution.
|
||||
# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
|
||||
# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
|
||||
# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
|
||||
# FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
|
||||
# COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
|
||||
# INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
|
||||
# BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
|
||||
# LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
|
||||
# CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
|
||||
# LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
|
||||
# ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
|
||||
# POSSIBILITY OF SUCH DAMAGE.
|
||||
#
|
||||
# SPDX-License-Identifier: BSD-2-Clause
|
||||
|
||||
#set -e
|
||||
shopt -s nocasematch
|
||||
|
||||
|
||||
print_help()
|
||||
{
|
||||
echo "Usage: isabelle env ./install-afp [OPTION] "
|
||||
echo ""
|
||||
echo "Warning: This tools is deprecated."
|
||||
echo ""
|
||||
echo "Run ..."
|
||||
echo ""
|
||||
echo " --help, -h display this help message"
|
||||
}
|
||||
|
||||
|
||||
|
||||
exit_error() {
|
||||
echo ""
|
||||
echo " *** Local AFP installation FAILED, please check the README.md for help ***"
|
||||
echo ""
|
||||
exit 1
|
||||
}
|
||||
|
||||
confirm_usage() {
|
||||
echo "* From Isabelle2021-1 on, the recommended method for making the whole AFP "
|
||||
echo " available to Isabelle is the isabelle components -u command."
|
||||
echo " For doing so, please follow the instructions at: "
|
||||
echo " https://www.isa-afp.org/help/"
|
||||
echo ""
|
||||
echo " Alternatively, you can continue, on your own risk, to install only"
|
||||
echo " the AFP entries required to run Isabelle/DOF."
|
||||
echo ""
|
||||
read -p " Still continue (y/N)? " -n 1 -r
|
||||
echo
|
||||
if [[ $REPLY =~ ^[Yy]$ ]];
|
||||
then
|
||||
echo " Continuing installation on your OWN risk."
|
||||
else
|
||||
exit_error
|
||||
fi
|
||||
}
|
||||
check_isabelle_version() {
|
||||
echo "* Checking Isabelle version:"
|
||||
if [ "Isabelle" == "$ACTUAL_ISABELLE_VERSION" ]; then
|
||||
echo " ERROR:"
|
||||
echo " This script does not support the development version of Isabelle."
|
||||
echo " The recommended way for installing the AFP for the development"
|
||||
echo " version of Isabelle is to clone the AFP repository:"
|
||||
echo " https://foss.heptapod.net/isa-afp/afp-devel/"
|
||||
exit_error
|
||||
fi
|
||||
if [ "$ISABELLE_VERSION" != "$ACTUAL_ISABELLE_VERSION" ]; then
|
||||
echo " WARNING:"
|
||||
echo " The version of Isabelle (i.e., $ACTUAL_ISABELLE_VERSION) you are using"
|
||||
echo " IS NOT SUPPORTED"
|
||||
echo " by the current version of Isabelle/DOF. Please install a supported"
|
||||
echo " version of Isabelle and rerun the install script, providing the"
|
||||
echo " the \"isabelle\" command as argument."
|
||||
echo " Isabelle ($ISABELLE_VERSION) can be obtained from:"
|
||||
echo " https://isabelle.in.tum.de/website-$ISABELLE_VERSION/"
|
||||
echo ""
|
||||
read -p " Still continue (y/N)? " -n 1 -r
|
||||
echo
|
||||
if [[ $REPLY =~ ^[Yy]$ ]];
|
||||
then
|
||||
echo " Continuing installation on your OWN risk."
|
||||
else
|
||||
exit_error
|
||||
fi
|
||||
else
|
||||
echo " Success: found supported Isabelle version ($ISABELLE_VERSION)"
|
||||
fi
|
||||
}
|
||||
|
||||
check_afp_entries() {
|
||||
echo "* Checking availability of AFP entries:"
|
||||
missing=""
|
||||
required="Regular-Sets Functional-Automata Physical_Quantities Metalogic_ProofChecker"
|
||||
for afp in $required; do
|
||||
res=`$ISABELLE_TOOL build -n $afp 2>/dev/null || true`
|
||||
if [ "$res" != "" ]; then
|
||||
echo " Success: found APF entry $afp."
|
||||
else
|
||||
echo " Warning: could not find AFP entry $afp."
|
||||
missing="$missing $afp"
|
||||
fi
|
||||
done
|
||||
if [ "$missing" != "" ]; then
|
||||
echo " Trying to install AFP (this might take a few *minutes*) ...."
|
||||
extract=""
|
||||
for e in $missing; do
|
||||
extract="$extract $AFP_DATE/thys/$e"
|
||||
done
|
||||
mkdir -p .afp
|
||||
if curl -s -L $AFP_URL | tar zxf - -C .afp $extract; then
|
||||
for e in $missing; do
|
||||
echo " Registering $e"
|
||||
$ISABELLE_TOOL components -u "$PWD/.afp/$AFP_DATE/thys/$e"
|
||||
done
|
||||
echo " AFP installation successful."
|
||||
else
|
||||
echo " FAILURE: could not find AFP entries: $missing."
|
||||
echo " Please obtain the AFP from"
|
||||
echo " $AFP_URL"
|
||||
echo " and follow the following instructions:"
|
||||
echo " https://www.isa-afp.org/using.html"
|
||||
exit_error
|
||||
fi
|
||||
fi
|
||||
}
|
||||
|
||||
while [ $# -gt 0 ]
|
||||
do
|
||||
case "$1" in
|
||||
--help|-h)
|
||||
print_help
|
||||
exit 0;;
|
||||
*) print_help
|
||||
exit 1;;
|
||||
esac
|
||||
shift
|
||||
done
|
||||
|
||||
if [ -z ${ISABELLE_TOOL+x} ];
|
||||
then
|
||||
print_help
|
||||
exit 1
|
||||
fi
|
||||
|
||||
ACTUAL_ISABELLE_VERSION=`$ISABELLE_TOOL version`
|
||||
|
||||
ISABELLE_VERSION="Isabelle$($ISABELLE_TOOL dof_param -b isabelle_version)"
|
||||
|
||||
if [ ${ISABELLE_VERSION} = "Isabelle" ];
|
||||
then
|
||||
echo "Error: cannot find Isabelle/DOF configuration, please check that you"
|
||||
echo " registered Isabelle/DOF as an Isabelle component, e.g., using"
|
||||
echo " isabelle components -u ."
|
||||
exit 1
|
||||
fi
|
||||
|
||||
|
||||
|
||||
AFP_DATE="$($ISABELLE_TOOL dof_param -b afp_version)"
|
||||
AFP_URL="https://www.isa-afp.org/release/"$AFP_DATE".tar.gz"
|
||||
|
||||
echo ""
|
||||
echo "Isabelle/DOF AFP Installation Utility"
|
||||
echo "====================================="
|
||||
confirm_usage
|
||||
check_isabelle_version
|
||||
check_afp_entries
|
||||
echo "* AFP Installation successful."
|
||||
echo " You should now be able to enjoy Isabelle/DOF by building its session"
|
||||
echo " and all example documents by executing:"
|
||||
echo " $ISABELLE_TOOL build -D ."
|
||||
exit 0
|
||||
Loading…
Reference in New Issue
Block a user