Job 240

CakeML:9a2655f7735aa23d019b7517664f3e2d9eec707e
  Merge remote-tracking branch 'origin/master' into drule-revised [Feb 23 02:21:15]
#463 (drule-revised)
Merging into:78a58694402dc04c3291458d9c91eb1daef723d7
  Again move preamble to be last open [Feb 24 05:25:10]
HOL:bb8718e25c79755dfae141521dc625be831d4a40
  tactictoe: evaluation warnings [Feb 23 08:18:45]
Machine:cakeml1797 4.4.0-22-generic x86_64 GNU/Linux

Feb 24 11:28:36 Claimed job
Feb 24 11:28:42 Reusing HOL
Feb 24 11:28:55 Starting semantics/ffi
Feb 24 11:29:16 Finished semantics/ffi                                           19s 249MB
Feb 24 11:29:18 Starting semantics
Feb 24 11:31:29 Finished semantics                                             2m08s 966MB
Feb 24 11:31:30 Starting semantics/proofs
Feb 24 11:35:00 Finished semantics/proofs                                      3m27s 963MB
Feb 24 11:35:02 Starting basis/pure
Feb 24 11:36:26 Finished basis/pure                                            1m22s 772MB
Feb 24 11:36:28 Starting translator
Feb 24 11:43:31 Finished translator                                            7m01s   1GB
Feb 24 11:43:33 Starting compiler/parsing
Feb 24 11:45:55 Finished compiler/parsing                                      2m20s   2GB
Feb 24 11:45:58 Starting characteristic
Feb 24 11:50:39 Finished characteristic                                        4m38s   1GB
Feb 24 11:50:41 Starting basis
Feb 24 12:24:53 Finished basis                                                34m10s   3GB
Feb 24 12:24:55 Starting translator/monadic
Feb 24 12:24:58 Finished translator/monadic                                       1s  21MB
Feb 24 12:25:00 Starting compiler/inference
Feb 24 12:27:18 Finished compiler/inference                                    2m15s   1GB
Feb 24 12:27:20 Starting compiler/backend/reg_alloc
Feb 24 12:28:11 Finished compiler/backend/reg_alloc                              49s 843MB
Feb 24 12:28:13 Starting compiler/backend/gc
Feb 24 12:42:17 Finished compiler/backend/gc                                  14m02s   2GB
Feb 24 12:42:19 Starting compiler/backend
Feb 24 12:42:23 Finished compiler/backend                                         2s  16MB
Feb 24 12:42:25 Starting compiler/encoders/asm
Feb 24 12:42:28 Finished compiler/encoders/asm                                    0s  25MB
Feb 24 12:42:30 Starting compiler/encoders/x64
Feb 24 12:43:06 Finished compiler/encoders/x64                                   34s 505MB
Feb 24 12:43:08 Starting compiler/encoders/arm6
Feb 24 12:44:33 Finished compiler/encoders/arm6                                1m23s 499MB
Feb 24 12:44:35 Starting compiler/encoders/arm8
Feb 24 12:44:53 Finished compiler/encoders/arm8                                  16s 408MB
Feb 24 12:44:55 Starting compiler/encoders/mips
Feb 24 12:45:15 Finished compiler/encoders/mips                                  18s 457MB
Feb 24 12:45:17 Starting compiler/encoders/riscv
Feb 24 12:45:33 Finished compiler/encoders/riscv                                 13s 422MB
Feb 24 12:45:34 Starting compiler/backend/x64
Feb 24 12:46:20 Finished compiler/backend/x64                                    43s   1GB
Feb 24 12:46:22 Starting compiler/backend/arm6
Feb 24 12:47:09 Finished compiler/backend/arm6                                   45s   1GB
Feb 24 12:47:11 Starting compiler/backend/arm8
Feb 24 12:47:57 Finished compiler/backend/arm8                                   43s   1GB
Feb 24 12:47:59 Starting compiler/backend/mips
Feb 24 12:48:43 Finished compiler/backend/mips                                   42s   1GB
Feb 24 12:48:45 Starting compiler/backend/riscv
Feb 24 12:49:33 Finished compiler/backend/riscv                                  45s   1GB
Feb 24 12:49:34 Starting compiler/parsing/proofs
Feb 24 12:54:09 Finished compiler/parsing/proofs                               4m32s 759MB
Feb 24 12:54:11 Starting compiler/inference/proofs
Feb 24 12:55:02 FAILED: compiler/inference/proofs
]0;Holmake: ..Recursively calling Holmake in /scratch/cakeml/regression/HOL-bb8718e25c79755dfae141521dc625be831d4a40/examples/unification/triangular/first-order
]0;Holmake: /scratch/cakeml/regression/HOL-bb8718e25c79755dfae141521dc625be831d4a40/examples/unification/triangular/first-orderRecursively calling Holmake in /scratch/cakeml/regression/HOL-bb8718e25c79755dfae141521dc625be831d4a40/examples/unification/triangular
]0;Holmake: /scratch/cakeml/regression/HOL-bb8718e25c79755dfae141521dc625be831d4a40/examples/unification/triangular]0;Holmake: /scratch/cakeml/regression/HOL-bb8718e25c79755dfae141521dc625be831d4a40/examples/unification/triangularFinished recursive invocation in /scratch/cakeml/regression/HOL-bb8718e25c79755dfae141521dc625be831d4a40/examples/unification/triangular
]0;Holmake: /scratch/cakeml/regression/HOL-bb8718e25c79755dfae141521dc625be831d4a40/examples/unification/triangular/first-order]0;Holmake: /scratch/cakeml/regression/HOL-bb8718e25c79755dfae141521dc625be831d4a40/examples/unification/triangular/first-orderFinished recursive invocation in /scratch/cakeml/regression/HOL-bb8718e25c79755dfae141521dc625be831d4a40/examples/unification/triangular/first-order
]0;Holmake: ..Recursively calling Holmake in ../../../basis/pure
]0;Holmake: ../../../basis/pureRecursively calling Holmake in /scratch/cakeml/regression/HOL-bb8718e25c79755dfae141521dc625be831d4a40/examples/formal-languages/regular
]0;Holmake: /scratch/cakeml/regression/HOL-bb8718e25c79755dfae141521dc625be831d4a40/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-bb8718e25c79755dfae141521dc625be831d4a40/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-bb8718e25c79755dfae141521dc625be831d4a40/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL-bb8718e25c79755dfae141521dc625be831d4a40/examples/balanced_bstFinished recursive invocation in /scratch/cakeml/regression/HOL-bb8718e25c79755dfae141521dc625be831d4a40/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-bb8718e25c79755dfae141521dc625be831d4a40/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-bb8718e25c79755dfae141521dc625be831d4a40/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-bb8718e25c79755dfae141521dc625be831d4a40/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-bb8718e25c79755dfae141521dc625be831d4a40/examples/formal-languagesFinished recursive invocation in /scratch/cakeml/regression/HOL-bb8718e25c79755dfae141521dc625be831d4a40/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-bb8718e25c79755dfae141521dc625be831d4a40/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-bb8718e25c79755dfae141521dc625be831d4a40/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-bb8718e25c79755dfae141521dc625be831d4a40/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/HOL-bb8718e25c79755dfae141521dc625be831d4a40/examples/formal-languages/context-freeFinished recursive invocation in /scratch/cakeml/regression/HOL-bb8718e25c79755dfae141521dc625be831d4a40/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-bb8718e25c79755dfae141521dc625be831d4a40/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-bb8718e25c79755dfae141521dc625be831d4a40/examples/formal-languages/regularFinished recursive invocation in /scratch/cakeml/regression/HOL-bb8718e25c79755dfae141521dc625be831d4a40/examples/formal-languages/regular
]0;Holmake: ../../../basis/pureRecursively calling Holmake in ../../../misc
]0;Holmake: ../../../miscRecursively calling Holmake in /scratch/cakeml/regression/HOL-bb8718e25c79755dfae141521dc625be831d4a40/examples/fun-op-sem/lprefix_lub
]0;Holmake: /scratch/cakeml/regression/HOL-bb8718e25c79755dfae141521dc625be831d4a40/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-bb8718e25c79755dfae141521dc625be831d4a40/examples/fun-op-sem/lprefix_lubFinished recursive invocation in /scratch/cakeml/regression/HOL-bb8718e25c79755dfae141521dc625be831d4a40/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../../../miscRecursively calling Holmake in /scratch/cakeml/regression/HOL-bb8718e25c79755dfae141521dc625be831d4a40/examples/machine-code/hoare-triple
]0;Holmake: /scratch/cakeml/regression/HOL-bb8718e25c79755dfae141521dc625be831d4a40/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-bb8718e25c79755dfae141521dc625be831d4a40/examples/machine-code/hoare-tripleFinished recursive invocation in /scratch/cakeml/regression/HOL-bb8718e25c79755dfae141521dc625be831d4a40/examples/machine-code/hoare-triple
]0;Holmake: ../../../miscRecursively calling Holmake in ../../../developers
]0;Holmake: ../../../developers]0;Holmake: ../../../developersFinished recursive invocation in ../../../developers
]0;Holmake: ../../../miscRecursively calling Holmake in ../../../misc/lem_lib_stub
]0;Holmake: ../../../misc/lem_lib_stub]0;Holmake: ../../../misc/lem_lib_stubFinished recursive invocation in ../../../misc/lem_lib_stub
]0;Holmake: ../../../misc]0;Holmake: ../../../miscFinished recursive invocation in ../../../misc
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../basis/pureFinished recursive invocation in ../../../basis/pure
]0;Holmake: ..Recursively calling Holmake in ../../../semantics
]0;Holmake: ../../../semanticsRecursively calling Holmake in ../../../semantics/ffi
]0;Holmake: ../../../semantics/ffi]0;Holmake: ../../../semantics/ffiFinished recursive invocation in ../../../semantics/ffi
]0;Holmake: ../../../semantics]0;Holmake: ../../../semanticsFinished recursive invocation in ../../../semantics
]0;Holmake: ..Recursively calling Holmake in ../../../semantics/proofs
]0;Holmake: ../../../semantics/proofs]0;Holmake: ../../../semantics/proofsFinished recursive invocation in ../../../semantics/proofs
]0;Holmake: ..Recursively calling Holmake in ../../../translator/monadic
]0;Holmake: ../../../translator/monadicRecursively calling Holmake in ../../../characteristic
]0;Holmake: ../../../characteristicRecursively calling Holmake in ../../../compiler/parsing
]0;Holmake: ../../../compiler/parsing]0;Holmake: ../../../compiler/parsingFinished recursive invocation in ../../../compiler/parsing
]0;Holmake: ../../../characteristicRecursively calling Holmake in ../../../semantics/alt_semantics/proofs
]0;Holmake: ../../../semantics/alt_semantics/proofsRecursively calling Holmake in ../../../semantics/alt_semantics
]0;Holmake: ../../../semantics/alt_semantics]0;Holmake: ../../../semantics/alt_semanticsFinished recursive invocation in ../../../semantics/alt_semantics
]0;Holmake: ../../../semantics/alt_semantics/proofs]0;Holmake: ../../../semantics/alt_semantics/proofsFinished recursive invocation in ../../../semantics/alt_semantics/proofs
]0;Holmake: ../../../characteristicRecursively calling Holmake in ../../../translator
]0;Holmake: ../../../translator]0;Holmake: ../../../translatorFinished recursive invocation in ../../../translator
]0;Holmake: ../../../characteristic]0;Holmake: ../../../characteristicFinished recursive invocation in ../../../characteristic
]0;Holmake: ../../../translator/monadic]0;Holmake: ../../../translator/monadicFinished recursive invocation in ../../../translator/monadic
]0;Holmake: ..]0;Holmake: ..Finished recursive invocation in ..
]0;Holmake: .]0;Holmake: .Starting work on heap
heap                                                                         OK
Starting work on inferPropsTheory
inferPropsTheory                                                    FAILED! <1>
 Uncaught exception: HOL_ERR {message = "", origin_function = "DISCH_THEN", origin_structure = "Thm_cont"}
 Proof of 
 
 s.
    t_wfs s 
    t max_tvs uvs.
       check_t max_tvs uvs (t_walkstar s t) 
       check_t max_tvs (uvs  FDOM s) t
 
 failed.