CakeML:4545556a74fc514d40693abe6d681984170cb92f
Merge branch 'master' into fix_build_instrs
#744 (fix_build_instrs)
Merging into:3f95e30b3a56a7232be14b466ac8bee08db5fbe9
Fix inferComplete for abbrev changes in HOL master
HOL:ff3ac4c4c36730c3560764bd9487f22baea5d7a9
Avoid GC test warnings on low user times, and avoid a MoscowML bug
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux
Claimed job
Reusing HOL
Starting developers
Finished developers 0s 34MB
Starting developers/bin
Finished developers/bin 6s 1GB
Starting semantics/ffi
Finished semantics/ffi 10s 241MB
Starting semantics
Finished semantics 1m28s 1GB
Starting semantics/proofs
Finished semantics/proofs 3m28s 1GB
Starting semantics/alt_semantics
Finished semantics/alt_semantics 8s 327MB
Starting semantics/alt_semantics/proofs
Finished semantics/alt_semantics/proofs 2m10s 845MB
Starting basis/pure
Finished basis/pure 52s 959MB
Starting translator
Finished translator 2m46s 1GB
Starting compiler/parsing
Finished compiler/parsing 1m07s 3GB
Starting characteristic
Finished characteristic 5m50s 2GB
Starting translator/monadic
Finished translator/monadic 1m33s 1GB
Starting basis
Finished basis 32m57s 13GB
Starting compiler/inference
Finished compiler/inference 59s 1GB
Starting compiler/backend/reg_alloc
Finished compiler/backend/reg_alloc 1m02s 1GB
Starting compiler/backend/gc
Finished compiler/backend/gc 3m14s 2GB
Starting compiler/backend
Finished compiler/backend 4m31s 3GB
Starting compiler/encoders/asm
Finished compiler/encoders/asm 20s 596MB
Starting compiler/encoders/x64
Finished compiler/encoders/x64 24s 752MB
Starting compiler/encoders/arm7
Finished compiler/encoders/arm7 49s 649MB
Starting compiler/encoders/arm8
Finished compiler/encoders/arm8 12s 644MB
Starting compiler/encoders/mips
Finished compiler/encoders/mips 16s 1GB
Starting compiler/encoders/riscv
Finished compiler/encoders/riscv 15s 929MB
Starting compiler/encoders/ag32
Finished compiler/encoders/ag32 16s 889MB
Starting compiler/backend/x64
Finished compiler/backend/x64 18s 1GB
Starting compiler/backend/arm7
Finished compiler/backend/arm7 19s 1GB
Starting compiler/backend/arm8
Finished compiler/backend/arm8 18s 1GB
Starting compiler/backend/mips
Finished compiler/backend/mips 18s 1GB
Starting compiler/backend/riscv
Finished compiler/backend/riscv 18s 1GB
Starting compiler/backend/ag32
Finished compiler/backend/ag32 1m06s 1GB
Starting compiler/parsing/proofs
Finished compiler/parsing/proofs 5m37s 1GB
Starting compiler/inference/proofs
Finished compiler/inference/proofs 2m24s 1GB
Starting compiler/backend/semantics
FAILED: compiler/backend/semantics
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc/lem_lib_stub[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reachability[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Starting work on backendPropsTheory
Starting work on closSemTheory
Starting work on flatSemTheory
Starting work on wordSemTheory
backendPropsTheory real: 11s user: 11s OK
closSemTheory real: 24s user: 23s OK
Starting work on bvlSemTheory
Starting work on closPropsTheory
flatSemTheory real: 24s user: 24s OK
Starting work on dataSemTheory
bvlSemTheory real: 19s user: 18s OK
Starting work on bviSemTheory
wordSemTheory real: 48s user: 47s OK
Starting work on flatPropsTheory
bviSemTheory real: 18s user: 17s OK
Starting work on targetSemTheory
targetSemTheory real: 14s user: 13s OK
Starting work on labSemTheory
labSemTheory real: 21s user: 20s OK
Starting work on labPropsTheory
dataSemTheory real: 108s user: 107s OK
Starting work on dataPropsTheory
flatPropsTheory real: 92s user: 91s OK
Starting work on data_monadTheory
labPropsTheory real: 61s user: 60s OK
Starting work on stackSemTheory
data_monadTheory real: 18s user: 18s OK
Starting work on targetPropsTheory
targetPropsTheory real: 14s user: 14s OK
Starting work on wordPropsTheory
stackSemTheory real: 33s user: 32s OK
Starting work on stackPropsTheory
closPropsTheory real: 186s user: 185s OK
Starting work on bvlPropsTheory
bvlPropsTheory real: 106s user: 104s OK
Starting work on bviPropsTheory
stackPropsTheory real: 142s user: 140s OK
bviPropsTheory real: 54s user: 53s OK
wordPropsTheory real: 330s user: 326s OK
dataPropsTheory real: 1511s user: 1491sFAIL<1>
t1. evaluate (prog,t) = (res,t1) cc_co_only_diff s1 t1
failed.
Failed to prove theorem evaluate_cc_co_only_diff.
Exception raised at Tactical.THEN1:
first subgoal not solved by second tactic (THEN1 on line 2623) (THEN1 on line 2660) (THEN1 on line 2663) (THEN1 on line 2668) (THEN1 on line 2672) (THEN1 on line 2676) (THEN1 on line 2683) (THEN1 on line 2695) (THEN1 on line 2706)
error in quse /home/myreen/regression/cakeml-1312/compiler/backend/semantics/dataPropsScript.sml : HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 2623) (THEN1 on line 2660) (THEN1 on line 2663) (THEN1 on line 2668) (THEN1 on line 2672) (THEN1 on line 2676) (THEN1 on line 2683) (THEN1 on line 2695) (THEN1 on line 2706)", origin_function = "THEN1", origin_structure = "Tactical"}
error in load /home/myreen/regression/cakeml-1312/compiler/backend/semantics/dataPropsScript : HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 2623) (THEN1 on line 2660) (THEN1 on line 2663) (THEN1 on line 2668) (THEN1 on line 2672) (THEN1 on line 2676) (THEN1 on line 2683) (THEN1 on line 2695) (THEN1 on line 2706)", origin_function = "THEN1", origin_structure = "Tactical"}
Uncaught exception: HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 2623) (THEN1 on line 2660) (THEN1 on line 2663) (THEN1 on line 2668) (THEN1 on line 2672) (THEN1 on line 2676) (THEN1 on line 2683) (THEN1 on line 2695) (THEN1 on line 2706)", origin_function = "THEN1", origin_structure = "Tactical"}