Job 708

CakeML: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:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Jan 31 07:30:23 Claimed job
Jan 31 07:30:49 Building HOL
Jan 31 07:39:57 Starting developers
Jan 31 07:40:00 Finished developers                                               2s  20MB
Jan 31 07:40:00 Starting developers/bin
Jan 31 07:41:13 Finished developers/bin                                        1m12s 918MB
Jan 31 07:41:14 Starting semantics/ffi
Jan 31 07:41:53 Finished semantics/ffi                                           37s 382MB
Jan 31 07:41:53 Starting semantics
Jan 31 07:43:28 Finished semantics                                             1m34s 915MB
Jan 31 07:43:29 Starting semantics/proofs
Jan 31 07:46:37 Finished semantics/proofs                                      3m07s 953MB
Jan 31 07:46:38 Starting basis/pure
Jan 31 07:50:11 Finished basis/pure                                            3m32s 619MB
Jan 31 07:50:12 Starting translator
Jan 31 07:51:52 Finished translator                                            1m39s   1GB
Jan 31 07:51:53 Starting compiler/parsing
Jan 31 07:52:51 Finished compiler/parsing                                        57s   1GB
Jan 31 07:52:52 Starting characteristic
Jan 31 07:57:11 Finished characteristic                                        4m18s   1GB
Jan 31 07:57:12 Starting translator/monadic
Jan 31 07:58:40 Finished translator/monadic                                    1m27s   1GB
Jan 31 07:58:41 Starting basis
Jan 31 08:14:59 Finished basis                                                16m15s   3GB
Jan 31 08:14:59 Starting compiler/inference
Jan 31 08:15:57 FAILED: compiler/inference
Starting work on commonUnifTheory
commonUnifTheory                                                             OK
]0;Holmake: ~/oven/regression/HOL-e53c040a60b6ad258c99b0887434bda862eb81a8/examples/unification/triangular/first-order]0;Holmake: ~/oven/regression/HOL-e53c040a60b6ad258c99b0887434bda862eb81a8/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: ~/oven/regression/cakeml-708/basis/pure]0;Holmake: ~/oven/regression/HOL-e53c040a60b6ad258c99b0887434bda862eb81a8/examples/balanced_bst]0;Holmake: ~/oven/regression/HOL-e53c040a60b6ad258c99b0887434bda862eb81a8/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: ~/oven/regression/cakeml-708/basis/pure]0;Holmake: ~/oven/regression/HOL-e53c040a60b6ad258c99b0887434bda862eb81a8/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-e53c040a60b6ad258c99b0887434bda862eb81a8/examples/formal-languages]0;Holmake: ~/oven/regression/HOL-e53c040a60b6ad258c99b0887434bda862eb81a8/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/oven/regression/HOL-e53c040a60b6ad258c99b0887434bda862eb81a8/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-e53c040a60b6ad258c99b0887434bda862eb81a8/examples/formal-languages/context-free]0;Holmake: ~/oven/regression/HOL-e53c040a60b6ad258c99b0887434bda862eb81a8/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/oven/regression/HOL-e53c040a60b6ad258c99b0887434bda862eb81a8/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-e53c040a60b6ad258c99b0887434bda862eb81a8/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ~/oven/regression/cakeml-708/basis/pure]0;Holmake: ~/oven/regression/cakeml-708/misc]0;Holmake: ~/oven/regression/HOL-e53c040a60b6ad258c99b0887434bda862eb81a8/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/oven/regression/HOL-e53c040a60b6ad258c99b0887434bda862eb81a8/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/oven/regression/cakeml-708/misc]0;Holmake: ~/oven/regression/HOL-e53c040a60b6ad258c99b0887434bda862eb81a8/examples/machine-code/hoare-triple]0;Holmake: ~/oven/regression/HOL-e53c040a60b6ad258c99b0887434bda862eb81a8/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/oven/regression/cakeml-708/misc]0;Holmake: ~/oven/regression/cakeml-708/developers]0;Holmake: ~/oven/regression/cakeml-708/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/oven/regression/cakeml-708/misc]0;Holmake: ~/oven/regression/cakeml-708/misc/lem_lib_stub]0;Holmake: ~/oven/regression/cakeml-708/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/oven/regression/cakeml-708/misc]0;Holmake: ~/oven/regression/cakeml-708/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/oven/regression/cakeml-708/basis/pure]0;Holmake: ~/oven/regression/cakeml-708/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: .]0;Holmake: ~/oven/regression/cakeml-708/semantics]0;Holmake: ~/oven/regression/cakeml-708/semantics/ffi]0;Holmake: ~/oven/regression/cakeml-708/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/oven/regression/cakeml-708/semantics]0;Holmake: ~/oven/regression/cakeml-708/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: .]0;Holmake: ~/oven/regression/cakeml-708/semantics/proofs]0;Holmake: ~/oven/regression/cakeml-708/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"