Job 709

CakeML:01444fe36cb917d1f0d64a94cf521fd86435a181
  Also update mlton-derived CakeML benchmarks for new datatype syntax [Jan 31 10:28:34]
#613 (gh611)
Merging into:be8c718bd26f8f7df6310ab4c48d33c300c1d23a
  Merge pull request #612 from CakeML/cleanup [Jan 28 07:33:16]
HOL:e53c040a60b6ad258c99b0887434bda862eb81a8
  Build sequences must have src/finite_maps before src/integer [Jan 31 01:43:52]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Jan 31 10:39:45 Claimed job
Jan 31 10:39:49 Reusing HOL
Jan 31 10:40:03 Starting developers
Jan 31 10:40:04 Finished developers                                               0s  21MB
Jan 31 10:40:05 Starting developers/bin
Jan 31 10:40:40 Finished developers/bin                                          34s 142MB
Jan 31 10:40:41 Starting semantics/ffi
Jan 31 10:40:50 Finished semantics/ffi                                            7s 226MB
Jan 31 10:40:51 Starting semantics
Jan 31 10:42:08 Finished semantics                                             1m17s   1GB
Jan 31 10:42:09 Starting semantics/proofs
Jan 31 10:45:20 Finished semantics/proofs                                      3m10s   1GB
Jan 31 10:45:21 Starting basis/pure
Jan 31 10:46:06 Finished basis/pure                                              44s 714MB
Jan 31 10:46:07 Starting translator
Jan 31 10:47:45 Finished translator                                            1m37s   1GB
Jan 31 10:47:46 Starting compiler/parsing
Jan 31 10:48:44 Finished compiler/parsing                                        56s   2GB
Jan 31 10:48:44 Starting characteristic
Jan 31 10:53:02 Finished characteristic                                        4m16s   1GB
Jan 31 10:53:03 Starting translator/monadic
Jan 31 10:54:29 Finished translator/monadic                                    1m25s   1GB
Jan 31 10:54:30 Starting basis
Jan 31 11:10:44 Finished basis                                                16m13s   3GB
Jan 31 11:10:45 Starting compiler/inference
Jan 31 11:11:24 FAILED: compiler/inference
]0;Holmake: ~/regression/HOL-e53c040a60b6ad258c99b0887434bda862eb81a8/examples/unification/triangular/first-order]0;Holmake: ~/regression/HOL-e53c040a60b6ad258c99b0887434bda862eb81a8/examples/unification/triangular/first-order[1mWorking in $(HOLDIR)/examples/unification/triangular/first-order[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-709/basis/pure]0;Holmake: ~/regression/HOL-e53c040a60b6ad258c99b0887434bda862eb81a8/examples/balanced_bst]0;Holmake: ~/regression/HOL-e53c040a60b6ad258c99b0887434bda862eb81a8/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: ~/regression/cakeml-709/basis/pure]0;Holmake: ~/regression/HOL-e53c040a60b6ad258c99b0887434bda862eb81a8/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-e53c040a60b6ad258c99b0887434bda862eb81a8/examples/formal-languages]0;Holmake: ~/regression/HOL-e53c040a60b6ad258c99b0887434bda862eb81a8/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-e53c040a60b6ad258c99b0887434bda862eb81a8/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-e53c040a60b6ad258c99b0887434bda862eb81a8/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-e53c040a60b6ad258c99b0887434bda862eb81a8/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-e53c040a60b6ad258c99b0887434bda862eb81a8/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-e53c040a60b6ad258c99b0887434bda862eb81a8/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ~/regression/cakeml-709/basis/pure]0;Holmake: ~/regression/cakeml-709/misc]0;Holmake: ~/regression/HOL-e53c040a60b6ad258c99b0887434bda862eb81a8/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-e53c040a60b6ad258c99b0887434bda862eb81a8/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-709/misc]0;Holmake: ~/regression/HOL-e53c040a60b6ad258c99b0887434bda862eb81a8/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-e53c040a60b6ad258c99b0887434bda862eb81a8/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/regression/cakeml-709/misc]0;Holmake: ~/regression/cakeml-709/developers]0;Holmake: ~/regression/cakeml-709/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-709/misc]0;Holmake: ~/regression/cakeml-709/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-709/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-709/misc]0;Holmake: ~/regression/cakeml-709/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression/cakeml-709/basis/pure]0;Holmake: ~/regression/cakeml-709/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-709/semantics]0;Holmake: ~/regression/cakeml-709/semantics/ffi]0;Holmake: ~/regression/cakeml-709/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-709/semantics]0;Holmake: ~/regression/cakeml-709/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-709/semantics/proofs]0;Holmake: ~/regression/cakeml-709/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/compiler/inference[0m
Starting work on infer_tTheory
Starting work on README.md
README.md                                           OK
infer_tTheory                                       OK
Starting work on unifyTheory
unifyTheory                                         OK
Starting work on inferTheory
inferTheory                                FAILED! <1>
          )) : thm
    Reason:
       Can't unify term frag list (*In Basis*) with
          thm (*Created from opaque signature*) (Different type constructors)
 Found near
   (fn q => fn tac => ... ...)
   (
   Q.prove
   ([... ...] @ (constrain_op_quotation |> ... ...), ... >> ... >> ... ...))
 Uncaught exception: Fail "Static Errors"