AutoCorres 1.11 + CParser 1.21 release

misc/scripts/thydeps

@@ -51,7 +51,7 @@ def session_theory_deps(isabelle_dir, ROOT_dirs, sessions):
             isabelle_dir, cmdline, ignore_exit_code=True).splitlines():
         l = l.decode('utf-8')
         # 'Session HOL/HOL-Library (main timing)'
-        m = re.match(r'Session (' + session_name_re + ')/(' + session_name_re + ')(?: \(.*\))?', l)
+        m = re.match(r'Session (' + session_name_re + ')/(' + session_name_re + r')(?: \(.*\))?', l)
         if m:
             # start processing next session
             _, session = m.groups()

tools/autocorres/README.md

@@ -4,7 +4,9 @@
      SPDX-License-Identifier: CC-BY-SA-4.0
 -->
 
+<!--
 Note to maintainer: sync with tools/release_files/README
+-->
 
 AutoCorres
 ==========
@@ -15,9 +17,13 @@ in [Isabelle/HOL][1]. In particular, it uses Norrish's
 abstracts the result to produce a result that is (hopefully)
 more pleasant to reason about.
 
+Before using this version of AutoCorres, consider using [AutoCorres2]
+available from the [Archive of Formal Proofs][AFP].
+
   [1]: https://isabelle.in.tum.de
   [2]: https://github.com/seL4/l4v/blob/master/tools/c-parser/README.md
-
+  [AutoCorres2]: https://www.isa-afp.org/entries/AutoCorres2.html
+  [AFP]: https://www.isa-afp.org
 
 
 Contents of this README
@@ -35,7 +41,7 @@ Contents of this README
 Installation
 ------------
 
-AutoCorres is packaged as a theory for Isabelle2022:
+AutoCorres is packaged as a theory for Isabelle2024:
 
     https://isabelle.in.tum.de
 

tools/autocorres/tools/release_files/ChangeLog

@@ -1,6 +1,14 @@
 AutoCorres Change Log
 =====================
 
+AutoCorres 1.11 (11 Oct 2024)
+----------------------------
+
+        * Isabelle2024 edition of both AutoCorres and the C parser.
+
+        * Further clean-up and restructure of monad libraries.
+
+
 AutoCorres 1.10 (3 Nov 2023)
 ----------------------------
 

tools/autocorres/tools/release_files/README

@@ -7,9 +7,13 @@ in [Isabelle/HOL][1]. In particular, it uses Norrish's
 abstracts the result to produce a result that is (hopefully)
 more pleasant to reason about.
 
+Before using this version of AutoCorres, consider using [AutoCorres2]
+available from the [Archive of Formal Proofs][AFP].
+
   [1]: https://isabelle.in.tum.de/
   [2]: https://github.com/seL4/l4v/blob/master/tools/c-parser/README.md
-
+  [AutoCorres2]: https://www.isa-afp.org/entries/AutoCorres2.html
+  [AFP]: https://www.isa-afp.org
 
 
 Contents of this README
@@ -28,7 +32,7 @@ Contents of this README
 Installation
 ------------
 
-AutoCorres is packaged as a theory for Isabelle2023:
+AutoCorres is packaged as a theory for Isabelle2024:
 
     https://isabelle.in.tum.de
 

tools/c-parser/README.md

@@ -88,10 +88,11 @@ Releases
 
 Current release:
 
-- [c-parser-1.20.tar.gz][1.20] (Released 2023-11-03, Isabelle 2023)
+- [c-parser-1.21.tar.gz][1.21] (Released 2024-10-11, Isabelle 2024)
 
 Older releases:
 
+- [c-parser-1.20.tar.gz][1.20] (Released 2023-11-03, Isabelle 2023)
 - [c-parser-1.19.tar.gz][1.19] (Released 2022-10-31, Isabelle 2021-1)
 - [c-parser-1.18.tar.gz][1.18] (Released 2021-10-31, Isabelle 2021)
 - [c-parser-1.17.tar.gz][1.17] (Released 2020-11-02, Isabelle 2020)
@@ -103,6 +104,7 @@ Older releases:
 - [c-parser-1.12.0.tar.gz][1.12] (Released 2012-12-05, Isabelle 2012)
 - [c-parser-1.0.tar.gz][1.0] (Released 2012-09-24, Isabelle 2011-1)
 
+[1.21]: https://github.com/seL4/l4v/releases/download/autocorres-1.11/c-parser-1.21.tar.gz
 [1.20]: https://github.com/seL4/l4v/releases/download/autocorres-1.10/c-parser-1.20.tar.gz
 [1.19]: https://github.com/seL4/l4v/releases/download/autocorres-1.9/c-parser-1.19.tar.gz
 [1.18]: https://github.com/seL4/l4v/releases/download/autocorres-1.8/c-parser-1.18.tar.gz

tools/c-parser/RELEASES.md

@@ -162,3 +162,10 @@
 - Builds with Isabelle2023
 - Rearranged library session structure and included more libraries for heap
   reasoning in the release. See e.g. files TypHeapLib.thy and LemmaBucket_C.thy
+
+## 1.21
+
+- Builds with Isabelle2024
+- Updated SIMPL from the AFP
+- Ensure that umm_types.txt is saved relative to theory file
+- If cpp_path is relative, make it relative to the current theory

tools/c-parser/mkrelease

@@ -12,8 +12,8 @@
 set -e
 
 case $(uname) in
-  Darwin* ) TAR=gtar ; SEDIOPT="-i ''" ;;
-  * ) TAR=tar ; SEDIOPT=-i ;;
+  Darwin* ) TAR=gtar ;;
+  * ) TAR=tar ;;
 esac
 
 
@@ -145,18 +145,20 @@ echo "Hacking Makefile to remove ROOT generation."
 if ! grep -q '^testfiles/\$(L4V_ARCH)/ROOT' "$outputdir/src/c-parser/Makefile"; then
     die "failed to process c-parser/Makefile"
 fi
-sed $SEDIOPT \
+sed -i .bak \
     -e '/^testfiles\/\$(L4V_ARCH)\/ROOT/,/CParserTest/d' \
     -e '/^all_tests_\$(L4V_ARCH)\.thy/,/CParser/d' \
     "$outputdir/src/c-parser/Makefile"
+rm -f "$outputdir/src/c-parser/Makefile.bak"
 
 echo "Hacking Makefile to change root dir."
 if ! grep -q '^L4V_ROOT_DIR = ' "$outputdir/src/c-parser/Makefile"; then
     die "failed to process c-parser/Makefile"
 fi
-sed $SEDIOPT \
+sed -i .bak \
     -e 's/^L4V_ROOT_DIR = .*$/L4V_ROOT_DIR = ../' \
     "$outputdir/src/c-parser/Makefile"
+rm -f "$outputdir/src/c-parser/Makefile.bak"
 
 echo "Generating standalone-parser/table.ML"
 pushd "$TOPLEVEL_DIR/tools/c-parser" > /dev/null
@@ -165,10 +167,10 @@ pushd "$TOPLEVEL_DIR/tools/c-parser" > /dev/null
 cp standalone-parser/table.ML "$outputdir/src/c-parser/standalone-parser"
 echo "Cleaning up standalone-parser's Makefile"
 sed '
-  1i\
-  SML_COMPILER ?= mlton
+  /^STP_PFX :=/i\
+SML_COMPILER ?= mlton
   /^include/d
-  /General\/table.ML/,/pretty-printing/d
+  /General\/table.ML/,/unsynchronized_cache/d
   /ISABELLE_HOME/d
   /CLEAN_TARGETS/s|\$(STP_PFX)/table.ML||
 ' < standalone-parser/Makefile > "$outputdir/src/c-parser/standalone-parser/Makefile"
@@ -177,7 +179,7 @@ popd > /dev/null
 echo "Making PDF of ctranslation file."
 cd "$outputdir/src/c-parser/doc"
 make ctranslation.pdf > /dev/null
-/bin/rm ctranslation.{log,aux,blg,bbl,toc}
+/bin/rm -f ctranslation.{log,aux,blg,bbl,toc}
 mv ctranslation.pdf "$outputdir/doc"
 
 popd > /dev/null