From c7f74c92ae75b87b4df55a0b1a99ce99e52d5f85 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Wed, 9 Oct 2024 19:02:51 +1100 Subject: [PATCH 1/5] misc/thydeps: correct regexp escape Signed-off-by: Gerwin Klein --- misc/scripts/thydeps | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/misc/scripts/thydeps b/misc/scripts/thydeps index b0cc667613..f2fab83403 100755 --- a/misc/scripts/thydeps +++ b/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() From 007a0861ed215c604d6161e3c18430ade83d2893 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Wed, 9 Oct 2024 18:13:00 +1100 Subject: [PATCH 2/5] autocorres: update change log and readme for release Signed-off-by: Gerwin Klein --- tools/autocorres/README.md | 10 ++++++++-- tools/autocorres/tools/release_files/ChangeLog | 8 ++++++++ tools/autocorres/tools/release_files/README | 8 ++++++-- 3 files changed, 22 insertions(+), 4 deletions(-) diff --git a/tools/autocorres/README.md b/tools/autocorres/README.md index e564e53413..42d09b19e9 100644 --- a/tools/autocorres/README.md +++ b/tools/autocorres/README.md @@ -4,7 +4,9 @@ SPDX-License-Identifier: CC-BY-SA-4.0 --> + 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 diff --git a/tools/autocorres/tools/release_files/ChangeLog b/tools/autocorres/tools/release_files/ChangeLog index e95f216e9b..ab0360bce3 100644 --- a/tools/autocorres/tools/release_files/ChangeLog +++ b/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) ---------------------------- diff --git a/tools/autocorres/tools/release_files/README b/tools/autocorres/tools/release_files/README index 45a68444ee..0283eb8057 100644 --- a/tools/autocorres/tools/release_files/README +++ b/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 From 0c9f326a51beeb5082520b26db5f8f1b0862f926 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Wed, 9 Oct 2024 18:34:35 +1100 Subject: [PATCH 3/5] c-parser: update change log and readme for release Signed-off-by: Gerwin Klein --- tools/c-parser/README.md | 4 +++- tools/c-parser/RELEASES.md | 7 +++++++ 2 files changed, 10 insertions(+), 1 deletion(-) diff --git a/tools/c-parser/README.md b/tools/c-parser/README.md index f765baeea4..2e4ded61f5 100644 --- a/tools/c-parser/README.md +++ b/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 diff --git a/tools/c-parser/RELEASES.md b/tools/c-parser/RELEASES.md index 58c9473433..29a47a33cb 100644 --- a/tools/c-parser/RELEASES.md +++ b/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 From 6122e247d7e4486fa9634d8ded97afc2524de8d3 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Thu, 10 Oct 2024 19:20:09 +1100 Subject: [PATCH 4/5] c-parser: adjust release script for Makefile changes The Makefile of the standalone parser has changed, so the patterns used in the sed script in mkrelease no longer fit the content. Signed-off-by: Gerwin Klein --- tools/c-parser/mkrelease | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/tools/c-parser/mkrelease b/tools/c-parser/mkrelease index 97afbdddd4..27be698bcb 100755 --- a/tools/c-parser/mkrelease +++ b/tools/c-parser/mkrelease @@ -165,10 +165,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" From 4f1563a8f343e6c7062c55c7d7f16922a2e811ba Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Fri, 11 Oct 2024 09:17:12 +1100 Subject: [PATCH 5/5] c-parser: handle sed backup files uniformly in mkrelease mkrelease was trying to distinguish BSD and GNU sed command line options, but was using shell substitution incorrectly. Instead, use backup files for both versions, and then manually remove the backup file afterwards. Signed-off-by: Gerwin Klein --- tools/c-parser/mkrelease | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/tools/c-parser/mkrelease b/tools/c-parser/mkrelease index 27be698bcb..5dc135dae5 100755 --- a/tools/c-parser/mkrelease +++ b/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 @@ -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