Job 1433

CakeML:1f7df1c11e3f6dfdbbb02505390d22095273946d
  Fix whitespace [Jan 12 11:49:59]
#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 11:51:03 Claimed job
Jan 12 11:51:05 Reusing HOL
Jan 12 11:51:11 Starting developers
Jan 12 11:51:13 Finished developers                                               2s 110MB
Jan 12 11:51:13 Starting developers/bin
Jan 12 11:51:19 Finished developers/bin                                           5s   1GB
Jan 12 11:51:20 Starting semantics/ffi
Jan 12 11:51:30 Finished semantics/ffi                                           10s 305MB
Jan 12 11:51:30 Starting semantics
Jan 12 11:52:55 Finished semantics                                             1m25s   1GB
Jan 12 11:52:55 Starting semantics/proofs
Jan 12 11:56:28 Finished semantics/proofs                                      3m32s   2GB
Jan 12 11:56:28 Starting semantics/alt_semantics
Jan 12 11:56:36 Finished semantics/alt_semantics                                  8s 397MB
Jan 12 11:56:36 Starting semantics/alt_semantics/proofs
Jan 12 11:57:26 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:   12s  user:   11s     OK
Starting work on bigClockTheory
bigStepPropsTheory                                                            real:   20s  user:   20s     OK
bigClockTheory                                                                real:   22s  user:   21s     OK
Starting work on bigSmallEquivTheory
Starting work on interpTheory
interpTheory                                                                  real:   13s  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-1433/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-1433/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