Overview

Job 679

CakeML:4fb9e50d7a344591bbc86cb216293527de1dc745
  Update how-to.md for change to True, False, Ref
#591 (better-names)
Merging into:901708feeaa4cd0a8263ec24d39144eeb1f6d15d
  Merge pull request #599 from CakeML/lem-readme
HOL:9884befd7ef626e7a20cde7aedb6f358330d8ba4
  Merge remote-tracking branch 'origin/pr/637' into develop
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

 Claimed job
 Reusing HOL
 Starting developers
 Finished developers                                               0s  38MB
 Starting developers/bin
 Finished developers/bin                                          31s 140MB
 Starting semantics/ffi
 Finished semantics/ffi                                            8s 223MB
 Starting semantics
 Finished semantics                                             1m20s   1GB
 Starting semantics/proofs
 Finished semantics/proofs                                      3m13s   1GB
 Starting basis/pure
 Finished basis/pure                                              50s 748MB
 Starting translator
 Finished translator                                            1m38s   1GB
 Starting compiler/parsing
 Finished compiler/parsing                                      1m02s   2GB
 Starting characteristic
 Finished characteristic                                        3m12s   1GB
 Starting translator/monadic
 Finished translator/monadic                                    1m25s   1GB
 Starting basis
 Finished basis                                                15m51s   2GB
 Starting compiler/inference
 Finished compiler/inference                                    1m37s   1GB
 Starting compiler/backend/reg_alloc
 Finished compiler/backend/reg_alloc                              51s   1GB
 Starting compiler/backend/gc
 Finished compiler/backend/gc                                   7m49s   2GB
 Starting compiler/backend
 Finished compiler/backend                                         1s  17MB
 Starting compiler/encoders/asm
 Finished compiler/encoders/asm                                    0s  17MB
 Starting compiler/encoders/x64
 Finished compiler/encoders/x64                                   23s 840MB
 Starting compiler/encoders/arm6
 Finished compiler/encoders/arm6                                  50s   1GB
 Starting compiler/encoders/arm8
 Finished compiler/encoders/arm8                                  12s 846MB
 Starting compiler/encoders/mips
 Finished compiler/encoders/mips                                  15s 798MB
 Starting compiler/encoders/riscv
 Finished compiler/encoders/riscv                                 13s 745MB
 Starting compiler/encoders/ag32
 Finished compiler/encoders/ag32                                  16s 798MB
 Starting compiler/backend/x64
 Finished compiler/backend/x64                                    15s 757MB
 Starting compiler/backend/arm6
 Finished compiler/backend/arm6                                   18s   1GB
 Starting compiler/backend/arm8
 Finished compiler/backend/arm8                                   17s 895MB
 Starting compiler/backend/mips
 Finished compiler/backend/mips                                   16s 808MB
 Starting compiler/backend/riscv
 Finished compiler/backend/riscv                                  16s   1GB
 Starting compiler/backend/ag32
 Finished compiler/backend/ag32                                 1m14s   1GB
 Starting compiler/parsing/proofs
 Finished compiler/parsing/proofs                               5m51s   1GB
 Starting compiler/inference/proofs
 Finished compiler/inference/proofs                             3m05s   1GB
 Starting compiler/backend/semantics
 Finished compiler/backend/semantics                            9m09s   1GB
 Starting compiler/backend/reg_alloc/proofs
 Finished compiler/backend/reg_alloc/proofs                     2m49s 947MB
 Starting compiler/backend/proofs
 Finished compiler/backend/proofs                              44m48s   4GB
 Starting compiler/encoders/x64/proofs
 Finished compiler/encoders/x64/proofs                         11m20s   4GB
 Starting compiler/encoders/arm6/proofs
 Finished compiler/encoders/arm6/proofs                        15m37s   3GB
 Starting compiler/encoders/arm8/proofs
 Finished compiler/encoders/arm8/proofs                         6m31s   1GB
 Starting compiler/encoders/mips/proofs
 Finished compiler/encoders/mips/proofs                        11m29s   1GB
 Starting compiler/encoders/riscv/proofs
 Finished compiler/encoders/riscv/proofs                        8m21s 935MB
 Starting compiler/encoders/ag32/proofs
 Finished compiler/encoders/ag32/proofs                         2m53s 824MB
 Starting compiler/backend/x64/proofs
 Finished compiler/backend/x64/proofs                             19s   1GB
 Starting compiler/backend/arm6/proofs
 Finished compiler/backend/arm6/proofs                            23s   1GB
 Starting compiler/backend/arm8/proofs
 Finished compiler/backend/arm8/proofs                            19s   1GB
 Starting compiler/backend/mips/proofs
 Finished compiler/backend/mips/proofs                            20s   1GB
 Starting compiler/backend/riscv/proofs
 Finished compiler/backend/riscv/proofs                           19s   1GB
 Starting compiler/backend/ag32/proofs
 Finished compiler/backend/ag32/proofs                         10m55s   3GB
 Starting compiler/proofs
 Finished compiler/proofs                                       1m27s   3GB
 Starting candle/set-theory
 Finished candle/set-theory                                       29s 680MB
 Starting candle/syntax-lib
 Finished candle/syntax-lib                                       10s 580MB
 Starting candle/standard/syntax
 Finished candle/standard/syntax                                1m58s   1GB
 Starting candle/standard/semantics
 Finished candle/standard/semantics                             1m51s   1GB
 Starting candle/standard/monadic
 Finished candle/standard/monadic                               1m56s   1GB
 Starting candle/standard/ml_kernel
 Finished candle/standard/ml_kernel                             4m27s   3GB
 Starting candle/standard/opentheory
 Finished candle/standard/opentheory                            9m44s   4GB
 Starting candle/standard/opentheory/compilation
 Finished candle/standard/opentheory/compilation               34m03s  10GB
 Starting candle/standard/opentheory/compilation/proofs
 Finished candle/standard/opentheory/compilation/proofs         1m06s   3GB
 Starting characteristic/examples
 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