Job 1006

CakeML:a8c6c8bfac053932e7c9a1a1bea5053bdad55faa
  Fix drule breakages in compiler/backend/ag32/proofs [Aug 17 02:01:47]
HOL:8cc876e8e492e4f4045670ff53549a04cf1fdc65
  Further document drule breakage by linking to CakeML's old_drule [Aug 16 01:09:50]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Aug 17 02:05:12 Claimed job
Aug 17 02:05:15 Reusing HOL
Aug 17 02:06:07 Starting developers
Aug 17 02:06:09 Finished developers                                               2s  21MB
Aug 17 02:06:09 Starting developers/bin
Aug 17 02:06:16 Finished developers/bin                                           6s 960MB
Aug 17 02:06:16 Starting semantics/ffi
Aug 17 02:06:26 Finished semantics/ffi                                           10s 226MB
Aug 17 02:06:27 Starting semantics
Aug 17 02:07:48 Finished semantics                                             1m20s   1GB
Aug 17 02:07:48 Starting semantics/proofs
Aug 17 02:10:47 Finished semantics/proofs                                      2m58s   1GB
Aug 17 02:10:47 Starting semantics/alt_semantics
Aug 17 02:10:55 Finished semantics/alt_semantics                                  7s 278MB
Aug 17 02:10:55 Starting semantics/alt_semantics/proofs
Aug 17 02:12:45 Finished semantics/alt_semantics/proofs                        1m49s 772MB
Aug 17 02:12:45 Starting basis/pure
Aug 17 02:13:32 Finished basis/pure                                              46s 612MB
Aug 17 02:13:32 Starting translator
Aug 17 02:15:20 Finished translator                                            1m47s   1GB
Aug 17 02:15:20 Starting compiler/parsing
Aug 17 02:16:17 Finished compiler/parsing                                        56s   1GB
Aug 17 02:16:17 Starting characteristic
Aug 17 02:21:35 Finished characteristic                                        5m17s   1GB
Aug 17 02:21:35 Starting translator/monadic
Aug 17 02:23:05 Finished translator/monadic                                    1m29s   1GB
Aug 17 02:23:05 Starting basis
Aug 17 02:40:59 Finished basis                                                17m53s   2GB
Aug 17 02:40:59 Starting compiler/inference
Aug 17 02:42:36 Finished compiler/inference                                    1m36s   1GB
Aug 17 02:42:36 Starting compiler/backend/reg_alloc
Aug 17 02:43:36 Finished compiler/backend/reg_alloc                              59s   1GB
Aug 17 02:43:36 Starting compiler/backend/gc
Aug 17 02:51:48 Finished compiler/backend/gc                                   8m11s   2GB
Aug 17 02:51:48 Starting compiler/backend
Aug 17 02:51:51 Finished compiler/backend                                         2s  18MB
Aug 17 02:51:51 Starting compiler/encoders/asm
Aug 17 02:51:53 Finished compiler/encoders/asm                                    1s  11MB
Aug 17 02:51:53 Starting compiler/encoders/x64
Aug 17 02:52:18 Finished compiler/encoders/x64                                   25s 954MB
Aug 17 02:52:18 Starting compiler/encoders/arm7
Aug 17 02:53:05 Finished compiler/encoders/arm7                                  46s 727MB
Aug 17 02:53:05 Starting compiler/encoders/arm8
Aug 17 02:53:19 Finished compiler/encoders/arm8                                  13s 532MB
Aug 17 02:53:19 Starting compiler/encoders/mips
Aug 17 02:53:37 Finished compiler/encoders/mips                                  17s 872MB
Aug 17 02:53:37 Starting compiler/encoders/riscv
Aug 17 02:53:52 Finished compiler/encoders/riscv                                 14s 897MB
Aug 17 02:53:52 Starting compiler/encoders/ag32
Aug 17 02:54:09 Finished compiler/encoders/ag32                                  17s 774MB
Aug 17 02:54:10 Starting compiler/backend/x64
Aug 17 02:54:28 Finished compiler/backend/x64                                    18s   1GB
Aug 17 02:54:28 Starting compiler/backend/arm7
Aug 17 02:54:49 Finished compiler/backend/arm7                                   20s   1GB
Aug 17 02:54:49 Starting compiler/backend/arm8
Aug 17 02:55:08 Finished compiler/backend/arm8                                   18s   1GB
Aug 17 02:55:08 Starting compiler/backend/mips
Aug 17 02:55:27 Finished compiler/backend/mips                                   18s   1GB
Aug 17 02:55:27 Starting compiler/backend/riscv
Aug 17 02:55:46 Finished compiler/backend/riscv                                  18s   1GB
Aug 17 02:55:46 Starting compiler/backend/ag32
Aug 17 02:56:55 Finished compiler/backend/ag32                                 1m08s   1GB
Aug 17 02:56:55 Starting compiler/parsing/proofs
Aug 17 03:02:28 Finished compiler/parsing/proofs                               5m32s   1GB
Aug 17 03:02:28 Starting compiler/inference/proofs
Aug 17 03:05:14 Finished compiler/inference/proofs                             2m45s   1GB
Aug 17 03:05:14 Starting compiler/backend/semantics
Aug 17 03:12:20 Finished compiler/backend/semantics                            7m06s   1GB
Aug 17 03:12:21 Starting compiler/backend/reg_alloc/proofs
Aug 17 03:15:34 Finished compiler/backend/reg_alloc/proofs                     3m13s 747MB
Aug 17 03:15:34 Starting compiler/backend/proofs
Aug 17 03:54:11 Finished compiler/backend/proofs                              38m35s   5GB
Aug 17 03:54:11 Starting compiler/encoders/x64/proofs
Aug 17 04:03:03 Finished compiler/encoders/x64/proofs                          8m52s   5GB
Aug 17 04:03:04 Starting compiler/encoders/arm7/proofs
Aug 17 04:15:17 Finished compiler/encoders/arm7/proofs                        12m12s   3GB
Aug 17 04:15:17 Starting compiler/encoders/arm8/proofs
Aug 17 04:21:40 Finished compiler/encoders/arm8/proofs                         6m22s   1GB
Aug 17 04:21:40 Starting compiler/encoders/mips/proofs
Aug 17 04:31:04 Finished compiler/encoders/mips/proofs                         9m23s   2GB
Aug 17 04:31:04 Starting compiler/encoders/riscv/proofs
Aug 17 04:39:18 Finished compiler/encoders/riscv/proofs                        8m14s 959MB
Aug 17 04:39:18 Starting compiler/encoders/ag32/proofs
Aug 17 04:41:44 Finished compiler/encoders/ag32/proofs                         2m25s 811MB
Aug 17 04:41:44 Starting compiler/backend/x64/proofs
Aug 17 04:42:04 Finished compiler/backend/x64/proofs                             20s   1GB
Aug 17 04:42:04 Starting compiler/backend/arm7/proofs
Aug 17 04:42:25 Finished compiler/backend/arm7/proofs                            20s 788MB
Aug 17 04:42:25 Starting compiler/backend/arm8/proofs
Aug 17 04:42:45 Finished compiler/backend/arm8/proofs                            19s   1GB
Aug 17 04:42:45 Starting compiler/backend/mips/proofs
Aug 17 04:43:05 Finished compiler/backend/mips/proofs                            19s 949MB
Aug 17 04:43:05 Starting compiler/backend/riscv/proofs
Aug 17 04:43:25 Finished compiler/backend/riscv/proofs                           19s   1GB
Aug 17 04:43:25 Starting compiler/backend/ag32/proofs
Aug 17 04:52:07 Finished compiler/backend/ag32/proofs                          8m41s   2GB
Aug 17 04:52:07 Starting compiler/proofs
Aug 17 04:53:29 Finished compiler/proofs                                       1m21s   2GB
Aug 17 04:53:29 Starting candle/set-theory
Aug 17 04:53:56 Finished candle/set-theory                                       26s 685MB
Aug 17 04:53:56 Starting candle/syntax-lib
Aug 17 04:54:07 Finished candle/syntax-lib                                       10s 622MB
Aug 17 04:54:07 Starting candle/standard/syntax
Aug 17 04:55:51 Finished candle/standard/syntax                                1m43s   1GB
Aug 17 04:55:51 Starting candle/standard/semantics
Aug 17 04:57:28 Finished candle/standard/semantics                             1m37s   1GB
Aug 17 04:57:28 Starting candle/standard/monadic
Aug 17 04:59:01 Finished candle/standard/monadic                               1m32s   1GB
Aug 17 04:59:01 Starting candle/standard/ml_kernel
Aug 17 05:02:47 Finished candle/standard/ml_kernel                             3m45s   3GB
Aug 17 05:02:48 Starting candle/standard/opentheory
Aug 17 05:04:59 FAILED: candle/standard/opentheory
]0;Holmake: ~/oven/regression/cakeml-1006/basis/pure]0;Holmake: ~/oven/regression/HOL-8cc876e8e492e4f4045670ff53549a04cf1fdc65/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-8cc876e8e492e4f4045670ff53549a04cf1fdc65/examples/formal-languages]0;Holmake: ~/oven/regression/HOL-8cc876e8e492e4f4045670ff53549a04cf1fdc65/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: ~/oven/regression/HOL-8cc876e8e492e4f4045670ff53549a04cf1fdc65/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-8cc876e8e492e4f4045670ff53549a04cf1fdc65/examples/formal-languages/context-free]0;Holmake: ~/oven/regression/HOL-8cc876e8e492e4f4045670ff53549a04cf1fdc65/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: ~/oven/regression/HOL-8cc876e8e492e4f4045670ff53549a04cf1fdc65/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-8cc876e8e492e4f4045670ff53549a04cf1fdc65/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: ~/oven/regression/cakeml-1006/basis/pure]0;Holmake: ~/oven/regression/cakeml-1006/misc]0;Holmake: ~/oven/regression/HOL-8cc876e8e492e4f4045670ff53549a04cf1fdc65/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/oven/regression/HOL-8cc876e8e492e4f4045670ff53549a04cf1fdc65/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ~/oven/regression/cakeml-1006/misc]0;Holmake: ~/oven/regression/HOL-8cc876e8e492e4f4045670ff53549a04cf1fdc65/examples/machine-code/hoare-triple]0;Holmake: ~/oven/regression/HOL-8cc876e8e492e4f4045670ff53549a04cf1fdc65/examples/machine-code/hoare-tripleWorking in $(HOLDIR)/examples/machine-code/hoare-triple
]0;Holmake: ~/oven/regression/cakeml-1006/misc]0;Holmake: ~/oven/regression/cakeml-1006/developers]0;Holmake: ~/oven/regression/cakeml-1006/developersWorking in $(CAKEMLDIR)/developers
]0;Holmake: ~/oven/regression/cakeml-1006/misc]0;Holmake: ~/oven/regression/cakeml-1006/misc/lem_lib_stub]0;Holmake: ~/oven/regression/cakeml-1006/misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ~/oven/regression/cakeml-1006/misc]0;Holmake: ~/oven/regression/cakeml-1006/miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: ~/oven/regression/cakeml-1006/basis/pure]0;Holmake: ~/oven/regression/cakeml-1006/basis/pureWorking in $(CAKEMLDIR)/basis/pure
]0;Holmake: ~/oven/regression/cakeml-1006/basis]0;Holmake: ~/oven/regression/cakeml-1006/characteristic]0;Holmake: ~/oven/regression/cakeml-1006/compiler/parsing]0;Holmake: ~/oven/regression/cakeml-1006/semantics]0;Holmake: ~/oven/regression/cakeml-1006/semantics/ffi]0;Holmake: ~/oven/regression/cakeml-1006/semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: ~/oven/regression/cakeml-1006/semantics]0;Holmake: ~/oven/regression/cakeml-1006/semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: ~/oven/regression/cakeml-1006/compiler/parsing]0;Holmake: ~/oven/regression/cakeml-1006/compiler/parsingWorking in $(CAKEMLDIR)/compiler/parsing
]0;Holmake: ~/oven/regression/cakeml-1006/characteristic]0;Holmake: ~/oven/regression/cakeml-1006/semantics/proofs]0;Holmake: ~/oven/regression/cakeml-1006/semantics/proofsWorking in $(CAKEMLDIR)/semantics/proofs
]0;Holmake: ~/oven/regression/cakeml-1006/characteristic]0;Holmake: ~/oven/regression/cakeml-1006/translator]0;Holmake: ~/oven/regression/cakeml-1006/translatorWorking in $(CAKEMLDIR)/translator
]0;Holmake: ~/oven/regression/cakeml-1006/characteristic]0;Holmake: ~/oven/regression/cakeml-1006/characteristicWorking in $(CAKEMLDIR)/characteristic
]0;Holmake: ~/oven/regression/cakeml-1006/basis]0;Holmake: ~/oven/regression/cakeml-1006/translator/monadic]0;Holmake: ~/oven/regression/cakeml-1006/translator/monadic/monad_base]0;Holmake: ~/oven/regression/cakeml-1006/translator/monadic/monad_baseWorking in $(CAKEMLDIR)/translator/monadic/monad_base
]0;Holmake: ~/oven/regression/cakeml-1006/translator/monadic]0;Holmake: ~/oven/regression/cakeml-1006/translator/monadicWorking in $(CAKEMLDIR)/translator/monadic
]0;Holmake: ~/oven/regression/cakeml-1006/basis]0;Holmake: ~/oven/regression/cakeml-1006/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                                                   FAILED! <1>
 Proof of 
 
 STATE defs refs  READER_STATE defs st  readLine line st refs = (res,refs') 
 ds.
     STATE (ds ++ defs) refs' 
     st'. res = Success st'  READER_STATE (ds ++ defs) st'
 
 failed.
 Failed to prove theorem readLine_thm.
 Uncaught exception: HOL_ERR {message = "no solution found (THEN1 on line 1075) (THEN1 on line 1105) (THEN1 on line 1114) (THEN1 on line 1123) (THEN1 on line 1128) (THEN1 on line 1137) (THEN1 on line 1143) (THEN1 on line 1150) (THEN1 on line 1159) (THEN1 on line 1168) (THEN1 on line 1176) (THEN1 on line 1185) (THEN1 on line 1199) (THEN1 on line 1207) (THEN1 on line 1216) (THEN1 on line 1225) (THEN1 on line 1232) (THEN1 on line 1242) (THEN1 on line 1251)", origin_function = "FOL_FIND", origin_structure = "folTools"}