Job 167

CakeML:f3431d1f462c0007fcb30eb522025c633a99737d
  Finish inserting the register allocator in the bootstrap [Jan 20 12:39:24]
#439 (monad-cleanup)
Merging into:f8dd05aea6320bbd612745b9edc67b48646124a3
  Update diffTheory to use mlnumTheory [Jan 19 16:44:16]
HOL:8da85ad615f3f14a7db120e68d75138b6101bedb
  holyhammer: fix error by matching the changes in hhsPredict [Jan 18 23:08:13]
Machine:cakeml1797 4.4.0-22-generic x86_64 GNU/Linux

Jan 20 19:14:02 Claimed job
Jan 20 19:14:12 Building HOL
Jan 20 19:26:42 Starting semantics/ffi
Jan 20 19:27:50 Finished semantics/ffi                                         1m06s 339MB
Jan 20 19:27:52 Starting semantics
Jan 20 19:30:29 Finished semantics                                             2m34s   1GB
Jan 20 19:30:31 Starting semantics/proofs
Jan 20 19:33:59 Finished semantics/proofs                                      3m26s   1GB
Jan 20 19:34:01 Starting basis/pure
Jan 20 19:40:14 Finished basis/pure                                            6m11s 616MB
Jan 20 19:40:16 Starting translator
Jan 20 19:47:21 Finished translator                                            7m02s   1GB
Jan 20 19:47:23 Starting compiler/parsing
Jan 20 19:49:49 Finished compiler/parsing                                      2m24s   1GB
Jan 20 19:49:51 Starting characteristic
Jan 20 19:54:33 Finished characteristic                                        4m39s   1GB
Jan 20 19:54:35 Starting basis
Jan 20 20:24:15 Finished basis                                                29m38s   3GB
Jan 20 20:24:17 Starting translator/monadic
Jan 20 20:27:42 Finished translator/monadic                                    3m23s   1GB
Jan 20 20:27:44 Starting compiler/inference
Jan 20 20:30:33 Finished compiler/inference                                    2m47s   1GB
Jan 20 20:30:35 Starting compiler/backend/reg_alloc
Jan 20 20:31:24 Finished compiler/backend/reg_alloc                              46s 787MB
Jan 20 20:31:25 Starting compiler/backend/gc
Jan 20 20:47:17 Finished compiler/backend/gc                                  15m49s   2GB
Jan 20 20:47:19 Starting compiler/backend
Jan 20 20:47:23 Finished compiler/backend                                         2s  14MB
Jan 20 20:47:25 Starting compiler/encoders/asm
Jan 20 20:47:28 Finished compiler/encoders/asm                                    0s  11MB
Jan 20 20:47:30 Starting compiler/encoders/x64
Jan 20 20:49:11 Finished compiler/encoders/x64                                 1m39s 492MB
Jan 20 20:49:13 Starting compiler/encoders/arm6
Jan 20 20:52:13 Finished compiler/encoders/arm6                                2m57s   1GB
Jan 20 20:52:15 Starting compiler/encoders/arm8
Jan 20 20:53:04 Finished compiler/encoders/arm8                                  47s 402MB
Jan 20 20:53:06 Starting compiler/encoders/mips
Jan 20 20:54:33 Finished compiler/encoders/mips                                1m24s 754MB
Jan 20 20:54:35 Starting compiler/encoders/riscv
Jan 20 20:56:08 Finished compiler/encoders/riscv                               1m31s 521MB
Jan 20 20:56:10 Starting compiler/backend/x64
Jan 20 20:56:54 Finished compiler/backend/x64                                    42s   1GB
Jan 20 20:56:56 Starting compiler/backend/arm6
Jan 20 20:57:44 Finished compiler/backend/arm6                                   45s   1GB
Jan 20 20:57:45 Starting compiler/backend/arm8
Jan 20 20:58:28 Finished compiler/backend/arm8                                   40s   1GB
Jan 20 20:58:30 Starting compiler/backend/mips
Jan 20 20:59:16 Finished compiler/backend/mips                                   44s   1GB
Jan 20 20:59:18 Starting compiler/backend/riscv
Jan 20 21:00:04 Finished compiler/backend/riscv                                  43s   1GB
Jan 20 21:00:06 Starting compiler/parsing/proofs
Jan 20 21:04:50 Finished compiler/parsing/proofs                               4m42s 656MB
Jan 20 21:04:52 Starting compiler/inference/proofs
Jan 20 21:09:11 Finished compiler/inference/proofs                             4m16s   1GB
Jan 20 21:09:13 Starting compiler/backend/semantics
Jan 20 21:28:14 Finished compiler/backend/semantics                           18m58s   3GB
Jan 20 21:28:15 Starting compiler/backend/reg_alloc/proofs
Jan 20 21:29:32 Finished compiler/backend/reg_alloc/proofs                     1m14s 523MB
Jan 20 21:29:34 Starting compiler/backend/proofs
Jan 20 22:37:47 Finished compiler/backend/proofs                            1h08m10s   5GB
Jan 20 22:37:49 Starting compiler/encoders/x64/proofs
Jan 20 22:51:04 Finished compiler/encoders/x64/proofs                         13m12s   1GB
Jan 20 22:51:05 Starting compiler/encoders/arm6/proofs
Jan 20 23:04:30 Finished compiler/encoders/arm6/proofs                        13m22s   2GB
Jan 20 23:04:32 Starting compiler/encoders/arm8/proofs
Jan 20 23:13:43 Finished compiler/encoders/arm8/proofs                         9m09s   1GB
Jan 20 23:13:45 Starting compiler/encoders/mips/proofs
Jan 20 23:26:21 Finished compiler/encoders/mips/proofs                        12m33s   2GB
Jan 20 23:26:22 Starting compiler/encoders/riscv/proofs
Jan 20 23:40:06 Finished compiler/encoders/riscv/proofs                       13m41s   1GB
Jan 20 23:40:08 Starting compiler/backend/x64/proofs
Jan 20 23:41:02 Finished compiler/backend/x64/proofs                             52s   1GB
Jan 20 23:41:04 Starting compiler/backend/arm6/proofs
Jan 20 23:42:00 Finished compiler/backend/arm6/proofs                            54s   1GB
Jan 20 23:42:02 Starting compiler/backend/arm8/proofs
Jan 20 23:42:55 Finished compiler/backend/arm8/proofs                            51s   1GB
Jan 20 23:42:57 Starting compiler/backend/mips/proofs
Jan 20 23:43:52 Finished compiler/backend/mips/proofs                            52s   1GB
Jan 20 23:43:54 Starting compiler/backend/riscv/proofs
Jan 20 23:44:47 Finished compiler/backend/riscv/proofs                           51s   1GB
Jan 20 23:44:49 Starting compiler/proofs
Jan 20 23:47:34 Finished compiler/proofs                                       2m42s   2GB
Jan 20 23:47:36 Starting candle/set-theory
Jan 20 23:49:17 Finished candle/set-theory                                     1m38s 630MB
Jan 20 23:49:19 Starting candle/syntax-lib
Jan 20 23:49:41 Finished candle/syntax-lib                                       20s 377MB
Jan 20 23:49:43 Starting candle/standard/syntax
Jan 20 23:52:38 Finished candle/standard/syntax                                2m52s 941MB
Jan 20 23:52:40 Starting candle/standard/semantics
Jan 20 23:55:02 Finished candle/standard/semantics                             2m20s 792MB
Jan 20 23:55:04 Starting candle/standard/monadic
Jan 20 23:57:45 Finished candle/standard/monadic                               2m39s 853MB
Jan 20 23:57:47 Starting candle/standard/ml_kernel
Jan 21 00:08:34 FAILED: candle/standard/ml_kernel
]0;Holmake: ../../../basisRecursively calling Holmake in ../../../basis/pure
]0;Holmake: ../../../basis/pureRecursively calling Holmake in /scratch/cakeml/regression/HOL-8da85ad615f3f14a7db120e68d75138b6101bedb/examples/formal-languages/regular
]0;Holmake: /scratch/cakeml/regression/HOL-8da85ad615f3f14a7db120e68d75138b6101bedb/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-8da85ad615f3f14a7db120e68d75138b6101bedb/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-8da85ad615f3f14a7db120e68d75138b6101bedb/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL-8da85ad615f3f14a7db120e68d75138b6101bedb/examples/balanced_bstFinished recursive invocation in /scratch/cakeml/regression/HOL-8da85ad615f3f14a7db120e68d75138b6101bedb/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-8da85ad615f3f14a7db120e68d75138b6101bedb/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-8da85ad615f3f14a7db120e68d75138b6101bedb/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-8da85ad615f3f14a7db120e68d75138b6101bedb/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-8da85ad615f3f14a7db120e68d75138b6101bedb/examples/formal-languagesFinished recursive invocation in /scratch/cakeml/regression/HOL-8da85ad615f3f14a7db120e68d75138b6101bedb/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-8da85ad615f3f14a7db120e68d75138b6101bedb/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-8da85ad615f3f14a7db120e68d75138b6101bedb/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-8da85ad615f3f14a7db120e68d75138b6101bedb/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/HOL-8da85ad615f3f14a7db120e68d75138b6101bedb/examples/formal-languages/context-freeFinished recursive invocation in /scratch/cakeml/regression/HOL-8da85ad615f3f14a7db120e68d75138b6101bedb/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-8da85ad615f3f14a7db120e68d75138b6101bedb/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-8da85ad615f3f14a7db120e68d75138b6101bedb/examples/formal-languages/regularFinished recursive invocation in /scratch/cakeml/regression/HOL-8da85ad615f3f14a7db120e68d75138b6101bedb/examples/formal-languages/regular
]0;Holmake: ../../../basis/pureRecursively calling Holmake in ../../../misc
]0;Holmake: ../../../miscRecursively calling Holmake in /scratch/cakeml/regression/HOL-8da85ad615f3f14a7db120e68d75138b6101bedb/examples/fun-op-sem/lprefix_lub
]0;Holmake: /scratch/cakeml/regression/HOL-8da85ad615f3f14a7db120e68d75138b6101bedb/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-8da85ad615f3f14a7db120e68d75138b6101bedb/examples/fun-op-sem/lprefix_lubFinished recursive invocation in /scratch/cakeml/regression/HOL-8da85ad615f3f14a7db120e68d75138b6101bedb/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../../../miscRecursively calling Holmake in /scratch/cakeml/regression/HOL-8da85ad615f3f14a7db120e68d75138b6101bedb/examples/machine-code/hoare-triple
]0;Holmake: /scratch/cakeml/regression/HOL-8da85ad615f3f14a7db120e68d75138b6101bedb/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-8da85ad615f3f14a7db120e68d75138b6101bedb/examples/machine-code/hoare-tripleFinished recursive invocation in /scratch/cakeml/regression/HOL-8da85ad615f3f14a7db120e68d75138b6101bedb/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                                                      OK
Starting work on ml_hol_initTheory
Starting work on ppKernelTheory
ml_hol_initTheory                                                   FAILED! <1>
 Uncaught exception: HOL_ERR {message = "No parse for quotation (THEN1 on line 21)", origin_function = "Q_TAC", origin_structure = "Tactical"}
 Proof of 
 
 refs.
    p.
       (HOL_STORE refs * GC) (st2heap p (candle_init_state ffi)) 
       STATE init_ctxt refs
 
 failed.
 Failed to prove theorem kernel_init_thm.
ppKernelTheory                                                         M-KILLED