Job 885

CakeML:1694ad30b916ca2a059685b862eaa0cf965d4fe3
  Fix some broken proofs [May 20 05:34:31]
#635 (thm)
Merging into:c3cbbfd27bd9e1f2836f8f307279178dc76ac571
  Merge pull request #650 from CakeML/tweak-how-to [May 17 12:31:32]
HOL:f6c660ddb3151f18cd07b606f2439087858abe20
  Further polish Definition documentation (incl. schematic attribute) [May 16 14:38:46]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

May 20 06:41:06 Claimed job
May 20 06:41:09 Reusing HOL
May 20 06:41:13 Starting developers
May 20 06:41:14 Finished developers                                               0s  21MB
May 20 06:41:14 Starting developers/bin
May 20 06:41:17 Finished developers/bin                                           3s 144MB
May 20 06:41:18 Starting semantics/ffi
May 20 06:41:26 Finished semantics/ffi                                            7s 232MB
May 20 06:41:26 Starting semantics
May 20 06:42:42 Finished semantics                                             1m15s   1GB
May 20 06:42:42 Starting semantics/proofs
May 20 06:45:39 Finished semantics/proofs                                      2m55s   1GB
May 20 06:45:39 Starting basis/pure
May 20 06:46:23 Finished basis/pure                                              43s 674MB
May 20 06:46:23 Starting translator
May 20 06:48:00 Finished translator                                            1m36s   1GB
May 20 06:48:00 Starting compiler/parsing
May 20 06:48:58 Finished compiler/parsing                                        58s   2GB
May 20 06:48:58 Starting characteristic
May 20 06:54:04 Finished characteristic                                        5m05s   1GB
May 20 06:54:04 Starting translator/monadic
May 20 06:55:28 Finished translator/monadic                                    1m23s   1GB
May 20 06:55:28 Starting basis
May 20 07:12:16 Finished basis                                                16m48s   2GB
May 20 07:12:17 Starting compiler/inference
May 20 07:13:08 FAILED: compiler/inference
Starting work on commonUnifTheory
commonUnifTheory                                                                                           OK
]0;Holmake: ~/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/unification/triangular/first-order]0;Holmake: ~/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/unification/triangular/first-order[1mWorking in $(HOLDIR)/examples/unification/triangular/first-order[0m
Starting work on termTheory
termTheory                                                                                                 OK
Starting work on substTheory
substTheory                                                                                                OK
Starting work on walkTheory
walkTheory                                                                                                 OK
Starting work on walkstarTheory
walkstarTheory                                                                                             OK
Starting work on collapseTheory
Starting work on unifDefTheory
collapseTheory                                                                                             OK
unifDefTheory                                                                                              OK
Starting work on unifPropsTheory
unifPropsTheory                                                                                            OK
Starting work on redUnifTheory
redUnifTheory                                                                                              OK
]0;Holmake: .]0;Holmake: ~/regression/cakeml-885/basis/pure]0;Holmake: ~/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/balanced_bst]0;Holmake: ~/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: ~/regression/cakeml-885/basis/pure]0;Holmake: ~/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/formal-languages]0;Holmake: ~/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ~/regression/cakeml-885/basis/pure]0;Holmake: ~/regression/cakeml-885/misc]0;Holmake: ~/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-885/misc]0;Holmake: ~/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-f6c660ddb3151f18cd07b606f2439087858abe20/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/regression/cakeml-885/misc]0;Holmake: ~/regression/cakeml-885/developers]0;Holmake: ~/regression/cakeml-885/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-885/misc]0;Holmake: ~/regression/cakeml-885/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-885/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-885/misc]0;Holmake: ~/regression/cakeml-885/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression/cakeml-885/basis/pure]0;Holmake: ~/regression/cakeml-885/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-885/semantics]0;Holmake: ~/regression/cakeml-885/semantics/ffi]0;Holmake: ~/regression/cakeml-885/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-885/semantics]0;Holmake: ~/regression/cakeml-885/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-885/semantics/proofs]0;Holmake: ~/regression/cakeml-885/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/compiler/inference[0m
Starting work on infer_tTheory
infer_tTheory                                                                                              OK
Starting work on unifyTheory
unifyTheory                                                                                                OK
Starting work on inferTheory
inferTheory                                                                                       FAILED! <1>
 /home/myreen/regression/cakeml-885/compiler/inference/inferScript.sml:614: error: Value or constructor (constrain_op_pmatch) has not been declared
 Found near
   Theorem constrain_op_pmatch
   (
   [QUOTE " (*#loc 615 5*)\226\136\128op ts."] @
   (constrain_op_quotation |> map (fn ...)))
   (rpt strip_tac >> rpt (... ... >> every_case_tac) >> fs [constrain_op_def])
 error in quse /home/myreen/regression/cakeml-885/compiler/inference/inferScript.sml : Fail "Static Errors"
 error in load inferScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"