Job 1049

CakeML:c3ca0d41def5b445cd60312ec5d2bacc3a99890f
  Fix a weakness in PMATCH translation [Oct 06 05:48:37]
#692 (match-refactor-2)
Merging into:b8b20698feb965c78a1dc6dde4da81ce368ead3a
  Fix a proof broken by minor HOL change [Oct 05 13:27:47]
HOL:c80b32898bc7a3f692c1be84161e569112efdfa9
  Fix ARM_security_properties example for change in 44aabdd82 [Oct 02 12:15:29]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Oct 06 05:51:36 Claimed job
Oct 06 05:51:42 Building HOL
Oct 06 06:04:03 Starting developers
Oct 06 06:04:06 Finished developers                                               2s 118MB
Oct 06 06:04:06 Starting developers/bin
Oct 06 06:04:10 Finished developers/bin                                           3s 164MB
Oct 06 06:04:10 Starting semantics/ffi
Oct 06 06:04:58 Finished semantics/ffi                                           47s 512MB
Oct 06 06:04:59 Starting semantics
Oct 06 06:07:03 Finished semantics                                             2m04s   1GB
Oct 06 06:07:04 Starting semantics/proofs
Oct 06 06:10:24 Finished semantics/proofs                                      3m19s   1GB
Oct 06 06:10:24 Starting semantics/alt_semantics
Oct 06 06:10:31 Finished semantics/alt_semantics                                  6s 313MB
Oct 06 06:10:31 Starting semantics/alt_semantics/proofs
Oct 06 06:11:26 FAILED: semantics/alt_semantics/proofs
]0;Holmake: ~/regression/cakeml-1049/misc]0;Holmake: ~/regression/HOL-c80b32898bc7a3f692c1be84161e569112efdfa9/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-c80b32898bc7a3f692c1be84161e569112efdfa9/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/regression/cakeml-1049/misc]0;Holmake: ~/regression/cakeml-1049/developers]0;Holmake: ~/regression/cakeml-1049/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-1049/misc]0;Holmake: ~/regression/cakeml-1049/misc/lem_lib_stub]0;Holmake: ~/regression/HOL-c80b32898bc7a3f692c1be84161e569112efdfa9/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-c80b32898bc7a3f692c1be84161e569112efdfa9/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/cakeml-1049/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-1049/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-1049/misc]0;Holmake: ~/regression/cakeml-1049/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: .]0;Holmake: ../..]0;Holmake: ../../ffi]0;Holmake: ../../ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ../..]0;Holmake: ../..[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: .]0;Holmake: ..]0;Holmake: ..[1mWorking in $(CAKEMLDIR)/semantics/alt_semantics[0m
]0;Holmake: .]0;Holmake: ../../proofs]0;Holmake: ../../proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/semantics/alt_semantics/proofs[0m
Starting work on determTheory
Starting work on bigSmallInvariantsTheory
Starting work on bigStepPropsTheory
Starting work on README.md
README.md                                                                     real:    0s  user:    0s     OK
bigSmallInvariantsTheory                                                      real:    3s  user:    3s     OK
determTheory                                                                  real:   10s  user:   10s     OK
Starting work on bigClockTheory
bigStepPropsTheory                                                            real:   12s  user:   12s     OK
bigClockTheory                                                                real:   21s  user:   20s     OK
Starting work on bigSmallEquivTheory
Starting work on interpTheory
interpTheory                                                                  real:   12s  user:   12s     OK
Starting work on funBigStepEquivTheory
funBigStepEquivTheory                                                         real:   10s  user:    9sFAIL<1>
 
 F
 
 Failed to prove theorem evaluate_eq_run_eval_list.
 
 Exception raised at Tactical.TAC_PROOF:
 unsolved goals
 error in quse /home/myreen/regression/cakeml-1049/semantics/alt_semantics/proofs/funBigStepEquivScript.sml : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
 error in load funBigStepEquivScript : 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