Overview

Job 1895

CakeML:27966171eba31e086a266c4870d0e3f41e74c5a6
  Merge branch 'master' into Iced_cake
#865 (Iced_cake)
Merging into:b22ea8e8ba7e6a7474e33f8273f526a9360cc788
  Merge pull request #883 from CakeML/pan-lemma
HOL:db0c48a4df81300b8f4ab65af329cee860f6d921
  Fix a l3_equivalence_misc proof
Machine:oven3

 Claimed job
 Building HOL
 Starting developers
 Finished developers                                               9s  95MB
 Starting developers/bin
 Finished developers/bin                                          12s   1GB
 Starting semantics/ffi
 Finished semantics/ffi                                           24s 253MB
 Starting semantics
 Finished semantics                                             5m22s   1GB
 Starting semantics/proofs
 Finished semantics/proofs                                     15m41s   1GB
 Starting semantics/alt_semantics
 Finished semantics/alt_semantics                                 59s 573MB
 Starting semantics/alt_semantics/proofs
 Finished semantics/alt_semantics/proofs                       25m18s   1GB
 Starting basis/pure
 Finished basis/pure                                            7m35s 905MB
 Starting translator
 Finished translator                                            7m51s   1GB
 Starting compiler/parsing
 Finished compiler/parsing                                      3m02s   5GB
 Starting characteristic
 Finished characteristic                                       14m39s   2GB
 Starting translator/monadic
 Finished translator/monadic                                    4m16s   1GB
 Starting basis
 Finished basis                                              1h52m40s  11GB
 Starting compiler/inference
 Finished compiler/inference                                    3m29s   1GB
 Starting compiler/backend/reg_alloc
 Finished compiler/backend/reg_alloc                            3m16s   1GB
 Starting compiler/backend/gc
 Finished compiler/backend/gc                                   8m47s   3GB
 Starting compiler/backend
 Finished compiler/backend                                     11m25s   2GB
 Starting compiler/encoders/asm
 Finished compiler/encoders/asm                                 1m05s 816MB
 Starting compiler/encoders/x64
 Finished compiler/encoders/x64                                 2m30s   1GB
 Starting compiler/encoders/arm7
 Finished compiler/encoders/arm7                                4m43s   1GB
 Starting compiler/encoders/arm8
 Finished compiler/encoders/arm8                                1m33s   1GB
 Starting compiler/encoders/arm8_asl
 Finished compiler/encoders/arm8_asl                         4h22m05s  42GB
 Starting compiler/encoders/mips
 Finished compiler/encoders/mips                                3m22s 986MB
 Starting compiler/encoders/riscv
 Finished compiler/encoders/riscv                               3m51s 869MB
 Starting compiler/encoders/ag32
 Finished compiler/encoders/ag32                                  48s 657MB
 Starting compiler/backend/x64
 Finished compiler/backend/x64                                    48s   1GB
 Starting compiler/backend/arm7
 Finished compiler/backend/arm7                                   51s   1GB
 Starting compiler/backend/arm8
 Finished compiler/backend/arm8                                   48s   1GB
 Starting compiler/backend/mips
 Finished compiler/backend/mips                                   49s   1GB
 Starting compiler/backend/riscv
 Finished compiler/backend/riscv                                  49s   1GB
 Starting compiler/backend/ag32
 Finished compiler/backend/ag32                                 3m02s   1GB
 Starting compiler/parsing/proofs
 Finished compiler/parsing/proofs                               8m34s   1GB
 Starting compiler/inference/proofs
 Finished compiler/inference/proofs                             5m59s   1GB
 Starting compiler/backend/semantics
 Finished compiler/backend/semantics                         1h09m40s   2GB
 Starting compiler/backend/reg_alloc/proofs
 Finished compiler/backend/reg_alloc/proofs                     8m02s   1GB
 Starting compiler/backend/proofs
 Finished compiler/backend/proofs                            1h47m29s  19GB
 Starting compiler/backend/serialiser
 Finished compiler/backend/serialiser                           3m20s   2GB
 Starting compiler/encoders/x64/proofs
 Finished compiler/encoders/x64/proofs                         21m52s   4GB
 Starting compiler/encoders/arm7/proofs
 Finished compiler/encoders/arm7/proofs                        29m56s   6GB
 Starting compiler/encoders/arm8/proofs
 Finished compiler/encoders/arm8/proofs                        15m20s   1GB
 Starting compiler/encoders/arm8_asl/proofs
 Finished compiler/encoders/arm8_asl/proofs                  1h51m49s   6GB
 Starting compiler/encoders/mips/proofs
 Finished compiler/encoders/mips/proofs                        22m31s   3GB
 Starting compiler/encoders/riscv/proofs
 Finished compiler/encoders/riscv/proofs                       19m46s   1GB
 Starting compiler/encoders/ag32/proofs
 Finished compiler/encoders/ag32/proofs                         5m46s 859MB
 Starting compiler/backend/x64/proofs
 Finished compiler/backend/x64/proofs                           1m02s   1GB
 Starting compiler/backend/arm7/proofs
 Finished compiler/backend/arm7/proofs                          1m00s   1GB
 Starting compiler/backend/arm8/proofs
 Finished compiler/backend/arm8/proofs                          1m03s   1GB
 Starting compiler/backend/arm8_asl
 Finished compiler/backend/arm8_asl                               50s   1GB
 Starting compiler/backend/mips/proofs
 Finished compiler/backend/mips/proofs                            58s   1GB
 Starting compiler/backend/riscv/proofs
 Finished compiler/backend/riscv/proofs                         1m03s   1GB
 Starting compiler/backend/ag32/proofs
 Finished compiler/backend/ag32/proofs                         30m05s   3GB
 Starting compiler/proofs
 Finished compiler/proofs                                       5m14s   4GB
 Starting candle/set-theory
 Finished candle/set-theory                                     1m10s   1GB
 Starting candle/syntax-lib
 Finished candle/syntax-lib                                       28s 733MB
 Starting candle/standard/syntax
 Finished candle/standard/syntax                                4m27s   1GB
 Starting candle/standard/semantics
 Finished candle/standard/semantics                             4m03s   1GB
 Starting candle/standard/monadic
 Finished candle/standard/monadic                               4m02s   1GB
 Starting candle/standard/ml_kernel
 Finished candle/standard/ml_kernel                            13m52s   3GB
 Starting candle/overloading/syntax
 Finished candle/overloading/syntax                             6m50s   1GB
 Starting candle/overloading/semantics
 Finished candle/overloading/semantics                         26m19s   2GB
 Starting candle/overloading/monadic
 Finished candle/overloading/monadic                            5m35s   2GB
 Starting candle/overloading/ml_kernel
 Finished candle/overloading/ml_kernel                         15m37s   3GB
 Starting candle/overloading/ml_checker
 Finished candle/overloading/ml_checker                         5m25s   2GB
 Starting candle/prover
 Finished candle/prover                                        23m42s   2GB
 Starting pancake
 Finished pancake                                               7m54s   3GB
 Starting pancake/ffi
 Finished pancake/ffi                                              0s  30MB
 Starting pancake/semantics
 Finished pancake/semantics                                     5m18s   1GB
 Starting pancake/proofs
 Finished pancake/proofs                                       26m20s   6GB
 Starting characteristic/examples
 Finished characteristic/examples                               3m00s   2GB
 Starting tutorial/solutions
 Finished tutorial/solutions                                   37m12s   9GB
 Starting translator/monadic/examples
 Finished translator/monadic/examples                           7m14s   3GB
 Starting examples
 Finished examples                                             19m32s   3GB
 Starting examples/compilation/x64
 Finished examples/compilation/x64                           5h40m40s  25GB
 Starting examples/compilation/x64/proofs
 Finished examples/compilation/x64/proofs                       4m40s   3GB
 Starting examples/compilation/ag32
 Finished examples/compilation/ag32                          1h19m46s  11GB
 Starting examples/compilation/ag32/proofs
 Finished examples/compilation/ag32/proofs                      1m55s   3GB
 Starting examples/cost
 Finished examples/cost                                      2h06m37s  10GB
 Starting examples/lpr_checker
 Finished examples/lpr_checker                                  2m11s   1GB
 Starting examples/lpr_checker/array
 Finished examples/lpr_checker/array                         1h15m41s   5GB
 Starting examples/lpr_checker/array/compilation
 Finished examples/lpr_checker/array/compilation             3h05m05s  37GB
 Starting examples/lpr_checker/array/compilation/proofs
 Finished examples/lpr_checker/array/compilation/proofs         3m00s   6GB
 Starting examples/opentheory
 Finished examples/opentheory                                  22m57s   6GB
 Starting examples/opentheory
 Finished examples/opentheory                                      2s  35MB
 Starting examples/opentheory/compilation
 Finished examples/opentheory/compilation                    1h27m49s  29GB
 Starting examples/opentheory/compilation/proofs
 Finished examples/opentheory/compilation/proofs                2m06s   4GB
 Starting examples/opentheory/compilation/ag32
 Finished examples/opentheory/compilation/ag32               1h30m08s  41GB
 Starting examples/opentheory/compilation/ag32/proofs
 Finished examples/opentheory/compilation/ag32/proofs           4m00s   6GB
 Starting examples/sat_encodings
 Finished examples/sat_encodings                                4m23s 948MB
 Starting examples/sat_encodings/case_studies
 Finished examples/sat_encodings/case_studies                   3m38s 926MB
 Starting examples/sat_encodings/translation
 Finished examples/sat_encodings/translation                   11m53s   3GB
 Starting examples/sat_encodings/translation/compilation
 Finished examples/sat_encodings/translation/compilation     1h29m24s  28GB
 Starting translator/okasaki-examples
 Finished translator/okasaki-examples                          10m19s   1GB
 Starting translator/other-examples
 Finished translator/other-examples                             3m37s   1GB
 Starting compiler/parsing/tests
 Finished compiler/parsing/tests                                1m06s 546MB
 Starting compiler/inference/tests
 Finished compiler/inference/tests                             16m30s   5GB
 Starting compiler/printing/test
 Finished compiler/printing/test                                7m38s   3GB
 Starting icing/flover
 Finished icing/flover                                         27m42s   1GB
 Starting icing/
 Finished icing/                                             2h14m49s   7GB
 Starting icing/examples
 Finished icing/examples                                        2m59s   3GB
 Starting compiler/repl
 Finished compiler/repl                                        26m35s   5GB
 Starting compiler/bootstrap/translation
 Finished compiler/bootstrap/translation                     9h10m44s  40GB
 Starting unverified/sexpr-bootstrap/x64/64
 Finished unverified/sexpr-bootstrap/x64/64                    23m24s  11GB
 Starting unverified/sexpr-bootstrap/x64/32
 Finished unverified/sexpr-bootstrap/x64/32                    19m03s  10GB
 Starting compiler/benchmarks
 Finished compiler/benchmarks                                      5s  44MB
 Starting compiler/bootstrap/compilation/x64/64
 Finished compiler/bootstrap/compilation/x64/64             38h01m45s  80GB
 Starting compiler/bootstrap/compilation/x64/64/proofs
 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"}