Switched from Jenkins to Woodpecker CI.

.ci/Jenkinsfile

@@ -1,10 +0,0 @@
-pipeline {
-    agent any
-    stages {
-        stage('Build') {
-            steps {
-                sh 'docker run -v $PWD/Core_DOM:/Core_DOM logicalhacking:isabelle2020 isabelle build -D /Extended_Finite_State_Machine_Inference'
-            }
-        }
-    }
-}

.woodpecker/README.md

@@ -0,0 +1,13 @@
+# Continuous Build and Release Setup
+
+[![status-badge](https://ci.logicalhacking.com/api/badges/afp-mirror/Extended_Finite_State_Machine_Inference/status.svg)](https://ci.logicalhacking.com/afp-mirror/Extended_Finite_State_Machine_Inference)
+
+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
+
+* [browser_info](https://artifacts.logicalhacking.com/ci/afp-mirror/Extended_Finite_State_Machine_Inference/main/latest/browser_info/AFP/Extended_Finite_State_Machine_Inference-devel/)
+* [aux files](https://artifacts.logicalhacking.com/ci/afp-mirror/Extended_Finite_State_Machine_Inference/main/latest/)

.woodpecker/build.yml

@@ -0,0 +1,23 @@
+pipeline:
+  build:
+    image: docker.io/logicalhacking/isabelle2021-1
+    commands:
+      - export ARTIFACT_DIR=$CI_WORKSPACE/.artifacts/$CI_REPO/$CI_BRANCH/$CI_BUILD_NUMBER/
+      - mkdir -p $ARTIFACT_DIR
+      - isabelle build -D Extended_Finite_State_Machine_Inference -o browser_info  -o document=pdf
+      - export `isabelle getenv ISABELLE_HOME_USER`
+      - cp -r $ISABELLE_HOME_USER/browser_info $ARTIFACT_DIR
+      - cd $ARTIFACT_DIR
+      - cd ..
+      - ln -s * latest
+  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

Extended_Finite_State_Machine_Inference/Subsumption.thy

@@ -71,7 +71,7 @@ lemma inconsistent_updates:
            (\<exists>r' P. P (p2 $ r') \<and> (\<exists>y. p1 $ r' = Some y) \<and> \<not> P (p1 $ r')) \<Longrightarrow>
 
     \<not> subsumes t2 r t1"
-  by (metis (no_types, hide_lams) option.simps(3) subsumes_def)
+  by (metis (no_types, opaque_lifting) option.simps(3) subsumes_def)
 
 lemma bad_outputs:
   "\<exists>i. can_take_transition t1 i r \<and> evaluate_outputs t1 i r \<noteq> evaluate_outputs t2 i r \<Longrightarrow>

Extended_Finite_State_Machine_Inference/code-targets/Code_Target_FSet.thy

@@ -139,7 +139,7 @@ proof(induct l)
 next
   case (Cons a l)
   then show ?case
-    by (metis sorted_Max_Cons Max_singleton hd_rev last.simps list.set(1) list.simps(15) sorted.simps(2))
+    by (metis sorted_Max_Cons Max_singleton hd_rev last.simps list.set(1) list.simps(15) sorted_simps(2))
 qed
 
 lemma [code]: "fMax (fset_of_list (h#t)) = last (nativeSort (h#t))"

Extended_Finite_State_Machine_Inference/code-targets/Code_Target_Set.thy

@@ -5,7 +5,7 @@ sets. All of the sets we need to use here are finite so we present an alternativ
 basic set operations which generates much cleaner code.\<close>
 
 theory Code_Target_Set
-  imports "HOL-Library.Cardinality"
+  imports "HOL-Library.Code_Cardinality"
 begin
 
 code_datatype set
@@ -19,7 +19,7 @@ declare eq_set_code(2) [code del]
 declare eq_set_code(4) [code del]
 declare List.subset_code [code del]
 declare inter_coset_fold [code del]
-declare Cardinality.subset'_code [code del]
+declare Code_Cardinality.subset'_code [code del]
 
 declare subset_eq [code]
 
@@ -38,7 +38,7 @@ lemma [code]: "insert x (set s) = (if x \<in> set s then set s else set (x#s))"
   by auto
 
 lemma [code]:
-  "Cardinality.subset' (set l1) (set l2) = ((list_all (\<lambda>x. List.member l2 x)) l1)"
+  "Code_Cardinality.subset' (set l1) (set l2) = ((list_all (\<lambda>x. List.member l2 x)) l1)"
   by (meson in_set_member list.pred_set subset'_code(2))
 
 end

Extended_Finite_State_Machine_Inference/document/root.tex

@@ -1,4 +1,5 @@
 \documentclass[10pt,DIV16,a4paper,abstract=true,twoside=semi,openright]{scrreprt}
+\usepackage[T1]{fontenc}
 \usepackage[english]{babel}
 \usepackage[numbers, sort&compress]{natbib}
 \usepackage{isabelle,isabellesym}

README.md

@@ -27,10 +27,10 @@ This project is licensed under a 3-clause BSD-style license.
 
 SPDX-License-Identifier: BSD-3-Clause
 
-## Master Repository
+## Upstream Repository
 
-The master git repository for this project is hosted by the [Software
-Assurance & Security Research Team](https://logicalhacking.com) at
+The upstream git repository, i.e., the single source of truth, for this project is hosted 
+by the [Software Assurance & Security Research Team](https://logicalhacking.com) at
 <https://git.logicalhacking.com/afp-mirror/Extended_Finite_State_Machine_Inference>.
 
 ## Publications