Job 150

CakeML:0d7555f2d8090a54977129f12ce1893420b15ef9
  Update the monadic register translator translation [Jan 10 23:14:39]
#423 (monad-cleanup)
Merging into:d0fea5b543e219e955c6e5ebb0d47c0bb2ba6893
  Attempt to fix bootstrap proofs [Jan 11 20:08:11]
HOL:89cd819d8fb914b944915ca96d9161a6b2e134fb
  Canonicalise directory names better in Holmake [Jan 11 03:10:54]
Machine:cakeml1795 4.4.0-98-generic x86_64 GNU/Linux

Jan 11 21:46:52 Claimed job
Jan 11 21:47:02 Building HOL
Jan 11 21:59:35 Starting semantics/ffi
Jan 11 22:00:44 Finished semantics/ffi                                         1m06s 337MB
Jan 11 22:00:45 Starting semantics
Jan 11 22:03:20 Finished semantics                                             2m32s 907MB
Jan 11 22:03:22 Starting semantics/proofs
Jan 11 22:06:57 Finished semantics/proofs                                      3m32s 952MB
Jan 11 22:06:59 Starting basis/pure
Jan 11 22:13:01 Finished basis/pure                                            5m59s 698MB
Jan 11 22:13:03 Starting translator
Jan 11 22:20:19 Finished translator                                            7m14s   1GB
Jan 11 22:20:21 Starting compiler/parsing
Jan 11 22:22:49 Finished compiler/parsing                                      2m26s   1GB
Jan 11 22:22:51 Starting characteristic
Jan 11 22:27:32 Finished characteristic                                        4m39s   1GB
Jan 11 22:27:34 Starting basis
Jan 11 22:54:06 Finished basis                                                26m29s   2GB
Jan 11 22:54:08 Starting translator/monadic
Jan 11 22:57:36 Finished translator/monadic                                    3m25s   1GB
Jan 11 22:57:40 Starting compiler/inference
Jan 11 23:00:32 Finished compiler/inference                                    2m50s   1GB
Jan 11 23:00:34 Starting compiler/backend/reg_alloc
Jan 11 23:01:24 Finished compiler/backend/reg_alloc                              47s 774MB
Jan 11 23:01:26 Starting compiler/backend/gc
Jan 11 23:17:26 Finished compiler/backend/gc                                  15m57s   3GB
Jan 11 23:17:28 Starting compiler/backend
Jan 11 23:17:32 Finished compiler/backend                                         1s  16MB
Jan 11 23:17:34 Starting compiler/encoders/asm
Jan 11 23:17:36 Finished compiler/encoders/asm                                    0s  16MB
Jan 11 23:17:38 Starting compiler/encoders/x64
Jan 11 23:19:21 Finished compiler/encoders/x64                                 1m41s 519MB
Jan 11 23:19:23 Starting compiler/encoders/arm6
Jan 11 23:22:31 Finished compiler/encoders/arm6                                3m05s   1GB
Jan 11 23:22:33 Starting compiler/encoders/arm8
Jan 11 23:23:22 Finished compiler/encoders/arm8                                  47s 385MB
Jan 11 23:23:24 Starting compiler/encoders/mips
Jan 11 23:24:52 Finished compiler/encoders/mips                                1m26s 721MB
Jan 11 23:24:54 Starting compiler/encoders/riscv
Jan 11 23:26:27 Finished compiler/encoders/riscv                               1m30s 470MB
Jan 11 23:26:29 Starting compiler/backend/x64
Jan 11 23:27:11 Finished compiler/backend/x64                                    39s 866MB
Jan 11 23:27:13 Starting compiler/backend/arm6
Jan 11 23:27:59 Finished compiler/backend/arm6                                   44s   1GB
Jan 11 23:28:01 Starting compiler/backend/arm8
Jan 11 23:28:46 Finished compiler/backend/arm8                                   42s   1GB
Jan 11 23:28:48 Starting compiler/backend/mips
Jan 11 23:29:32 Finished compiler/backend/mips                                   42s 895MB
Jan 11 23:29:34 Starting compiler/backend/riscv
Jan 11 23:30:21 Finished compiler/backend/riscv                                  44s   1GB
Jan 11 23:30:23 Starting compiler/parsing/proofs
Jan 11 23:35:07 Finished compiler/parsing/proofs                               4m42s 676MB
Jan 11 23:35:08 Starting compiler/inference/proofs
Jan 11 23:39:29 Finished compiler/inference/proofs                             4m18s   1GB
Jan 11 23:39:31 Starting compiler/backend/semantics
Jan 11 23:58:35 Finished compiler/backend/semantics                           19m00s   3GB
Jan 11 23:58:37 Starting compiler/backend/reg_alloc/proofs
Jan 11 23:59:51 Finished compiler/backend/reg_alloc/proofs                     1m12s 485MB
Jan 11 23:59:53 Starting compiler/backend/proofs
Jan 12 01:09:24 Finished compiler/backend/proofs                            1h09m28s   3GB
Jan 12 01:09:26 Starting compiler/encoders/x64/proofs
Jan 12 01:22:47 Finished compiler/encoders/x64/proofs                         13m17s   2GB
Jan 12 01:22:49 Starting compiler/encoders/arm6/proofs
Jan 12 01:36:25 Finished compiler/encoders/arm6/proofs                        13m34s   2GB
Jan 12 01:36:27 Starting compiler/encoders/arm8/proofs
Jan 12 01:45:32 Finished compiler/encoders/arm8/proofs                         9m02s   1GB
Jan 12 01:45:34 Starting compiler/encoders/mips/proofs
Jan 12 01:58:19 Finished compiler/encoders/mips/proofs                        12m43s   2GB
Jan 12 01:58:21 Starting compiler/encoders/riscv/proofs
Jan 12 02:12:12 Finished compiler/encoders/riscv/proofs                       13m48s 847MB
Jan 12 02:12:14 Starting compiler/backend/x64/proofs
Jan 12 02:13:07 Finished compiler/backend/x64/proofs                             51s   1GB
Jan 12 02:13:09 Starting compiler/backend/arm6/proofs
Jan 12 02:14:06 Finished compiler/backend/arm6/proofs                            54s   1GB
Jan 12 02:14:08 Starting compiler/backend/arm8/proofs
Jan 12 02:14:59 Finished compiler/backend/arm8/proofs                            49s   1GB
Jan 12 02:15:01 Starting compiler/backend/mips/proofs
Jan 12 02:15:59 Finished compiler/backend/mips/proofs                            55s   1GB
Jan 12 02:16:01 Starting compiler/backend/riscv/proofs
Jan 12 02:16:55 Finished compiler/backend/riscv/proofs                           52s   1GB
Jan 12 02:16:57 Starting compiler/proofs
Jan 12 02:19:30 Finished compiler/proofs                                       2m30s   1GB
Jan 12 02:19:32 Starting candle/set-theory
Jan 12 02:21:13 Finished candle/set-theory                                     1m39s 553MB
Jan 12 02:21:15 Starting candle/syntax-lib
Jan 12 02:21:36 Finished candle/syntax-lib                                       19s 378MB
Jan 12 02:21:38 Starting candle/standard/syntax
Jan 12 02:24:39 Finished candle/standard/syntax                                2m58s 553MB
Jan 12 02:24:41 Starting candle/standard/semantics
Jan 12 02:27:06 Finished candle/standard/semantics                             2m22s 783MB
Jan 12 02:27:08 Starting candle/standard/monadic
Jan 12 02:29:50 Finished candle/standard/monadic                               2m40s   1GB
Jan 12 02:29:52 Starting candle/standard/ml_kernel
Jan 12 02:40:44 Finished candle/standard/ml_kernel                            10m48s   2GB
Jan 12 02:40:46 Starting candle/standard/opentheory
Jan 12 02:41:18 Finished candle/standard/opentheory                              30s 775MB
Jan 12 02:41:20 Starting characteristic/examples
Jan 12 02:43:35 Finished characteristic/examples                               2m12s   1GB
Jan 12 02:43:37 Starting tutorial/solutions
Jan 12 03:18:57 Finished tutorial/solutions                                   35m18s   8GB
Jan 12 03:18:59 Starting translator/monadic/examples
Jan 12 03:21:45 FAILED: translator/monadic/examples
]0;Holmake: ../../../characteristicRecursively calling Holmake in /scratch/cakeml/regression/HOL-89cd819d8fb914b944915ca96d9161a6b2e134fb/examples/machine-code/hoare-triple
]0;Holmake: /scratch/cakeml/regression/HOL-89cd819d8fb914b944915ca96d9161a6b2e134fb/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-89cd819d8fb914b944915ca96d9161a6b2e134fb/examples/machine-code/hoare-tripleFinished recursive invocation in /scratch/cakeml/regression/HOL-89cd819d8fb914b944915ca96d9161a6b2e134fb/examples/machine-code/hoare-triple
]0;Holmake: ../../../characteristicRecursively calling Holmake in ../../../basis/pure
]0;Holmake: ../../../basis/pureRecursively calling Holmake in /scratch/cakeml/regression/HOL-89cd819d8fb914b944915ca96d9161a6b2e134fb/examples/formal-languages/regular
]0;Holmake: /scratch/cakeml/regression/HOL-89cd819d8fb914b944915ca96d9161a6b2e134fb/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-89cd819d8fb914b944915ca96d9161a6b2e134fb/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-89cd819d8fb914b944915ca96d9161a6b2e134fb/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL-89cd819d8fb914b944915ca96d9161a6b2e134fb/examples/balanced_bstFinished recursive invocation in /scratch/cakeml/regression/HOL-89cd819d8fb914b944915ca96d9161a6b2e134fb/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-89cd819d8fb914b944915ca96d9161a6b2e134fb/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-89cd819d8fb914b944915ca96d9161a6b2e134fb/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-89cd819d8fb914b944915ca96d9161a6b2e134fb/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-89cd819d8fb914b944915ca96d9161a6b2e134fb/examples/formal-languagesFinished recursive invocation in /scratch/cakeml/regression/HOL-89cd819d8fb914b944915ca96d9161a6b2e134fb/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-89cd819d8fb914b944915ca96d9161a6b2e134fb/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-89cd819d8fb914b944915ca96d9161a6b2e134fb/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-89cd819d8fb914b944915ca96d9161a6b2e134fb/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/HOL-89cd819d8fb914b944915ca96d9161a6b2e134fb/examples/formal-languages/context-freeFinished recursive invocation in /scratch/cakeml/regression/HOL-89cd819d8fb914b944915ca96d9161a6b2e134fb/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-89cd819d8fb914b944915ca96d9161a6b2e134fb/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-89cd819d8fb914b944915ca96d9161a6b2e134fb/examples/formal-languages/regularFinished recursive invocation in /scratch/cakeml/regression/HOL-89cd819d8fb914b944915ca96d9161a6b2e134fb/examples/formal-languages/regular
]0;Holmake: ../../../basis/pureRecursively calling Holmake in ../../../misc
]0;Holmake: ../../../miscRecursively calling Holmake in /scratch/cakeml/regression/HOL-89cd819d8fb914b944915ca96d9161a6b2e134fb/examples/fun-op-sem/lprefix_lub
]0;Holmake: /scratch/cakeml/regression/HOL-89cd819d8fb914b944915ca96d9161a6b2e134fb/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-89cd819d8fb914b944915ca96d9161a6b2e134fb/examples/fun-op-sem/lprefix_lubFinished recursive invocation in /scratch/cakeml/regression/HOL-89cd819d8fb914b944915ca96d9161a6b2e134fb/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
runProgTheory                                                                OK
testAssumTheory                                                              OK
testPrecondProgTheory                                                        OK
testRunTheory                                                                OK