Job 1690

CakeML:59554731b54d37812555b75ecbfcb9185884ae1a
  Adjust for changes to quantHeuristicsTheory [Dec 17 21:20:41]
#850 (eval)
Merging into:ac6dd83f48ab211455fb85c60d3e20e212dc7b8a
  Remove some primes [Dec 12 21:27:55]
HOL:9511d2021f824ef967db312f1d1a41c58dbf7acb
  Fix a proof in face of automatic simp change in affbde85bd8 [Dec 16 05:35:31]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Dec 17 21:35:03 Claimed job
Dec 17 21:35:12 Reusing HOL
Dec 17 21:35:50 Starting developers
Dec 17 21:35:55 Finished developers                                               4s 105MB
Dec 17 21:35:55 Starting developers/bin
Dec 17 21:36:00 Finished developers/bin                                           5s 670MB
Dec 17 21:36:01 Starting semantics/ffi
Dec 17 21:36:09 Finished semantics/ffi                                            8s 211MB
Dec 17 21:36:10 Starting semantics
Dec 17 21:37:37 Finished semantics                                             1m27s   1GB
Dec 17 21:37:37 Starting semantics/proofs
Dec 17 21:41:21 Finished semantics/proofs                                      3m44s   1GB
Dec 17 21:41:22 Starting semantics/alt_semantics
Dec 17 21:41:33 Finished semantics/alt_semantics                                 11s 379MB
Dec 17 21:41:34 Starting semantics/alt_semantics/proofs
Dec 17 21:44:11 Finished semantics/alt_semantics/proofs                        2m37s 869MB
Dec 17 21:44:12 Starting basis/pure
Dec 17 21:45:04 Finished basis/pure                                              52s 844MB
Dec 17 21:45:04 Starting translator
Dec 17 21:48:00 Finished translator                                            2m56s   2GB
Dec 17 21:48:01 Starting compiler/parsing
Dec 17 21:49:21 Finished compiler/parsing                                      1m19s   2GB
Dec 17 21:49:21 Starting characteristic
Dec 17 21:55:16 Finished characteristic                                        5m54s   1GB
Dec 17 21:55:16 Starting translator/monadic
Dec 17 21:56:58 Finished translator/monadic                                    1m42s   1GB
Dec 17 21:56:58 Starting basis
Dec 17 22:46:00 Finished basis                                                49m01s  16GB
Dec 17 22:46:00 Starting compiler/inference
Dec 17 22:47:05 FAILED: compiler/inference
Scanning $(HOLDIR)/src/sort
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/quotient/src
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/examples/algorithms/unification/triangular
Scanning $(HOLDIR)/examples/algorithms/unification/triangular/first-order
Scanning $(HOLDIR)/examples/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/semantics/proofs
Starting work on commonUnifTheory
Starting work on README.md
Starting work on infer_tTheory
README.md                                       compiler/inference  (0s)     OK
commonUnifTheory        examples/algorithms/unification/triangular  (0s)     OK
Finished $(HOLDIR)/examples/algorithms/unification/triangular [#theories: 1] (0.598s) 
Starting work on termTheory
termTheory  examples/algorithms/unification/triangular/first-order  (0s)     OK
Starting work on substTheory
substTheory examples/algorithms/unification/triangular/first-order  (2s)     OK
Starting work on walkTheory
walkTheory  examples/algorithms/unification/triangular/first-order  (1s)     OK
Starting work on walkstarTheory
infer_tTheory                                   compiler/inference  (9s)     OK
walkstarTheory ...es/algorithms/unification/triangular/first-order  (1s)     OK
Starting work on collapseTheory
Starting work on unifDefTheory
collapseTheory ...es/algorithms/unification/triangular/first-order  (0s)     OK
unifDefTheory ...les/algorithms/unification/triangular/first-order  (3s)     OK
Starting work on unifPropsTheory
unifPropsTheory ...s/algorithms/unification/triangular/first-order  (3s)     OK
Finished $(HOLDIR)/examples/algorithms/unification/triangular/first-order [#theories: 7] (14.719s) 
Starting work on unifyTheory
unifyTheory                                     compiler/inference (16s)     OK
Starting work on inferTheory
inferTheory                                     compiler/inference (26s)FAIL<1>
 Saved definition ____ "constrain_op_def"
 <<HOL message: mk_functional: 
   pattern completion has added 64 clauses to the original specification.>>
 Saved theorem _______ "constrain_op_dtcase_def"
 error in quse /home/cake/oven/regression/cakeml-1690/compiler/inference/inferScript.sml : Fail "Static Errors"
 error in load /home/cake/oven/regression/cakeml-1690/compiler/inference/inferScript : Fail "Static Errors"
 Saved theorem _______ "st_ex_bind_failure"
 /home/cake/oven/regression/cakeml-1690/compiler/inference/inferScript.sml:575: error: Value or constructor (LIST_LENGTH_5) has not been declared in structure quantHeuristicsTheory
 Found near [quantHeuristicsTheory.LIST_LENGTH_5]
 Uncaught exception: Fail "Static Errors"