Overview

Job 707

CakeML:439765649dab969418d87f5592e9091a52fa175e
  Remove SML style datatype declarations from grammar
#613 (gh611)
Merging into:be8c718bd26f8f7df6310ab4c48d33c300c1d23a
  Merge pull request #612 from CakeML/cleanup
HOL:e53c040a60b6ad258c99b0887434bda862eb81a8
  Build sequences must have src/finite_maps before src/integer
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

 Claimed job
 Building HOL
 Starting developers
 Finished developers                                               0s  22MB
 Starting developers/bin
 Finished developers/bin                                          35s 205MB
 Starting semantics/ffi
 Finished semantics/ffi                                           35s 420MB
 Starting semantics
 Finished semantics                                             1m46s   1GB
 Starting semantics/proofs
 Finished semantics/proofs                                      3m15s   1GB
 Starting basis/pure
 Finished basis/pure                                            3m30s 709MB
 Starting translator
 Finished translator                                            1m37s   1GB
 Starting compiler/parsing
 Finished compiler/parsing                                        57s   1GB
 Starting characteristic
 Finished characteristic                                        4m16s   1GB
 Starting translator/monadic
 Finished translator/monadic                                    1m27s   1GB
 Starting basis
 Finished basis                                                16m17s   3GB
 Starting compiler/inference
 FAILED: compiler/inference
Starting work on commonUnifTheory
commonUnifTheory                                                                                           OK
]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
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-707/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-707/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-707/basis/pure]0;Holmake: ~/regression/cakeml-707/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-707/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-707/misc]0;Holmake: ~/regression/cakeml-707/developers]0;Holmake: ~/regression/cakeml-707/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-707/misc]0;Holmake: ~/regression/cakeml-707/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-707/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-707/misc]0;Holmake: ~/regression/cakeml-707/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression/cakeml-707/basis/pure]0;Holmake: ~/regression/cakeml-707/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-707/semantics]0;Holmake: ~/regression/cakeml-707/semantics/ffi]0;Holmake: ~/regression/cakeml-707/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-707/semantics]0;Holmake: ~/regression/cakeml-707/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-707/semantics/proofs]0;Holmake: ~/regression/cakeml-707/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"