Version README notes

kth-step · Jan 24, 2025 · 45afb59 · 45afb59
1 parent 4c10aa7
commit 45afb59
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 2 deletions.
diff --git a/hol/cake_sem/README.md b/hol/cake_sem/README.md
@@ -1,3 +1,7 @@
+NOTE: This directory uses HOL4 commit 814042201, and is not guaranteed to function properly with the Trindemossen-1 release.
+
+The CakeML release used in this directory is v2747.
+
 p4_exec_sem_cakeScript.sml contains a more CakeML-friendly reformulation of the regular executable semantics (found in p4_exec_semScript.sml).
 
 p4_cake_transformScript.sml contains HOL4 functions to transform the actx and astate of the regular semantics to those of the CakeML-adjusted version. The SML functions are found in p4_cake_transformLib.sml.

diff --git a/hol/cake_sem/p4_exec_sem_cakeProgScript.sml b/hol/cake_sem/p4_exec_sem_cakeProgScript.sml
@@ -6,8 +6,7 @@ open p4Theory p4_auxTheory p4_coreTheory p4_v1modelTheory;
 open p4_exec_sem_cakeTheory p4_arch_cakeTheory;
 
 (* CakeML: *)
-open preamble ml_translatorLib ml_translatorTheory ml_progLib basisProgTheory mlmapTheory basisFunctionsLib
-     astPP comparisonTheory;
+open preamble ml_translatorLib ml_progLib basisProgTheory;
 
 intLib.deprecate_int();
 val _ = (max_print_depth := 100);