Job 741

CakeML:8167ec151374c6a11a6651a7e8420ea199f48317
  Use full type names [Feb 21 09:34:21]
#618 (monadic-trans-cleanup)
Merging into:9feef1ec9f25ce1fd0474f285b4d07464ed21dbf
  Stop assuming term eqtype in ml_monad_translatorBase [Feb 16 11:48:28]
HOL:31f0cd619fcb55a888e26df3befd61f99e6d0578
  Fix minor problems in DESCRIPTION's description of parsing/printing [Feb 20 08:52:50]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Feb 21 10:18:43 Claimed job
Feb 21 10:18:47 Reusing HOL
Feb 21 10:18:52 Starting developers
Feb 21 10:18:53 Finished developers                                               0s  28MB
Feb 21 10:18:54 Starting developers/bin
Feb 21 10:19:26 Finished developers/bin                                          31s 142MB
Feb 21 10:19:27 Starting semantics/ffi
Feb 21 10:19:36 Finished semantics/ffi                                            8s 218MB
Feb 21 10:19:36 Starting semantics
Feb 21 10:20:59 Finished semantics                                             1m21s   1GB
Feb 21 10:20:59 Starting semantics/proofs
Feb 21 10:23:59 Finished semantics/proofs                                      2m59s   1GB
Feb 21 10:24:00 Starting basis/pure
Feb 21 10:24:47 Finished basis/pure                                              45s 622MB
Feb 21 10:24:47 Starting translator
Feb 21 10:26:31 Finished translator                                            1m42s   1GB
Feb 21 10:26:31 Starting compiler/parsing
Feb 21 10:27:37 Finished compiler/parsing                                      1m04s   1GB
Feb 21 10:27:37 Starting characteristic
Feb 21 10:32:05 Finished characteristic                                        4m26s   1GB
Feb 21 10:32:06 Starting translator/monadic
Feb 21 10:33:35 Finished translator/monadic                                    1m28s   1GB
Feb 21 10:33:35 Starting basis
Feb 21 10:51:16 Finished basis                                                17m40s   2GB
Feb 21 10:51:17 Starting compiler/inference
Feb 21 10:53:08 Finished compiler/inference                                    1m50s   2GB
Feb 21 10:53:08 Starting compiler/backend/reg_alloc
Feb 21 10:54:03 Finished compiler/backend/reg_alloc                              53s   1GB
Feb 21 10:54:03 Starting compiler/backend/gc
Feb 21 11:03:50 Finished compiler/backend/gc                                   9m45s   2GB
Feb 21 11:03:51 Starting compiler/backend
Feb 21 11:03:52 Finished compiler/backend                                         0s  41MB
Feb 21 11:03:53 Starting compiler/encoders/asm
Feb 21 11:03:54 Finished compiler/encoders/asm                                    0s  32MB
Feb 21 11:03:55 Starting compiler/encoders/x64
Feb 21 11:04:55 Finished compiler/encoders/x64                                   59s 920MB
Feb 21 11:04:56 Starting compiler/encoders/arm6
Feb 21 11:06:35 Finished compiler/encoders/arm6                                1m38s   1GB
Feb 21 11:06:36 Starting compiler/encoders/arm8
Feb 21 11:07:06 Finished compiler/encoders/arm8                                  29s 844MB
Feb 21 11:07:07 Starting compiler/encoders/mips
Feb 21 11:08:12 Finished compiler/encoders/mips                                1m05s   1GB
Feb 21 11:08:13 Starting compiler/encoders/riscv
Feb 21 11:09:22 Finished compiler/encoders/riscv                               1m08s 814MB
Feb 21 11:09:23 Starting compiler/encoders/ag32
Feb 21 11:09:39 Finished compiler/encoders/ag32                                  15s 493MB
Feb 21 11:09:40 Starting compiler/backend/x64
Feb 21 11:09:56 Finished compiler/backend/x64                                    16s 896MB
Feb 21 11:09:57 Starting compiler/backend/arm6
Feb 21 11:10:16 Finished compiler/backend/arm6                                   18s   1GB
Feb 21 11:10:17 Starting compiler/backend/arm8
Feb 21 11:10:34 Finished compiler/backend/arm8                                   16s   1GB
Feb 21 11:10:35 Starting compiler/backend/mips
Feb 21 11:10:52 Finished compiler/backend/mips                                   16s   1GB
Feb 21 11:10:53 Starting compiler/backend/riscv
Feb 21 11:11:10 Finished compiler/backend/riscv                                  16s   1GB
Feb 21 11:11:10 Starting compiler/backend/ag32
Feb 21 11:12:20 Finished compiler/backend/ag32                                 1m08s   1GB
Feb 21 11:12:21 Starting compiler/parsing/proofs
Feb 21 11:18:18 Finished compiler/parsing/proofs                               5m56s   1GB
Feb 21 11:18:18 Starting compiler/inference/proofs
Feb 21 11:21:09 Finished compiler/inference/proofs                             2m49s   1GB
Feb 21 11:21:10 Starting compiler/backend/semantics
Feb 21 11:29:11 Finished compiler/backend/semantics                            8m00s   1GB
Feb 21 11:29:12 Starting compiler/backend/reg_alloc/proofs
Feb 21 11:31:54 Finished compiler/backend/reg_alloc/proofs                     2m41s 800MB
Feb 21 11:31:55 Starting compiler/backend/proofs
Feb 21 12:15:06 Finished compiler/backend/proofs                              43m10s   3GB
Feb 21 12:15:07 Starting compiler/encoders/x64/proofs
Feb 21 12:25:40 Finished compiler/encoders/x64/proofs                         10m31s   7GB
Feb 21 12:25:40 Starting compiler/encoders/arm6/proofs
Feb 21 12:40:06 Finished compiler/encoders/arm6/proofs                        14m24s   3GB
Feb 21 12:40:07 Starting compiler/encoders/arm8/proofs
Feb 21 12:46:15 Finished compiler/encoders/arm8/proofs                         6m07s   1GB
Feb 21 12:46:16 Starting compiler/encoders/mips/proofs
Feb 21 12:56:38 Finished compiler/encoders/mips/proofs                        10m20s   2GB
Feb 21 12:56:38 Starting compiler/encoders/riscv/proofs
Feb 21 13:04:45 Finished compiler/encoders/riscv/proofs                        8m06s   1GB
Feb 21 13:04:46 Starting compiler/encoders/ag32/proofs
Feb 21 13:07:24 Finished compiler/encoders/ag32/proofs                         2m36s 699MB
Feb 21 13:07:24 Starting compiler/backend/x64/proofs
Feb 21 13:07:42 Finished compiler/backend/x64/proofs                             16s   1GB
Feb 21 13:07:43 Starting compiler/backend/arm6/proofs
Feb 21 13:08:02 Finished compiler/backend/arm6/proofs                            18s   1GB
Feb 21 13:08:03 Starting compiler/backend/arm8/proofs
Feb 21 13:08:19 Finished compiler/backend/arm8/proofs                            16s 722MB
Feb 21 13:08:20 Starting compiler/backend/mips/proofs
Feb 21 13:08:38 Finished compiler/backend/mips/proofs                            17s   1GB
Feb 21 13:08:39 Starting compiler/backend/riscv/proofs
Feb 21 13:08:58 Finished compiler/backend/riscv/proofs                           17s   1GB
Feb 21 13:08:58 Starting compiler/backend/ag32/proofs
Feb 21 13:18:18 Finished compiler/backend/ag32/proofs                          9m18s   4GB
Feb 21 13:18:19 Starting compiler/proofs
Feb 21 13:19:57 Finished compiler/proofs                                       1m37s   2GB
Feb 21 13:19:57 Starting candle/set-theory
Feb 21 13:20:25 Finished candle/set-theory                                       26s 670MB
Feb 21 13:20:25 Starting candle/syntax-lib
Feb 21 13:20:36 Finished candle/syntax-lib                                        9s 588MB
Feb 21 13:20:36 Starting candle/standard/syntax
Feb 21 13:22:24 Finished candle/standard/syntax                                1m46s   1GB
Feb 21 13:22:24 Starting candle/standard/semantics
Feb 21 13:24:05 Finished candle/standard/semantics                             1m39s   1GB
Feb 21 13:24:06 Starting candle/standard/monadic
Feb 21 13:25:43 Finished candle/standard/monadic                               1m37s   1GB
Feb 21 13:25:44 Starting candle/standard/ml_kernel
Feb 21 13:30:14 Finished candle/standard/ml_kernel                             4m29s   3GB
Feb 21 13:30:15 Starting candle/standard/opentheory
Feb 21 13:40:38 Finished candle/standard/opentheory                           10m21s   4GB
Feb 21 13:40:38 Starting candle/standard/opentheory/compilation
Feb 21 14:12:28 Finished candle/standard/opentheory/compilation               31m48s  29GB
Feb 21 14:12:29 Starting candle/standard/opentheory/compilation/proofs
Feb 21 14:16:25 Finished candle/standard/opentheory/compilation/proofs         3m55s   4GB
Feb 21 14:16:26 Starting characteristic/examples
Feb 21 14:19:09 Finished characteristic/examples                               2m41s   3GB
Feb 21 14:19:09 Starting tutorial/solutions
Feb 21 14:42:40 Finished tutorial/solutions                                   23m29s   3GB
Feb 21 14:42:40 Starting translator/monadic/examples
Feb 21 14:46:49 Finished translator/monadic/examples                           4m07s   2GB
Feb 21 14:46:50 Starting examples
Feb 21 15:00:19 Finished examples                                             13m28s   4GB
Feb 21 15:00:19 Starting examples/compilation/x64
Feb 21 17:14:52 Finished examples/compilation/x64                           2h14m31s  19GB
Feb 21 17:14:53 Starting examples/compilation/x64/proofs
Feb 21 17:18:35 Finished examples/compilation/x64/proofs                       3m41s   5GB
Feb 21 17:18:36 Starting examples/compilation/ag32
Feb 21 17:49:38 Finished examples/compilation/ag32                            31m01s   5GB
Feb 21 17:49:38 Starting examples/compilation/ag32/proofs
Feb 21 17:50:54 Finished examples/compilation/ag32/proofs                      1m14s   4GB
Feb 21 17:50:55 Starting translator/okasaki-examples
Feb 21 17:51:50 FAILED: translator/okasaki-examples
]0;Holmake: ~/regression/cakeml-741/basis/pure]0;Holmake: ~/regression/HOL-31f0cd619fcb55a888e26df3befd61f99e6d0578/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-31f0cd619fcb55a888e26df3befd61f99e6d0578/examples/formal-languages]0;Holmake: ~/regression/HOL-31f0cd619fcb55a888e26df3befd61f99e6d0578/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-31f0cd619fcb55a888e26df3befd61f99e6d0578/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-31f0cd619fcb55a888e26df3befd61f99e6d0578/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-31f0cd619fcb55a888e26df3befd61f99e6d0578/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-31f0cd619fcb55a888e26df3befd61f99e6d0578/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-31f0cd619fcb55a888e26df3befd61f99e6d0578/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ~/regression/cakeml-741/basis/pure]0;Holmake: ~/regression/cakeml-741/misc]0;Holmake: ~/regression/HOL-31f0cd619fcb55a888e26df3befd61f99e6d0578/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-31f0cd619fcb55a888e26df3befd61f99e6d0578/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-741/misc]0;Holmake: ~/regression/HOL-31f0cd619fcb55a888e26df3befd61f99e6d0578/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-31f0cd619fcb55a888e26df3befd61f99e6d0578/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/regression/cakeml-741/misc]0;Holmake: ~/regression/cakeml-741/developers]0;Holmake: ~/regression/cakeml-741/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-741/misc]0;Holmake: ~/regression/cakeml-741/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-741/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-741/misc]0;Holmake: ~/regression/cakeml-741/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression/cakeml-741/basis/pure]0;Holmake: ~/regression/cakeml-741/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ~/regression/cakeml-741/basis]0;Holmake: ~/regression/cakeml-741/characteristic]0;Holmake: ~/regression/cakeml-741/compiler/parsing]0;Holmake: ~/regression/cakeml-741/semantics]0;Holmake: ~/regression/cakeml-741/semantics/ffi]0;Holmake: ~/regression/cakeml-741/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-741/semantics]0;Holmake: ~/regression/cakeml-741/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression/cakeml-741/compiler/parsing]0;Holmake: ~/regression/cakeml-741/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/regression/cakeml-741/characteristic]0;Holmake: ~/regression/cakeml-741/semantics/proofs]0;Holmake: ~/regression/cakeml-741/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ~/regression/cakeml-741/characteristic]0;Holmake: ~/regression/cakeml-741/translator]0;Holmake: ~/regression/cakeml-741/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/regression/cakeml-741/characteristic]0;Holmake: ~/regression/cakeml-741/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ~/regression/cakeml-741/basis]0;Holmake: ~/regression/cakeml-741/translator/monadic]0;Holmake: ~/regression/cakeml-741/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-741/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ~/regression/cakeml-741/translator/monadic]0;Holmake: ~/regression/cakeml-741/translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ~/regression/cakeml-741/basis]0;Holmake: ~/regression/cakeml-741/basis[1mWorking in $(CAKEMLDIR)/basis[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/translator/okasaki-examples[0m
Starting work on BankersQueueTheory
Starting work on BatchedQueueTheory
Starting work on okasaki_miscTheory
Starting work on HoodMelvilleQueueTheory
okasaki_miscTheory                                                                                         OK
Starting work on BinaryRandomAccessListsTheory
BatchedQueueTheory                                                                                         OK
Starting work on BinomialHeapTheory
BankersQueueTheory                                                                                         OK
Starting work on BottomUpMergeSortTheory
HoodMelvilleQueueTheory                                                                                    OK
Starting work on ImplicitQueueTheory
BinaryRandomAccessListsTheory                                                                              OK
Starting work on LazyPairingHeapTheory
BinomialHeapTheory                                                                                FAILED! <1>
     y. y  heap_to_bag h'  leq (get_key (root t)) (get_key y)
 
 failed.
 First unsolved sub-goal is
 
 heap_to_bag t'  tree_to_bag h'' = EL_BAG a  heap_to_bag l  heap_to_bag r
 
 error in quse /home/myreen/regression/cakeml-741/translator/okasaki-examples/BinomialHeapScript.sml : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
 error in load BinomialHeapScript : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
 Uncaught exception: HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
BottomUpMergeSortTheory                                                                              M-KILLED
ImplicitQueueTheory                                                                                  M-KILLED
LazyPairingHeapTheory                                                                                M-KILLED