Initial commit.

.woodpecker/build.yml

@@ -1,11 +1,15 @@
 pipeline:
   build:
-    image: docker.io/logicalhacking/isabelle2021
+    image: docker.io/logicalhacking/isabelle2022
     commands:
+      - ./.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/
       - mkdir -p $ARTIFACT_DIR
       - export `isabelle getenv ISABELLE_HOME_USER`
       - isabelle build -D . -o browser_info
+      - isabelle scala .woodpecker/profiling.scala  --sort e isabelle-hacks
       - cp -r $ISABELLE_HOME_USER/browser_info $ARTIFACT_DIR
       - cp output/document.pdf $ARTIFACT_DIR
       - cd $ARTIFACT_DIR
@@ -23,7 +27,7 @@ pipeline:
         from_secret: artifacts_ssh
       user: artifacts
   notify:
-    image: drillster/drone-email
+    image: docker.io/drillster/drone-email
     settings:
       host: smtp.0x5f.org
       username: woodpecker

.woodpecker/check_dangling_theories

@@ -0,0 +1,33 @@
+#!/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

@@ -0,0 +1,45 @@
+#!/bin/bash
+
+
+
+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 -not -name "*.diff" | 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

@@ -0,0 +1,30 @@
+#!/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/profiling.scala

@@ -0,0 +1,88 @@
+#!/bin/sh
+exec isabelle scala "$0" "$@"
+!#
+
+import isabelle._
+import scala.io.Source
+import scala.math.Ordering.Implicits._
+
+def print_times (sessions:List[String], sort:String):Unit = {
+  val user_output_dir: Path = Path.explode("$ISABELLE_HEAPS/$ML_IDENTIFIER")
+  val store = Sessions.store(Options.init())
+  for (session <- sessions) {
+    val db_path = user_output_dir+store.database(session)
+    if (db_path.file.exists()) {
+      val db = SQLite.open_database(db_path)
+      val command_timings = store.read_command_timings(db, session)
+      val theory_timings = store.read_theory_timings(db, session)
+      if (!(theory_timings.isEmpty)) {
+        println()
+        println(f" +---------------------------------------------------------+-------------+------------+------------+")
+        println(f" | Theory                                                  | elapsed [s] | cpu [s]    | gc [s]     |")
+        println(f" +---------------------------------------------------------+-------------+------------+------------+")        
+        val timings = sort match {
+          case "n" => theory_timings.sortBy(p => p.filter(e => e._1 == "name").head)
+          case "e" => theory_timings.sortBy(p => p.filter(e => e._1 == "elapsed").head._2.toDouble).reverse
+          case "c" => theory_timings.sortBy(p => p.filter(e => e._1 == "cpu").head._2.toDouble).reverse
+          case "g" => theory_timings.sortBy(p => p.filter(e => e._1 == "gc").head._2.toDouble).reverse
+          case  _  => theory_timings
+        }
+        var telapsed = 0.0
+        var tcpu = 0.0
+        var tgc = 0.0
+        timings.foreach { p => {
+          val (_, theory) = p.filter (e => e._1 == "name").head
+          val (_, elapsed) = p.filter (e => e._1 == "elapsed").head
+          val (_, cpu) = p.filter (e => e._1 == "cpu").head
+          val (_, gc) = p.filter (e => e._1 == "gc").head
+          telapsed = telapsed + elapsed.toDouble
+          tcpu = tcpu + cpu.toDouble
+          tgc = tgc + gc.toDouble
+          println(f" | $theory%-55s | $elapsed%11s | $cpu%10s | $gc%10s |")}
+        }
+        println(f" +---------------------------------------------------------+-------------+------------+------------+")
+        println(f" | Total                                                   | $telapsed%11.3f | $tcpu%10.3f | $tgc%10.3f |")
+        println(f" +---------------------------------------------------------+-------------+------------+------------+")
+        println()
+      }else{
+        System.err.println("Warning: No theory timings found!")
+      }
+    }
+  }
+ } 
+def main(args: Array[String]):Unit = {
+val usage = """
+    Usage: isabelle scala extract_timing_as_csv.scala [--help] SESSION_NAME
+
+           --sort n|c|e|g sort by [n]ame, [c]pu, [e]lapsed, [g]c
+           --help       prints this help message
+  """
+  val arglist = args.toList
+  type OptionMap = Map[Symbol, Any]
+  Map(scala.Symbol("sort") -> "u")
+  def nextOption(map : OptionMap, list: List[String]) : OptionMap = {
+    def isSwitch(s : String) = (s(0) == '-')
+      list match {
+        case Nil => map
+        case "--help" :: tail      => println(usage) 
+                                      System.exit(0)
+                                      map
+        case "--sort" :: o :: tail => o match {
+                                        case "n" => nextOption(map ++ Map(scala.Symbol("sort") -> "n"), tail)
+                                        case "c" => nextOption(map ++ Map(scala.Symbol("sort") -> "c"), tail)
+                                        case "e" => nextOption(map ++ Map(scala.Symbol("sort") -> "e"), tail)
+                                        case "g" => nextOption(map ++ Map(scala.Symbol("sort") -> "g"), tail)
+        }
+        case string :: Nil         => nextOption(map ++ Map(scala.Symbol("session") -> string), list.tail)
+        case option :: tail        => println("Unknown option "+option) 
+                                      System.exit(1)
+                                      map
+      }
+  }
+  val options = nextOption(Map(),arglist)
+
+  val sessions = List(options(scala.Symbol("session")).asInstanceOf[String])
+  print_times (sessions, options(scala.Symbol("sort")).asInstanceOf[String])
+
+}
+

Code_Reflection.thy

@@ -28,7 +28,7 @@
  * Dependencies: None
  ***********************************************************************************)
 
-chapter\<open>Code Reflection for \<close>
+chapter\<open>Code Reflection for Isabelle\<close>
 theory
   "Code_Reflection"
 imports 
@@ -44,7 +44,7 @@ ML\<open>
       fun is_sml_file f = String.isSuffix ".ML" (Path.implode (#path f))
       val files = (map (Generated_Files.check_files_in (Context.proof_of ctxt)) args) 
       val ml_files = filter is_sml_file (map #1 (maps Generated_Files.get_files_in files))
-      val ml_content = map (fn f => Syntax.read_input (#content f)) ml_files
+      val ml_content = map (fn f => Syntax.read_input (Bytes.content (#content f))) ml_files
       fun eval ml_content   = fold (fn sml => (ML_Context.exec 
                                            (fn () => ML_Context.eval_source ML_Compiler.flags sml))) 
                                    ml_content 

README.md

@@ -5,7 +5,7 @@ functionality to [Isabelle](https://isabelle.in.tum.de) or showcase
 specific functionality. The individual hacks usually consist out of 
 a single theory file and all documentation is contained in that 
 theory file. The master branch should work with the latest official 
-release of Isabelle (Isabelle 2021-1, at time of writing), hacks for 
+release of Isabelle (Isabelle 2022, at time of writing), hacks for 
 older versions might be available on a dedicated branch.
 
 ## List of Isabelle Hacks