Job 1900

CakeML:75900ed6f1404310dd264d1023c3d773604078fb
  Add source_to_source to to_flatProg [May 10 10:34:45]
#884 (let-lift)
Merging into:a986431ac4c37f9c4e3ea55de543535a0b08637c
  Merge pull request #885 from CakeML/caml-pattern-guards [May 16 00:45:00]
HOL:db0c48a4df81300b8f4ab65af329cee860f6d921
  Fix a l3_equivalence_misc proof [May 10 01:22:03]
Machine:oven3

May 16 01:00:31 Claimed job
May 16 01:00:43 Reusing HOL
May 16 01:01:41 Starting developers
May 16 01:01:49 Finished developers                                               8s 170MB
May 16 01:01:49 Starting developers/bin
May 16 01:02:03 Finished developers/bin                                          13s   1GB
May 16 01:02:03 Starting semantics/ffi
May 16 01:02:27 Finished semantics/ffi                                           24s 252MB
May 16 01:02:28 Starting semantics
May 16 01:06:22 Finished semantics                                             3m54s   1GB
May 16 01:06:22 Starting semantics/proofs
May 16 01:15:38 Finished semantics/proofs                                      9m15s   3GB
May 16 01:15:38 Starting semantics/alt_semantics
May 16 01:16:28 Finished semantics/alt_semantics                                 50s 510MB
May 16 01:16:28 Starting semantics/alt_semantics/proofs
May 16 01:23:06 Finished semantics/alt_semantics/proofs                        6m37s   1GB
May 16 01:23:06 Starting basis/pure
May 16 01:25:25 Finished basis/pure                                            2m18s   1GB
May 16 01:25:25 Starting translator
May 16 01:31:33 Finished translator                                            6m07s   1GB
May 16 01:31:33 Starting compiler/parsing
May 16 01:34:25 Finished compiler/parsing                                      2m51s   2GB
May 16 01:34:25 Starting characteristic
May 16 01:48:03 Finished characteristic                                       13m36s   3GB
May 16 01:48:03 Starting translator/monadic
May 16 01:52:05 Finished translator/monadic                                    4m02s   1GB
May 16 01:52:06 Starting basis
May 16 03:36:34 Finished basis                                              1h44m27s  22GB
May 16 03:36:34 Starting compiler/inference
May 16 03:39:27 Finished compiler/inference                                    2m52s   1GB
May 16 03:39:27 Starting compiler/backend/reg_alloc
May 16 03:42:33 Finished compiler/backend/reg_alloc                            3m05s   1GB
May 16 03:42:33 Starting compiler/backend/gc
May 16 03:50:51 Finished compiler/backend/gc                                   8m17s   2GB
May 16 03:50:51 Starting compiler/backend
May 16 04:02:08 Finished compiler/backend                                     11m16s   2GB
May 16 04:02:08 Starting compiler/encoders/asm
May 16 04:03:11 Finished compiler/encoders/asm                                 1m02s 713MB
May 16 04:03:11 Starting compiler/encoders/x64
May 16 04:04:17 Finished compiler/encoders/x64                                 1m05s 954MB
May 16 04:04:17 Starting compiler/encoders/arm7
May 16 04:06:22 Finished compiler/encoders/arm7                                2m04s 792MB
May 16 04:06:22 Starting compiler/encoders/arm8
May 16 04:06:58 Finished compiler/encoders/arm8                                  36s 991MB
May 16 04:06:58 Starting compiler/encoders/arm8_asl
May 16 04:14:01 Finished compiler/encoders/arm8_asl                            7m02s   1GB
May 16 04:14:01 Starting compiler/encoders/mips
May 16 04:14:46 Finished compiler/encoders/mips                                  44s   1GB
May 16 04:14:46 Starting compiler/encoders/riscv
May 16 04:15:27 Finished compiler/encoders/riscv                                 40s 840MB
May 16 04:15:27 Starting compiler/encoders/ag32
May 16 04:16:16 Finished compiler/encoders/ag32                                  49s 914MB
May 16 04:16:17 Starting compiler/backend/x64
May 16 04:17:06 Finished compiler/backend/x64                                    49s   1GB
May 16 04:17:06 Starting compiler/backend/arm7
May 16 04:17:52 Finished compiler/backend/arm7                                   45s   1GB
May 16 04:17:52 Starting compiler/backend/arm8
May 16 04:18:40 Finished compiler/backend/arm8                                   47s   1GB
May 16 04:18:40 Starting compiler/backend/mips
May 16 04:19:29 Finished compiler/backend/mips                                   48s   1GB
May 16 04:19:29 Starting compiler/backend/riscv
May 16 04:20:18 Finished compiler/backend/riscv                                  48s   1GB
May 16 04:20:18 Starting compiler/backend/ag32
May 16 04:23:16 Finished compiler/backend/ag32                                 2m57s   1GB
May 16 04:23:17 Starting compiler/parsing/proofs
May 16 04:31:50 Finished compiler/parsing/proofs                               8m33s   1GB
May 16 04:31:51 Starting compiler/inference/proofs
May 16 04:37:27 Finished compiler/inference/proofs                             5m36s   1GB
May 16 04:37:27 Starting compiler/backend/semantics
May 16 05:41:24 Finished compiler/backend/semantics                         1h03m55s   2GB
May 16 05:41:24 Starting compiler/backend/reg_alloc/proofs
May 16 05:49:37 Finished compiler/backend/reg_alloc/proofs                     8m13s   1GB
May 16 05:49:38 Starting compiler/backend/proofs
May 16 07:31:16 Finished compiler/backend/proofs                            1h41m38s  16GB
May 16 07:31:16 Starting compiler/backend/serialiser
May 16 07:34:38 Finished compiler/backend/serialiser                           3m21s   1GB
May 16 07:34:38 Starting compiler/encoders/x64/proofs
May 16 07:56:00 Finished compiler/encoders/x64/proofs                         21m21s   6GB
May 16 07:56:00 Starting compiler/encoders/arm7/proofs
May 16 08:26:56 Finished compiler/encoders/arm7/proofs                        30m55s   3GB
May 16 08:26:56 Starting compiler/encoders/arm8/proofs
May 16 08:42:23 Finished compiler/encoders/arm8/proofs                        15m25s   1GB
May 16 08:42:23 Starting compiler/encoders/arm8_asl/proofs
May 16 09:16:50 Finished compiler/encoders/arm8_asl/proofs                    34m26s   2GB
May 16 09:16:50 Starting compiler/encoders/mips/proofs
May 16 09:39:29 Finished compiler/encoders/mips/proofs                        22m39s   2GB
May 16 09:39:30 Starting compiler/encoders/riscv/proofs
May 16 09:59:42 Finished compiler/encoders/riscv/proofs                       20m12s   1GB
May 16 09:59:42 Starting compiler/encoders/ag32/proofs
May 16 10:05:30 Finished compiler/encoders/ag32/proofs                         5m47s 815MB
May 16 10:05:31 Starting compiler/backend/x64/proofs
May 16 10:06:31 Finished compiler/backend/x64/proofs                           1m00s   1GB
May 16 10:06:31 Starting compiler/backend/arm7/proofs
May 16 10:07:32 Finished compiler/backend/arm7/proofs                          1m00s   1GB
May 16 10:07:33 Starting compiler/backend/arm8/proofs
May 16 10:08:35 Finished compiler/backend/arm8/proofs                          1m01s   1GB
May 16 10:08:35 Starting compiler/backend/arm8_asl
May 16 10:09:27 Finished compiler/backend/arm8_asl                               51s   1GB
May 16 10:09:27 Starting compiler/backend/mips/proofs
May 16 10:10:29 Finished compiler/backend/mips/proofs                          1m02s   1GB
May 16 10:10:30 Starting compiler/backend/riscv/proofs
May 16 10:11:32 Finished compiler/backend/riscv/proofs                         1m02s   1GB
May 16 10:11:32 Starting compiler/backend/ag32/proofs
May 16 10:40:03 Finished compiler/backend/ag32/proofs                         28m30s   2GB
May 16 10:40:03 Starting compiler/proofs
May 16 10:44:41 Finished compiler/proofs                                       4m37s   3GB
May 16 10:44:41 Starting candle/set-theory
May 16 10:45:52 Finished candle/set-theory                                     1m10s 992MB
May 16 10:45:52 Starting candle/syntax-lib
May 16 10:46:20 Finished candle/syntax-lib                                       28s 667MB
May 16 10:46:20 Starting candle/standard/syntax
May 16 10:50:45 Finished candle/standard/syntax                                4m24s   1GB
May 16 10:50:45 Starting candle/standard/semantics
May 16 10:54:45 Finished candle/standard/semantics                             3m59s   1GB
May 16 10:54:45 Starting candle/standard/monadic
May 16 10:58:47 Finished candle/standard/monadic                               4m01s   1GB
May 16 10:58:48 Starting candle/standard/ml_kernel
May 16 11:11:46 Finished candle/standard/ml_kernel                            12m57s   4GB
May 16 11:11:46 Starting candle/overloading/syntax
May 16 11:18:32 Finished candle/overloading/syntax                             6m45s   1GB
May 16 11:18:32 Starting candle/overloading/semantics
May 16 11:44:02 Finished candle/overloading/semantics                         25m30s   3GB
May 16 11:44:03 Starting candle/overloading/monadic
May 16 11:49:30 Finished candle/overloading/monadic                            5m27s   1GB
May 16 11:49:30 Starting candle/overloading/ml_kernel
May 16 12:03:59 Finished candle/overloading/ml_kernel                         14m28s   4GB
May 16 12:03:59 Starting candle/overloading/ml_checker
May 16 12:09:21 Finished candle/overloading/ml_checker                         5m21s   3GB
May 16 12:09:22 Starting candle/prover
May 16 12:27:37 Finished candle/prover                                        18m14s   3GB
May 16 12:27:37 Starting pancake
May 16 12:35:23 Finished pancake                                               7m46s   3GB
May 16 12:35:23 Starting pancake/ffi
May 16 12:35:24 Finished pancake/ffi                                              0s  31MB
May 16 12:35:25 Starting pancake/semantics
May 16 12:40:40 Finished pancake/semantics                                     5m14s   1GB
May 16 12:40:40 Starting pancake/proofs
May 16 13:07:02 Finished pancake/proofs                                       26m22s   6GB
May 16 13:07:03 Starting characteristic/examples
May 16 13:09:55 Finished characteristic/examples                               2m52s   3GB
May 16 13:09:55 Starting tutorial/solutions
May 16 13:47:21 Finished tutorial/solutions                                   37m25s   9GB
May 16 13:47:21 Starting translator/monadic/examples
May 16 13:54:23 Finished translator/monadic/examples                           7m01s   2GB
May 16 13:54:23 Starting examples
May 16 14:12:30 Finished examples                                             18m06s   3GB
May 16 14:12:30 Starting examples/compilation/x64
May 16 19:51:57 Finished examples/compilation/x64                           5h39m27s  25GB
May 16 19:51:58 Starting examples/compilation/x64/proofs
May 16 19:56:40 Finished examples/compilation/x64/proofs                       4m41s   3GB
May 16 19:56:40 Starting examples/compilation/ag32
May 16 21:15:10 Finished examples/compilation/ag32                          1h18m29s   9GB
May 16 21:15:10 Starting examples/compilation/ag32/proofs
May 16 21:17:02 Finished examples/compilation/ag32/proofs                      1m52s   3GB
May 16 21:17:02 Starting examples/cost
May 16 21:45:09 FAILED: examples/cost
Scanning [1m$(HOLDIR)/src/sort[0m
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/quotient/src[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
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)/src/coalgebras[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[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[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
Scanning [1m$(HOLDIR)/examples/algorithms[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(HOLDIR)/src/hol88[0m
Scanning [1m$(HOLDIR)/src/real[0m
Scanning [1m$(HOLDIR)/src/floating-point[0m
Scanning [1m$(HOLDIR)/src/monad/more_monads[0m
Scanning [1m$(HOLDIR)/src/update[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/ag32[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/ag32[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/model[0m
Scanning [1m$(HOLDIR)/examples/machine-code/decompiler[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm7[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm7[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm8[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm8[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/mips[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/mips[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/riscv[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/riscv[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/x64[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular/first-order[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/compiler[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/gc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/semantics/alt_semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/alt_semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/proofs[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/prog[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/x64/proofs[0m
Scanned 82 directories
Starting work on README.md
Starting work on costPropsTheory
Starting work on size_ofPropsTheory
Starting work on miniBasisProgTheory
README.md                                                                                                                                                                                             (0s)     OK
miniBasisProgTheory                                                                                                                                                                                  (70s)     OK
Starting work on lcgLoopProgTheory
size_ofPropsTheory                                                                                                                                                                                   (72s)     OK
costPropsTheory                                                                                                                                                                                     (166s)     OK
Starting work on allProgTheory
Starting work on cyesProgTheory
Starting work on pureLoopProgTheory
lcgLoopProgTheory                                                                                                                                                                                    (21m)     OK
Starting work on lcgLoopProofTheory
pureLoopProgTheory                                                                                                                                                                                   (20m)     OK
Starting work on pureLoopProofTheory
allProgTheory                                                                                                                                                                                        (20m)     OK
Starting work on allProofTheory
allProofTheory                                                                                                                                                                                      (332s)FAIL<1>
 
 ffi.
   backend_config_ok
     (x64_backend_config with
      word_to_word_conf := <|reg_alg := 2; col_oracle := oracle|>) 
   is_safe_for_space ffi all_x64_conf all_prog (56,81)
 
 failed.
 Failed to prove theorem data_safe_all.
 Uncaught exception: HOL_ERR {message = " (THEN1 on line 537) (THEN1 on line 551) (THEN1 on line 568) (THEN1 on line 587)", origin_function = "GEN_COND_CASES_TAC", origin_structure = "Tactic"}
cyesProgTheory                                                                                                                                                                                       (24m)MKILLED
lcgLoopProofTheory                                                                                                                                                                                  (377s)MKILLED
pureLoopProofTheory                                                                                                                                                                                 (335s)MKILLED