Job 312

CakeML:1e5a9c21d25ee0350e8af32055b4bc49d9befdbe
  Use --reg_alg=0 in unverified bootstrap [May 07 23:28:57]
#488 (update-reg-alloc)
Merging into:90b3601db1588e986ab69d2cc7f1ee6cc758bfc0
  Fix a bug in the monadic translator post-processing steps [May 04 14:50:27]
HOL:9d31c479b4b04cb87ab3bed186b657d646e8fffe
  Make quote-filter handle newlines in type quotations consistently [May 07 03:26:52]
Machine:cakeml1794 4.4.0-98-generic x86_64 GNU/Linux

May 08 02:25:55 Claimed job
May 08 02:26:10 Building HOL
May 08 02:37:38 Starting developers/bin
May 08 02:39:59 Finished developers/bin                                        2m19s 136MB
May 08 02:40:01 Starting semantics/ffi
May 08 02:41:03 Finished semantics/ffi                                           59s 329MB
May 08 02:41:05 Starting semantics
May 08 02:43:26 Finished semantics                                             2m19s 918MB
May 08 02:43:28 Starting semantics/proofs
May 08 02:46:38 Finished semantics/proofs                                      3m08s   1GB
May 08 02:46:40 Starting basis/pure
May 08 02:52:27 Finished basis/pure                                            5m45s 685MB
May 08 02:52:29 Starting translator
May 08 02:53:56 FAILED: translator
]0;Holmake: /scratch/cakeml/regression/HOL-9d31c479b4b04cb87ab3bed186b657d646e8fffe/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-9d31c479b4b04cb87ab3bed186b657d646e8fffe/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-9d31c479b4b04cb87ab3bed186b657d646e8fffe/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-9d31c479b4b04cb87ab3bed186b657d646e8fffe/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-9d31c479b4b04cb87ab3bed186b657d646e8fffe/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/HOL-9d31c479b4b04cb87ab3bed186b657d646e8fffe/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-9d31c479b4b04cb87ab3bed186b657d646e8fffe/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-9d31c479b4b04cb87ab3bed186b657d646e8fffe/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: ../basis/pure]0;Holmake: ../misc]0;Holmake: /scratch/cakeml/regression/HOL-9d31c479b4b04cb87ab3bed186b657d646e8fffe/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-9d31c479b4b04cb87ab3bed186b657d646e8fffe/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../misc]0;Holmake: /scratch/cakeml/regression/HOL-9d31c479b4b04cb87ab3bed186b657d646e8fffe/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-9d31c479b4b04cb87ab3bed186b657d646e8fffe/examples/machine-code/hoare-tripleWorking in $(HOLDIR)/examples/machine-code/hoare-triple
]0;Holmake: ../misc]0;Holmake: ../developers]0;Holmake: ../developersWorking in ../developers
]0;Holmake: ../misc]0;Holmake: ../misc/lem_lib_stub]0;Holmake: ../misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ../misc]0;Holmake: ../miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: ../basis/pure]0;Holmake: ../basis/pureWorking in $(CAKEMLDIR)/basis/pure
]0;Holmake: .]0;Holmake: ../semantics]0;Holmake: ../semantics/ffi]0;Holmake: ../semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: ../semantics]0;Holmake: ../semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: .]0;Holmake: ../semantics/alt_semantics]0;Holmake: ../semantics/alt_semanticsWorking in $(CAKEMLDIR)/semantics/alt_semantics
Starting work on bigStepScript
Starting work on heap
bigStepScript                                                                OK
heap                                                                         OK
Starting work on smallStepTheory
smallStepTheory                                                              OK
Starting work on bigStepTheory
bigStepTheory                                                                OK
]0;Holmake: .]0;Holmake: ../semantics/alt_semantics/proofs]0;Holmake: ../semantics/proofs]0;Holmake: ../semantics/proofsWorking in $(CAKEMLDIR)/semantics/proofs
]0;Holmake: ../semantics/alt_semantics/proofs]0;Holmake: ../semantics/alt_semantics/proofsWorking in $(CAKEMLDIR)/semantics/alt_semantics/proofs
Starting work on heap
Starting work on bigSmallInvariantsScript
bigSmallInvariantsScript                                                     OK
heap                                                                         OK
Starting work on determTheory
Starting work on bigSmallInvariantsTheory
Starting work on bigStepPropsTheory
bigSmallInvariantsTheory                                                     OK
determTheory                                                                 OK
Starting work on bigClockTheory
bigStepPropsTheory                                                           OK
bigClockTheory                                                               OK
Starting work on bigSmallEquivTheory
Starting work on interpTheory
interpTheory                                                        FAILED! <1>
 Saved theorem _____ "evaluate_run_eval_match"
 Saved definition __ "result_bind_def"
 Saved definition __ "result_return_def"
 Saved definition __ "result_raise_def"
 Saved definition __ "get_store_def"
 Saved definition __ "set_store_def"
 Saved definition __ "dec_clock_def"
 error in quse /scratch/cakeml/regression/cakeml-312/semantics/alt_semantics/proofs/interpScript.sml : HOL_ERR {message = "No consistent parse", origin_function = "typed_parse_in_context", origin_structure = "Parse"}
 error in load interpScript : HOL_ERR {message = "No consistent parse", origin_function = "typed_parse_in_context", origin_structure = "Parse"}
 Uncaught exception: HOL_ERR {message = "No consistent parse", origin_function = "typed_parse_in_context", origin_structure = "Parse"}
bigSmallEquivTheory                                                    M-KILLED
]0;Holmake: .