Job 1895

CakeML:27966171eba31e086a266c4870d0e3f41e74c5a6
  Merge branch 'master' into Iced_cake [May 10 08:02:28]
#865 (Iced_cake)
Merging into:b22ea8e8ba7e6a7474e33f8273f526a9360cc788
  Merge pull request #883 from CakeML/pan-lemma [May 09 03:44:38]
HOL:db0c48a4df81300b8f4ab65af329cee860f6d921
  Fix a l3_equivalence_misc proof [May 10 01:22:03]
Machine:oven3

May 10 08:03:12 Claimed job
May 10 08:03:21 Building HOL
May 10 08:23:40 Starting developers
May 10 08:23:50 Finished developers                                               9s  95MB
May 10 08:23:50 Starting developers/bin
May 10 08:24:03 Finished developers/bin                                          12s   1GB
May 10 08:24:03 Starting semantics/ffi
May 10 08:24:27 Finished semantics/ffi                                           24s 253MB
May 10 08:24:28 Starting semantics
May 10 08:29:51 Finished semantics                                             5m22s   1GB
May 10 08:29:51 Starting semantics/proofs
May 10 08:45:33 Finished semantics/proofs                                     15m41s   1GB
May 10 08:45:33 Starting semantics/alt_semantics
May 10 08:46:33 Finished semantics/alt_semantics                                 59s 573MB
May 10 08:46:33 Starting semantics/alt_semantics/proofs
May 10 09:11:52 Finished semantics/alt_semantics/proofs                       25m18s   1GB
May 10 09:11:53 Starting basis/pure
May 10 09:19:28 Finished basis/pure                                            7m35s 905MB
May 10 09:19:28 Starting translator
May 10 09:27:20 Finished translator                                            7m51s   1GB
May 10 09:27:20 Starting compiler/parsing
May 10 09:30:23 Finished compiler/parsing                                      3m02s   5GB
May 10 09:30:23 Starting characteristic
May 10 09:45:03 Finished characteristic                                       14m39s   2GB
May 10 09:45:03 Starting translator/monadic
May 10 09:49:19 Finished translator/monadic                                    4m16s   1GB
May 10 09:49:20 Starting basis
May 10 11:42:00 Finished basis                                              1h52m40s  11GB
May 10 11:42:01 Starting compiler/inference
May 10 11:45:30 Finished compiler/inference                                    3m29s   1GB
May 10 11:45:30 Starting compiler/backend/reg_alloc
May 10 11:48:47 Finished compiler/backend/reg_alloc                            3m16s   1GB
May 10 11:48:47 Starting compiler/backend/gc
May 10 11:57:35 Finished compiler/backend/gc                                   8m47s   3GB
May 10 11:57:35 Starting compiler/backend
May 10 12:09:01 Finished compiler/backend                                     11m25s   2GB
May 10 12:09:01 Starting compiler/encoders/asm
May 10 12:10:06 Finished compiler/encoders/asm                                 1m05s 816MB
May 10 12:10:07 Starting compiler/encoders/x64
May 10 12:12:37 Finished compiler/encoders/x64                                 2m30s   1GB
May 10 12:12:37 Starting compiler/encoders/arm7
May 10 12:17:21 Finished compiler/encoders/arm7                                4m43s   1GB
May 10 12:17:21 Starting compiler/encoders/arm8
May 10 12:18:54 Finished compiler/encoders/arm8                                1m33s   1GB
May 10 12:18:54 Starting compiler/encoders/arm8_asl
May 10 16:41:01 Finished compiler/encoders/arm8_asl                         4h22m05s  42GB
May 10 16:41:01 Starting compiler/encoders/mips
May 10 16:44:23 Finished compiler/encoders/mips                                3m22s 986MB
May 10 16:44:24 Starting compiler/encoders/riscv
May 10 16:48:15 Finished compiler/encoders/riscv                               3m51s 869MB
May 10 16:48:15 Starting compiler/encoders/ag32
May 10 16:49:04 Finished compiler/encoders/ag32                                  48s 657MB
May 10 16:49:04 Starting compiler/backend/x64
May 10 16:49:53 Finished compiler/backend/x64                                    48s   1GB
May 10 16:49:53 Starting compiler/backend/arm7
May 10 16:50:44 Finished compiler/backend/arm7                                   51s   1GB
May 10 16:50:44 Starting compiler/backend/arm8
May 10 16:51:33 Finished compiler/backend/arm8                                   48s   1GB
May 10 16:51:33 Starting compiler/backend/mips
May 10 16:52:22 Finished compiler/backend/mips                                   49s   1GB
May 10 16:52:23 Starting compiler/backend/riscv
May 10 16:53:12 Finished compiler/backend/riscv                                  49s   1GB
May 10 16:53:13 Starting compiler/backend/ag32
May 10 16:56:15 Finished compiler/backend/ag32                                 3m02s   1GB
May 10 16:56:16 Starting compiler/parsing/proofs
May 10 17:04:50 Finished compiler/parsing/proofs                               8m34s   1GB
May 10 17:04:50 Starting compiler/inference/proofs
May 10 17:10:50 Finished compiler/inference/proofs                             5m59s   1GB
May 10 17:10:50 Starting compiler/backend/semantics
May 10 18:20:31 Finished compiler/backend/semantics                         1h09m40s   2GB
May 10 18:20:32 Starting compiler/backend/reg_alloc/proofs
May 10 18:28:34 Finished compiler/backend/reg_alloc/proofs                     8m02s   1GB
May 10 18:28:34 Starting compiler/backend/proofs
May 10 20:16:04 Finished compiler/backend/proofs                            1h47m29s  19GB
May 10 20:16:04 Starting compiler/backend/serialiser
May 10 20:19:25 Finished compiler/backend/serialiser                           3m20s   2GB
May 10 20:19:25 Starting compiler/encoders/x64/proofs
May 10 20:41:18 Finished compiler/encoders/x64/proofs                         21m52s   4GB
May 10 20:41:18 Starting compiler/encoders/arm7/proofs
May 10 21:11:14 Finished compiler/encoders/arm7/proofs                        29m56s   6GB
May 10 21:11:15 Starting compiler/encoders/arm8/proofs
May 10 21:26:36 Finished compiler/encoders/arm8/proofs                        15m20s   1GB
May 10 21:26:36 Starting compiler/encoders/arm8_asl/proofs
May 10 23:18:26 Finished compiler/encoders/arm8_asl/proofs                  1h51m49s   6GB
May 10 23:18:27 Starting compiler/encoders/mips/proofs
May 10 23:40:58 Finished compiler/encoders/mips/proofs                        22m31s   3GB
May 10 23:40:59 Starting compiler/encoders/riscv/proofs
May 11 00:00:46 Finished compiler/encoders/riscv/proofs                       19m46s   1GB
May 11 00:00:46 Starting compiler/encoders/ag32/proofs
May 11 00:06:32 Finished compiler/encoders/ag32/proofs                         5m46s 859MB
May 11 00:06:33 Starting compiler/backend/x64/proofs
May 11 00:07:35 Finished compiler/backend/x64/proofs                           1m02s   1GB
May 11 00:07:36 Starting compiler/backend/arm7/proofs
May 11 00:08:36 Finished compiler/backend/arm7/proofs                          1m00s   1GB
May 11 00:08:36 Starting compiler/backend/arm8/proofs
May 11 00:09:40 Finished compiler/backend/arm8/proofs                          1m03s   1GB
May 11 00:09:40 Starting compiler/backend/arm8_asl
May 11 00:10:31 Finished compiler/backend/arm8_asl                               50s   1GB
May 11 00:10:31 Starting compiler/backend/mips/proofs
May 11 00:11:30 Finished compiler/backend/mips/proofs                            58s   1GB
May 11 00:11:30 Starting compiler/backend/riscv/proofs
May 11 00:12:34 Finished compiler/backend/riscv/proofs                         1m03s   1GB
May 11 00:12:35 Starting compiler/backend/ag32/proofs
May 11 00:42:41 Finished compiler/backend/ag32/proofs                         30m05s   3GB
May 11 00:42:41 Starting compiler/proofs
May 11 00:47:55 Finished compiler/proofs                                       5m14s   4GB
May 11 00:47:55 Starting candle/set-theory
May 11 00:49:06 Finished candle/set-theory                                     1m10s   1GB
May 11 00:49:07 Starting candle/syntax-lib
May 11 00:49:35 Finished candle/syntax-lib                                       28s 733MB
May 11 00:49:36 Starting candle/standard/syntax
May 11 00:54:03 Finished candle/standard/syntax                                4m27s   1GB
May 11 00:54:03 Starting candle/standard/semantics
May 11 00:58:06 Finished candle/standard/semantics                             4m03s   1GB
May 11 00:58:07 Starting candle/standard/monadic
May 11 01:02:09 Finished candle/standard/monadic                               4m02s   1GB
May 11 01:02:09 Starting candle/standard/ml_kernel
May 11 01:16:02 Finished candle/standard/ml_kernel                            13m52s   3GB
May 11 01:16:03 Starting candle/overloading/syntax
May 11 01:22:53 Finished candle/overloading/syntax                             6m50s   1GB
May 11 01:22:53 Starting candle/overloading/semantics
May 11 01:49:13 Finished candle/overloading/semantics                         26m19s   2GB
May 11 01:49:13 Starting candle/overloading/monadic
May 11 01:54:49 Finished candle/overloading/monadic                            5m35s   2GB
May 11 01:54:49 Starting candle/overloading/ml_kernel
May 11 02:10:26 Finished candle/overloading/ml_kernel                         15m37s   3GB
May 11 02:10:27 Starting candle/overloading/ml_checker
May 11 02:15:53 Finished candle/overloading/ml_checker                         5m25s   2GB
May 11 02:15:53 Starting candle/prover
May 11 02:39:36 Finished candle/prover                                        23m42s   2GB
May 11 02:39:36 Starting pancake
May 11 02:47:31 Finished pancake                                               7m54s   3GB
May 11 02:47:31 Starting pancake/ffi
May 11 02:47:32 Finished pancake/ffi                                              0s  30MB
May 11 02:47:32 Starting pancake/semantics
May 11 02:52:51 Finished pancake/semantics                                     5m18s   1GB
May 11 02:52:51 Starting pancake/proofs
May 11 03:19:12 Finished pancake/proofs                                       26m20s   6GB
May 11 03:19:12 Starting characteristic/examples
May 11 03:22:12 Finished characteristic/examples                               3m00s   2GB
May 11 03:22:12 Starting tutorial/solutions
May 11 03:59:25 Finished tutorial/solutions                                   37m12s   9GB
May 11 03:59:25 Starting translator/monadic/examples
May 11 04:06:40 Finished translator/monadic/examples                           7m14s   3GB
May 11 04:06:40 Starting examples
May 11 04:26:13 Finished examples                                             19m32s   3GB
May 11 04:26:14 Starting examples/compilation/x64
May 11 10:06:55 Finished examples/compilation/x64                           5h40m40s  25GB
May 11 10:06:55 Starting examples/compilation/x64/proofs
May 11 10:11:35 Finished examples/compilation/x64/proofs                       4m40s   3GB
May 11 10:11:36 Starting examples/compilation/ag32
May 11 11:31:23 Finished examples/compilation/ag32                          1h19m46s  11GB
May 11 11:31:23 Starting examples/compilation/ag32/proofs
May 11 11:33:19 Finished examples/compilation/ag32/proofs                      1m55s   3GB
May 11 11:33:19 Starting examples/cost
May 11 13:39:57 Finished examples/cost                                      2h06m37s  10GB
May 11 13:39:58 Starting examples/lpr_checker
May 11 13:42:10 Finished examples/lpr_checker                                  2m11s   1GB
May 11 13:42:10 Starting examples/lpr_checker/array
May 11 14:57:53 Finished examples/lpr_checker/array                         1h15m41s   5GB
May 11 14:57:53 Starting examples/lpr_checker/array/compilation
May 11 18:02:59 Finished examples/lpr_checker/array/compilation             3h05m05s  37GB
May 11 18:03:00 Starting examples/lpr_checker/array/compilation/proofs
May 11 18:06:00 Finished examples/lpr_checker/array/compilation/proofs         3m00s   6GB
May 11 18:06:01 Starting examples/opentheory
May 11 18:28:59 Finished examples/opentheory                                  22m57s   6GB
May 11 18:28:59 Starting examples/opentheory
May 11 18:29:02 Finished examples/opentheory                                      2s  35MB
May 11 18:29:02 Starting examples/opentheory/compilation
May 11 19:56:52 Finished examples/opentheory/compilation                    1h27m49s  29GB
May 11 19:56:52 Starting examples/opentheory/compilation/proofs
May 11 19:58:58 Finished examples/opentheory/compilation/proofs                2m06s   4GB
May 11 19:58:59 Starting examples/opentheory/compilation/ag32
May 11 21:29:08 Finished examples/opentheory/compilation/ag32               1h30m08s  41GB
May 11 21:29:08 Starting examples/opentheory/compilation/ag32/proofs
May 11 21:33:08 Finished examples/opentheory/compilation/ag32/proofs           4m00s   6GB
May 11 21:33:09 Starting examples/sat_encodings
May 11 21:37:33 Finished examples/sat_encodings                                4m23s 948MB
May 11 21:37:33 Starting examples/sat_encodings/case_studies
May 11 21:41:12 Finished examples/sat_encodings/case_studies                   3m38s 926MB
May 11 21:41:12 Starting examples/sat_encodings/translation
May 11 21:53:06 Finished examples/sat_encodings/translation                   11m53s   3GB
May 11 21:53:06 Starting examples/sat_encodings/translation/compilation
May 11 23:22:32 Finished examples/sat_encodings/translation/compilation     1h29m24s  28GB
May 11 23:22:32 Starting translator/okasaki-examples
May 11 23:32:51 Finished translator/okasaki-examples                          10m19s   1GB
May 11 23:32:52 Starting translator/other-examples
May 11 23:36:30 Finished translator/other-examples                             3m37s   1GB
May 11 23:36:30 Starting compiler/parsing/tests
May 11 23:37:36 Finished compiler/parsing/tests                                1m06s 546MB
May 11 23:37:37 Starting compiler/inference/tests
May 11 23:54:08 Finished compiler/inference/tests                             16m30s   5GB
May 11 23:54:08 Starting compiler/printing/test
May 12 00:01:46 Finished compiler/printing/test                                7m38s   3GB
May 12 00:01:46 Starting icing/flover
May 12 00:29:29 Finished icing/flover                                         27m42s   1GB
May 12 00:29:29 Starting icing/
May 12 02:44:19 Finished icing/                                             2h14m49s   7GB
May 12 02:44:20 Starting icing/examples
May 12 02:47:19 Finished icing/examples                                        2m59s   3GB
May 12 02:47:19 Starting compiler/repl
May 12 03:13:55 Finished compiler/repl                                        26m35s   5GB
May 12 03:13:55 Starting compiler/bootstrap/translation
May 12 12:24:40 Finished compiler/bootstrap/translation                     9h10m44s  40GB
May 12 12:24:40 Starting unverified/sexpr-bootstrap/x64/64
May 12 12:48:05 Finished unverified/sexpr-bootstrap/x64/64                    23m24s  11GB
May 12 12:48:05 Starting unverified/sexpr-bootstrap/x64/32
May 12 13:07:08 Finished unverified/sexpr-bootstrap/x64/32                    19m03s  10GB
May 12 13:07:09 Starting compiler/benchmarks
May 12 13:07:14 Finished compiler/benchmarks                                      5s  44MB
May 12 13:07:15 Starting compiler/bootstrap/compilation/x64/64
May 14 03:09:00 Finished compiler/bootstrap/compilation/x64/64             38h01m45s  80GB
May 14 03:09:01 Starting compiler/bootstrap/compilation/x64/64/proofs
May 14 03:27:54 FAILED: compiler/bootstrap/compilation/x64/64/proofs
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$(CAKEMLDIR)/candle/standard/ml_kernel/lisp[0m
Scanning [1m$(CAKEMLDIR)/candle/syntax-lib[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/syntax[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/monadic[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/ml_kernel[0m
Scanning [1m$(CAKEMLDIR)/candle/set-theory[0m
Scanning [1m$(CAKEMLDIR)/candle/standard/semantics[0m
Scanning [1m$(CAKEMLDIR)/candle/prover[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/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/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/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/x64/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/x64[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
Scanning [1m$(CAKEMLDIR)/compiler/encoders/ag32[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/ag32[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/model[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/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/serialiser[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/monadic_enc[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing/ocaml[0m
Scanning [1m$(CAKEMLDIR)/compiler/printing[0m
Scanning [1m$(CAKEMLDIR)/compiler/repl[0m
Scanning [1m$(CAKEMLDIR)/compiler/bootstrap/translation[0m
Scanning [1m$(CAKEMLDIR)/unverified/sexpr-bootstrap[0m
Scanning [1m$(CAKEMLDIR)/compiler/bootstrap/compilation/x64/64[0m
Scanned 99 directories
Starting work on README.md
Starting work on replProofTheory
README.md                                                                                                                                                                                             (0s)     OK
replProofTheory                                                                                                                                                                                      (17m)FAIL<1>
 s.compiler = compiler_inst x64_config 
 s.decode_decs = v_fun_abs decs_allowed (LIST_v AST_DEC_v) 
 s.env_id_counter = (0,0,1)  has_repl_flag (TL cl)  wfcl cl  wfFS fs 
 STD_streams fs  hasFreeFD fs  ... .compiler_state = ... ...  ... = ... 
 ... = ... 
 res  Rerr (Rabort Rtype_error)
 
 failed.
 Failed to prove theorem evaluate_decs_compiler64_prog.
 Uncaught exception: HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 1143) (THEN1 on line 1161) (THEN1 on line 1171) (THEN1 on line 1177) (THEN1 on line 1180) (THEN1 on line 1192) (THEN1 on line 1195) (THEN1 on line 1208) (THEN1 on line 1219) (THEN1 on line 1222) (THEN1 on line 1225) (THEN1 on line 1238) (THEN1 on line 1241) (THEN1 on line 1257) (THEN1 on line 1264) (THEN1 on line 1266)", origin_function = "THEN1", origin_structure = "Tactical"}