Job 147

CakeML:3e697e7e7e2951daf19553246512275227a9f731
  Tidy up bootstrap translation in inferProg [Jan 10 03:02:37]
#423 (monad-cleanup)
Merging into:9fd5560b349e4f60ce88f761db376c356a7033eb
  Fix use before definition of HOLHEAP in Holmakefiles [Jan 10 00:44:06]
HOL:d6a10c713c9efa69f9361130a68b1d528c863cee
  Correctly record dependency for Thm.sig [Jan 10 11:23:35]
Machine:cakeml1794 4.4.0-98-generic x86_64 GNU/Linux

Jan 10 20:47:53 Claimed job
Jan 10 20:48:02 Building HOL
Jan 10 21:00:51 Starting semantics/ffi
Jan 10 21:01:59 Finished semantics/ffi                                         1m06s 397MB
Jan 10 21:02:01 Starting semantics
Jan 10 21:04:45 Finished semantics                                             2m41s   1GB
Jan 10 21:04:47 Starting semantics/proofs
Jan 10 21:08:31 Finished semantics/proofs                                      3m42s   1GB
Jan 10 21:08:33 Starting basis/pure
Jan 10 21:14:43 Finished basis/pure                                            6m08s 621MB
Jan 10 21:14:45 Starting translator
Jan 10 21:22:08 Finished translator                                            7m20s 889MB
Jan 10 21:22:10 Starting compiler/parsing
Jan 10 21:24:41 Finished compiler/parsing                                      2m29s   1GB
Jan 10 21:24:43 Starting characteristic
Jan 10 21:29:36 Finished characteristic                                        4m51s   1GB
Jan 10 21:29:38 Starting basis
Jan 10 21:56:49 Finished basis                                                27m09s   2GB
Jan 10 21:56:51 Starting translator/monadic
Jan 10 22:00:27 Finished translator/monadic                                    3m33s 996MB
Jan 10 22:00:29 Starting compiler/inference
Jan 10 22:03:24 Finished compiler/inference                                    2m53s   1GB
Jan 10 22:03:26 Starting compiler/backend/reg_alloc
Jan 10 22:04:18 Finished compiler/backend/reg_alloc                              49s 852MB
Jan 10 22:04:20 Starting compiler/backend/gc
Jan 10 22:20:52 Finished compiler/backend/gc                                  16m29s   2GB
Jan 10 22:20:54 Starting compiler/backend
Jan 10 22:20:57 Finished compiler/backend                                         1s  16MB
Jan 10 22:20:59 Starting compiler/encoders/asm
Jan 10 22:21:02 Finished compiler/encoders/asm                                    0s  19MB
Jan 10 22:21:04 Starting compiler/encoders/x64
Jan 10 22:22:45 Finished compiler/encoders/x64                                 1m39s 559MB
Jan 10 22:22:47 Starting compiler/encoders/arm6
Jan 10 22:25:58 Finished compiler/encoders/arm6                                3m09s   1GB
Jan 10 22:26:00 Starting compiler/encoders/arm8
Jan 10 22:26:50 Finished compiler/encoders/arm8                                  47s 463MB
Jan 10 22:26:51 Starting compiler/encoders/mips
Jan 10 22:28:21 Finished compiler/encoders/mips                                1m28s 828MB
Jan 10 22:28:23 Starting compiler/encoders/riscv
Jan 10 22:29:59 Finished compiler/encoders/riscv                               1m33s 451MB
Jan 10 22:30:01 Starting compiler/backend/x64
Jan 10 22:30:47 Finished compiler/backend/x64                                    44s   1GB
Jan 10 22:30:49 Starting compiler/backend/arm6
Jan 10 22:31:39 Finished compiler/backend/arm6                                   48s   1GB
Jan 10 22:31:41 Starting compiler/backend/arm8
Jan 10 22:32:24 Finished compiler/backend/arm8                                   41s 952MB
Jan 10 22:32:26 Starting compiler/backend/mips
Jan 10 22:33:11 Finished compiler/backend/mips                                   42s   1GB
Jan 10 22:33:13 Starting compiler/backend/riscv
Jan 10 22:33:59 Finished compiler/backend/riscv                                  44s   1GB
Jan 10 22:34:01 Starting compiler/parsing/proofs
Jan 10 22:38:44 Finished compiler/parsing/proofs                               4m41s 903MB
Jan 10 22:38:46 Starting compiler/inference/proofs
Jan 10 22:43:15 Finished compiler/inference/proofs                             4m26s   1GB
Jan 10 22:43:17 Starting compiler/backend/semantics
Jan 10 23:03:15 Finished compiler/backend/semantics                           19m56s   3GB
Jan 10 23:03:17 Starting compiler/backend/reg_alloc/proofs
Jan 10 23:04:33 Finished compiler/backend/reg_alloc/proofs                     1m14s 407MB
Jan 10 23:04:35 Starting compiler/backend/proofs
Jan 11 00:18:25 Finished compiler/backend/proofs                            1h13m47s   3GB
Jan 11 00:18:27 Starting compiler/encoders/x64/proofs
Jan 11 00:32:17 Finished compiler/encoders/x64/proofs                         13m47s   1GB
Jan 11 00:32:19 Starting compiler/encoders/arm6/proofs
Jan 11 00:46:26 Finished compiler/encoders/arm6/proofs                        14m04s   2GB
Jan 11 00:46:28 Starting compiler/encoders/arm8/proofs
Jan 11 00:56:10 Finished compiler/encoders/arm8/proofs                         9m40s   1GB
Jan 11 00:56:12 Starting compiler/encoders/mips/proofs
Jan 11 01:09:41 Finished compiler/encoders/mips/proofs                        13m27s   1GB
Jan 11 01:09:43 Starting compiler/encoders/riscv/proofs
Jan 11 01:24:12 Finished compiler/encoders/riscv/proofs                       14m26s 921MB
Jan 11 01:24:14 Starting compiler/backend/x64/proofs
Jan 11 01:25:12 Finished compiler/backend/x64/proofs                             56s   1GB
Jan 11 01:25:14 Starting compiler/backend/arm6/proofs
Jan 11 01:26:17 Finished compiler/backend/arm6/proofs                          1m00s   1GB
Jan 11 01:26:19 Starting compiler/backend/arm8/proofs
Jan 11 01:27:15 Finished compiler/backend/arm8/proofs                            54s   1GB
Jan 11 01:27:18 Starting compiler/backend/mips/proofs
Jan 11 01:28:17 Finished compiler/backend/mips/proofs                            57s   1GB
Jan 11 01:28:19 Starting compiler/backend/riscv/proofs
Jan 11 01:29:16 Finished compiler/backend/riscv/proofs                           55s   1GB
Jan 11 01:29:18 Starting compiler/proofs
Jan 11 01:32:08 Finished compiler/proofs                                       2m47s   1GB
Jan 11 01:32:10 Starting candle/set-theory
Jan 11 01:33:58 Finished candle/set-theory                                     1m45s 608MB
Jan 11 01:34:00 Starting candle/syntax-lib
Jan 11 01:34:23 Finished candle/syntax-lib                                       21s 544MB
Jan 11 01:34:25 Starting candle/standard/syntax
Jan 11 01:37:34 Finished candle/standard/syntax                                3m06s 633MB
Jan 11 01:37:36 Starting candle/standard/semantics
Jan 11 01:40:11 Finished candle/standard/semantics                             2m33s 914MB
Jan 11 01:40:13 Starting candle/standard/monadic
Jan 11 01:43:06 Finished candle/standard/monadic                               2m50s 833MB
Jan 11 01:43:08 Starting candle/standard/ml_kernel
Jan 11 01:54:39 Finished candle/standard/ml_kernel                            11m29s   1GB
Jan 11 01:54:41 Starting candle/standard/opentheory
Jan 11 01:55:14 Finished candle/standard/opentheory                              31s 612MB
Jan 11 01:55:16 Starting characteristic/examples
Jan 11 01:57:38 Finished characteristic/examples                               2m19s   1GB
Jan 11 01:57:40 Starting tutorial/solutions
Jan 11 02:33:35 Finished tutorial/solutions                                   35m52s   8GB
Jan 11 02:33:37 Starting translator/monadic/examples
Jan 11 02:36:34 FAILED: translator/monadic/examples
]0;Holmake: ../../../characteristicRecursively calling Holmake in /scratch/cakeml/regression/HOL-d6a10c713c9efa69f9361130a68b1d528c863cee/examples/machine-code/hoare-triple
]0;Holmake: /scratch/cakeml/regression/HOL-d6a10c713c9efa69f9361130a68b1d528c863cee/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-d6a10c713c9efa69f9361130a68b1d528c863cee/examples/machine-code/hoare-tripleFinished recursive invocation in /scratch/cakeml/regression/HOL-d6a10c713c9efa69f9361130a68b1d528c863cee/examples/machine-code/hoare-triple
]0;Holmake: ../../../characteristicRecursively calling Holmake in ../../../basis/pure
]0;Holmake: ../../../basis/pureRecursively calling Holmake in /scratch/cakeml/regression/HOL-d6a10c713c9efa69f9361130a68b1d528c863cee/examples/formal-languages/regular
]0;Holmake: /scratch/cakeml/regression/HOL-d6a10c713c9efa69f9361130a68b1d528c863cee/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-d6a10c713c9efa69f9361130a68b1d528c863cee/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-d6a10c713c9efa69f9361130a68b1d528c863cee/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL-d6a10c713c9efa69f9361130a68b1d528c863cee/examples/balanced_bstFinished recursive invocation in /scratch/cakeml/regression/HOL-d6a10c713c9efa69f9361130a68b1d528c863cee/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-d6a10c713c9efa69f9361130a68b1d528c863cee/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-d6a10c713c9efa69f9361130a68b1d528c863cee/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-d6a10c713c9efa69f9361130a68b1d528c863cee/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-d6a10c713c9efa69f9361130a68b1d528c863cee/examples/formal-languagesFinished recursive invocation in /scratch/cakeml/regression/HOL-d6a10c713c9efa69f9361130a68b1d528c863cee/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-d6a10c713c9efa69f9361130a68b1d528c863cee/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-d6a10c713c9efa69f9361130a68b1d528c863cee/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-d6a10c713c9efa69f9361130a68b1d528c863cee/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/HOL-d6a10c713c9efa69f9361130a68b1d528c863cee/examples/formal-languages/context-freeFinished recursive invocation in /scratch/cakeml/regression/HOL-d6a10c713c9efa69f9361130a68b1d528c863cee/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-d6a10c713c9efa69f9361130a68b1d528c863cee/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-d6a10c713c9efa69f9361130a68b1d528c863cee/examples/formal-languages/regularFinished recursive invocation in /scratch/cakeml/regression/HOL-d6a10c713c9efa69f9361130a68b1d528c863cee/examples/formal-languages/regular
]0;Holmake: ../../../basis/pureRecursively calling Holmake in ../../../misc
]0;Holmake: ../../../miscRecursively calling Holmake in /scratch/cakeml/regression/HOL-d6a10c713c9efa69f9361130a68b1d528c863cee/examples/fun-op-sem/lprefix_lub
]0;Holmake: /scratch/cakeml/regression/HOL-d6a10c713c9efa69f9361130a68b1d528c863cee/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-d6a10c713c9efa69f9361130a68b1d528c863cee/examples/fun-op-sem/lprefix_lubFinished recursive invocation in /scratch/cakeml/regression/HOL-d6a10c713c9efa69f9361130a68b1d528c863cee/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