Job 696

CakeML:d3bfdc58453ce290becb584aaa04f4085e2a9c5c
  Replace an xlet_auto with a manual xlet [Jan 22 13:41:08]
#609 (cf-div-io)
Merging into:132124a020e9f4e4bb00fb0274f9505461195904
  Merge pull request #608 from CakeML/cheats [Jan 21 17:46:50]
HOL:ce7414f3a9b67a55c010a5194ca0029e347b7810
  More easily moved theorems from CakeML (this time to finite_map) [Jan 17 00:42:39]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Jan 22 14:31:14 Claimed job
Jan 22 14:31:19 Reusing HOL
Jan 22 14:31:29 Starting developers
Jan 22 14:31:31 Finished developers                                               0s  38MB
Jan 22 14:31:31 Starting developers/bin
Jan 22 14:32:04 Finished developers/bin                                          31s 142MB
Jan 22 14:32:05 Starting semantics/ffi
Jan 22 14:32:13 Finished semantics/ffi                                            7s 224MB
Jan 22 14:32:14 Starting semantics
Jan 22 14:33:34 Finished semantics                                             1m19s   1GB
Jan 22 14:33:35 Starting semantics/proofs
Jan 22 14:36:51 Finished semantics/proofs                                      3m14s   1GB
Jan 22 14:36:52 Starting basis/pure
Jan 22 14:37:37 Finished basis/pure                                              44s 603MB
Jan 22 14:37:38 Starting translator
Jan 22 14:39:17 Finished translator                                            1m38s   1GB
Jan 22 14:39:18 Starting compiler/parsing
Jan 22 14:40:22 Finished compiler/parsing                                      1m03s   2GB
Jan 22 14:40:23 Starting characteristic
Jan 22 14:44:47 Finished characteristic                                        4m22s   1GB
Jan 22 14:44:47 Starting translator/monadic
Jan 22 14:46:12 Finished translator/monadic                                    1m23s   1GB
Jan 22 14:46:13 Starting basis
Jan 22 15:03:08 Finished basis                                                16m54s   3GB
Jan 22 15:03:09 Starting compiler/inference
Jan 22 15:04:46 Finished compiler/inference                                    1m36s   1GB
Jan 22 15:04:47 Starting compiler/backend/reg_alloc
Jan 22 15:05:38 Finished compiler/backend/reg_alloc                              50s   1GB
Jan 22 15:05:39 Starting compiler/backend/gc
Jan 22 15:13:32 Finished compiler/backend/gc                                   7m52s   2GB
Jan 22 15:13:33 Starting compiler/backend
Jan 22 15:13:36 Finished compiler/backend                                         1s  17MB
Jan 22 15:13:36 Starting compiler/encoders/asm
Jan 22 15:13:38 Finished compiler/encoders/asm                                    0s  16MB
Jan 22 15:13:39 Starting compiler/encoders/x64
Jan 22 15:14:03 Finished compiler/encoders/x64                                   23s 913MB
Jan 22 15:14:04 Starting compiler/encoders/arm6
Jan 22 15:14:56 Finished compiler/encoders/arm6                                  50s 950MB
Jan 22 15:14:56 Starting compiler/encoders/arm8
Jan 22 15:15:10 Finished compiler/encoders/arm8                                  12s 841MB
Jan 22 15:15:10 Starting compiler/encoders/mips
Jan 22 15:15:28 Finished compiler/encoders/mips                                  16s   1GB
Jan 22 15:15:28 Starting compiler/encoders/riscv
Jan 22 15:15:43 Finished compiler/encoders/riscv                                 13s 771MB
Jan 22 15:15:43 Starting compiler/encoders/ag32
Jan 22 15:16:00 Finished compiler/encoders/ag32                                  16s 780MB
Jan 22 15:16:01 Starting compiler/backend/x64
Jan 22 15:16:18 Finished compiler/backend/x64                                    15s 802MB
Jan 22 15:16:18 Starting compiler/backend/arm6
Jan 22 15:16:38 Finished compiler/backend/arm6                                   18s   1GB
Jan 22 15:16:39 Starting compiler/backend/arm8
Jan 22 15:16:56 Finished compiler/backend/arm8                                   16s   1GB
Jan 22 15:16:57 Starting compiler/backend/mips
Jan 22 15:17:15 Finished compiler/backend/mips                                   17s   1GB
Jan 22 15:17:16 Starting compiler/backend/riscv
Jan 22 15:17:33 Finished compiler/backend/riscv                                  16s 898MB
Jan 22 15:17:34 Starting compiler/backend/ag32
Jan 22 15:18:49 Finished compiler/backend/ag32                                 1m13s   1GB
Jan 22 15:18:50 Starting compiler/parsing/proofs
Jan 22 15:24:43 Finished compiler/parsing/proofs                               5m52s   1GB
Jan 22 15:24:43 Starting compiler/inference/proofs
Jan 22 15:27:39 Finished compiler/inference/proofs                             2m54s   1GB
Jan 22 15:27:40 Starting compiler/backend/semantics
Jan 22 15:35:11 Finished compiler/backend/semantics                            7m30s   2GB
Jan 22 15:35:12 Starting compiler/backend/reg_alloc/proofs
Jan 22 15:37:56 Finished compiler/backend/reg_alloc/proofs                     2m43s   1GB
Jan 22 15:37:57 Starting compiler/backend/proofs
Jan 22 16:16:57 Finished compiler/backend/proofs                              38m59s   3GB
Jan 22 16:16:58 Starting compiler/encoders/x64/proofs
Jan 22 16:26:46 Finished compiler/encoders/x64/proofs                          9m47s   6GB
Jan 22 16:26:47 Starting compiler/encoders/arm6/proofs
Jan 22 16:40:54 Finished compiler/encoders/arm6/proofs                        14m06s   3GB
Jan 22 16:40:55 Starting compiler/encoders/arm8/proofs
Jan 22 16:46:56 Finished compiler/encoders/arm8/proofs                         6m00s   1GB
Jan 22 16:46:56 Starting compiler/encoders/mips/proofs
Jan 22 16:57:32 Finished compiler/encoders/mips/proofs                        10m34s   2GB
Jan 22 16:57:33 Starting compiler/encoders/riscv/proofs
Jan 22 17:05:20 Finished compiler/encoders/riscv/proofs                        7m46s   1GB
Jan 22 17:05:20 Starting compiler/encoders/ag32/proofs
Jan 22 17:08:03 Finished compiler/encoders/ag32/proofs                         2m40s 913MB
Jan 22 17:08:04 Starting compiler/backend/x64/proofs
Jan 22 17:08:24 Finished compiler/backend/x64/proofs                             18s   1GB
Jan 22 17:08:24 Starting compiler/backend/arm6/proofs
Jan 22 17:08:45 Finished compiler/backend/arm6/proofs                            20s   1GB
Jan 22 17:08:46 Starting compiler/backend/arm8/proofs
Jan 22 17:09:05 Finished compiler/backend/arm8/proofs                            18s   1GB
Jan 22 17:09:06 Starting compiler/backend/mips/proofs
Jan 22 17:09:26 Finished compiler/backend/mips/proofs                            18s   1GB
Jan 22 17:09:26 Starting compiler/backend/riscv/proofs
Jan 22 17:09:46 Finished compiler/backend/riscv/proofs                           19s   1GB
Jan 22 17:09:47 Starting compiler/backend/ag32/proofs
Jan 22 17:19:18 Finished compiler/backend/ag32/proofs                          9m29s   2GB
Jan 22 17:19:18 Starting compiler/proofs
Jan 22 17:20:40 Finished compiler/proofs                                       1m21s   3GB
Jan 22 17:20:41 Starting candle/set-theory
Jan 22 17:21:08 Finished candle/set-theory                                       26s 693MB
Jan 22 17:21:09 Starting candle/syntax-lib
Jan 22 17:21:19 Finished candle/syntax-lib                                        9s 639MB
Jan 22 17:21:20 Starting candle/standard/syntax
Jan 22 17:23:08 Finished candle/standard/syntax                                1m47s   1GB
Jan 22 17:23:09 Starting candle/standard/semantics
Jan 22 17:24:48 Finished candle/standard/semantics                             1m38s   1GB
Jan 22 17:24:49 Starting candle/standard/monadic
Jan 22 17:26:30 Finished candle/standard/monadic                               1m40s   1GB
Jan 22 17:26:31 Starting candle/standard/ml_kernel
Jan 22 17:30:31 Finished candle/standard/ml_kernel                             3m59s   4GB
Jan 22 17:30:32 Starting candle/standard/opentheory
Jan 22 17:37:41 FAILED: candle/standard/opentheory
]0;Holmake: ~/regression/cakeml-696/basis/pure]0;Holmake: ~/regression/HOL-ce7414f3a9b67a55c010a5194ca0029e347b7810/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-ce7414f3a9b67a55c010a5194ca0029e347b7810/examples/formal-languages]0;Holmake: ~/regression/HOL-ce7414f3a9b67a55c010a5194ca0029e347b7810/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-ce7414f3a9b67a55c010a5194ca0029e347b7810/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-ce7414f3a9b67a55c010a5194ca0029e347b7810/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-ce7414f3a9b67a55c010a5194ca0029e347b7810/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-ce7414f3a9b67a55c010a5194ca0029e347b7810/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-ce7414f3a9b67a55c010a5194ca0029e347b7810/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ~/regression/cakeml-696/basis/pure]0;Holmake: ~/regression/cakeml-696/misc]0;Holmake: ~/regression/HOL-ce7414f3a9b67a55c010a5194ca0029e347b7810/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-ce7414f3a9b67a55c010a5194ca0029e347b7810/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-696/misc]0;Holmake: ~/regression/HOL-ce7414f3a9b67a55c010a5194ca0029e347b7810/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-ce7414f3a9b67a55c010a5194ca0029e347b7810/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/regression/cakeml-696/misc]0;Holmake: ~/regression/cakeml-696/developers]0;Holmake: ~/regression/cakeml-696/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-696/misc]0;Holmake: ~/regression/cakeml-696/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-696/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-696/misc]0;Holmake: ~/regression/cakeml-696/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression/cakeml-696/basis/pure]0;Holmake: ~/regression/cakeml-696/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ~/regression/cakeml-696/basis]0;Holmake: ~/regression/cakeml-696/characteristic]0;Holmake: ~/regression/cakeml-696/compiler/parsing]0;Holmake: ~/regression/cakeml-696/semantics]0;Holmake: ~/regression/cakeml-696/semantics/ffi]0;Holmake: ~/regression/cakeml-696/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-696/semantics]0;Holmake: ~/regression/cakeml-696/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression/cakeml-696/compiler/parsing]0;Holmake: ~/regression/cakeml-696/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/regression/cakeml-696/characteristic]0;Holmake: ~/regression/cakeml-696/semantics/proofs]0;Holmake: ~/regression/cakeml-696/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ~/regression/cakeml-696/characteristic]0;Holmake: ~/regression/cakeml-696/translator]0;Holmake: ~/regression/cakeml-696/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/regression/cakeml-696/characteristic]0;Holmake: ~/regression/cakeml-696/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ~/regression/cakeml-696/basis]0;Holmake: ~/regression/cakeml-696/translator/monadic]0;Holmake: ~/regression/cakeml-696/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-696/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ~/regression/cakeml-696/translator/monadic]0;Holmake: ~/regression/cakeml-696/translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ~/regression/cakeml-696/basis]0;Holmake: ~/regression/cakeml-696/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                                                                                    OK
Starting work on readerProgTheory
readerProgTheory                                                                                  FAILED! <1>
 READER_STATE_TYPE st stv  STRING_TYPE ln lnv 
 app p process_line_v [stv; lnv] (HOL_STORE refs)
   (POSTv stv.
        HOL_STORE (SND (process_line st refs ln)) *
        &SUM_TYPE READER_STATE_TYPE STRING_TYPE
          (FST (process_line st refs ln)) stv)
 
 failed.
 Failed to prove theorem process_line_spec.
 Uncaught exception: HOL_ERR {message = "QCHANGED_CONSEQ_CONV (THEN1 on line 66) (THEN1 on line 55) (THEN1 on line 72)", origin_function = "ConseqConv", origin_structure = "bool"}