Job 679

CakeML:4fb9e50d7a344591bbc86cb216293527de1dc745
  Update how-to.md for change to True, False, Ref [Jan 14 21:12:00]
#591 (better-names)
Merging into:901708feeaa4cd0a8263ec24d39144eeb1f6d15d
  Merge pull request #599 from CakeML/lem-readme [Jan 14 09:15:32]
HOL:9884befd7ef626e7a20cde7aedb6f358330d8ba4
  Merge remote-tracking branch 'origin/pr/637' into develop [Jan 11 23:27:51]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Jan 14 21:12:42 Claimed job
Jan 14 21:12:46 Reusing HOL
Jan 14 21:12:56 Starting developers
Jan 14 21:12:57 Finished developers                                               0s  38MB
Jan 14 21:12:57 Starting developers/bin
Jan 14 21:13:30 Finished developers/bin                                          31s 140MB
Jan 14 21:13:30 Starting semantics/ffi
Jan 14 21:13:39 Finished semantics/ffi                                            8s 223MB
Jan 14 21:13:40 Starting semantics
Jan 14 21:15:01 Finished semantics                                             1m20s   1GB
Jan 14 21:15:02 Starting semantics/proofs
Jan 14 21:18:16 Finished semantics/proofs                                      3m13s   1GB
Jan 14 21:18:17 Starting basis/pure
Jan 14 21:19:08 Finished basis/pure                                              50s 748MB
Jan 14 21:19:09 Starting translator
Jan 14 21:20:48 Finished translator                                            1m38s   1GB
Jan 14 21:20:49 Starting compiler/parsing
Jan 14 21:21:52 Finished compiler/parsing                                      1m02s   2GB
Jan 14 21:21:52 Starting characteristic
Jan 14 21:25:06 Finished characteristic                                        3m12s   1GB
Jan 14 21:25:07 Starting translator/monadic
Jan 14 21:26:33 Finished translator/monadic                                    1m25s   1GB
Jan 14 21:26:34 Starting basis
Jan 14 21:42:26 Finished basis                                                15m51s   2GB
Jan 14 21:42:27 Starting compiler/inference
Jan 14 21:44:05 Finished compiler/inference                                    1m37s   1GB
Jan 14 21:44:06 Starting compiler/backend/reg_alloc
Jan 14 21:44:58 Finished compiler/backend/reg_alloc                              51s   1GB
Jan 14 21:44:58 Starting compiler/backend/gc
Jan 14 21:52:49 Finished compiler/backend/gc                                   7m49s   2GB
Jan 14 21:52:49 Starting compiler/backend
Jan 14 21:52:51 Finished compiler/backend                                         1s  17MB
Jan 14 21:52:52 Starting compiler/encoders/asm
Jan 14 21:52:53 Finished compiler/encoders/asm                                    0s  17MB
Jan 14 21:52:54 Starting compiler/encoders/x64
Jan 14 21:53:19 Finished compiler/encoders/x64                                   23s 840MB
Jan 14 21:53:20 Starting compiler/encoders/arm6
Jan 14 21:54:11 Finished compiler/encoders/arm6                                  50s   1GB
Jan 14 21:54:12 Starting compiler/encoders/arm8
Jan 14 21:54:25 Finished compiler/encoders/arm8                                  12s 846MB
Jan 14 21:54:26 Starting compiler/encoders/mips
Jan 14 21:54:43 Finished compiler/encoders/mips                                  15s 798MB
Jan 14 21:54:43 Starting compiler/encoders/riscv
Jan 14 21:54:58 Finished compiler/encoders/riscv                                 13s 745MB
Jan 14 21:54:59 Starting compiler/encoders/ag32
Jan 14 21:55:16 Finished compiler/encoders/ag32                                  16s 798MB
Jan 14 21:55:17 Starting compiler/backend/x64
Jan 14 21:55:33 Finished compiler/backend/x64                                    15s 757MB
Jan 14 21:55:34 Starting compiler/backend/arm6
Jan 14 21:55:53 Finished compiler/backend/arm6                                   18s   1GB
Jan 14 21:55:54 Starting compiler/backend/arm8
Jan 14 21:56:13 Finished compiler/backend/arm8                                   17s 895MB
Jan 14 21:56:13 Starting compiler/backend/mips
Jan 14 21:56:31 Finished compiler/backend/mips                                   16s 808MB
Jan 14 21:56:32 Starting compiler/backend/riscv
Jan 14 21:56:49 Finished compiler/backend/riscv                                  16s   1GB
Jan 14 21:56:49 Starting compiler/backend/ag32
Jan 14 21:58:05 Finished compiler/backend/ag32                                 1m14s   1GB
Jan 14 21:58:06 Starting compiler/parsing/proofs
Jan 14 22:03:58 Finished compiler/parsing/proofs                               5m51s   1GB
Jan 14 22:03:59 Starting compiler/inference/proofs
Jan 14 22:07:06 Finished compiler/inference/proofs                             3m05s   1GB
Jan 14 22:07:07 Starting compiler/backend/semantics
Jan 14 22:16:17 Finished compiler/backend/semantics                            9m09s   1GB
Jan 14 22:16:18 Starting compiler/backend/reg_alloc/proofs
Jan 14 22:19:08 Finished compiler/backend/reg_alloc/proofs                     2m49s 947MB
Jan 14 22:19:08 Starting compiler/backend/proofs
Jan 14 23:03:58 Finished compiler/backend/proofs                              44m48s   4GB
Jan 14 23:03:58 Starting compiler/encoders/x64/proofs
Jan 14 23:15:19 Finished compiler/encoders/x64/proofs                         11m20s   4GB
Jan 14 23:15:20 Starting compiler/encoders/arm6/proofs
Jan 14 23:31:00 Finished compiler/encoders/arm6/proofs                        15m37s   3GB
Jan 14 23:31:00 Starting compiler/encoders/arm8/proofs
Jan 14 23:37:33 Finished compiler/encoders/arm8/proofs                         6m31s   1GB
Jan 14 23:37:34 Starting compiler/encoders/mips/proofs
Jan 14 23:49:04 Finished compiler/encoders/mips/proofs                        11m29s   1GB
Jan 14 23:49:04 Starting compiler/encoders/riscv/proofs
Jan 14 23:57:26 Finished compiler/encoders/riscv/proofs                        8m21s 935MB
Jan 14 23:57:27 Starting compiler/encoders/ag32/proofs
Jan 15 00:00:21 Finished compiler/encoders/ag32/proofs                         2m53s 824MB
Jan 15 00:00:22 Starting compiler/backend/x64/proofs
Jan 15 00:00:42 Finished compiler/backend/x64/proofs                             19s   1GB
Jan 15 00:00:43 Starting compiler/backend/arm6/proofs
Jan 15 00:01:08 Finished compiler/backend/arm6/proofs                            23s   1GB
Jan 15 00:01:08 Starting compiler/backend/arm8/proofs
Jan 15 00:01:29 Finished compiler/backend/arm8/proofs                            19s   1GB
Jan 15 00:01:29 Starting compiler/backend/mips/proofs
Jan 15 00:01:51 Finished compiler/backend/mips/proofs                            20s   1GB
Jan 15 00:01:51 Starting compiler/backend/riscv/proofs
Jan 15 00:02:12 Finished compiler/backend/riscv/proofs                           19s   1GB
Jan 15 00:02:13 Starting compiler/backend/ag32/proofs
Jan 15 00:13:09 Finished compiler/backend/ag32/proofs                         10m55s   3GB
Jan 15 00:13:10 Starting compiler/proofs
Jan 15 00:14:38 Finished compiler/proofs                                       1m27s   3GB
Jan 15 00:14:38 Starting candle/set-theory
Jan 15 00:15:09 Finished candle/set-theory                                       29s 680MB
Jan 15 00:15:09 Starting candle/syntax-lib
Jan 15 00:15:21 Finished candle/syntax-lib                                       10s 580MB
Jan 15 00:15:21 Starting candle/standard/syntax
Jan 15 00:17:20 Finished candle/standard/syntax                                1m58s   1GB
Jan 15 00:17:21 Starting candle/standard/semantics
Jan 15 00:19:13 Finished candle/standard/semantics                             1m51s   1GB
Jan 15 00:19:14 Starting candle/standard/monadic
Jan 15 00:21:11 Finished candle/standard/monadic                               1m56s   1GB
Jan 15 00:21:11 Starting candle/standard/ml_kernel
Jan 15 00:25:40 Finished candle/standard/ml_kernel                             4m27s   3GB
Jan 15 00:25:41 Starting candle/standard/opentheory
Jan 15 00:35:26 Finished candle/standard/opentheory                            9m44s   4GB
Jan 15 00:35:27 Starting candle/standard/opentheory/compilation
Jan 15 01:09:31 Finished candle/standard/opentheory/compilation               34m03s  10GB
Jan 15 01:09:32 Starting candle/standard/opentheory/compilation/proofs
Jan 15 01:10:39 Finished candle/standard/opentheory/compilation/proofs         1m06s   3GB
Jan 15 01:10:40 Starting characteristic/examples
Jan 15 01:11:23 FAILED: characteristic/examples
]0;Holmake: ~/regression/HOL-9884befd7ef626e7a20cde7aedb6f358330d8ba4/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-9884befd7ef626e7a20cde7aedb6f358330d8ba4/examples/formal-languages]0;Holmake: ~/regression/HOL-9884befd7ef626e7a20cde7aedb6f358330d8ba4/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-9884befd7ef626e7a20cde7aedb6f358330d8ba4/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-9884befd7ef626e7a20cde7aedb6f358330d8ba4/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-9884befd7ef626e7a20cde7aedb6f358330d8ba4/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-9884befd7ef626e7a20cde7aedb6f358330d8ba4/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-9884befd7ef626e7a20cde7aedb6f358330d8ba4/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-679/basis]0;Holmake: ~/regression/cakeml-679/basis/pure]0;Holmake: ~/regression/cakeml-679/misc]0;Holmake: ~/regression/HOL-9884befd7ef626e7a20cde7aedb6f358330d8ba4/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-9884befd7ef626e7a20cde7aedb6f358330d8ba4/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-679/misc]0;Holmake: ~/regression/HOL-9884befd7ef626e7a20cde7aedb6f358330d8ba4/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-9884befd7ef626e7a20cde7aedb6f358330d8ba4/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/regression/cakeml-679/misc]0;Holmake: ~/regression/cakeml-679/developers]0;Holmake: ~/regression/cakeml-679/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-679/misc]0;Holmake: ~/regression/cakeml-679/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-679/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-679/misc]0;Holmake: ~/regression/cakeml-679/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression/cakeml-679/basis/pure]0;Holmake: ~/regression/cakeml-679/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ~/regression/cakeml-679/basis]0;Holmake: ~/regression/cakeml-679/characteristic]0;Holmake: ~/regression/cakeml-679/compiler/parsing]0;Holmake: ~/regression/cakeml-679/semantics]0;Holmake: ~/regression/cakeml-679/semantics/ffi]0;Holmake: ~/regression/cakeml-679/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-679/semantics]0;Holmake: ~/regression/cakeml-679/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression/cakeml-679/compiler/parsing]0;Holmake: ~/regression/cakeml-679/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/regression/cakeml-679/characteristic]0;Holmake: ~/regression/cakeml-679/semantics/proofs]0;Holmake: ~/regression/cakeml-679/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ~/regression/cakeml-679/characteristic]0;Holmake: ~/regression/cakeml-679/translator]0;Holmake: ~/regression/cakeml-679/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/regression/cakeml-679/characteristic]0;Holmake: ~/regression/cakeml-679/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ~/regression/cakeml-679/basis]0;Holmake: ~/regression/cakeml-679/translator/monadic]0;Holmake: ~/regression/cakeml-679/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-679/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ~/regression/cakeml-679/translator/monadic]0;Holmake: ~/regression/cakeml-679/translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ~/regression/cakeml-679/basis]0;Holmake: ~/regression/cakeml-679/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_examplesTheory                                                                                 FAILED! <1>
 
 av bv a b r1v r2v r1 r2.
     INT a av  INT b bv 
     app p alloc_ref2_v [av; bv] emp
       (POSTv p.
            SEP_EXISTS r1 r2.
                &PAIR_TYPE $= $= (r1,r2) p * r1 ~~> av * r2 ~~> bv)
 
 failed.
 Uncaught exception: HOL_ERR {message = "REWR_CONV: lhs of thm doesn't match term (THEN1 on line 89) (THEN1 on line 90)", origin_function = "RATOR_CONV", origin_structure = "Conv"}
cf_tutorialTheory                                                                                    M-KILLED