Overview

Job 167

CakeML:f3431d1f462c0007fcb30eb522025c633a99737d
  Finish inserting the register allocator in the bootstrap
#439 (monad-cleanup)
Merging into:f8dd05aea6320bbd612745b9edc67b48646124a3
  Update diffTheory to use mlnumTheory
HOL:8da85ad615f3f14a7db120e68d75138b6101bedb
  holyhammer: fix error by matching the changes in hhsPredict
Machine:cakeml1797 4.4.0-22-generic x86_64 GNU/Linux

 Claimed job
 Building HOL
 Starting semantics/ffi
 Finished semantics/ffi                                         1m06s 339MB
 Starting semantics
 Finished semantics                                             2m34s   1GB
 Starting semantics/proofs
 Finished semantics/proofs                                      3m26s   1GB
 Starting basis/pure
 Finished basis/pure                                            6m11s 616MB
 Starting translator
 Finished translator                                            7m02s   1GB
 Starting compiler/parsing
 Finished compiler/parsing                                      2m24s   1GB
 Starting characteristic
 Finished characteristic                                        4m39s   1GB
 Starting basis
 Finished basis                                                29m38s   3GB
 Starting translator/monadic
 Finished translator/monadic                                    3m23s   1GB
 Starting compiler/inference
 Finished compiler/inference                                    2m47s   1GB
 Starting compiler/backend/reg_alloc
 Finished compiler/backend/reg_alloc                              46s 787MB
 Starting compiler/backend/gc
 Finished compiler/backend/gc                                  15m49s   2GB
 Starting compiler/backend
 Finished compiler/backend                                         2s  14MB
 Starting compiler/encoders/asm
 Finished compiler/encoders/asm                                    0s  11MB
 Starting compiler/encoders/x64
 Finished compiler/encoders/x64                                 1m39s 492MB
 Starting compiler/encoders/arm6
 Finished compiler/encoders/arm6                                2m57s   1GB
 Starting compiler/encoders/arm8
 Finished compiler/encoders/arm8                                  47s 402MB
 Starting compiler/encoders/mips
 Finished compiler/encoders/mips                                1m24s 754MB
 Starting compiler/encoders/riscv
 Finished compiler/encoders/riscv                               1m31s 521MB
 Starting compiler/backend/x64
 Finished compiler/backend/x64                                    42s   1GB
 Starting compiler/backend/arm6
 Finished compiler/backend/arm6                                   45s   1GB
 Starting compiler/backend/arm8
 Finished compiler/backend/arm8                                   40s   1GB
 Starting compiler/backend/mips
 Finished compiler/backend/mips                                   44s   1GB
 Starting compiler/backend/riscv
 Finished compiler/backend/riscv                                  43s   1GB
 Starting compiler/parsing/proofs
 Finished compiler/parsing/proofs                               4m42s 656MB
 Starting compiler/inference/proofs
 Finished compiler/inference/proofs                             4m16s   1GB
 Starting compiler/backend/semantics
 Finished compiler/backend/semantics                           18m58s   3GB
 Starting compiler/backend/reg_alloc/proofs
 Finished compiler/backend/reg_alloc/proofs                     1m14s 523MB
 Starting compiler/backend/proofs
 Finished compiler/backend/proofs                            1h08m10s   5GB
 Starting compiler/encoders/x64/proofs
 Finished compiler/encoders/x64/proofs                         13m12s   1GB
 Starting compiler/encoders/arm6/proofs
 Finished compiler/encoders/arm6/proofs                        13m22s   2GB
 Starting compiler/encoders/arm8/proofs
 Finished compiler/encoders/arm8/proofs                         9m09s   1GB
 Starting compiler/encoders/mips/proofs
 Finished compiler/encoders/mips/proofs                        12m33s   2GB
 Starting compiler/encoders/riscv/proofs
 Finished compiler/encoders/riscv/proofs                       13m41s   1GB
 Starting compiler/backend/x64/proofs
 Finished compiler/backend/x64/proofs                             52s   1GB
 Starting compiler/backend/arm6/proofs
 Finished compiler/backend/arm6/proofs                            54s   1GB
 Starting compiler/backend/arm8/proofs
 Finished compiler/backend/arm8/proofs                            51s   1GB
 Starting compiler/backend/mips/proofs
 Finished compiler/backend/mips/proofs                            52s   1GB
 Starting compiler/backend/riscv/proofs
 Finished compiler/backend/riscv/proofs                           51s   1GB
 Starting compiler/proofs
 Finished compiler/proofs                                       2m42s   2GB
 Starting candle/set-theory
 Finished candle/set-theory                                     1m38s 630MB
 Starting candle/syntax-lib
 Finished candle/syntax-lib                                       20s 377MB
 Starting candle/standard/syntax
 Finished candle/standard/syntax                                2m52s 941MB
 Starting candle/standard/semantics
 Finished candle/standard/semantics                             2m20s 792MB
 Starting candle/standard/monadic
 Finished candle/standard/monadic                               2m39s 853MB
 Starting candle/standard/ml_kernel
 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