diff --git a/.ci/mk_release b/.ci/mk_release index e56bcfc..9c9148e 100755 --- a/.ci/mk_release +++ b/.ci/mk_release @@ -26,7 +26,7 @@ # # SPDX-License-Identifier: BSD-2-Clause -#set -e +set -e shopt -s nocasematch @@ -84,18 +84,30 @@ clone_repo() } -build_and_install_manual() +build_and_install_manuals() { echo "* Building manual" ROOTS=$ISABELLE_HOME_USER/ROOTS if [ -f $ROOTS ]; then mv $ROOTS $ROOTS.backup fi + (cd $ISADOF_WORK_DIR && ./install) + + echo "Isabelle/DOF Manuals!" > $ISADOF_WORK_DIR/doc/Contents + (cd $ISADOF_WORK_DIR && $ISABELLE build -c Isabelle_DOF-Manual) mkdir -p $ISADOF_WORK_DIR/doc cp $ISADOF_WORK_DIR/examples/technical_report/Isabelle_DOF-Manual/output/document.pdf \ $ISADOF_WORK_DIR/doc/Isabelle_DOF-Manual.pdf + echo " Isabelle_DOF-Manual User and Implementation Manual for Isabelle/DOF" >> $ISADOF_WORK_DIR/doc/Contents + + (cd $ISADOF_WORK_DIR && $ISABELLE build -c 2018-cicm-isabelle_dof-applications) + mkdir -p $ISADOF_WORK_DIR/doc + cp $ISADOF_WORK_DIR/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/output/document.pdf \ + $ISADOF_WORK_DIR/doc/2018-cicm-isabelle_dof-applications.pdf + echo " 2018-cicm-isabelle_dof-applications Example academic paper" >> $ISADOF_WORK_DIR/doc/Contents + find $ISADOF_WORK_DIR -type d -name "output" -exec rm -rf {} \; &> /dev/null || true rm -rf $ISADOF_WORK_DIR/.git* $ISADOF_WORK_DIR/.ci $ISADOF_WORK_DIR/.afp if [ -f $ROOTS.backup ]; then @@ -171,7 +183,7 @@ for i in $VARS; do export "$i" done -build_and_install_manual +build_and_install_manuals create_archive diff --git a/install b/install index 6fd9bd8..7aad1e8 100755 --- a/install +++ b/install @@ -235,6 +235,13 @@ install_and_register(){ echo 'ISABELLE_TOOLS=$ISABELLE_TOOLS:$ISABELLE_HOME_USER/DOF/Tools' \ >> "$DIR/settings" fi + if [[ $ISABELLE_DOCS = *DOF* ]]; then + echo " * Docs already registered in $DIR/settings" + else + echo " * Registering docs in $DIR/settings" + echo "ISABELLE_DOCS=$PWD/doc"':$ISABELLE_DOCS' \ + >> "$DIR/settings" + fi sed -i -e "s||$DOF_URL|" $ISABELLE_HOME_USER/DOF/*/* LTX_VERSION="$DATE $DOF_VERSION/$ISABELLE_SHORT_VERSION" sed -i -e "s||$LTX_VERSION|" $ISABELLE_HOME_USER/DOF/*/* diff --git a/src/DOF/RegExpChecker.sml b/src/DOF/RegExpChecker.sml index 404d741..d74a947 100644 --- a/src/DOF/RegExpChecker.sml +++ b/src/DOF/RegExpChecker.sml @@ -1,3 +1,16 @@ +(************************************************************************* + * Copyright (C) + * 2019 The University of Exeter + * 2018-2019 The University of Paris-Saclay + * 2018 The University of Sheffield + * + * License: + * This program can be redistributed and/or modified under the terms + * of the 2-clause BSD-style license. + * + * SPDX-License-Identifier: BSD-2-Clause + *************************************************************************) + structure RegExpChecker : sig type 'a equal type num