Update for new way of doing in-logic compilation

CakeML · Aug 8, 2024 · 9bf0053 · 9bf0053
1 parent 7208aa9
commit 9bf0053
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 2 deletions.
diff --git a/compiler/binary/Holmakefile b/compiler/binary/Holmakefile
@@ -8,6 +8,11 @@ INCLUDES = ../../language \
            $(CAKEMLDIR)/examples \
            $(CAKEMLDIR)/translator \
            $(CAKEMLDIR)/compiler \
+           $(CAKEMLDIR)/cv_translator \
            $(HOLDIR)/examples/formal-languages/context-free \
            $(HOLDIR)/examples/algorithms \
            $(HOLDIR)/examples/algorithms/unification/triangular/first-order
+
+ifdef POLY
+HOLHEAP = $(CAKEMLDIR)/cv_translator/cake_compile_heap
+endif
diff --git a/compiler/binary/pure_compilerCompileScript.sml b/compiler/binary/pure_compilerCompileScript.sml
@@ -2,11 +2,11 @@
   Compiles the PureCake compiler using the CakeML compiler
 *)
 
-open preamble compilationLib pure_compilerProgTheory;
+open preamble pure_compilerProgTheory eval_cake_compile_x64Lib
 
 val _ = new_theory "pure_compilerCompile"
 
 Theorem pure_compiler_compiled =
-  compile_x64 "pure" pure_compiler_prog_def;
+  eval_cake_compile_x64 "" pure_compiler_prog_def "pure.S";
 
 val _ = export_theory ();