Job 997

CakeML:aed98c922e3b207e145f2bec7c3c09217c9ce952
  Fix now-broken drule applications (viz recent HOL change) [Aug 12 05:18:56]
HOL:c4ffdebc24abcae15e664f9603d3f5ce699cfaed
  Fix proof broken by change to drule in 812a08a5a8 [Aug 11 09:47:03]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Aug 12 23:21:02 Claimed job
Aug 12 23:21:44 Building HOL
Aug 12 23:29:42 Starting developers
Aug 12 23:29:43 Finished developers                                               0s  40MB
Aug 12 23:29:43 Starting developers/bin
Aug 12 23:31:11 Finished developers/bin                                        1m26s 165MB
Aug 12 23:31:11 Starting semantics/ffi
Aug 12 23:31:45 Finished semantics/ffi                                           33s 372MB
Aug 12 23:31:45 Starting semantics
Aug 12 23:33:15 Finished semantics                                             1m29s   1GB
Aug 12 23:33:15 Starting semantics/proofs
Aug 12 23:36:15 Finished semantics/proofs                                      2m59s   1GB
Aug 12 23:36:15 Starting semantics/alt_semantics
Aug 12 23:36:22 Finished semantics/alt_semantics                                  5s 272MB
Aug 12 23:36:22 Starting semantics/alt_semantics/proofs
Aug 12 23:38:11 Finished semantics/alt_semantics/proofs                        1m48s 765MB
Aug 12 23:38:11 Starting basis/pure
Aug 12 23:41:44 Finished basis/pure                                            3m32s 719MB
Aug 12 23:41:44 Starting translator
Aug 12 23:43:28 Finished translator                                            1m43s   1GB
Aug 12 23:43:28 Starting compiler/parsing
Aug 12 23:44:24 Finished compiler/parsing                                        55s   1GB
Aug 12 23:44:26 Starting characteristic
Aug 12 23:49:34 Finished characteristic                                        5m07s   2GB
Aug 12 23:49:34 Starting translator/monadic
Aug 12 23:50:31 FAILED: translator/monadic
]0;Holmake: ~/regression/cakeml-997/characteristic]0;Holmake: ~/regression/cakeml-997/basis/pure]0;Holmake: ~/regression/HOL-c4ffdebc24abcae15e664f9603d3f5ce699cfaed/examples/balanced_bst]0;Holmake: ~/regression/HOL-c4ffdebc24abcae15e664f9603d3f5ce699cfaed/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: ~/regression/cakeml-997/basis/pure]0;Holmake: ~/regression/HOL-c4ffdebc24abcae15e664f9603d3f5ce699cfaed/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-c4ffdebc24abcae15e664f9603d3f5ce699cfaed/examples/formal-languages]0;Holmake: ~/regression/HOL-c4ffdebc24abcae15e664f9603d3f5ce699cfaed/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-c4ffdebc24abcae15e664f9603d3f5ce699cfaed/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-c4ffdebc24abcae15e664f9603d3f5ce699cfaed/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-c4ffdebc24abcae15e664f9603d3f5ce699cfaed/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-c4ffdebc24abcae15e664f9603d3f5ce699cfaed/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-c4ffdebc24abcae15e664f9603d3f5ce699cfaed/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ~/regression/cakeml-997/basis/pure]0;Holmake: ~/regression/cakeml-997/misc]0;Holmake: ~/regression/HOL-c4ffdebc24abcae15e664f9603d3f5ce699cfaed/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-c4ffdebc24abcae15e664f9603d3f5ce699cfaed/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-997/misc]0;Holmake: ~/regression/cakeml-997/developers]0;Holmake: ~/regression/cakeml-997/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-997/misc]0;Holmake: ~/regression/cakeml-997/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-997/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-997/misc]0;Holmake: ~/regression/cakeml-997/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression/cakeml-997/basis/pure]0;Holmake: ~/regression/cakeml-997/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ~/regression/cakeml-997/characteristic]0;Holmake: ~/regression/cakeml-997/compiler/parsing]0;Holmake: ~/regression/cakeml-997/semantics]0;Holmake: ~/regression/cakeml-997/semantics/ffi]0;Holmake: ~/regression/cakeml-997/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-997/semantics]0;Holmake: ~/regression/cakeml-997/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression/cakeml-997/compiler/parsing]0;Holmake: ~/regression/cakeml-997/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/regression/cakeml-997/characteristic]0;Holmake: ~/regression/cakeml-997/semantics/proofs]0;Holmake: ~/regression/cakeml-997/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ~/regression/cakeml-997/characteristic]0;Holmake: ~/regression/cakeml-997/translator]0;Holmake: ~/regression/cakeml-997/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/regression/cakeml-997/characteristic]0;Holmake: ~/regression/cakeml-997/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: .]0;Holmake: monad_base]0;Holmake: monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
Starting work on ml_monadBaseTheory
Starting work on README.md
README.md                                                                                                  OK
ml_monadBaseTheory                                                                                         OK
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
Starting work on ml_monad_translatorBaseTheory
Starting work on README.md
README.md                                                                                                  OK
ml_monad_translatorBaseTheory                                                                              OK
Starting work on ml_monad_translatorTheory
Starting work on ml_monadStoreTheory
ml_monadStoreTheory                                                                                        OK
ml_monad_translatorTheory                                                                         FAILED! <1>
     EvalM ro env st (Var (Short fname)) (ArrowM ro H (PURE (Eq a n)) b f) H
 
 failed.
 Failed to prove theorem EvalM_Recclosure_ALT.
 
 Exception raised at Tactical.FIRST_ASSUM:
 
 error in quse /home/myreen/regression/cakeml-997/translator/monadic/ml_monad_translatorScript.sml : HOL_ERR {message = "", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}
 error in load ml_monad_translatorScript : HOL_ERR {message = "", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}
 Uncaught exception: HOL_ERR {message = "", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}