Overview

Job 1006

CakeML:a8c6c8bfac053932e7c9a1a1bea5053bdad55faa
  Fix drule breakages in compiler/backend/ag32/proofs
HOL:8cc876e8e492e4f4045670ff53549a04cf1fdc65
  Further document drule breakage by linking to CakeML's old_drule
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

 Claimed job
 Reusing HOL
 Starting developers
 Finished developers                                               2s  21MB
 Starting developers/bin
 Finished developers/bin                                           6s 960MB
 Starting semantics/ffi
 Finished semantics/ffi                                           10s 226MB
 Starting semantics
 Finished semantics                                             1m20s   1GB
 Starting semantics/proofs
 Finished semantics/proofs                                      2m58s   1GB
 Starting semantics/alt_semantics
 Finished semantics/alt_semantics                                  7s 278MB
 Starting semantics/alt_semantics/proofs
 Finished semantics/alt_semantics/proofs                        1m49s 772MB
 Starting basis/pure
 Finished basis/pure                                              46s 612MB
 Starting translator
 Finished translator                                            1m47s   1GB
 Starting compiler/parsing
 Finished compiler/parsing                                        56s   1GB
 Starting characteristic
 Finished characteristic                                        5m17s   1GB
 Starting translator/monadic
 Finished translator/monadic                                    1m29s   1GB
 Starting basis
 Finished basis                                                17m53s   2GB
 Starting compiler/inference
 Finished compiler/inference                                    1m36s   1GB
 Starting compiler/backend/reg_alloc
 Finished compiler/backend/reg_alloc                              59s   1GB
 Starting compiler/backend/gc
 Finished compiler/backend/gc                                   8m11s   2GB
 Starting compiler/backend
 Finished compiler/backend                                         2s  18MB
 Starting compiler/encoders/asm
 Finished compiler/encoders/asm                                    1s  11MB
 Starting compiler/encoders/x64
 Finished compiler/encoders/x64                                   25s 954MB
 Starting compiler/encoders/arm7
 Finished compiler/encoders/arm7                                  46s 727MB
 Starting compiler/encoders/arm8
 Finished compiler/encoders/arm8                                  13s 532MB
 Starting compiler/encoders/mips
 Finished compiler/encoders/mips                                  17s 872MB
 Starting compiler/encoders/riscv
 Finished compiler/encoders/riscv                                 14s 897MB
 Starting compiler/encoders/ag32
 Finished compiler/encoders/ag32                                  17s 774MB
 Starting compiler/backend/x64
 Finished compiler/backend/x64                                    18s   1GB
 Starting compiler/backend/arm7
 Finished compiler/backend/arm7                                   20s   1GB
 Starting compiler/backend/arm8
 Finished compiler/backend/arm8                                   18s   1GB
 Starting compiler/backend/mips
 Finished compiler/backend/mips                                   18s   1GB
 Starting compiler/backend/riscv
 Finished compiler/backend/riscv                                  18s   1GB
 Starting compiler/backend/ag32
 Finished compiler/backend/ag32                                 1m08s   1GB
 Starting compiler/parsing/proofs
 Finished compiler/parsing/proofs                               5m32s   1GB
 Starting compiler/inference/proofs
 Finished compiler/inference/proofs                             2m45s   1GB
 Starting compiler/backend/semantics
 Finished compiler/backend/semantics                            7m06s   1GB
 Starting compiler/backend/reg_alloc/proofs
 Finished compiler/backend/reg_alloc/proofs                     3m13s 747MB
 Starting compiler/backend/proofs
 Finished compiler/backend/proofs                              38m35s   5GB
 Starting compiler/encoders/x64/proofs
 Finished compiler/encoders/x64/proofs                          8m52s   5GB
 Starting compiler/encoders/arm7/proofs
 Finished compiler/encoders/arm7/proofs                        12m12s   3GB
 Starting compiler/encoders/arm8/proofs
 Finished compiler/encoders/arm8/proofs                         6m22s   1GB
 Starting compiler/encoders/mips/proofs
 Finished compiler/encoders/mips/proofs                         9m23s   2GB
 Starting compiler/encoders/riscv/proofs
 Finished compiler/encoders/riscv/proofs                        8m14s 959MB
 Starting compiler/encoders/ag32/proofs
 Finished compiler/encoders/ag32/proofs                         2m25s 811MB
 Starting compiler/backend/x64/proofs
 Finished compiler/backend/x64/proofs                             20s   1GB
 Starting compiler/backend/arm7/proofs
 Finished compiler/backend/arm7/proofs                            20s 788MB
 Starting compiler/backend/arm8/proofs
 Finished compiler/backend/arm8/proofs                            19s   1GB
 Starting compiler/backend/mips/proofs
 Finished compiler/backend/mips/proofs                            19s 949MB
 Starting compiler/backend/riscv/proofs
 Finished compiler/backend/riscv/proofs                           19s   1GB
 Starting compiler/backend/ag32/proofs
 Finished compiler/backend/ag32/proofs                          8m41s   2GB
 Starting compiler/proofs
 Finished compiler/proofs                                       1m21s   2GB
 Starting candle/set-theory
 Finished candle/set-theory                                       26s 685MB
 Starting candle/syntax-lib
 Finished candle/syntax-lib                                       10s 622MB
 Starting candle/standard/syntax
 Finished candle/standard/syntax                                1m43s   1GB
 Starting candle/standard/semantics
 Finished candle/standard/semantics                             1m37s   1GB
 Starting candle/standard/monadic
 Finished candle/standard/monadic                               1m32s   1GB
 Starting candle/standard/ml_kernel
 Finished candle/standard/ml_kernel                             3m45s   3GB
 Starting candle/standard/opentheory
 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"}