From 36ed8aeef20d243991fc5b0b99212fcbf658e6b4 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sun, 16 Mar 2025 18:08:03 +0000 Subject: [PATCH] Re-added install-afp script (unsupported)! --- install-afp | 187 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 187 insertions(+) create mode 100755 install-afp diff --git a/install-afp b/install-afp new file mode 100755 index 0000000..ff6eeff --- /dev/null +++ b/install-afp @@ -0,0 +1,187 @@ +#!/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