Commit 6fcc5341 authored by Heiko Becker's avatar Heiko Becker

Fast-forward CakeML submodule to latest stable commit, add some debug lines to...

Fast-forward CakeML submodule to latest stable commit, add some debug lines to ci script and fix transScript broken due to upstream CakeML changes
parent b0a01c5c
Subproject commit 1c47169d571439c9a00eaf31af90fadca2139402
Subproject commit 993321ec18c82a08de25de644745215d5ec3fc28
......@@ -486,7 +486,7 @@ val main_whole_prog_spec = Q.store_thm("main_whole_prog_spec",
`hasFreeFD fs /\ inFS_fname fs (File fname) /\
cl = [pname; fname] /\
contents = lines_of (implode (THE (ALOOKUP fs.files (File fname)))) ==>
whole_prog_spec ^(fetch_v "main" st) cl fs
whole_prog_spec ^(fetch_v "main" st) cl fs NONE
((=) (add_stdout fs (runchecker_output_spec contents)))`,
disch_then assume_tac
\\ simp[whole_prog_spec_def]
......
......@@ -50,6 +50,9 @@ $HOLDIR/bin/Holmake
cd ./binary
#$HOLDIR/bin/Holmake -q checkerBinaryTheory.uo
#$HOLDIR/bin/Holmake -q checker.S
#$HOLDIR/bin/Holmake -q cake_checker
#TODO Remove me when CI is stable again?
$HOLDIR/bin/Holmake cleanAll -r
$HOLDIR/bin/Holmake checkerBinaryTheory.uo
$HOLDIR/bin/Holmake checker.S
$HOLDIR/bin/Holmake cake_checker
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment