Job 146

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:de190c871a4c3c7c3d0131a85f020b3fd7bdb791
  Merge pull request #508 from barakeel/master [Jan 10 02:10:28]
Machine:cakeml1794 4.4.0-98-generic x86_64 GNU/Linux

Jan 10 04:48:33 Claimed job
Jan 10 04:48:42 Building HOL
Jan 10 05:02:16 Starting semantics/ffi
Jan 10 05:03:29 Finished semantics/ffi                                         1m10s 386MB
Jan 10 05:03:31 Starting semantics
Jan 10 05:06:23 Finished semantics                                             2m50s   1GB
Jan 10 05:06:25 Starting semantics/proofs
Jan 10 05:10:12 Finished semantics/proofs                                      3m44s   1GB
Jan 10 05:10:14 Starting basis/pure
Jan 10 05:16:55 Finished basis/pure                                            6m39s 603MB
Jan 10 05:16:57 Starting translator
Jan 10 05:24:29 Finished translator                                            7m29s 902MB
Jan 10 05:24:30 Starting compiler/parsing
Jan 10 05:27:00 Finished compiler/parsing                                      2m27s   1GB
Jan 10 05:27:02 Starting characteristic
Jan 10 05:32:00 Finished characteristic                                        4m56s   1GB
Jan 10 05:32:02 Starting basis
Jan 10 05:59:57 Finished basis                                                27m52s   2GB
Jan 10 05:59:59 Starting translator/monadic
Jan 10 06:03:34 Finished translator/monadic                                    3m33s   1GB
Jan 10 06:03:36 Starting compiler/inference
Jan 10 06:06:38 Finished compiler/inference                                    2m59s   1GB
Jan 10 06:06:40 Starting compiler/backend/reg_alloc
Jan 10 06:07:32 Finished compiler/backend/reg_alloc                              50s 817MB
Jan 10 06:07:34 Starting compiler/backend/gc
Jan 10 06:24:53 Finished compiler/backend/gc                                  17m17s   2GB
Jan 10 06:24:55 Starting compiler/backend
Jan 10 06:24:59 Finished compiler/backend                                         2s  14MB
Jan 10 06:25:01 Starting compiler/encoders/asm
Jan 10 06:25:04 Finished compiler/encoders/asm                                    0s  11MB
Jan 10 06:25:06 Starting compiler/encoders/x64
Jan 10 06:26:52 Finished compiler/encoders/x64                                 1m43s 488MB
Jan 10 06:26:54 Starting compiler/encoders/arm6
Jan 10 06:30:19 Finished compiler/encoders/arm6                                3m23s   1GB
Jan 10 06:30:21 Starting compiler/encoders/arm8
Jan 10 06:31:08 Finished compiler/encoders/arm8                                  45s 409MB
Jan 10 06:31:10 Starting compiler/encoders/mips
Jan 10 06:32:41 Finished compiler/encoders/mips                                1m29s 556MB
Jan 10 06:32:43 Starting compiler/encoders/riscv
Jan 10 06:34:22 Finished compiler/encoders/riscv                               1m36s 437MB
Jan 10 06:34:23 Starting compiler/backend/x64
Jan 10 06:35:10 Finished compiler/backend/x64                                    44s   1GB
Jan 10 06:35:12 Starting compiler/backend/arm6
Jan 10 06:36:04 Finished compiler/backend/arm6                                   49s   1GB
Jan 10 06:36:06 Starting compiler/backend/arm8
Jan 10 06:36:52 Finished compiler/backend/arm8                                   44s   1GB
Jan 10 06:36:54 Starting compiler/backend/mips
Jan 10 06:37:41 Finished compiler/backend/mips                                   45s   1GB
Jan 10 06:37:43 Starting compiler/backend/riscv
Jan 10 06:38:31 Finished compiler/backend/riscv                                  45s   1GB
Jan 10 06:38:33 Starting compiler/parsing/proofs
Jan 10 06:43:40 Finished compiler/parsing/proofs                               5m05s 580MB
Jan 10 06:43:42 Starting compiler/inference/proofs
Jan 10 06:48:23 Finished compiler/inference/proofs                             4m39s   1GB
Jan 10 06:48:25 Starting compiler/backend/semantics
Jan 10 07:09:07 Finished compiler/backend/semantics                           20m39s   4GB
Jan 10 07:09:09 Starting compiler/backend/reg_alloc/proofs
Jan 10 07:10:32 Finished compiler/backend/reg_alloc/proofs                     1m20s 402MB
Jan 10 07:10:34 Starting compiler/backend/proofs
Jan 10 08:24:52 Finished compiler/backend/proofs                            1h14m15s   7GB
Jan 10 08:24:54 Starting compiler/encoders/x64/proofs
Jan 10 08:39:17 Finished compiler/encoders/x64/proofs                         14m19s   1GB
Jan 10 08:39:19 Starting compiler/encoders/arm6/proofs
Jan 10 08:53:35 Finished compiler/encoders/arm6/proofs                        14m14s   2GB
Jan 10 08:53:37 Starting compiler/encoders/arm8/proofs
Jan 10 09:03:17 Finished compiler/encoders/arm8/proofs                         9m38s   1GB
Jan 10 09:03:19 Starting compiler/encoders/mips/proofs
Jan 10 09:16:56 Finished compiler/encoders/mips/proofs                        13m35s   1GB
Jan 10 09:16:58 Starting compiler/encoders/riscv/proofs
Jan 10 09:31:33 Finished compiler/encoders/riscv/proofs                       14m32s   1GB
Jan 10 09:31:35 Starting compiler/backend/x64/proofs
Jan 10 09:32:30 Finished compiler/backend/x64/proofs                             53s   1GB
Jan 10 09:32:32 Starting compiler/backend/arm6/proofs
Jan 10 09:33:34 Finished compiler/backend/arm6/proofs                          1m00s   1GB
Jan 10 09:33:36 Starting compiler/backend/arm8/proofs
Jan 10 09:34:31 Finished compiler/backend/arm8/proofs                            53s   1GB
Jan 10 09:34:33 Starting compiler/backend/mips/proofs
Jan 10 09:35:31 Finished compiler/backend/mips/proofs                            55s   1GB
Jan 10 09:35:33 Starting compiler/backend/riscv/proofs
Jan 10 09:36:29 Finished compiler/backend/riscv/proofs                           54s   1GB
Jan 10 09:36:31 Starting compiler/proofs
Jan 10 09:39:15 Finished compiler/proofs                                       2m41s   1GB
Jan 10 09:39:17 Starting candle/set-theory
Jan 10 09:41:06 Finished candle/set-theory                                     1m47s 697MB
Jan 10 09:41:08 Starting candle/syntax-lib
Jan 10 09:41:31 Finished candle/syntax-lib                                       20s 535MB
Jan 10 09:41:33 Starting candle/standard/syntax
Jan 10 09:44:39 Finished candle/standard/syntax                                3m04s 622MB
Jan 10 09:44:41 Starting candle/standard/semantics
Jan 10 09:47:13 Finished candle/standard/semantics                             2m29s 710MB
Jan 10 09:47:15 Starting candle/standard/monadic
Jan 10 09:50:05 Finished candle/standard/monadic                               2m48s 883MB
Jan 10 09:50:07 Starting candle/standard/ml_kernel
Jan 10 10:01:40 Finished candle/standard/ml_kernel                            11m30s   2GB
Jan 10 10:01:42 Starting candle/standard/opentheory
Jan 10 10:02:15 Finished candle/standard/opentheory                              31s 567MB
Jan 10 10:02:17 Starting characteristic/examples
Jan 10 10:04:41 Finished characteristic/examples                               2m22s   1GB
Jan 10 10:04:43 Starting tutorial/solutions
Jan 10 10:43:06 Finished tutorial/solutions                                   38m20s  11GB
Jan 10 10:43:09 Starting translator/monadic/examples
Jan 10 10:46:03 FAILED: translator/monadic/examples
]0;Holmake: ../../../characteristicRecursively calling Holmake in /scratch/cakeml/regression/HOL-de190c871a4c3c7c3d0131a85f020b3fd7bdb791/examples/machine-code/hoare-triple
]0;Holmake: /scratch/cakeml/regression/HOL-de190c871a4c3c7c3d0131a85f020b3fd7bdb791/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-de190c871a4c3c7c3d0131a85f020b3fd7bdb791/examples/machine-code/hoare-tripleFinished recursive invocation in /scratch/cakeml/regression/HOL-de190c871a4c3c7c3d0131a85f020b3fd7bdb791/examples/machine-code/hoare-triple
]0;Holmake: ../../../characteristicRecursively calling Holmake in ../../../basis/pure
]0;Holmake: ../../../basis/pureRecursively calling Holmake in /scratch/cakeml/regression/HOL-de190c871a4c3c7c3d0131a85f020b3fd7bdb791/examples/formal-languages/regular
]0;Holmake: /scratch/cakeml/regression/HOL-de190c871a4c3c7c3d0131a85f020b3fd7bdb791/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-de190c871a4c3c7c3d0131a85f020b3fd7bdb791/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-de190c871a4c3c7c3d0131a85f020b3fd7bdb791/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL-de190c871a4c3c7c3d0131a85f020b3fd7bdb791/examples/balanced_bstFinished recursive invocation in /scratch/cakeml/regression/HOL-de190c871a4c3c7c3d0131a85f020b3fd7bdb791/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-de190c871a4c3c7c3d0131a85f020b3fd7bdb791/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-de190c871a4c3c7c3d0131a85f020b3fd7bdb791/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-de190c871a4c3c7c3d0131a85f020b3fd7bdb791/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-de190c871a4c3c7c3d0131a85f020b3fd7bdb791/examples/formal-languagesFinished recursive invocation in /scratch/cakeml/regression/HOL-de190c871a4c3c7c3d0131a85f020b3fd7bdb791/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-de190c871a4c3c7c3d0131a85f020b3fd7bdb791/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-de190c871a4c3c7c3d0131a85f020b3fd7bdb791/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-de190c871a4c3c7c3d0131a85f020b3fd7bdb791/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/HOL-de190c871a4c3c7c3d0131a85f020b3fd7bdb791/examples/formal-languages/context-freeFinished recursive invocation in /scratch/cakeml/regression/HOL-de190c871a4c3c7c3d0131a85f020b3fd7bdb791/examples/formal-languages/context-free
]0;Holmake: /scratch/cakeml/regression/HOL-de190c871a4c3c7c3d0131a85f020b3fd7bdb791/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-de190c871a4c3c7c3d0131a85f020b3fd7bdb791/examples/formal-languages/regularFinished recursive invocation in /scratch/cakeml/regression/HOL-de190c871a4c3c7c3d0131a85f020b3fd7bdb791/examples/formal-languages/regular
]0;Holmake: ../../../basis/pureRecursively calling Holmake in ../../../misc
]0;Holmake: ../../../miscRecursively calling Holmake in /scratch/cakeml/regression/HOL-de190c871a4c3c7c3d0131a85f020b3fd7bdb791/examples/fun-op-sem/lprefix_lub
]0;Holmake: /scratch/cakeml/regression/HOL-de190c871a4c3c7c3d0131a85f020b3fd7bdb791/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-de190c871a4c3c7c3d0131a85f020b3fd7bdb791/examples/fun-op-sem/lprefix_lubFinished recursive invocation in /scratch/cakeml/regression/HOL-de190c871a4c3c7c3d0131a85f020b3fd7bdb791/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