Job 172

CakeML:138eca2a9c615f73c23676b03ac1ea4aa4f5bd09
  Add missing defs to reg_allocComputeLib [Jan 22 14:36:16]
#439 (monad-cleanup)
Merging into:820c6b2156d7b6f7ad94ad67aae70135371c9fd5
  Move full_compile defns into compilerTheory [Jan 21 18:44:19]
HOL:a061a8d27a88af555eb42dd1030099a4ecedea45
  Fixes to build logic/ltl/concrGBArepScript.sml on --expk [Jan 21 06:00:31]
Machine:cakeml1853 4.4.0-22-generic x86_64 GNU/Linux

Jan 22 15:39:37 Claimed job
Jan 22 15:39:55 Building HOL
Jan 22 15:53:06 Starting semantics/ffi
Jan 22 15:54:14 Finished semantics/ffi                                         1m06s 437MB
Jan 22 15:54:16 Starting semantics
Jan 22 15:57:10 Finished semantics                                             2m51s   1GB
Jan 22 15:57:12 Starting semantics/proofs
Jan 22 16:00:41 Finished semantics/proofs                                      3m27s   1GB
Jan 22 16:00:43 Starting basis/pure
Jan 22 16:06:56 Finished basis/pure                                            6m10s 767MB
Jan 22 16:06:57 Starting translator
Jan 22 16:13:46 Finished translator                                            6m46s   1GB
Jan 22 16:13:48 Starting compiler/parsing
Jan 22 16:16:17 Finished compiler/parsing                                      2m27s   1GB
Jan 22 16:16:19 Starting characteristic
Jan 22 16:20:56 Finished characteristic                                        4m34s   1GB
Jan 22 16:20:58 Starting basis
Jan 22 16:51:09 Finished basis                                                30m08s   3GB
Jan 22 16:51:11 Starting translator/monadic
Jan 22 16:54:44 Finished translator/monadic                                    3m30s   1GB
Jan 22 16:54:46 Starting compiler/inference
Jan 22 16:57:33 Finished compiler/inference                                    2m44s   1GB
Jan 22 16:57:34 Starting compiler/backend/reg_alloc
Jan 22 16:58:24 Finished compiler/backend/reg_alloc                              47s 749MB
Jan 22 16:58:26 Starting compiler/backend/gc
Jan 22 17:14:21 Finished compiler/backend/gc                                  15m52s   2GB
Jan 22 17:14:23 Starting compiler/backend
Jan 22 17:14:27 Finished compiler/backend                                         2s  23MB
Jan 22 17:14:29 Starting compiler/encoders/asm
Jan 22 17:14:32 Finished compiler/encoders/asm                                    0s  19MB
Jan 22 17:14:34 Starting compiler/encoders/x64
Jan 22 17:16:13 Finished compiler/encoders/x64                                 1m37s 473MB
Jan 22 17:16:15 Starting compiler/encoders/arm6
Jan 22 17:19:22 Finished compiler/encoders/arm6                                3m05s   1GB
Jan 22 17:19:24 Starting compiler/encoders/arm8
Jan 22 17:20:10 Finished compiler/encoders/arm8                                  44s 401MB
Jan 22 17:20:12 Starting compiler/encoders/mips
Jan 22 17:21:38 Finished compiler/encoders/mips                                1m23s 635MB
Jan 22 17:21:40 Starting compiler/encoders/riscv
Jan 22 17:23:09 Finished compiler/encoders/riscv                               1m27s 464MB
Jan 22 17:23:11 Starting compiler/backend/x64
Jan 22 17:23:53 Finished compiler/backend/x64                                    40s   1GB
Jan 22 17:23:55 Starting compiler/backend/arm6
Jan 22 17:24:43 Finished compiler/backend/arm6                                   46s   1GB
Jan 22 17:24:45 Starting compiler/backend/arm8
Jan 22 17:25:26 Finished compiler/backend/arm8                                   38s 926MB
Jan 22 17:25:28 Starting compiler/backend/mips
Jan 22 17:26:10 Finished compiler/backend/mips                                   39s 962MB
Jan 22 17:26:12 Starting compiler/backend/riscv
Jan 22 17:26:54 Finished compiler/backend/riscv                                  40s 890MB
Jan 22 17:26:56 Starting compiler/parsing/proofs
Jan 22 17:31:33 Finished compiler/parsing/proofs                               4m34s 741MB
Jan 22 17:31:35 Starting compiler/inference/proofs
Jan 22 17:35:48 Finished compiler/inference/proofs                             4m11s   1GB
Jan 22 17:35:50 Starting compiler/backend/semantics
Jan 22 17:54:24 Finished compiler/backend/semantics                           18m31s   2GB
Jan 22 17:54:26 Starting compiler/backend/reg_alloc/proofs
Jan 22 17:55:43 Finished compiler/backend/reg_alloc/proofs                     1m14s 506MB
Jan 22 17:55:44 Starting compiler/backend/proofs
Jan 22 19:03:20 Finished compiler/backend/proofs                            1h07m32s   4GB
Jan 22 19:03:22 Starting compiler/encoders/x64/proofs
Jan 22 19:16:42 Finished compiler/encoders/x64/proofs                         13m18s   2GB
Jan 22 19:16:44 Starting compiler/encoders/arm6/proofs
Jan 22 19:29:49 Finished compiler/encoders/arm6/proofs                        13m02s   3GB
Jan 22 19:29:51 Starting compiler/encoders/arm8/proofs
Jan 22 19:38:53 Finished compiler/encoders/arm8/proofs                         9m00s   1GB
Jan 22 19:38:55 Starting compiler/encoders/mips/proofs
Jan 22 19:51:30 Finished compiler/encoders/mips/proofs                        12m33s   1GB
Jan 22 19:51:32 Starting compiler/encoders/riscv/proofs
Jan 22 20:04:56 Finished compiler/encoders/riscv/proofs                       13m20s   1GB
Jan 22 20:04:58 Starting compiler/backend/x64/proofs
Jan 22 20:05:50 Finished compiler/backend/x64/proofs                             50s   1GB
Jan 22 20:05:52 Starting compiler/backend/arm6/proofs
Jan 22 20:06:49 Finished compiler/backend/arm6/proofs                            55s   1GB
Jan 22 20:06:51 Starting compiler/backend/arm8/proofs
Jan 22 20:07:45 Finished compiler/backend/arm8/proofs                            52s   1GB
Jan 22 20:07:47 Starting compiler/backend/mips/proofs
Jan 22 20:08:41 Finished compiler/backend/mips/proofs                            52s   1GB
Jan 22 20:08:43 Starting compiler/backend/riscv/proofs
Jan 22 20:09:37 Finished compiler/backend/riscv/proofs                           51s   1GB
Jan 22 20:09:39 Starting compiler/proofs
Jan 22 20:12:22 Finished compiler/proofs                                       2m41s   2GB
Jan 22 20:12:24 Starting candle/set-theory
Jan 22 20:14:04 Finished candle/set-theory                                     1m38s 550MB
Jan 22 20:14:06 Starting candle/syntax-lib
Jan 22 20:14:28 Finished candle/syntax-lib                                       19s 584MB
Jan 22 20:14:30 Starting candle/standard/syntax
Jan 22 20:17:26 Finished candle/standard/syntax                                2m53s   1GB
Jan 22 20:17:28 Starting candle/standard/semantics
Jan 22 20:19:47 Finished candle/standard/semantics                             2m16s 876MB
Jan 22 20:19:49 Starting candle/standard/monadic
Jan 22 20:22:27 Finished candle/standard/monadic                               2m36s   1GB
Jan 22 20:22:29 Starting candle/standard/ml_kernel
Jan 22 20:33:09 Finished candle/standard/ml_kernel                            10m37s   2GB
Jan 22 20:33:11 Starting candle/standard/opentheory
Jan 22 20:33:42 Finished candle/standard/opentheory                              29s 641MB
Jan 22 20:33:44 Starting characteristic/examples
Jan 22 20:36:12 Finished characteristic/examples                               2m26s   2GB
Jan 22 20:36:14 Starting tutorial/solutions
Jan 22 21:13:34 Finished tutorial/solutions                                   37m17s  10GB
Jan 22 21:13:36 Starting translator/monadic/examples
Jan 22 21:16:27 FAILED: translator/monadic/examples
]0;Holmake: ../../../characteristicRecursively calling Holmake in /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/machine-code/hoare-triple
]0;Holmake: /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/machine-code/hoare-tripleFinished recursive invocation in /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/machine-code/hoare-triple
]0;Holmake: ../../../characteristicRecursively calling Holmake in ../../../basis/pure
]0;Holmake: ../../../basis/pureRecursively calling Holmake in /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/formal-languages/regular
]0;Holmake: /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/balanced_bstFinished recursive invocation in /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/formal-languagesFinished recursive invocation in /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/formal-languages/context-freeFinished recursive invocation in /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/formal-languages/regularFinished recursive invocation in /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/formal-languages/regular
]0;Holmake: ../../../basis/pureRecursively calling Holmake in ../../../misc
]0;Holmake: ../../../miscRecursively calling Holmake in /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/fun-op-sem/lprefix_lub
]0;Holmake: /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/examples/fun-op-sem/lprefix_lubFinished recursive invocation in /scratch/cakeml/regression/HOL-a061a8d27a88af555eb42dd1030099a4ecedea45/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 exceptionArityTestProgTheory
Starting work on exceptionProgTheory
exceptionProgTheory                                                          OK
Starting work on graphStateProgTheory
exceptionArityTestProgTheory                                                 OK
Starting work on refStateProgTheory
arrayGlobalStateProgTheory                                                   OK
Starting work on runProgTheory
arrayLocalStateProgTheory                                                    OK
Starting work on testAssumTheory
refStateProgTheory                                                           OK
Starting work on testPrecondProgTheory
graphStateProgTheory                                                    CHEATED
Starting work on testRunTheory
runProgTheory                                                                OK
testAssumTheory                                                              OK
testPrecondProgTheory                                                        OK
testRunTheory                                                                OK