Overview

Job 1120

CakeML:13adc5628f534baa566c11709ab526a7c8d7f2d4
  Tweak various CF proofs for new goal from xmatch
#692 (match-refactor-2)
Merging into:10943f8db35376f05a51dc0c63484da1b62abee6
  Merge pull request #708 from CakeML/lrat
HOL:481761b292689788e0b28e013337d6a16c4a6fa4
  adding back combinTheory dependency to hhExportLib
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

 Claimed job
 Reusing HOL
 Starting developers
 Finished developers                                               0s  21MB
 Starting developers/bin
 Finished developers/bin                                           3s 164MB
 Starting semantics/ffi
 Finished semantics/ffi                                            8s 196MB
 Starting semantics
 Finished semantics                                             1m23s   1GB
 Starting semantics/proofs
 Finished semantics/proofs                                      3m11s   1GB
 Starting semantics/alt_semantics
 Finished semantics/alt_semantics                                  6s 296MB
 Starting semantics/alt_semantics/proofs
 Finished semantics/alt_semantics/proofs                        1m56s   1GB
 Starting basis/pure
 Finished basis/pure                                              46s 746MB
 Starting translator
 Finished translator                                            2m32s   1GB
 Starting compiler/parsing
 Finished compiler/parsing                                      1m14s   1GB
 Starting characteristic
 Finished characteristic                                        5m45s   2GB
 Starting translator/monadic
 Finished translator/monadic                                    1m35s   1GB
 Starting basis
 Finished basis                                                34m44s  17GB
 Starting compiler/inference
 Finished compiler/inference                                    1m40s   2GB
 Starting compiler/backend/reg_alloc
 Finished compiler/backend/reg_alloc                            1m02s   1GB
 Starting compiler/backend/gc
 Finished compiler/backend/gc                                   3m28s   1GB
 Starting compiler/backend
 Finished compiler/backend                                      4m20s   2GB
 Starting compiler/encoders/asm
 Finished compiler/encoders/asm                                   20s 742MB
 Starting compiler/encoders/x64
 Finished compiler/encoders/x64                                   24s 799MB
 Starting compiler/encoders/arm7
 Finished compiler/encoders/arm7                                  46s 734MB
 Starting compiler/encoders/arm8
 Finished compiler/encoders/arm8                                  11s 590MB
 Starting compiler/encoders/mips
 Finished compiler/encoders/mips                                  16s   1GB
 Starting compiler/encoders/riscv
 Finished compiler/encoders/riscv                                 14s 818MB
 Starting compiler/encoders/ag32
 Finished compiler/encoders/ag32                                  16s 617MB
 Starting compiler/backend/x64
 Finished compiler/backend/x64                                    16s 834MB
 Starting compiler/backend/arm7
 Finished compiler/backend/arm7                                   19s   1GB
 Starting compiler/backend/arm8
 Finished compiler/backend/arm8                                   17s   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                                 1m11s   1GB
 Starting compiler/parsing/proofs
 Finished compiler/parsing/proofs                               7m34s 858MB
 Starting compiler/inference/proofs
 Finished compiler/inference/proofs                             3m33s   1GB
 Starting compiler/backend/semantics
 Finished compiler/backend/semantics                           19m31s   1GB
 Starting compiler/backend/reg_alloc/proofs
 Finished compiler/backend/reg_alloc/proofs                     3m20s 780MB
 Starting compiler/backend/proofs
 Finished compiler/backend/proofs                              58m01s  22GB
 Starting compiler/encoders/x64/proofs
 Finished compiler/encoders/x64/proofs                          9m15s   4GB
 Starting compiler/encoders/arm7/proofs
 Finished compiler/encoders/arm7/proofs                        12m29s   3GB
 Starting compiler/encoders/arm8/proofs
 Finished compiler/encoders/arm8/proofs                         6m14s   1GB
 Starting compiler/encoders/mips/proofs
 Finished compiler/encoders/mips/proofs                         9m26s   3GB
 Starting compiler/encoders/riscv/proofs
 Finished compiler/encoders/riscv/proofs                        8m22s   1GB
 Starting compiler/encoders/ag32/proofs
 Finished compiler/encoders/ag32/proofs                         2m24s 855MB
 Starting compiler/backend/x64/proofs
 Finished compiler/backend/x64/proofs                             17s   1GB
 Starting compiler/backend/arm7/proofs
 Finished compiler/backend/arm7/proofs                            19s 818MB
 Starting compiler/backend/arm8/proofs
 Finished compiler/backend/arm8/proofs                            17s 772MB
 Starting compiler/backend/mips/proofs
 Finished compiler/backend/mips/proofs                            17s   1GB
 Starting compiler/backend/riscv/proofs
 Finished compiler/backend/riscv/proofs                           17s   1GB
 Starting compiler/backend/ag32/proofs
 Finished compiler/backend/ag32/proofs                          9m07s   2GB
 Starting compiler/proofs
 Finished compiler/proofs                                       1m35s   3GB
 Starting candle/set-theory
 Finished candle/set-theory                                       25s 738MB
 Starting candle/syntax-lib
 Finished candle/syntax-lib                                        9s 585MB
 Starting candle/standard/syntax
 Finished candle/standard/syntax                                1m42s 811MB
 Starting candle/standard/semantics
 Finished candle/standard/semantics                             1m34s   1GB
 Starting candle/standard/monadic
 Finished candle/standard/monadic                               1m33s   1GB
 Starting candle/standard/ml_kernel
 Finished candle/standard/ml_kernel                             4m56s   4GB
 Starting candle/standard/opentheory
 Finished candle/standard/opentheory                            9m04s   4GB
 Starting candle/standard/opentheory/compilation
 Finished candle/standard/opentheory/compilation               31m32s  16GB
 Starting candle/standard/opentheory/compilation/proofs
 Finished candle/standard/opentheory/compilation/proofs           44s   2GB
 Starting characteristic/examples
 Finished characteristic/examples                               1m29s   2GB
 Starting tutorial/solutions
 Finished tutorial/solutions                                   13m24s   7GB
 Starting translator/monadic/examples
 Finished translator/monadic/examples                           2m52s   2GB
 Starting examples
 Finished examples                                              9m08s   5GB
 Starting examples/compilation/x64
 Finished examples/compilation/x64                           2h05m13s  14GB
 Starting examples/compilation/x64/proofs
 Finished examples/compilation/x64/proofs                       1m49s   3GB
 Starting examples/compilation/ag32
 Finished examples/compilation/ag32                            28m53s   6GB
 Starting examples/compilation/ag32/proofs
 Finished examples/compilation/ag32/proofs                        50s   3GB
 Starting examples/cost
 Finished examples/cost                                        22m19s   6GB
 Starting examples/lrat_checker
 FAILED: examples/lrat_checker
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc/lem_lib_stub[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/basis[0m
Starting work on lratTheory
lratTheory                                                                                                                                     real:   13s  user:   12s     OK
Starting work on parsingTheory
Starting work on ramseyTheory
parsingTheory                                                                                                                                  real:    9s  user:    9s     OK
Starting work on lrat_commonProgTheory
ramseyTheory                                                                                                                                   real:   24s  user:   23s     OK
lrat_commonProgTheory                                                                                                                          real:   68s  user:   67sFAIL<1>
           else add_stderr fs (notfound_string f)))
 
 failed.
 Failed to prove theorem check_unsat'_spec.
 
 Exception raised at ??.??:
 fail (THEN1 on line 345) (THEN1 on line 359) (THEN1 on line 334) (THEN1 on line 375) (THEN1 on line 385) (THEN1 on line 386) (THEN1 on line 388) (THEN1 on line 392)
 error in quse /home/myreen/regression/cakeml-1120/examples/lrat_checker/lrat_commonProgScript.sml : HOL_ERR {message = "fail (THEN1 on line 345) (THEN1 on line 359) (THEN1 on line 334) (THEN1 on line 375) (THEN1 on line 385) (THEN1 on line 386) (THEN1 on line 388) (THEN1 on line 392)", origin_function = "??", origin_structure = "??"}
 error in load /home/myreen/regression/cakeml-1120/examples/lrat_checker/lrat_commonProgScript : HOL_ERR {message = "fail (THEN1 on line 345) (THEN1 on line 359) (THEN1 on line 334) (THEN1 on line 375) (THEN1 on line 385) (THEN1 on line 386) (THEN1 on line 388) (THEN1 on line 392)", origin_function = "??", origin_structure = "??"}
 Uncaught exception: HOL_ERR {message = "fail (THEN1 on line 345) (THEN1 on line 359) (THEN1 on line 334) (THEN1 on line 375) (THEN1 on line 385) (THEN1 on line 386) (THEN1 on line 388) (THEN1 on line 392)", origin_function = "??", origin_structure = "??"}