Job 25

CakeML:c39007a0c469723a21108451c9ee38aeaeba3565
  Merge remote-tracking branch 'origin/master' into command-line-args [Nov 14 20:41:58]
#378 (command-line-args)
Merging into:e5d595d044abadb371c203d374c6640296155a96
  Minor speedups for xcf and xfun_spec [Nov 15 03:26:12]
HOL:4e4687878257043b885bf696e614e85572e9fc6c
  Add oHD and oEL (option-valued) functions from CakeML [Nov 14 05:25:57]
Machine:cakeml1853 4.4.0-22-generic x86_64 GNU/Linux

Nov 15 07:38:41 Claimed job
Nov 15 07:39:03 Building HOL
Nov 15 07:52:00 Starting semantics/ffi
Nov 15 07:53:11 Finished semantics/ffi                                         1m08s 329MB
Nov 15 07:53:14 Starting semantics
Nov 15 07:56:03 Finished semantics                                             2m46s   1GB
Nov 15 07:56:06 Starting semantics/proofs
Nov 15 07:59:51 Finished semantics/proofs                                      3m41s 980MB
Nov 15 07:59:53 Starting basis/pure
Nov 15 08:06:11 Finished basis/pure                                            6m13s 636MB
Nov 15 08:06:13 Starting translator
Nov 15 08:13:40 Finished translator                                            7m23s   1GB
Nov 15 08:13:42 Starting compiler/parsing
Nov 15 08:16:17 Finished compiler/parsing                                      2m31s   1GB
Nov 15 08:16:19 Starting characteristic
Nov 15 08:21:17 Finished characteristic                                        4m54s   1GB
Nov 15 08:21:20 Starting basis
Nov 15 08:50:29 Finished basis                                                29m06s   2GB
Nov 15 08:50:32 Starting translator/monadic
Nov 15 08:54:26 Finished translator/monadic                                    3m51s   1GB
Nov 15 08:54:29 Starting compiler/inference
Nov 15 08:57:23 Finished compiler/inference                                    2m51s   1GB
Nov 15 08:57:26 Starting compiler/backend/reg_alloc
Nov 15 08:58:17 Finished compiler/backend/reg_alloc                              47s 709MB
Nov 15 08:58:19 Starting compiler/backend/gc
Nov 15 09:14:54 Finished compiler/backend/gc                                  16m31s   3GB
Nov 15 09:14:57 Starting compiler/backend
Nov 15 09:15:01 Finished compiler/backend                                         1s  20MB
Nov 15 09:15:04 Starting compiler/encoders/asm
Nov 15 09:15:07 Finished compiler/encoders/asm                                    0s  19MB
Nov 15 09:15:10 Starting compiler/encoders/x64
Nov 15 09:16:25 Finished compiler/encoders/x64                                 1m12s 394MB
Nov 15 09:16:28 Starting compiler/encoders/arm6
Nov 15 09:19:40 Finished compiler/encoders/arm6                                3m09s   1GB
Nov 15 09:19:43 Starting compiler/encoders/arm8
Nov 15 09:20:33 Finished compiler/encoders/arm8                                  47s 409MB
Nov 15 09:20:36 Starting compiler/encoders/mips
Nov 15 09:22:01 Finished compiler/encoders/mips                                1m22s 617MB
Nov 15 09:22:04 Starting compiler/encoders/riscv
Nov 15 09:23:39 Finished compiler/encoders/riscv                               1m32s 483MB
Nov 15 09:23:42 Starting compiler/backend/x64
Nov 15 09:24:29 Finished compiler/backend/x64                                    44s   1GB
Nov 15 09:24:32 Starting compiler/backend/arm6
Nov 15 09:25:22 Finished compiler/backend/arm6                                   48s   1GB
Nov 15 09:25:25 Starting compiler/backend/arm8
Nov 15 09:26:11 Finished compiler/backend/arm8                                   43s   1GB
Nov 15 09:26:14 Starting compiler/backend/mips
Nov 15 09:27:00 Finished compiler/backend/mips                                   43s 906MB
Nov 15 09:27:03 Starting compiler/backend/riscv
Nov 15 09:27:48 Finished compiler/backend/riscv                                  42s 968MB
Nov 15 09:27:50 Starting compiler/parsing/proofs
Nov 15 09:32:58 Finished compiler/parsing/proofs                               5m06s 584MB
Nov 15 09:32:59 Starting compiler/inference/proofs
Nov 15 09:37:31 Finished compiler/inference/proofs                             4m30s   1GB
Nov 15 09:37:33 Starting compiler/backend/semantics
Nov 15 09:57:21 Finished compiler/backend/semantics                           19m46s   3GB
Nov 15 09:57:22 Starting compiler/backend/reg_alloc/proofs
Nov 15 09:58:35 Finished compiler/backend/reg_alloc/proofs                     1m11s 402MB
Nov 15 09:58:37 Starting compiler/backend/proofs
Nov 15 11:14:40 Finished compiler/backend/proofs                            1h16m01s   4GB
Nov 15 11:14:42 Starting compiler/encoders/x64/proofs
Nov 15 11:27:00 Finished compiler/encoders/x64/proofs                         12m16s   1GB
Nov 15 11:27:02 Starting compiler/encoders/arm6/proofs
Nov 15 11:41:23 Finished compiler/encoders/arm6/proofs                        14m19s   3GB
Nov 15 11:41:44 Starting compiler/encoders/arm8/proofs
Nov 15 11:51:48 Finished compiler/encoders/arm8/proofs                        10m01s   1GB
Nov 15 11:51:49 Starting compiler/encoders/mips/proofs
Nov 15 12:05:40 Finished compiler/encoders/mips/proofs                        13m49s   1GB
Nov 15 12:05:42 Starting compiler/encoders/riscv/proofs
Nov 15 12:20:29 Finished compiler/encoders/riscv/proofs                       14m45s 998MB
Nov 15 12:20:30 Starting compiler/backend/x64/proofs
Nov 15 12:21:27 Finished compiler/backend/x64/proofs                             55s   1GB
Nov 15 12:21:29 Starting compiler/backend/arm6/proofs
Nov 15 12:22:32 Finished compiler/backend/arm6/proofs                          1m01s   1GB
Nov 15 12:22:33 Starting compiler/backend/arm8/proofs
Nov 15 12:23:27 Finished compiler/backend/arm8/proofs                            52s   1GB
Nov 15 12:23:29 Starting compiler/backend/mips/proofs
Nov 15 12:24:25 Finished compiler/backend/mips/proofs                            54s   1GB
Nov 15 12:24:27 Starting compiler/backend/riscv/proofs
Nov 15 12:25:23 Finished compiler/backend/riscv/proofs                           54s   1GB
Nov 15 12:25:24 Starting compiler/proofs
Nov 15 12:27:12 Finished compiler/proofs                                       1m46s   1GB
Nov 15 12:27:13 Starting candle/set-theory
Nov 15 12:28:56 Finished candle/set-theory                                     1m41s 556MB
Nov 15 12:28:58 Starting candle/syntax-lib
Nov 15 12:29:20 Finished candle/syntax-lib                                       20s 363MB
Nov 15 12:29:22 Starting candle/standard/syntax
Nov 15 12:32:31 Finished candle/standard/syntax                                3m07s 606MB
Nov 15 12:32:33 Starting candle/standard/semantics
Nov 15 12:35:07 Finished candle/standard/semantics                             2m32s 929MB
Nov 15 12:35:08 Starting candle/standard/monadic
Nov 15 12:38:03 Finished candle/standard/monadic                               2m53s 887MB
Nov 15 12:38:05 Starting candle/standard/ml_kernel
Nov 15 12:39:16 FAILED: candle/standard/ml_kernel
]0;Holmake: ../../../basisRecursively calling Holmake in ../../../basis/pure
]0;Holmake: ../../../basis/pureRecursively calling Holmake in /scratch/cakeml/regression/HOL/examples/formal-languages/regular
]0;Holmake: /scratch/cakeml/regression/HOL/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL/examples/balanced_bstFinished recursive invocation in /scratch/cakeml/regression/HOL/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL/examples/formal-languagesFinished recursive invocation in /scratch/cakeml/regression/HOL/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/HOL/examples/formal-languages/context-freeFinished recursive invocation in /scratch/cakeml/regression/HOL/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL/examples/formal-languages/regularFinished recursive invocation in /scratch/cakeml/regression/HOL/examples/formal-languages/regular
]0;Holmake: ../../../basis/pureRecursively calling Holmake in ../../../misc
]0;Holmake: ../../../miscRecursively calling Holmake in /scratch/cakeml/regression/HOL/examples/fun-op-sem/lprefix_lub
]0;Holmake: /scratch/cakeml/regression/HOL/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL/examples/fun-op-sem/lprefix_lubFinished recursive invocation in /scratch/cakeml/regression/HOL/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../../../miscRecursively calling Holmake in /scratch/cakeml/regression/HOL/examples/machine-code/hoare-triple
]0;Holmake: /scratch/cakeml/regression/HOL/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL/examples/machine-code/hoare-tripleFinished recursive invocation in /scratch/cakeml/regression/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>
        {TypeExn (Long "Kernel" (Short "Fail"));
         TypeExn (Long "Kernel" (Short "Clash"));
         TypeId (... ... (... ... )); TypeId (... ... ); ... ... ; ... ;
         ... }; defined_mods :=  |>  init_type_constants_v = v 
    Loc (LENGTH init_type_constants_refs) = x) 
 evaluate F (merge_env auto_env_5 (merge_env auto_env_0 init_env))
   (auto_state_5 ffi) (App Opref [Var (Short "init_type_constants")])
   (s3,Rval x)
 
 failed.