Job 697

CakeML:bd5e28d245d745cdeb385341cfd108469b694053
  Fix broken proofs in readerProgScript [Jan 22 20:30:06]
#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 20:47:29 Claimed job
Jan 22 20:47:32 Reusing HOL
Jan 22 20:47:42 Starting developers
Jan 22 20:47:43 Finished developers                                               0s  34MB
Jan 22 20:47:44 Starting developers/bin
Jan 22 20:48:17 Finished developers/bin                                          32s 204MB
Jan 22 20:48:17 Starting semantics/ffi
Jan 22 20:48:26 Finished semantics/ffi                                            7s 227MB
Jan 22 20:48:27 Starting semantics
Jan 22 20:49:47 Finished semantics                                             1m19s 921MB
Jan 22 20:49:48 Starting semantics/proofs
Jan 22 20:53:06 Finished semantics/proofs                                      3m16s   1GB
Jan 22 20:53:07 Starting basis/pure
Jan 22 20:53:52 Finished basis/pure                                              44s 727MB
Jan 22 20:53:53 Starting translator
Jan 22 20:55:32 Finished translator                                            1m38s   1GB
Jan 22 20:55:33 Starting compiler/parsing
Jan 22 20:56:36 Finished compiler/parsing                                      1m02s   2GB
Jan 22 20:56:37 Starting characteristic
Jan 22 21:01:01 Finished characteristic                                        4m23s   1GB
Jan 22 21:01:01 Starting translator/monadic
Jan 22 21:02:28 Finished translator/monadic                                    1m25s   1GB
Jan 22 21:02:29 Starting basis
Jan 22 21:19:19 Finished basis                                                16m49s   3GB
Jan 22 21:19:20 Starting compiler/inference
Jan 22 21:20:58 Finished compiler/inference                                    1m37s   1GB
Jan 22 21:20:59 Starting compiler/backend/reg_alloc
Jan 22 21:21:50 Finished compiler/backend/reg_alloc                              50s   1GB
Jan 22 21:21:51 Starting compiler/backend/gc
Jan 22 21:29:38 Finished compiler/backend/gc                                   7m46s   2GB
Jan 22 21:29:39 Starting compiler/backend
Jan 22 21:29:41 Finished compiler/backend                                         1s  17MB
Jan 22 21:29:42 Starting compiler/encoders/asm
Jan 22 21:29:43 Finished compiler/encoders/asm                                    0s  17MB
Jan 22 21:29:44 Starting compiler/encoders/x64
Jan 22 21:30:09 Finished compiler/encoders/x64                                   23s 960MB
Jan 22 21:30:10 Starting compiler/encoders/arm6
Jan 22 21:31:01 Finished compiler/encoders/arm6                                  50s 999MB
Jan 22 21:31:02 Starting compiler/encoders/arm8
Jan 22 21:31:15 Finished compiler/encoders/arm8                                  12s 875MB
Jan 22 21:31:16 Starting compiler/encoders/mips
Jan 22 21:31:32 Finished compiler/encoders/mips                                  15s 798MB
Jan 22 21:31:32 Starting compiler/encoders/riscv
Jan 22 21:31:47 Finished compiler/encoders/riscv                                 13s 865MB
Jan 22 21:31:48 Starting compiler/encoders/ag32
Jan 22 21:32:04 Finished compiler/encoders/ag32                                  15s 775MB
Jan 22 21:32:05 Starting compiler/backend/x64
Jan 22 21:32:23 Finished compiler/backend/x64                                    17s 973MB
Jan 22 21:32:24 Starting compiler/backend/arm6
Jan 22 21:32:42 Finished compiler/backend/arm6                                   17s   1GB
Jan 22 21:32:43 Starting compiler/backend/arm8
Jan 22 21:33:00 Finished compiler/backend/arm8                                   16s 901MB
Jan 22 21:33:01 Starting compiler/backend/mips
Jan 22 21:33:19 Finished compiler/backend/mips                                   17s   1GB
Jan 22 21:33:20 Starting compiler/backend/riscv
Jan 22 21:33:38 Finished compiler/backend/riscv                                  17s   1GB
Jan 22 21:33:39 Starting compiler/backend/ag32
Jan 22 21:34:52 Finished compiler/backend/ag32                                 1m12s 865MB
Jan 22 21:34:52 Starting compiler/parsing/proofs
Jan 22 21:40:48 Finished compiler/parsing/proofs                               5m54s 944MB
Jan 22 21:40:49 Starting compiler/inference/proofs
Jan 22 21:43:43 Finished compiler/inference/proofs                             2m53s 997MB
Jan 22 21:43:43 Starting compiler/backend/semantics
Jan 22 21:51:18 Finished compiler/backend/semantics                            7m33s   1GB
Jan 22 21:51:19 Starting compiler/backend/reg_alloc/proofs
Jan 22 21:54:02 Finished compiler/backend/reg_alloc/proofs                     2m42s 788MB
Jan 22 21:54:03 Starting compiler/backend/proofs
Jan 22 22:33:00 Finished compiler/backend/proofs                              38m55s   4GB
Jan 22 22:33:00 Starting compiler/encoders/x64/proofs
Jan 22 22:42:52 Finished compiler/encoders/x64/proofs                          9m50s   4GB
Jan 22 22:42:53 Starting compiler/encoders/arm6/proofs
Jan 22 22:56:56 Finished compiler/encoders/arm6/proofs                        14m02s   3GB
Jan 22 22:56:57 Starting compiler/encoders/arm8/proofs
Jan 22 23:02:58 Finished compiler/encoders/arm8/proofs                         5m59s   1GB
Jan 22 23:02:59 Starting compiler/encoders/mips/proofs
Jan 22 23:13:43 Finished compiler/encoders/mips/proofs                        10m42s   2GB
Jan 22 23:13:43 Starting compiler/encoders/riscv/proofs
Jan 22 23:21:45 Finished compiler/encoders/riscv/proofs                        8m00s 990MB
Jan 22 23:21:45 Starting compiler/encoders/ag32/proofs
Jan 22 23:24:30 Finished compiler/encoders/ag32/proofs                         2m43s 947MB
Jan 22 23:24:31 Starting compiler/backend/x64/proofs
Jan 22 23:24:50 Finished compiler/backend/x64/proofs                             18s   1GB
Jan 22 23:24:51 Starting compiler/backend/arm6/proofs
Jan 22 23:25:13 Finished compiler/backend/arm6/proofs                            21s   1GB
Jan 22 23:25:14 Starting compiler/backend/arm8/proofs
Jan 22 23:25:32 Finished compiler/backend/arm8/proofs                            17s 888MB
Jan 22 23:25:33 Starting compiler/backend/mips/proofs
Jan 22 23:25:54 Finished compiler/backend/mips/proofs                            19s   1GB
Jan 22 23:25:55 Starting compiler/backend/riscv/proofs
Jan 22 23:26:14 Finished compiler/backend/riscv/proofs                           18s 966MB
Jan 22 23:26:15 Starting compiler/backend/ag32/proofs
Jan 22 23:35:54 Finished compiler/backend/ag32/proofs                          9m37s   2GB
Jan 22 23:35:54 Starting compiler/proofs
Jan 22 23:37:15 Finished compiler/proofs                                       1m19s   2GB
Jan 22 23:37:16 Starting candle/set-theory
Jan 22 23:37:42 Finished candle/set-theory                                       25s 689MB
Jan 22 23:37:43 Starting candle/syntax-lib
Jan 22 23:37:53 Finished candle/syntax-lib                                        9s 612MB
Jan 22 23:37:54 Starting candle/standard/syntax
Jan 22 23:39:42 Finished candle/standard/syntax                                1m46s 852MB
Jan 22 23:39:42 Starting candle/standard/semantics
Jan 22 23:41:21 Finished candle/standard/semantics                             1m37s   1GB
Jan 22 23:41:21 Starting candle/standard/monadic
Jan 22 23:43:04 Finished candle/standard/monadic                               1m41s   1GB
Jan 22 23:43:05 Starting candle/standard/ml_kernel
Jan 22 23:47:03 Finished candle/standard/ml_kernel                             3m56s   3GB
Jan 22 23:47:03 Starting candle/standard/opentheory
Jan 22 23:56:09 Finished candle/standard/opentheory                            9m05s   3GB
Jan 22 23:56:10 Starting candle/standard/opentheory/compilation
Jan 23 00:26:14 Finished candle/standard/opentheory/compilation               30m02s  15GB
Jan 23 00:26:14 Starting candle/standard/opentheory/compilation/proofs
Jan 23 00:27:04 Finished candle/standard/opentheory/compilation/proofs           48s   6GB
Jan 23 00:27:04 Starting characteristic/examples
Jan 23 00:28:06 FAILED: characteristic/examples
]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: .]0;Holmake: ~/regression/cakeml-697/basis]0;Holmake: ~/regression/cakeml-697/basis/pure]0;Holmake: ~/regression/cakeml-697/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-697/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-697/misc]0;Holmake: ~/regression/cakeml-697/developers]0;Holmake: ~/regression/cakeml-697/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-697/misc]0;Holmake: ~/regression/cakeml-697/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-697/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-697/misc]0;Holmake: ~/regression/cakeml-697/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression/cakeml-697/basis/pure]0;Holmake: ~/regression/cakeml-697/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ~/regression/cakeml-697/basis]0;Holmake: ~/regression/cakeml-697/characteristic]0;Holmake: ~/regression/cakeml-697/compiler/parsing]0;Holmake: ~/regression/cakeml-697/semantics]0;Holmake: ~/regression/cakeml-697/semantics/ffi]0;Holmake: ~/regression/cakeml-697/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-697/semantics]0;Holmake: ~/regression/cakeml-697/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression/cakeml-697/compiler/parsing]0;Holmake: ~/regression/cakeml-697/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/regression/cakeml-697/characteristic]0;Holmake: ~/regression/cakeml-697/semantics/proofs]0;Holmake: ~/regression/cakeml-697/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ~/regression/cakeml-697/characteristic]0;Holmake: ~/regression/cakeml-697/translator]0;Holmake: ~/regression/cakeml-697/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/regression/cakeml-697/characteristic]0;Holmake: ~/regression/cakeml-697/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ~/regression/cakeml-697/basis]0;Holmake: ~/regression/cakeml-697/translator/monadic]0;Holmake: ~/regression/cakeml-697/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-697/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ~/regression/cakeml-697/translator/monadic]0;Holmake: ~/regression/cakeml-697/translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ~/regression/cakeml-697/basis]0;Holmake: ~/regression/cakeml-697/basis[1mWorking in $(CAKEMLDIR)/basis[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/characteristic/examples[0m
Starting work on cf_examplesTheory
Starting work on cf_tutorialTheory
Starting work on README.md
README.md                                                                                                  OK
cf_tutorialTheory                                                                                          OK
cf_examplesTheory                                                                                 FAILED! <1>
 Saved definition __ "Foo_exn_def"
 Adding nsLookup representation thms for [cf_examples_env_13, cf_examples_env_12]
 error in quse /home/myreen/regression/cakeml-697/characteristic/examples/cf_examplesScript.sml : HOL_ERR {message = "QCHANGED_CONSEQ_CONV", origin_function = "ConseqConv", origin_structure = "bool"}
 error in load cf_examplesScript : HOL_ERR {message = "QCHANGED_CONSEQ_CONV", origin_function = "ConseqConv", origin_structure = "bool"}
 Proof of 
 
 uv. UNIT_TYPE () uv  app p example_handle_v [uv] emp (POSTv v. &INT 3 v)
 
 failed.
 Uncaught exception: HOL_ERR {message = "QCHANGED_CONSEQ_CONV", origin_function = "ConseqConv", origin_structure = "bool"}