Updated Isabelle version and removed scala builds from AFP.

.gitattributes

@@ -1,2 +0,0 @@
-core.autocrlf false
-core.eol lf

.gitignore

@@ -1,5 +0,0 @@
-output
-.afp
-*~
-*#
-Isabelle_DOF-Unit-Tests/latex_test/

.woodpecker/README.md

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

.woodpecker/build.yml

@@ -1,61 +0,0 @@
-pipeline:
-  build:
-    image: git.logicalhacking.com/lh-docker/lh-docker-isabelle/isabelle_nightly:latest
-    pull: true
-    commands:
-      - hg log --limit 2 /root/isabelle
-      - ./.woodpecker/check_dangling_theories
-      - ./.woodpecker/check_external_file_refs
-      - ./.woodpecker/check_quick_and_dirty
-      - export ARTIFACT_DIR=$CI_WORKSPACE/.artifacts/$CI_REPO/$CI_BRANCH/$CI_BUILD_NUMBER/$LATEX
-      - mkdir -p $ARTIFACT_DIR
-      - export `isabelle getenv ISABELLE_HOME_USER`
-      - mkdir -p $ISABELLE_HOME_USER/etc
-      - echo "ISABELLE_PDFLATEX=\"$LATEX --file-line-error\"" >> $ISABELLE_HOME_USER/etc/settings
-      - isabelle build -x HOL-Proofs -x Isabelle_DOF-Proofs -D . -o browser_info
-      - if [ "$LATEX" = "lualatex" ]; then isabelle build -o 'timeout_scale=2' -D . -o browser_info; else echo "Skipping Isabelle_DOF-Proofs for pdflatex build."; fi
-      - find . -name 'root.tex' -prune -o -name 'output' -type f | xargs latexmk -$LATEX -cd  -quiet -Werror
-      - isabelle components -u .
-      - isabelle dof_mkroot -q DOF_test
-      - isabelle build -D DOF_test
-      - cp -r $ISABELLE_HOME_USER/browser_info $ARTIFACT_DIR
-      - cd $ARTIFACT_DIR
-      - cd ../..
-      - ln -s * latest
-  archive:
-    image: git.logicalhacking.com/lh-docker/lh-docker-isabelle/isabelle_nightly:latest
-    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:
-    image: docker.io/drillster/drone-rsync
-    settings:
-      hosts: [ "ci.logicalhacking.com"]
-      port: 22
-      source: .artifacts/$CI_REPO_OWNER/*
-      target: $CI_REPO_OWNER
-      include: [ "**.*"]
-      key:
-        from_secret: artifacts_ssh
-      user: artifacts
-  notify:
-    image: docker.io/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

.woodpecker/check_dangling_theories

@@ -1,33 +0,0 @@
-#!/bin/bash
-
-set -e
-
-failuremsg="Error"
-failurecode=1
-
-while [ $# -gt 0 ]
-do
-    case "$1" in
-        --warning|-w)
-            failuremsg="Warning"
-            failurecode=0;;
-    esac
-    shift
-done
-
-echo "Checking for theories that are not part of an Isabelle session:"
-echo "==============================================================="
-
-PWD=`pwd`
-TMPDIR=`mktemp -d`
-isabelle build  -D . -l -n | grep $PWD | sed -e "s| *${PWD}/||" | sort -u | grep thy$ > ${TMPDIR}/sessions-thy-files.txt
-find * -type f | sort -u | grep thy$ > ${TMPDIR}/actual-thy-files.txt
-thylist=`comm -13 ${TMPDIR}/sessions-thy-files.txt ${TMPDIR}/actual-thy-files.txt`
-if [ -z "$thylist" ] ; then
-    echo "  * Success: No dangling theories found."
-    exit 0
-else
-    echo -e "$thylist"
-    echo "$failuremsg: Dangling theories found (see list above)!" 
-    exit $failurecode 
-fi

.woodpecker/check_external_file_refs

@@ -1,45 +0,0 @@
-#!/bin/sh
-
-
-
-failuremsg="Error"
-failurecode=1
-
-while [ $# -gt 0 ]
-do
-    case "$1" in
-        --warning|-w)
-            failuremsg="Warning"
-            failurecode=0;;
-    esac
-    shift
-done
-
-DIRREGEXP="\\.\\./"
-
-echo "Checking for references pointing outside of session directory:"
-echo "=============================================================="
-
-REGEXP=$DIRREGEXP
-DIR=$DIRMATCH
-failed=0
-for i in $(seq 1 10); do 
-  FILES=`find * -mindepth $((i-1)) -maxdepth $i -type f | xargs`
-  if [ -n "$FILES" ]; then 
-    grep -s ${REGEXP} ${FILES}
-    exit=$?
-    if [ "$exit" -eq 0 ] ; then
-      failed=1
-    fi
-  fi
-  REGEXP="${DIRREGEXP}${REGEXP}"
-done
-
-
-if [ "$failed" -ne 0 ] ; then
-    echo "$failuremsg: Forbidden reference to files outside of their session directory!" 
-    exit $failurecode 
-fi
-
-echo "  * Success: No relative references to files outside of their session directory found."
-exit 0

.woodpecker/check_quick_and_dirty

@@ -1,30 +0,0 @@
-#!/bin/bash
-
-set -e
-
-failuremsg="Error"
-failurecode=1
-
-while [ $# -gt 0 ]
-do
-    case "$1" in
-        --warning|-w)
-            failuremsg="Warning"
-            failurecode=0;;
-    esac
-    shift
-done
-
-echo "Checking for sessions with quick_and_dirty mode enabled:"
-echo "========================================================"
-
-rootlist=`find -name 'ROOT' -exec grep -l 'quick_and_dirty *= *true' {} \;`
-
-if [ -z "$rootlist" ] ; then
-    echo "  * Success: No sessions with quick_and_dirty mode enabled found."
-    exit 0
-else
-    echo -e "$rootlist"
-    echo "$failuremsg: Sessions with quick_and_dirty mode enabled found (see list above)!" 
-    exit $failurecode 
-fi

.woodpecker/mk_release

@@ -1,222 +0,0 @@
-#!/usr/bin/env bash
-# Copyright (c) 2019-2022 University of Exeter. 
-#               2019 University of Paris-Saclay. 
-#
-# Redistribution and use in source and binary forms, with or without
-# modification, are permitted provided that the following conditions
-# 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: mk_release [OPTION] "
-    echo ""
-    echo "       A tool for building an Isabelle/DOF release archive."
-    echo ""
-    echo "Run ..."
-    echo ""
-    echo "  --help, -h                display this help message"
-    echo "  --sign, -s                sign release archive"
-    echo "                            (default: $SIGN)"
-    echo "  --isabelle, -i isabelle   isabelle command used for installation"
-    echo "                            (default: $ISABELLE)"
-    echo "  --tag tag, -t tag         use tag for release archive"
-    echo "                            (default: use master branch)"
-    echo "  --publish, -p             publish generated artefact"
-    echo "                            (default: $PUBLISH)"
-    echo "  --quick-and-dirty, -d     only build required artifacts, no complete test"
-    echo "                            (default: $DIRTY)"
-}
-
-check_isabelle_version() {
-    ACTUAL_ISABELLE_VERSION=`$ISABELLE version`
-    echo "* Checking Isabelle version:"
-    if [ "$ISABELLE_VERSION" != "$ACTUAL_ISABELLE_VERSION" ]; then
-        echo "* Expecting $ISABELLE_VERSION, found $ACTUAL_ISABELLE_VERSION: ERROR"
-        exit 1
-    else
-        echo "* Expecting $ISABELLE_VERSION, found $ACTUAL_ISABELLE_VERSION: success"
-    fi
-}
-
-clone_repo()
-{
-    echo "* Cloning into $ISADOF_WORK_DIR"
-    git clone . $ISADOF_WORK_DIR
-    if [ "$USE_TAG" = "true" ]; then
-        echo "  * Switching to tag $TAG"
-        (cd $ISADOF_WORK_DIR && git checkout $TAG)
-    else
-        echo "  * No tag specified, using master branch"
-    fi
-    (cd $ISADOF_WORK_DIR && git show -s --format="COMMIT=%H%nDATE=%cd" --date=short | sed -e 's|-|/|g') >> $ISADOF_WORK_DIR/etc/settings
-    
-}
-
-build_and_install_manuals()
-{
-    echo "* Building manual"
-
-    if [ "$DIRTY" = "true" ]; then
-        if [ -z ${ARTIFACT_DIR+x} ]; then
-            echo "  * Quick and Dirty Mode (local build)"
-            $ISABELLE build -d . Isabelle_DOF Isabelle_DOF-Example-I
-            mkdir -p $ISADOF_WORK_DIR/Isabelle_DOF-Example-I/output/
-            cp Isabelle_DOF-Example-I/output/document.pdf \
-               $ISADOF_WORK_DIR/Isabelle_DOF-Example-I/output/
-            mkdir -p $ISADOF_WORK_DIR/Isabelle_DOF/output/
-            cp Isabelle_DOF/output/document.pdf \
-               $ISADOF_WORK_DIR/Isabelle_DOF/output/;
-        else
-            echo "  * Quick and Dirty Mode (running on CI)"
-            mkdir -p $ISADOF_WORK_DIR/Isabelle_DOF-Example-I/output/
-            cp $ARTIFACT_DIR/browser_info/AFP/Isabelle_DOF-Example-I/document.pdf \
-               $ISADOF_WORK_DIR/Isabelle_DOF-Example-I/output/
- 
-            mkdir -p $ISADOF_WORK_DIR/Isabelle_DOF/output/
-            cp $ARTIFACT_DIR/browser_info/AFP/Isabelle_DOF/document.pdf \
-               $ISADOF_WORK_DIR/Isabelle_DOF/output/;
-        fi
-    else
-        (cd $ISADOF_WORK_DIR && $ISABELLE env ./install-afp)
-        (cd $ISADOF_WORK_DIR && $ISABELLE build -c -D . )
-    fi
-    mkdir -p $ISADOF_WORK_DIR/doc
-    echo "Isabelle/DOF Manuals!" > $ISADOF_WORK_DIR/doc/Contents
-    
-    cp $ISADOF_WORK_DIR/Isabelle_DOF/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
-
-    cp $ISADOF_WORK_DIR/Isabelle_DOF-Example-I/output/document.pdf \
-        $ISADOF_WORK_DIR/doc/Isabelle_DOF-Example-I.pdf
-    echo "  Isabelle_DOF-Example-I       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/.woodpecker $ISADOF_WORK_DIR/.afp 
-    
-}
-
-create_archive()
-{    
-    echo "* Creating archive"
-    cp $ISADOF_WORK_DIR/doc/Isabelle_DOF-Manual.pdf  $ISADOF_TAR.pdf
-    (mv $ISADOF_WORK_DIR $ISADOF_DIR)    
-    (cd $BUILD_DIR && tar cf $ISADOF_TAR.tar $ISADOF_TAR && xz $ISADOF_DIR.tar)
-    mv $BUILD_DIR/$ISADOF_TAR.tar.xz .
-}
-
-sign_archive()
-{
-    echo "* Signing archive"
-    gpg --armor --output $ISADOF_TAR.tar.xz.asc --detach-sig $ISADOF_TAR.tar.xz
-}
-
-publish_archive()
-{
-    echo "* Publish archive"
-    ssh 0x5f.org mkdir -p www/$DOF_ARTIFACT_HOST/htdocs/$DOF_ARTIFACT_DIR
-    scp $ISADOF_TAR.* 0x5f.org:www/$DOF_ARTIFACT_HOST/htdocs/$DOF_ARTIFACT_DIR/
-    ssh 0x5f.org chmod go+u-w -R www/$DOF_ARTIFACT_HOST/htdocs/$DOF_ARTIFACT_DIR
-}
-
-ISABELLE=`which isabelle`
-USE_TAG="false"
-SIGN="false"
-PUBLISH="false"
-DIRTY="false"
-BUILD_DIR=`mktemp -d`
-ISADOF_WORK_DIR="$BUILD_DIR/Isabelle_DOF"
-while [ $# -gt 0 ]
-do
-    case "$1" in
-        --isabelle|-i)
-            ISABELLE="$2";
-            shift;;
-        --tag|-t)
-            TAG="$2";
-            USE_TAG="true"
-            shift;;
-        --sign|-s)
-            SIGN="true";;
-        --publish|-p)
-            PUBLISH="true";;
-        --quick-and-dirty|-d)
-            DIRTY="true";;
-        --help|-h)
-            print_help
-            exit 0;;
-        *)  print_help
-            exit 1;;
-    esac
-    shift
-done
-
-
-clone_repo
-
-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 dof_param -b isabelle_version)"
-DOF_VERSION="$($ISABELLE_TOOL dof_param -b dof_version)"
-
-ISABELLE_SHORT_VERSION=`echo $ISABELLE_VERSION | sed -e 's/:.*$//'`
-ISADOF_TAR="Isabelle_DOF-"$DOF_VERSION"_"$ISABELLE_SHORT_VERSION
-ISADOF_DIR="$BUILD_DIR/$ISADOF_TAR"
-
-check_isabelle_version
-build_and_install_manuals
-
-if [ "$DIRTY" != "true" ]; then
-    $ISABELLE components -x $ISADOF_WORK_DIR
-    $ISABELLE components -u $ISADOF_MAIN_DIR
-fi
-
-create_archive
-
-if [ "$SIGN" = "true" ]; then
-    sign_archive
-fi
-
-if [ "$PUBLISH" = "true" ]; then
-    publish_archive
-fi
-
-rm -rf $BUILD_DIR
-