Job 784

CakeML:213923c3f2526d9bef27bdcf069c8b2dd20a5169
  Merge remote-tracking branch 'origin/ThmSetData-API-change' into mona [Apr 10 10:52:48]
#627 (monadic-trans-cleanup)
Merging into:dd8ca4fca024b5b629a7c3ed7d3d4b1844c82f3d
  Merge pull request #628 from CakeML/ThmSetData-API-change [Apr 10 21:53:38]
HOL:729baf5e526741114f4346767d17d0da3a1b6c20
  Remove (generated file) Thm-sig.sml when cleaning src/thm [Apr 07 04:31:14]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Apr 10 21:55:08 Claimed job
Apr 10 21:55:11 Reusing HOL
Apr 10 21:55:58 Starting developers
Apr 10 21:56:00 Finished developers                                               2s  21MB
Apr 10 21:56:01 Starting developers/bin
Apr 10 21:57:17 Finished developers/bin                                        1m16s 918MB
Apr 10 21:57:17 Starting semantics/ffi
Apr 10 21:57:27 Finished semantics/ffi                                           10s 227MB
Apr 10 21:57:28 Starting semantics
Apr 10 21:58:49 Finished semantics                                             1m21s   1GB
Apr 10 21:58:50 Starting semantics/proofs
Apr 10 22:01:46 Finished semantics/proofs                                      2m56s   1GB
Apr 10 22:01:46 Starting basis/pure
Apr 10 22:02:34 Finished basis/pure                                              46s 620MB
Apr 10 22:02:34 Starting translator
Apr 10 22:04:15 Finished translator                                            1m40s   1GB
Apr 10 22:04:15 Starting compiler/parsing
Apr 10 22:05:12 Finished compiler/parsing                                        56s   3GB
Apr 10 22:05:13 Starting characteristic
Apr 10 22:10:21 Finished characteristic                                        5m08s   2GB
Apr 10 22:10:21 Starting translator/monadic
Apr 10 22:11:52 Finished translator/monadic                                    1m30s   1GB
Apr 10 22:11:52 Starting basis
Apr 10 22:28:18 Finished basis                                                16m25s   2GB
Apr 10 22:28:18 Starting compiler/inference
Apr 10 22:29:50 Finished compiler/inference                                    1m31s   1GB
Apr 10 22:29:50 Starting compiler/backend/reg_alloc
Apr 10 22:30:51 Finished compiler/backend/reg_alloc                              59s   1GB
Apr 10 22:30:51 Starting compiler/backend/gc
Apr 10 22:38:48 Finished compiler/backend/gc                                   7m56s   1GB
Apr 10 22:38:49 Starting compiler/backend
Apr 10 22:38:51 Finished compiler/backend                                         2s  21MB
Apr 10 22:38:51 Starting compiler/encoders/asm
Apr 10 22:38:53 Finished compiler/encoders/asm                                    1s  14MB
Apr 10 22:38:53 Starting compiler/encoders/x64
Apr 10 22:39:19 Finished compiler/encoders/x64                                   25s 704MB
Apr 10 22:39:19 Starting compiler/encoders/arm6
Apr 10 22:40:04 Finished compiler/encoders/arm6                                  45s 718MB
Apr 10 22:40:04 Starting compiler/encoders/arm8
Apr 10 22:40:18 Finished compiler/encoders/arm8                                  13s 624MB
Apr 10 22:40:18 Starting compiler/encoders/mips
Apr 10 22:40:36 Finished compiler/encoders/mips                                  17s 901MB
Apr 10 22:40:36 Starting compiler/encoders/riscv
Apr 10 22:40:51 Finished compiler/encoders/riscv                                 14s 688MB
Apr 10 22:40:52 Starting compiler/encoders/ag32
Apr 10 22:41:09 Finished compiler/encoders/ag32                                  16s 631MB
Apr 10 22:41:09 Starting compiler/backend/x64
Apr 10 22:41:27 Finished compiler/backend/x64                                    17s   1GB
Apr 10 22:41:28 Starting compiler/backend/arm6
Apr 10 22:41:48 Finished compiler/backend/arm6                                   20s   1GB
Apr 10 22:41:48 Starting compiler/backend/arm8
Apr 10 22:42:07 Finished compiler/backend/arm8                                   18s   1GB
Apr 10 22:42:07 Starting compiler/backend/mips
Apr 10 22:42:26 Finished compiler/backend/mips                                   18s   1GB
Apr 10 22:42:26 Starting compiler/backend/riscv
Apr 10 22:42:46 Finished compiler/backend/riscv                                  19s   1GB
Apr 10 22:42:46 Starting compiler/backend/ag32
Apr 10 22:43:53 Finished compiler/backend/ag32                                 1m07s   1GB
Apr 10 22:43:54 Starting compiler/parsing/proofs
Apr 10 22:49:25 Finished compiler/parsing/proofs                               5m31s   1GB
Apr 10 22:49:25 Starting compiler/inference/proofs
Apr 10 22:52:06 Finished compiler/inference/proofs                             2m40s 820MB
Apr 10 22:52:06 Starting compiler/backend/semantics
Apr 10 22:58:57 Finished compiler/backend/semantics                            6m50s   2GB
Apr 10 22:58:57 Starting compiler/backend/reg_alloc/proofs
Apr 10 23:02:11 Finished compiler/backend/reg_alloc/proofs                     3m13s 785MB
Apr 10 23:02:11 Starting compiler/backend/proofs
Apr 10 23:39:14 Finished compiler/backend/proofs                              37m03s   3GB
Apr 10 23:39:14 Starting compiler/encoders/x64/proofs
Apr 10 23:48:07 Finished compiler/encoders/x64/proofs                          8m51s   4GB
Apr 10 23:48:07 Starting compiler/encoders/arm6/proofs
Apr 11 00:00:04 Finished compiler/encoders/arm6/proofs                        11m56s   3GB
Apr 11 00:00:04 Starting compiler/encoders/arm8/proofs
Apr 11 00:05:27 Finished compiler/encoders/arm8/proofs                         5m22s   1GB
Apr 11 00:05:27 Starting compiler/encoders/mips/proofs
Apr 11 00:14:46 Finished compiler/encoders/mips/proofs                         9m18s   2GB
Apr 11 00:14:46 Starting compiler/encoders/riscv/proofs
Apr 11 00:23:00 Finished compiler/encoders/riscv/proofs                        8m13s   1GB
Apr 11 00:23:00 Starting compiler/encoders/ag32/proofs
Apr 11 00:25:28 Finished compiler/encoders/ag32/proofs                         2m27s 724MB
Apr 11 00:25:29 Starting compiler/backend/x64/proofs
Apr 11 00:25:48 Finished compiler/backend/x64/proofs                             19s   1GB
Apr 11 00:25:49 Starting compiler/backend/arm6/proofs
Apr 11 00:26:11 Finished compiler/backend/arm6/proofs                            22s   1GB
Apr 11 00:26:11 Starting compiler/backend/arm8/proofs
Apr 11 00:26:30 Finished compiler/backend/arm8/proofs                            18s 789MB
Apr 11 00:26:30 Starting compiler/backend/mips/proofs
Apr 11 00:26:50 Finished compiler/backend/mips/proofs                            20s 829MB
Apr 11 00:26:50 Starting compiler/backend/riscv/proofs
Apr 11 00:27:11 Finished compiler/backend/riscv/proofs                           19s   1GB
Apr 11 00:27:11 Starting compiler/backend/ag32/proofs
Apr 11 00:35:47 Finished compiler/backend/ag32/proofs                          8m36s   2GB
Apr 11 00:35:47 Starting compiler/proofs
Apr 11 00:37:28 Finished compiler/proofs                                       1m39s   2GB
Apr 11 00:37:28 Starting candle/set-theory
Apr 11 00:37:55 Finished candle/set-theory                                       26s 657MB
Apr 11 00:37:55 Starting candle/syntax-lib
Apr 11 00:38:06 Finished candle/syntax-lib                                       10s 675MB
Apr 11 00:38:06 Starting candle/standard/syntax
Apr 11 00:39:52 Finished candle/standard/syntax                                1m44s   1GB
Apr 11 00:39:52 Starting candle/standard/semantics
Apr 11 00:41:29 Finished candle/standard/semantics                             1m37s   1GB
Apr 11 00:41:30 Starting candle/standard/monadic
Apr 11 00:43:03 Finished candle/standard/monadic                               1m33s   1GB
Apr 11 00:43:04 Starting candle/standard/ml_kernel
Apr 11 00:46:52 Finished candle/standard/ml_kernel                             3m48s   3GB
Apr 11 00:46:52 Starting candle/standard/opentheory
Apr 11 00:50:11 FAILED: candle/standard/opentheory
]0;Holmake: ~/oven/regression/cakeml-784/basis/pure]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languages]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languages/context-free]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: ~/oven/regression/cakeml-784/basis/pure]0;Holmake: ~/oven/regression/cakeml-784/misc]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ~/oven/regression/cakeml-784/misc]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/machine-code/hoare-triple]0;Holmake: ~/oven/regression/HOL-729baf5e526741114f4346767d17d0da3a1b6c20/examples/machine-code/hoare-tripleWorking in $(HOLDIR)/examples/machine-code/hoare-triple
]0;Holmake: ~/oven/regression/cakeml-784/misc]0;Holmake: ~/oven/regression/cakeml-784/developers]0;Holmake: ~/oven/regression/cakeml-784/developersWorking in $(CAKEMLDIR)/developers
]0;Holmake: ~/oven/regression/cakeml-784/misc]0;Holmake: ~/oven/regression/cakeml-784/misc/lem_lib_stub]0;Holmake: ~/oven/regression/cakeml-784/misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ~/oven/regression/cakeml-784/misc]0;Holmake: ~/oven/regression/cakeml-784/miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: ~/oven/regression/cakeml-784/basis/pure]0;Holmake: ~/oven/regression/cakeml-784/basis/pureWorking in $(CAKEMLDIR)/basis/pure
]0;Holmake: ~/oven/regression/cakeml-784/basis]0;Holmake: ~/oven/regression/cakeml-784/characteristic]0;Holmake: ~/oven/regression/cakeml-784/compiler/parsing]0;Holmake: ~/oven/regression/cakeml-784/semantics]0;Holmake: ~/oven/regression/cakeml-784/semantics/ffi]0;Holmake: ~/oven/regression/cakeml-784/semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: ~/oven/regression/cakeml-784/semantics]0;Holmake: ~/oven/regression/cakeml-784/semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: ~/oven/regression/cakeml-784/compiler/parsing]0;Holmake: ~/oven/regression/cakeml-784/compiler/parsingWorking in $(CAKEMLDIR)/compiler/parsing
]0;Holmake: ~/oven/regression/cakeml-784/characteristic]0;Holmake: ~/oven/regression/cakeml-784/semantics/proofs]0;Holmake: ~/oven/regression/cakeml-784/semantics/proofsWorking in $(CAKEMLDIR)/semantics/proofs
]0;Holmake: ~/oven/regression/cakeml-784/characteristic]0;Holmake: ~/oven/regression/cakeml-784/translator]0;Holmake: ~/oven/regression/cakeml-784/translatorWorking in $(CAKEMLDIR)/translator
]0;Holmake: ~/oven/regression/cakeml-784/characteristic]0;Holmake: ~/oven/regression/cakeml-784/characteristicWorking in $(CAKEMLDIR)/characteristic
]0;Holmake: ~/oven/regression/cakeml-784/basis]0;Holmake: ~/oven/regression/cakeml-784/translator/monadic]0;Holmake: ~/oven/regression/cakeml-784/translator/monadic/monad_base]0;Holmake: ~/oven/regression/cakeml-784/translator/monadic/monad_baseWorking in $(CAKEMLDIR)/translator/monadic/monad_base
]0;Holmake: ~/oven/regression/cakeml-784/translator/monadic]0;Holmake: ~/oven/regression/cakeml-784/translator/monadicWorking in $(CAKEMLDIR)/translator/monadic
]0;Holmake: ~/oven/regression/cakeml-784/basis]0;Holmake: ~/oven/regression/cakeml-784/basisWorking in $(CAKEMLDIR)/basis
]0;Holmake: .]0;Holmake: ../ml_kernel]0;Holmake: ../monadic]0;Holmake: ../syntax]0;Holmake: ../../syntax-lib]0;Holmake: ../../syntax-libWorking in $(CAKEMLDIR)/candle/syntax-lib
]0;Holmake: ../syntax]0;Holmake: ../syntaxWorking in $(CAKEMLDIR)/candle/standard/syntax
]0;Holmake: ../monadic]0;Holmake: ../monadicWorking in $(CAKEMLDIR)/candle/standard/monadic
]0;Holmake: ../ml_kernel]0;Holmake: ../ml_kernelWorking in $(CAKEMLDIR)/candle/standard/ml_kernel
]0;Holmake: .]0;Holmake: ../semantics]0;Holmake: ../../set-theory]0;Holmake: ../../set-theoryWorking in $(CAKEMLDIR)/candle/set-theory
]0;Holmake: ../semantics]0;Holmake: ../semanticsWorking in $(CAKEMLDIR)/candle/standard/semantics
]0;Holmake: .]0;Holmake: .Working in $(CAKEMLDIR)/candle/standard/opentheory
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>
 error in quse /home/cake/oven/regression/cakeml-784/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 = "??"}
 <<HOL message: Created theory "reader_commonProg">>
 Loading monadic translator state from: ml_hol_kernelProg... Uncaught exception: HOL_ERR {message = "Could not load translator state.", origin_function = "failwith", origin_structure = "??"}