Job 1434

CakeML:2b02fc2b23f91aaa62ed7a81d6959657556936e0
  More EnvID -> Env_id changes [Jan 12 14:05:58]
#811 (eval)
Merging into:3c6495906dc020e093e2f5cf101cea1cba2fc468
  Fix breakage caused by change to sorted_map in HOL [Jan 05 15:57:59]
HOL:89e07c5a43c0637bc614b4396e6a8b3cb902cedb
  Get the Interaction-emacs manual built properly as part of release [Jan 06 05:48:29]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Jan 12 14:23:20 Claimed job
Jan 12 14:23:23 Reusing HOL
Jan 12 14:23:28 Starting developers
Jan 12 14:23:31 Finished developers                                               2s  93MB
Jan 12 14:23:31 Starting developers/bin
Jan 12 14:23:37 Finished developers/bin                                           5s   1GB
Jan 12 14:23:37 Starting semantics/ffi
Jan 12 14:23:47 Finished semantics/ffi                                            9s 307MB
Jan 12 14:23:47 Starting semantics
Jan 12 14:25:14 Finished semantics                                             1m26s   1GB
Jan 12 14:25:14 Starting semantics/proofs
Jan 12 14:28:47 Finished semantics/proofs                                      3m32s   1GB
Jan 12 14:28:47 Starting semantics/alt_semantics
Jan 12 14:28:56 Finished semantics/alt_semantics                                  8s 419MB
Jan 12 14:28:56 Starting semantics/alt_semantics/proofs
Jan 12 14:29:46 FAILED: semantics/alt_semantics/proofs
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(CAKEMLDIR)/misc/lem_lib_stub[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
Starting work on README.md
Starting work on determTheory
Starting work on bigSmallInvariantsTheory
Starting work on bigStepPropsTheory
README.md                                                                     real:    0s  user:    0s     OK
bigSmallInvariantsTheory                                                      real:    3s  user:    3s     OK
determTheory                                                                  real:   11s  user:   11s     OK
Starting work on bigClockTheory
bigStepPropsTheory                                                            real:   20s  user:   19s     OK
bigClockTheory                                                                real:   22s  user:   22s     OK
Starting work on bigSmallEquivTheory
Starting work on interpTheory
interpTheory                                                                  real:   14s  user:   13sFAIL<1>
 
 evaluate_dec T env st (Denv s) (st',r)
 
 Failed to prove theorem run_eval_decs_spec.
 
 Exception raised at Tactical.TAC_PROOF:
 unsolved goals
 error in quse /home/myreen/regression/cakeml-1434/semantics/alt_semantics/proofs/interpScript.sml : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
 error in load /home/myreen/regression/cakeml-1434/semantics/alt_semantics/proofs/interpScript : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
 Uncaught exception: HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
bigSmallEquivTheory                                                                                   M-KILLED