OverviewCakeML:4cd953474ce72ae40ffdbb303741a04124d4fb2a
prove word_to_word_compile_semantics
#909 (word_to_word_Pancake)
Merging into:5124cba7723d5cf97e6dad4abef67f2f91257971
Remove now-redundant calls to diminish_srw_ss
HOL:893dead4b6f59a9be7fc251533d0a5ee77e12e56
Add some simple test for bitArithLib and document in next-release.md
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux
Claimed job
Building HOL
Starting developers
Finished developers 0s 37MB
Starting developers/bin
Finished developers/bin 6s 1GB
Starting semantics/ffi
Finished semantics/ffi 8s 273MB
Starting semantics
Finished semantics 2m33s 1GB
Starting semantics/proofs
Finished semantics/proofs 6m48s 2GB
Starting semantics/alt_semantics
Finished semantics/alt_semantics 25s 567MB
Starting semantics/alt_semantics/proofs
FAILED: semantics/alt_semantics/proofs
Scanning [1m$(HOLDIR)/src/sort[0m
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/quotient/src[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/alt_semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanned 20 directories
Starting work on determTheory
Starting work on bigSmallInvariantsTheory
Starting work on bigStepPropsTheory
bigSmallInvariantsTheory (4s) OK
determTheory (30s) OK
Starting work on bigClockTheory
Starting work on smallStepPropsTheory
bigStepPropsTheory (62s) OK
bigClockTheory (111s) OK
Starting work on interpTheory
interpTheory (22s) OK
Starting work on funBigStepEquivTheory
funBigStepEquivTheory (32s) OK
smallStepPropsTheory (287s)FAIL<1>
Saved theorem _______ "small_eval_match_cases"
Saved definition ____ "alt_small_eval_def"
Saved induction _____ "alt_small_eval_ind"
Saved theorem _______ "small_eval_match_thm"
Saved theorem _______ "small_eval_opapp_err"
Saved theorem _______ "small_eval_app_err"
Saved theorem _______ "small_eval_app_err_more"
error in quse /home/myreen/regression/cakeml-1988/semantics/alt_semantics/proofs/smallStepPropsScript.sml : UNCHANGED
error in load /home/myreen/regression/cakeml-1988/semantics/alt_semantics/proofs/smallStepPropsScript : UNCHANGED
Uncaught exception: UNCHANGED