Job 148

CakeML:0d7555f2d8090a54977129f12ce1893420b15ef9
  Update the monadic register translator translation [Jan 10 23:14:39]
#423 (monad-cleanup)
Merging into:7982b740eaa616bbfc1460d03f769fe720c02716
  Support large heap+stack on x64 [Jan 11 00:19:44]
HOL:a587378e2452022aca043c008a357e9ebd67ce79
  Make experimental kernel's term representation visible to Thm [Jan 10 23:00:07]
Machine:cakeml1794 4.4.0-98-generic x86_64 GNU/Linux

Jan 11 02:36:44 Claimed job
Jan 11 02:36:51 Building HOL
Jan 11 02:49:40 Starting semantics/ffi
Jan 11 02:50:51 Finished semantics/ffi                                         1m08s 427MB
Jan 11 02:50:53 Starting semantics
Jan 11 02:53:38 Finished semantics                                             2m43s   1GB
Jan 11 02:53:40 Starting semantics/proofs
Jan 11 02:57:20 Finished semantics/proofs                                      3m38s   1GB
Jan 11 02:57:22 Starting basis/pure
Jan 11 03:03:33 Finished basis/pure                                            6m08s 768MB
Jan 11 03:03:35 Starting translator
Jan 11 03:10:58 Finished translator                                            7m20s   1GB
Jan 11 03:11:00 Starting compiler/parsing
Jan 11 03:13:33 Finished compiler/parsing                                      2m30s   1GB
Jan 11 03:13:35 Starting characteristic
Jan 11 03:18:33 Finished characteristic                                        4m56s   1GB
Jan 11 03:18:35 Starting basis
Jan 11 03:46:10 Finished basis                                                27m32s   2GB
Jan 11 03:46:12 Starting translator/monadic
Jan 11 03:49:49 Finished translator/monadic                                    3m35s   1GB
Jan 11 03:49:51 Starting compiler/inference
Jan 11 03:52:48 Finished compiler/inference                                    2m55s   1GB
Jan 11 03:52:50 Starting compiler/backend/reg_alloc
Jan 11 03:53:43 Finished compiler/backend/reg_alloc                              50s 760MB
Jan 11 03:53:45 Starting compiler/backend/gc
Jan 11 04:10:37 Finished compiler/backend/gc                                  16m49s   2GB
Jan 11 04:10:39 Starting compiler/backend
Jan 11 04:10:43 Finished compiler/backend                                         1s  14MB
Jan 11 04:10:45 Starting compiler/encoders/asm
Jan 11 04:10:47 Finished compiler/encoders/asm                                    0s  26MB
Jan 11 04:10:49 Starting compiler/encoders/x64
Jan 11 04:12:31 Finished compiler/encoders/x64                                 1m39s 523MB
Jan 11 04:12:33 Starting compiler/encoders/arm6
Jan 11 04:15:41 Finished compiler/encoders/arm6                                3m05s   1GB
Jan 11 04:15:43 Starting compiler/encoders/arm8
Jan 11 04:16:31 Finished compiler/encoders/arm8                                  46s 418MB
Jan 11 04:16:33 Starting compiler/encoders/mips
Jan 11 04:18:05 Finished compiler/encoders/mips                                1m29s 598MB
Jan 11 04:18:07 Starting compiler/encoders/riscv
Jan 11 04:19:45 Finished compiler/encoders/riscv                               1m36s 507MB
Jan 11 04:19:46 Starting compiler/backend/x64
Jan 11 04:20:33 Finished compiler/backend/x64                                    44s   1GB
Jan 11 04:20:35 Starting compiler/backend/arm6
Jan 11 04:21:23 Finished compiler/backend/arm6                                   45s   1GB
Jan 11 04:21:25 Starting compiler/backend/arm8
Jan 11 04:22:12 Finished compiler/backend/arm8                                   44s   1GB
Jan 11 04:22:14 Starting compiler/backend/mips
Jan 11 04:23:01 Finished compiler/backend/mips                                   44s   1GB
Jan 11 04:23:03 Starting compiler/backend/riscv
Jan 11 04:23:48 Finished compiler/backend/riscv                                  42s   1GB
Jan 11 04:23:50 Starting compiler/parsing/proofs
Jan 11 04:28:54 Finished compiler/parsing/proofs                               5m02s 615MB
Jan 11 04:28:56 Starting compiler/inference/proofs
Jan 11 04:33:33 Finished compiler/inference/proofs                             4m34s   1GB
Jan 11 04:33:35 Starting compiler/backend/semantics
Jan 11 04:54:00 Finished compiler/backend/semantics                           20m22s   3GB
Jan 11 04:54:02 Starting compiler/backend/reg_alloc/proofs
Jan 11 04:55:23 Finished compiler/backend/reg_alloc/proofs                     1m19s 391MB
Jan 11 04:55:26 Starting compiler/backend/proofs
Jan 11 06:10:03 Finished compiler/backend/proofs                            1h14m35s   5GB
Jan 11 06:10:05 Starting compiler/encoders/x64/proofs
Jan 11 06:24:32 Finished compiler/encoders/x64/proofs                         14m24s   1GB
Jan 11 06:24:34 Starting compiler/encoders/arm6/proofs
Jan 11 06:38:45 Finished compiler/encoders/arm6/proofs                        14m08s   3GB
Jan 11 06:38:47 Starting compiler/encoders/arm8/proofs
Jan 11 06:48:47 Finished compiler/encoders/arm8/proofs                         9m57s   1GB
Jan 11 06:48:49 Starting compiler/encoders/mips/proofs
Jan 11 07:02:31 Finished compiler/encoders/mips/proofs                        13m40s   2GB
Jan 11 07:02:33 Starting compiler/encoders/riscv/proofs
Jan 11 07:17:22 Finished compiler/encoders/riscv/proofs                       14m47s   1GB
Jan 11 07:17:24 Starting compiler/backend/x64/proofs
Jan 11 07:18:23 Finished compiler/backend/x64/proofs                             56s   1GB
Jan 11 07:18:25 Starting compiler/backend/arm6/proofs
Jan 11 07:19:28 Finished compiler/backend/arm6/proofs                          1m00s   1GB
Jan 11 07:19:30 Starting compiler/backend/arm8/proofs
Jan 11 07:20:25 Finished compiler/backend/arm8/proofs                            52s   1GB
Jan 11 07:20:27 Starting compiler/backend/mips/proofs
Jan 11 07:21:25 Finished compiler/backend/mips/proofs                            56s   1GB
Jan 11 07:21:27 Starting compiler/backend/riscv/proofs
Jan 11 07:22:27 Finished compiler/backend/riscv/proofs                           57s   1GB
Jan 11 07:22:29 Starting compiler/proofs
Jan 11 07:25:24 Finished compiler/proofs                                       2m52s   1GB
Jan 11 07:25:26 Starting candle/set-theory
Jan 11 07:27:15 Finished candle/set-theory                                     1m47s 580MB
Jan 11 07:27:17 Starting candle/syntax-lib
Jan 11 07:27:39 Finished candle/syntax-lib                                       20s 409MB
Jan 11 07:27:41 Starting candle/standard/syntax
Jan 11 07:30:53 Finished candle/standard/syntax                                3m09s 629MB
Jan 11 07:30:55 Starting candle/standard/semantics
Jan 11 07:33:31 Finished candle/standard/semantics                             2m34s 715MB
Jan 11 07:33:33 Starting candle/standard/monadic
Jan 11 07:36:22 Finished candle/standard/monadic                               2m46s 868MB
Jan 11 07:36:24 Starting candle/standard/ml_kernel
Jan 11 07:47:59 Finished candle/standard/ml_kernel                            11m33s   2GB
Jan 11 07:48:01 Starting candle/standard/opentheory
Jan 11 07:48:35 Finished candle/standard/opentheory                              31s 793MB
Jan 11 07:48:37 Starting characteristic/examples
Jan 11 07:51:02 Finished characteristic/examples                               2m23s   1GB
Jan 11 07:51:04 Starting tutorial/solutions
Jan 11 08:27:42 Finished tutorial/solutions                                   36m35s   9GB
Jan 11 08:27:44 Starting translator/monadic/examples
Jan 11 08:30:33 FAILED: translator/monadic/examples
]0;Holmake: ../../../characteristicRecursively calling Holmake in /scratch/cakeml/regression/HOL-a587378e2452022aca043c008a357e9ebd67ce79/examples/machine-code/hoare-triple
]0;Holmake: /scratch/cakeml/regression/HOL-a587378e2452022aca043c008a357e9ebd67ce79/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-a587378e2452022aca043c008a357e9ebd67ce79/examples/machine-code/hoare-tripleFinished recursive invocation in /scratch/cakeml/regression/HOL-a587378e2452022aca043c008a357e9ebd67ce79/examples/machine-code/hoare-triple
]0;Holmake: ../../../characteristicRecursively calling Holmake in ../../../basis/pure
]0;Holmake: ../../../basis/pureRecursively calling Holmake in /scratch/cakeml/regression/HOL-a587378e2452022aca043c008a357e9ebd67ce79/examples/formal-languages/regular
]0;Holmake: /scratch/cakeml/regression/HOL-a587378e2452022aca043c008a357e9ebd67ce79/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-a587378e2452022aca043c008a357e9ebd67ce79/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-a587378e2452022aca043c008a357e9ebd67ce79/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL-a587378e2452022aca043c008a357e9ebd67ce79/examples/balanced_bstFinished recursive invocation in /scratch/cakeml/regression/HOL-a587378e2452022aca043c008a357e9ebd67ce79/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-a587378e2452022aca043c008a357e9ebd67ce79/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-a587378e2452022aca043c008a357e9ebd67ce79/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-a587378e2452022aca043c008a357e9ebd67ce79/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-a587378e2452022aca043c008a357e9ebd67ce79/examples/formal-languagesFinished recursive invocation in /scratch/cakeml/regression/HOL-a587378e2452022aca043c008a357e9ebd67ce79/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-a587378e2452022aca043c008a357e9ebd67ce79/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-a587378e2452022aca043c008a357e9ebd67ce79/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-a587378e2452022aca043c008a357e9ebd67ce79/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/HOL-a587378e2452022aca043c008a357e9ebd67ce79/examples/formal-languages/context-freeFinished recursive invocation in /scratch/cakeml/regression/HOL-a587378e2452022aca043c008a357e9ebd67ce79/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-a587378e2452022aca043c008a357e9ebd67ce79/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-a587378e2452022aca043c008a357e9ebd67ce79/examples/formal-languages/regularFinished recursive invocation in /scratch/cakeml/regression/HOL-a587378e2452022aca043c008a357e9ebd67ce79/examples/formal-languages/regular
]0;Holmake: ../../../basis/pureRecursively calling Holmake in ../../../misc
]0;Holmake: ../../../miscRecursively calling Holmake in /scratch/cakeml/regression/HOL-a587378e2452022aca043c008a357e9ebd67ce79/examples/fun-op-sem/lprefix_lub
]0;Holmake: /scratch/cakeml/regression/HOL-a587378e2452022aca043c008a357e9ebd67ce79/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-a587378e2452022aca043c008a357e9ebd67ce79/examples/fun-op-sem/lprefix_lubFinished recursive invocation in /scratch/cakeml/regression/HOL-a587378e2452022aca043c008a357e9ebd67ce79/examples/fun-op-sem/lprefix_lub
]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: ../../../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: .Recursively calling Holmake in ..
]0;Holmake: ..]0;Holmake: ..Finished recursive invocation in ..
]0;Holmake: .]0;Holmake: .Starting work on heap
heap                                                                         OK
Starting work on arrayGlobalStateProgTheory
Starting work on arrayLocalStateProgTheory
Starting work on exceptionProgTheory
Starting work on graphStateProgTheory
exceptionProgTheory                                                          OK
Starting work on refStateProgTheory
graphStateProgTheory                                                    CHEATED
Starting work on runProgTheory
arrayGlobalStateProgTheory                                                   OK
Starting work on testAssumTheory
refStateProgTheory                                                           OK
Starting work on testPrecondProgTheory
arrayLocalStateProgTheory                                                    OK
Starting work on testRunTheory
testAssumTheory                                                              OK
runProgTheory                                                                OK
testPrecondProgTheory                                                        OK
testRunTheory                                                                OK