Job 4

CakeML:a580584f6755d3b703b68a58783047045206ff81
  Merge branch 'master' into term-not-eqtype [Nov 02 00:00:00]
#361 (term-not-eqtype)
Merging into:6d8819a319654ff1e3a9bbf6c6d7e3f96af265f3
  Move new regression test infrastructure [Nov 08 00:00:00]
HOL:adf95fed567e76641363a906871d9110e3d12f71
  Useful functions for dealing with terms up-to aconv [Nov 08 00:00:00]
Machine:cakeml1795 4.4.0-98-generic x86_64 GNU/Linux

Nov 09 07:24:07 Claimed job
Nov 09 07:37:17 Starting semantics/ffi
Nov 09 07:38:24 Finished semantics/ffi                                         1m06s   0kB
Nov 09 07:38:26 Starting semantics
Nov 09 07:41:10 Finished semantics                                             2m42s   0kB
Nov 09 07:41:11 Starting semantics/proofs
Nov 09 07:44:40 Finished semantics/proofs                                      3m27s   0kB
Nov 09 07:44:41 Starting basis/pure
Nov 09 07:50:47 Finished basis/pure                                            6m04s   0kB
Nov 09 07:50:49 Starting translator
Nov 09 07:57:59 Finished translator                                            7m08s   0kB
Nov 09 07:58:01 Starting compiler/parsing
Nov 09 08:00:27 Finished compiler/parsing                                      2m25s   0kB
Nov 09 08:00:29 Starting characteristic
Nov 09 08:05:08 Finished characteristic                                        4m37s   0kB
Nov 09 08:05:10 Starting basis
Nov 09 08:33:27 Finished basis                                                28m15s   0kB
Nov 09 08:33:28 Starting translator/monadic
Nov 09 08:37:04 Finished translator/monadic                                    3m34s   0kB
Nov 09 08:37:06 Starting compiler/inference
Nov 09 08:39:48 Finished compiler/inference                                    2m40s   0kB
Nov 09 08:39:50 Starting compiler/backend/reg_alloc
Nov 09 08:40:39 Finished compiler/backend/reg_alloc                              48s   0kB
Nov 09 08:40:41 Starting compiler/backend/gc
Nov 09 08:56:06 Finished compiler/backend/gc                                  15m24s   0kB
Nov 09 08:56:08 Starting compiler/backend
Nov 09 08:56:11 Finished compiler/backend                                         1s   0kB
Nov 09 08:56:13 Starting compiler/encoders/asm
Nov 09 08:56:35 Finished compiler/encoders/asm                                    0s   0kB
Nov 09 08:56:36 Starting compiler/encoders/x64
Nov 09 08:57:52 Finished compiler/encoders/x64                                 1m13s   0kB
Nov 09 08:57:53 Starting compiler/encoders/arm6
Nov 09 09:00:54 Finished compiler/encoders/arm6                                2m59s   0kB
Nov 09 09:00:56 Starting compiler/encoders/arm8
Nov 09 09:01:46 Finished compiler/encoders/arm8                                  48s   0kB
Nov 09 09:01:48 Starting compiler/encoders/mips
Nov 09 09:03:09 Finished compiler/encoders/mips                                1m20s   0kB
Nov 09 09:03:11 Starting compiler/encoders/riscv
Nov 09 09:04:47 Finished compiler/encoders/riscv                               1m34s   0kB
Nov 09 09:04:49 Starting compiler/backend/x64
Nov 09 09:05:31 Finished compiler/backend/x64                                    40s   0kB
Nov 09 09:05:32 Starting compiler/backend/arm6
Nov 09 09:06:20 Finished compiler/backend/arm6                                   45s   0kB
Nov 09 09:06:21 Starting compiler/backend/arm8
Nov 09 09:07:04 Finished compiler/backend/arm8                                   40s   0kB
Nov 09 09:07:05 Starting compiler/backend/mips
Nov 09 09:07:50 Finished compiler/backend/mips                                   43s   0kB
Nov 09 09:07:52 Starting compiler/backend/riscv
Nov 09 09:08:36 Finished compiler/backend/riscv                                  42s   0kB
Nov 09 09:08:38 Starting compiler/parsing/proofs
Nov 09 09:13:22 Finished compiler/parsing/proofs                               4m43s   0kB
Nov 09 09:13:24 Starting compiler/inference/proofs
Nov 09 09:17:38 Finished compiler/inference/proofs                             4m12s   0kB
Nov 09 09:17:39 Starting compiler/backend/semantics
Nov 09 09:36:19 Finished compiler/backend/semantics                           18m37s   0kB
Nov 09 09:36:21 Starting compiler/backend/reg_alloc/proofs
Nov 09 09:37:32 Finished compiler/backend/reg_alloc/proofs                     1m09s   0kB
Nov 09 09:37:33 Starting compiler/backend/proofs
Nov 09 10:47:35 Finished compiler/backend/proofs                            1h10m00s   0kB
Nov 09 10:47:37 Starting compiler/encoders/x64/proofs
Nov 09 10:59:10 Finished compiler/encoders/x64/proofs                         11m30s   0kB
Nov 09 10:59:11 Starting compiler/encoders/arm6/proofs
Nov 09 11:13:06 Finished compiler/encoders/arm6/proofs                        13m52s   0kB
Nov 09 11:13:07 Starting compiler/encoders/arm8/proofs
Nov 09 11:22:29 Finished compiler/encoders/arm8/proofs                         9m20s   0kB
Nov 09 11:22:31 Starting compiler/encoders/mips/proofs
Nov 09 11:35:37 Finished compiler/encoders/mips/proofs                        13m04s   0kB
Nov 09 11:35:39 Starting compiler/encoders/riscv/proofs
Nov 09 11:49:31 Finished compiler/encoders/riscv/proofs                       13m50s   0kB
Nov 09 11:49:32 Starting compiler/backend/x64/proofs
Nov 09 11:50:26 Finished compiler/backend/x64/proofs                             51s   0kB
Nov 09 11:50:27 Starting compiler/backend/arm6/proofs
Nov 09 11:51:24 Finished compiler/backend/arm6/proofs                            55s   0kB
Nov 09 11:51:26 Starting compiler/backend/arm8/proofs
Nov 09 11:52:19 Finished compiler/backend/arm8/proofs                            51s   0kB
Nov 09 11:52:20 Starting compiler/backend/mips/proofs
Nov 09 11:53:14 Finished compiler/backend/mips/proofs                            52s   0kB
Nov 09 11:53:16 Starting compiler/backend/riscv/proofs
Nov 09 11:54:10 Finished compiler/backend/riscv/proofs                           52s   0kB
Nov 09 11:54:11 Starting compiler/proofs
Nov 09 11:55:52 Finished compiler/proofs                                       1m38s   0kB
Nov 09 11:55:53 Starting candle/set-theory
Nov 09 11:57:52 Finished candle/set-theory                                     1m37s   0kB
Nov 09 11:57:54 Starting candle/syntax-lib
Nov 09 11:58:14 Finished candle/syntax-lib                                       18s   0kB
Nov 09 11:58:16 Starting candle/standard/syntax
Nov 09 12:01:19 Finished candle/standard/syntax                                3m01s   0kB
Nov 09 12:01:20 Starting candle/standard/semantics
Nov 09 12:03:43 Finished candle/standard/semantics                             2m20s   0kB
Nov 09 12:03:44 Starting candle/standard/monadic
Nov 09 12:06:26 Finished candle/standard/monadic                               2m40s   0kB
Nov 09 12:06:27 Starting candle/standard/ml_kernel
Nov 09 12:07:24 FAILED: candle/standard/ml_kernel
]0;Holmake: ../../../basisRecursively calling Holmake in ../../../basis/pure
]0;Holmake: ../../../basis/pureRecursively calling Holmake in /scratch/cakeml/worker/HOL/examples/formal-languages/regular
]0;Holmake: /scratch/cakeml/worker/HOL/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/worker/HOL/examples/balanced_bst
]0;Holmake: /scratch/cakeml/worker/HOL/examples/balanced_bst]0;Holmake: /scratch/cakeml/worker/HOL/examples/balanced_bstFinished recursive invocation in /scratch/cakeml/worker/HOL/examples/balanced_bst
]0;Holmake: /scratch/cakeml/worker/HOL/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/worker/HOL/examples/formal-languages
]0;Holmake: /scratch/cakeml/worker/HOL/examples/formal-languages]0;Holmake: /scratch/cakeml/worker/HOL/examples/formal-languagesFinished recursive invocation in /scratch/cakeml/worker/HOL/examples/formal-languages
]0;Holmake: /scratch/cakeml/worker/HOL/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/worker/HOL/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/worker/HOL/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/worker/HOL/examples/formal-languages/context-freeFinished recursive invocation in /scratch/cakeml/worker/HOL/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/worker/HOL/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/worker/HOL/examples/formal-languages/regularFinished recursive invocation in /scratch/cakeml/worker/HOL/examples/formal-languages/regular
]0;Holmake: ../../../basis/pureRecursively calling Holmake in ../../../misc
]0;Holmake: ../../../miscRecursively calling Holmake in /scratch/cakeml/worker/HOL/examples/fun-op-sem/lprefix_lub
]0;Holmake: /scratch/cakeml/worker/HOL/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/worker/HOL/examples/fun-op-sem/lprefix_lubFinished recursive invocation in /scratch/cakeml/worker/HOL/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../../../miscRecursively calling Holmake in /scratch/cakeml/worker/HOL/examples/machine-code/hoare-triple
]0;Holmake: /scratch/cakeml/worker/HOL/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/worker/HOL/examples/machine-code/hoare-tripleFinished recursive invocation in /scratch/cakeml/worker/HOL/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: ../../../basisRecursively calling Holmake in ../../../characteristic
]0;Holmake: ../../../characteristicRecursively calling Holmake in ../../../compiler/parsing
]0;Holmake: ../../../compiler/parsingRecursively 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: ../../../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/proofsRecursively calling Holmake in ../../../semantics/proofs
]0;Holmake: ../../../semantics/proofs]0;Holmake: ../../../semantics/proofsFinished recursive invocation in ../../../semantics/proofs
]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: ../../../basis]0;Holmake: ../../../basisFinished recursive invocation in ../../../basis
]0;Holmake: .Recursively calling Holmake in ../monadic
]0;Holmake: ../monadicRecursively calling Holmake in ../syntax
]0;Holmake: ../syntaxRecursively calling Holmake in ../../syntax-lib
]0;Holmake: ../../syntax-lib]0;Holmake: ../../syntax-libFinished recursive invocation in ../../syntax-lib
]0;Holmake: ../syntax]0;Holmake: ../syntaxFinished recursive invocation in ../syntax
]0;Holmake: ../monadicRecursively calling Holmake in ../../../translator/monadic
]0;Holmake: ../../../translator/monadic]0;Holmake: ../../../translator/monadicFinished recursive invocation in ../../../translator/monadic
]0;Holmake: ../monadic]0;Holmake: ../monadicFinished recursive invocation in ../monadic
]0;Holmake: .]0;Holmake: .Starting work on heap
heap                                                                         OK
Starting work on ml_hol_kernelProgTheory
ml_hol_kernelProgTheory                                             FAILED! <1>
 /scratch/cakeml/worker/cakeml/characteristic/cfLetAutoLib.sml:721: warning: Pattern is not exhaustive. Found near val [t2, _] = dest_type t' |> snd
 /scratch/cakeml/worker/cakeml/characteristic/cfLetAutoLib.sml:1250: warning: Pattern is not exhaustive. Found near val [{redex = _, residue = ...}] = ts
 /scratch/cakeml/worker/cakeml/characteristic/cfLetAutoLib.sml:1601: warning: Pattern is not exhaustive.
 Found near val [con_name, con_args] = let_expr_args
 /scratch/cakeml/worker/cakeml/translator/monadic/ml_monad_translatorLib.sml:1733: error: Value or constructor (diff) has not been declared
 Found near diff (free_vars tm) all_pre_vars
 error in quse /scratch/cakeml/worker/cakeml/translator/monadic/ml_monad_translatorLib.sml : Fail "Static Errors"
 error in load $(CAKEMLDIR)/translator/monadic/ml_monad_translatorLib : Fail "Static Errors"
 error in load ml_hol_kernelProgScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"