Job 1120

CakeML:13adc5628f534baa566c11709ab526a7c8d7f2d4
  Tweak various CF proofs for new goal from xmatch [Dec 10 03:20:06]
#692 (match-refactor-2)
Merging into:10943f8db35376f05a51dc0c63484da1b62abee6
  Merge pull request #708 from CakeML/lrat [Dec 09 23:25:17]
HOL:481761b292689788e0b28e013337d6a16c4a6fa4
  adding back combinTheory dependency to hhExportLib [Nov 26 08:34:04]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Dec 10 03:21:16 Claimed job
Dec 10 03:21:22 Reusing HOL
Dec 10 03:21:28 Starting developers
Dec 10 03:21:28 Finished developers                                               0s  21MB
Dec 10 03:21:29 Starting developers/bin
Dec 10 03:21:33 Finished developers/bin                                           3s 164MB
Dec 10 03:21:33 Starting semantics/ffi
Dec 10 03:21:42 Finished semantics/ffi                                            8s 196MB
Dec 10 03:21:42 Starting semantics
Dec 10 03:23:06 Finished semantics                                             1m23s   1GB
Dec 10 03:23:06 Starting semantics/proofs
Dec 10 03:26:18 Finished semantics/proofs                                      3m11s   1GB
Dec 10 03:26:18 Starting semantics/alt_semantics
Dec 10 03:26:25 Finished semantics/alt_semantics                                  6s 296MB
Dec 10 03:26:25 Starting semantics/alt_semantics/proofs
Dec 10 03:28:22 Finished semantics/alt_semantics/proofs                        1m56s   1GB
Dec 10 03:28:23 Starting basis/pure
Dec 10 03:29:10 Finished basis/pure                                              46s 746MB
Dec 10 03:29:10 Starting translator
Dec 10 03:31:42 Finished translator                                            2m32s   1GB
Dec 10 03:31:43 Starting compiler/parsing
Dec 10 03:32:57 Finished compiler/parsing                                      1m14s   1GB
Dec 10 03:32:58 Starting characteristic
Dec 10 03:38:43 Finished characteristic                                        5m45s   2GB
Dec 10 03:38:43 Starting translator/monadic
Dec 10 03:40:19 Finished translator/monadic                                    1m35s   1GB
Dec 10 03:40:19 Starting basis
Dec 10 04:15:04 Finished basis                                                34m44s  17GB
Dec 10 04:15:04 Starting compiler/inference
Dec 10 04:16:45 Finished compiler/inference                                    1m40s   2GB
Dec 10 04:16:45 Starting compiler/backend/reg_alloc
Dec 10 04:17:48 Finished compiler/backend/reg_alloc                            1m02s   1GB
Dec 10 04:17:48 Starting compiler/backend/gc
Dec 10 04:21:17 Finished compiler/backend/gc                                   3m28s   1GB
Dec 10 04:21:17 Starting compiler/backend
Dec 10 04:25:38 Finished compiler/backend                                      4m20s   2GB
Dec 10 04:25:38 Starting compiler/encoders/asm
Dec 10 04:25:58 Finished compiler/encoders/asm                                   20s 742MB
Dec 10 04:25:59 Starting compiler/encoders/x64
Dec 10 04:26:23 Finished compiler/encoders/x64                                   24s 799MB
Dec 10 04:26:24 Starting compiler/encoders/arm7
Dec 10 04:27:10 Finished compiler/encoders/arm7                                  46s 734MB
Dec 10 04:27:11 Starting compiler/encoders/arm8
Dec 10 04:27:23 Finished compiler/encoders/arm8                                  11s 590MB
Dec 10 04:27:23 Starting compiler/encoders/mips
Dec 10 04:27:40 Finished compiler/encoders/mips                                  16s   1GB
Dec 10 04:27:40 Starting compiler/encoders/riscv
Dec 10 04:27:55 Finished compiler/encoders/riscv                                 14s 818MB
Dec 10 04:27:55 Starting compiler/encoders/ag32
Dec 10 04:28:12 Finished compiler/encoders/ag32                                  16s 617MB
Dec 10 04:28:12 Starting compiler/backend/x64
Dec 10 04:28:29 Finished compiler/backend/x64                                    16s 834MB
Dec 10 04:28:29 Starting compiler/backend/arm7
Dec 10 04:28:49 Finished compiler/backend/arm7                                   19s   1GB
Dec 10 04:28:49 Starting compiler/backend/arm8
Dec 10 04:29:08 Finished compiler/backend/arm8                                   17s   1GB
Dec 10 04:29:08 Starting compiler/backend/mips
Dec 10 04:29:26 Finished compiler/backend/mips                                   18s   1GB
Dec 10 04:29:26 Starting compiler/backend/riscv
Dec 10 04:29:45 Finished compiler/backend/riscv                                  18s   1GB
Dec 10 04:29:45 Starting compiler/backend/ag32
Dec 10 04:30:57 Finished compiler/backend/ag32                                 1m11s   1GB
Dec 10 04:30:58 Starting compiler/parsing/proofs
Dec 10 04:38:32 Finished compiler/parsing/proofs                               7m34s 858MB
Dec 10 04:38:33 Starting compiler/inference/proofs
Dec 10 04:42:07 Finished compiler/inference/proofs                             3m33s   1GB
Dec 10 04:42:07 Starting compiler/backend/semantics
Dec 10 05:01:39 Finished compiler/backend/semantics                           19m31s   1GB
Dec 10 05:01:39 Starting compiler/backend/reg_alloc/proofs
Dec 10 05:04:59 Finished compiler/backend/reg_alloc/proofs                     3m20s 780MB
Dec 10 05:05:00 Starting compiler/backend/proofs
Dec 10 06:03:01 Finished compiler/backend/proofs                              58m01s  22GB
Dec 10 06:03:01 Starting compiler/encoders/x64/proofs
Dec 10 06:12:17 Finished compiler/encoders/x64/proofs                          9m15s   4GB
Dec 10 06:12:18 Starting compiler/encoders/arm7/proofs
Dec 10 06:24:47 Finished compiler/encoders/arm7/proofs                        12m29s   3GB
Dec 10 06:24:48 Starting compiler/encoders/arm8/proofs
Dec 10 06:31:02 Finished compiler/encoders/arm8/proofs                         6m14s   1GB
Dec 10 06:31:03 Starting compiler/encoders/mips/proofs
Dec 10 06:40:29 Finished compiler/encoders/mips/proofs                         9m26s   3GB
Dec 10 06:40:30 Starting compiler/encoders/riscv/proofs
Dec 10 06:48:53 Finished compiler/encoders/riscv/proofs                        8m22s   1GB
Dec 10 06:48:53 Starting compiler/encoders/ag32/proofs
Dec 10 06:51:18 Finished compiler/encoders/ag32/proofs                         2m24s 855MB
Dec 10 06:51:18 Starting compiler/backend/x64/proofs
Dec 10 06:51:36 Finished compiler/backend/x64/proofs                             17s   1GB
Dec 10 06:51:36 Starting compiler/backend/arm7/proofs
Dec 10 06:51:56 Finished compiler/backend/arm7/proofs                            19s 818MB
Dec 10 06:51:56 Starting compiler/backend/arm8/proofs
Dec 10 06:52:13 Finished compiler/backend/arm8/proofs                            17s 772MB
Dec 10 06:52:14 Starting compiler/backend/mips/proofs
Dec 10 06:52:31 Finished compiler/backend/mips/proofs                            17s   1GB
Dec 10 06:52:32 Starting compiler/backend/riscv/proofs
Dec 10 06:52:50 Finished compiler/backend/riscv/proofs                           17s   1GB
Dec 10 06:52:50 Starting compiler/backend/ag32/proofs
Dec 10 07:01:58 Finished compiler/backend/ag32/proofs                          9m07s   2GB
Dec 10 07:01:58 Starting compiler/proofs
Dec 10 07:03:34 Finished compiler/proofs                                       1m35s   3GB
Dec 10 07:03:34 Starting candle/set-theory
Dec 10 07:04:00 Finished candle/set-theory                                       25s 738MB
Dec 10 07:04:00 Starting candle/syntax-lib
Dec 10 07:04:10 Finished candle/syntax-lib                                        9s 585MB
Dec 10 07:04:10 Starting candle/standard/syntax
Dec 10 07:05:53 Finished candle/standard/syntax                                1m42s 811MB
Dec 10 07:05:53 Starting candle/standard/semantics
Dec 10 07:07:28 Finished candle/standard/semantics                             1m34s   1GB
Dec 10 07:07:28 Starting candle/standard/monadic
Dec 10 07:09:02 Finished candle/standard/monadic                               1m33s   1GB
Dec 10 07:09:02 Starting candle/standard/ml_kernel
Dec 10 07:13:59 Finished candle/standard/ml_kernel                             4m56s   4GB
Dec 10 07:13:59 Starting candle/standard/opentheory
Dec 10 07:23:04 Finished candle/standard/opentheory                            9m04s   4GB
Dec 10 07:23:05 Starting candle/standard/opentheory/compilation
Dec 10 07:54:37 Finished candle/standard/opentheory/compilation               31m32s  16GB
Dec 10 07:54:37 Starting candle/standard/opentheory/compilation/proofs
Dec 10 07:55:22 Finished candle/standard/opentheory/compilation/proofs           44s   2GB
Dec 10 07:55:22 Starting characteristic/examples
Dec 10 07:56:52 Finished characteristic/examples                               1m29s   2GB
Dec 10 07:56:52 Starting tutorial/solutions
Dec 10 08:10:17 Finished tutorial/solutions                                   13m24s   7GB
Dec 10 08:10:17 Starting translator/monadic/examples
Dec 10 08:13:10 Finished translator/monadic/examples                           2m52s   2GB
Dec 10 08:13:10 Starting examples
Dec 10 08:22:19 Finished examples                                              9m08s   5GB
Dec 10 08:22:19 Starting examples/compilation/x64
Dec 10 10:27:33 Finished examples/compilation/x64                           2h05m13s  14GB
Dec 10 10:27:33 Starting examples/compilation/x64/proofs
Dec 10 10:29:23 Finished examples/compilation/x64/proofs                       1m49s   3GB
Dec 10 10:29:23 Starting examples/compilation/ag32
Dec 10 10:58:17 Finished examples/compilation/ag32                            28m53s   6GB
Dec 10 10:58:17 Starting examples/compilation/ag32/proofs
Dec 10 10:59:08 Finished examples/compilation/ag32/proofs                        50s   3GB
Dec 10 10:59:08 Starting examples/cost
Dec 10 11:21:28 Finished examples/cost                                        22m19s   6GB
Dec 10 11:21:28 Starting examples/lrat_checker
Dec 10 11:23:01 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 = "??"}