Job 781

CakeML:213923c3f2526d9bef27bdcf069c8b2dd20a5169
  Merge remote-tracking branch 'origin/ThmSetData-API-change' into mona [Apr 10 10:52:48]
#627 (monadic-trans-cleanup)
Merging into:ab7ea440afff89d5f90e2b85415c2e27f7894561
  Use Theory.current_definitions instead of fetch [Apr 10 09:36:45]
HOL:729baf5e526741114f4346767d17d0da3a1b6c20
  Remove (generated file) Thm-sig.sml when cleaning src/thm [Apr 07 04:31:14]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Apr 10 10:53:32 Claimed job
Apr 10 10:53:36 Reusing HOL
Apr 10 10:53:41 Starting developers
Apr 10 10:53:42 Finished developers                                               0s  31MB
Apr 10 10:53:43 Starting developers/bin
Apr 10 10:54:18 Finished developers/bin                                          34s 205MB
Apr 10 10:54:18 Starting semantics/ffi
Apr 10 10:54:26 Finished semantics/ffi                                            7s 238MB
Apr 10 10:54:27 Starting semantics
Apr 10 10:55:45 Finished semantics                                             1m18s 970MB
Apr 10 10:55:46 Starting semantics/proofs
Apr 10 10:58:41 Finished semantics/proofs                                      2m55s   1GB
Apr 10 10:58:42 Starting basis/pure
Apr 10 10:59:26 Finished basis/pure                                              43s 681MB
Apr 10 10:59:26 Starting translator
Apr 10 11:01:08 Finished translator                                            1m41s   1GB
Apr 10 11:01:08 Starting compiler/parsing
Apr 10 11:02:08 Finished compiler/parsing                                        59s   2GB
Apr 10 11:02:09 Starting characteristic
Apr 10 11:07:13 Finished characteristic                                        5m04s   1GB
Apr 10 11:07:14 Starting translator/monadic
Apr 10 11:08:37 Finished translator/monadic                                    1m22s   1GB
Apr 10 11:08:37 Starting basis
Apr 10 11:24:57 Finished basis                                                16m19s   3GB
Apr 10 11:24:58 Starting compiler/inference
Apr 10 11:26:43 Finished compiler/inference                                    1m44s   1GB
Apr 10 11:26:43 Starting compiler/backend/reg_alloc
Apr 10 11:27:42 Finished compiler/backend/reg_alloc                              58s   1GB
Apr 10 11:27:42 Starting compiler/backend/gc
Apr 10 11:36:55 Finished compiler/backend/gc                                   9m12s   2GB
Apr 10 11:36:55 Starting compiler/backend
Apr 10 11:36:56 Finished compiler/backend                                         0s  42MB
Apr 10 11:36:56 Starting compiler/encoders/asm
Apr 10 11:36:57 Finished compiler/encoders/asm                                    0s  32MB
Apr 10 11:36:58 Starting compiler/encoders/x64
Apr 10 11:37:54 Finished compiler/encoders/x64                                   55s 805MB
Apr 10 11:37:55 Starting compiler/encoders/arm6
Apr 10 11:39:30 Finished compiler/encoders/arm6                                1m34s   1GB
Apr 10 11:39:30 Starting compiler/encoders/arm8
Apr 10 11:39:59 Finished compiler/encoders/arm8                                  28s 550MB
Apr 10 11:39:59 Starting compiler/encoders/mips
Apr 10 11:41:04 Finished compiler/encoders/mips                                1m04s   1GB
Apr 10 11:41:05 Starting compiler/encoders/riscv
Apr 10 11:42:22 Finished compiler/encoders/riscv                               1m17s 957MB
Apr 10 11:42:23 Starting compiler/encoders/ag32
Apr 10 11:42:38 Finished compiler/encoders/ag32                                  14s 654MB
Apr 10 11:42:38 Starting compiler/backend/x64
Apr 10 11:42:53 Finished compiler/backend/x64                                    14s 817MB
Apr 10 11:42:54 Starting compiler/backend/arm6
Apr 10 11:43:12 Finished compiler/backend/arm6                                   17s   1GB
Apr 10 11:43:12 Starting compiler/backend/arm8
Apr 10 11:43:28 Finished compiler/backend/arm8                                   15s   1GB
Apr 10 11:43:28 Starting compiler/backend/mips
Apr 10 11:43:45 Finished compiler/backend/mips                                   15s   1GB
Apr 10 11:43:45 Starting compiler/backend/riscv
Apr 10 11:44:02 Finished compiler/backend/riscv                                  16s   1GB
Apr 10 11:44:03 Starting compiler/backend/ag32
Apr 10 11:45:08 Finished compiler/backend/ag32                                 1m05s   1GB
Apr 10 11:45:09 Starting compiler/parsing/proofs
Apr 10 11:50:46 Finished compiler/parsing/proofs                               5m36s 793MB
Apr 10 11:50:46 Starting compiler/inference/proofs
Apr 10 11:53:22 Finished compiler/inference/proofs                             2m35s 994MB
Apr 10 11:53:23 Starting compiler/backend/semantics
Apr 10 12:00:18 Finished compiler/backend/semantics                            6m54s   2GB
Apr 10 12:00:18 Starting compiler/backend/reg_alloc/proofs
Apr 10 12:03:31 Finished compiler/backend/reg_alloc/proofs                     3m12s 679MB
Apr 10 12:03:31 Starting compiler/backend/proofs
Apr 10 12:40:48 Finished compiler/backend/proofs                              37m15s   3GB
Apr 10 12:40:48 Starting compiler/encoders/x64/proofs
Apr 10 12:50:46 Finished compiler/encoders/x64/proofs                          9m57s   7GB
Apr 10 12:50:46 Starting compiler/encoders/arm6/proofs
Apr 10 13:04:13 Finished compiler/encoders/arm6/proofs                        13m26s   4GB
Apr 10 13:04:14 Starting compiler/encoders/arm8/proofs
Apr 10 13:09:50 Finished compiler/encoders/arm8/proofs                         5m36s   1GB
Apr 10 13:09:51 Starting compiler/encoders/mips/proofs
Apr 10 13:19:51 Finished compiler/encoders/mips/proofs                         9m59s   2GB
Apr 10 13:19:51 Starting compiler/encoders/riscv/proofs
Apr 10 13:28:12 Finished compiler/encoders/riscv/proofs                        8m20s   1GB
Apr 10 13:28:13 Starting compiler/encoders/ag32/proofs
Apr 10 13:30:41 Finished compiler/encoders/ag32/proofs                         2m27s 616MB
Apr 10 13:30:41 Starting compiler/backend/x64/proofs
Apr 10 13:30:57 Finished compiler/backend/x64/proofs                             15s 981MB
Apr 10 13:30:58 Starting compiler/backend/arm6/proofs
Apr 10 13:31:17 Finished compiler/backend/arm6/proofs                            18s   1GB
Apr 10 13:31:17 Starting compiler/backend/arm8/proofs
Apr 10 13:31:34 Finished compiler/backend/arm8/proofs                            15s   1GB
Apr 10 13:31:34 Starting compiler/backend/mips/proofs
Apr 10 13:31:51 Finished compiler/backend/mips/proofs                            16s 954MB
Apr 10 13:31:51 Starting compiler/backend/riscv/proofs
Apr 10 13:32:08 Finished compiler/backend/riscv/proofs                           16s   1GB
Apr 10 13:32:08 Starting compiler/backend/ag32/proofs
Apr 10 13:40:54 Finished compiler/backend/ag32/proofs                          8m45s   2GB
Apr 10 13:40:55 Starting compiler/proofs
Apr 10 13:42:06 Finished compiler/proofs                                       1m10s   3GB
Apr 10 13:42:06 Starting candle/set-theory
Apr 10 13:42:31 Finished candle/set-theory                                       24s 665MB
Apr 10 13:42:31 Starting candle/syntax-lib
Apr 10 13:42:41 Finished candle/syntax-lib                                        8s 637MB
Apr 10 13:42:41 Starting candle/standard/syntax
Apr 10 13:44:21 Finished candle/standard/syntax                                1m39s   1GB
Apr 10 13:44:21 Starting candle/standard/semantics
Apr 10 13:45:54 Finished candle/standard/semantics                             1m32s 903MB
Apr 10 13:45:54 Starting candle/standard/monadic
Apr 10 13:47:24 Finished candle/standard/monadic                               1m29s   1GB
Apr 10 13:47:25 Starting candle/standard/ml_kernel
Apr 10 13:51:06 Finished candle/standard/ml_kernel                             3m40s   3GB
Apr 10 13:51:06 Starting candle/standard/opentheory
Apr 10 13:54:12 FAILED: candle/standard/opentheory
]0;Holmake: ~/regression/cakeml-781/basis/pure]0;Holmake: ~/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languages]0;Holmake: ~/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ~/regression/cakeml-781/basis/pure]0;Holmake: ~/regression/cakeml-781/misc]0;Holmake: ~/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-781/misc]0;Holmake: ~/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/regression/cakeml-781/misc]0;Holmake: ~/regression/cakeml-781/developers]0;Holmake: ~/regression/cakeml-781/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-781/misc]0;Holmake: ~/regression/cakeml-781/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-781/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-781/misc]0;Holmake: ~/regression/cakeml-781/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression/cakeml-781/basis/pure]0;Holmake: ~/regression/cakeml-781/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ~/regression/cakeml-781/basis]0;Holmake: ~/regression/cakeml-781/characteristic]0;Holmake: ~/regression/cakeml-781/compiler/parsing]0;Holmake: ~/regression/cakeml-781/semantics]0;Holmake: ~/regression/cakeml-781/semantics/ffi]0;Holmake: ~/regression/cakeml-781/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-781/semantics]0;Holmake: ~/regression/cakeml-781/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression/cakeml-781/compiler/parsing]0;Holmake: ~/regression/cakeml-781/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/regression/cakeml-781/characteristic]0;Holmake: ~/regression/cakeml-781/semantics/proofs]0;Holmake: ~/regression/cakeml-781/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ~/regression/cakeml-781/characteristic]0;Holmake: ~/regression/cakeml-781/translator]0;Holmake: ~/regression/cakeml-781/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/regression/cakeml-781/characteristic]0;Holmake: ~/regression/cakeml-781/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ~/regression/cakeml-781/basis]0;Holmake: ~/regression/cakeml-781/translator/monadic]0;Holmake: ~/regression/cakeml-781/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-781/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ~/regression/cakeml-781/translator/monadic]0;Holmake: ~/regression/cakeml-781/translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ~/regression/cakeml-781/basis]0;Holmake: ~/regression/cakeml-781/basis[1mWorking in $(CAKEMLDIR)/basis[0m
]0;Holmake: .]0;Holmake: ../ml_kernel]0;Holmake: ../monadic]0;Holmake: ../syntax]0;Holmake: ../../syntax-lib]0;Holmake: ../../syntax-lib[1mWorking in $(CAKEMLDIR)/candle/syntax-lib[0m
]0;Holmake: ../syntax]0;Holmake: ../syntax[1mWorking in $(CAKEMLDIR)/candle/standard/syntax[0m
]0;Holmake: ../monadic]0;Holmake: ../monadic[1mWorking in $(CAKEMLDIR)/candle/standard/monadic[0m
]0;Holmake: ../ml_kernel]0;Holmake: ../ml_kernel[1mWorking in $(CAKEMLDIR)/candle/standard/ml_kernel[0m
]0;Holmake: .]0;Holmake: ../semantics]0;Holmake: ../../set-theory]0;Holmake: ../../set-theory[1mWorking in $(CAKEMLDIR)/candle/set-theory[0m
]0;Holmake: ../semantics]0;Holmake: ../semantics[1mWorking in $(CAKEMLDIR)/candle/standard/semantics[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/candle/standard/opentheory[0m
Starting work on prettyTheory
Starting work on README.md
README.md                                                                    OK
prettyTheory                                                                 OK
Starting work on readerTheory
readerTheory                                                                 OK
Starting work on reader_initTheory
reader_initTheory                                                            OK
Starting work on readerProofTheory
readerProofTheory                                                            OK
Starting work on reader_commonProgTheory
Starting work on readerSoundnessTheory
readerSoundnessTheory                                                        OK
reader_commonProgTheory                                             FAILED! <1>
 <<HOL message: Created theory "reader_commonProg">>
 Loading monadic translator state from: ml_hol_kernelProg... error in quse /home/myreen/regression/cakeml-781/candle/standard/opentheory/reader_commonProgScript.sml : HOL_ERR {message = "Could not load translator state.", origin_function = "failwith", origin_structure = "??"}
 error in load reader_commonProgScript : HOL_ERR {message = "Could not load translator state.", origin_function = "failwith", origin_structure = "??"}
 Uncaught exception: HOL_ERR {message = "Could not load translator state.", origin_function = "failwith", origin_structure = "??"}