Job 2878

CakeML:2a9deab6e91db380747768935512d60a84818734
  letrec progress/validity [May 31 01:26:21]
#1183 (scheme)
Merging into:95250d9f6b9bfe3b39fe1d30ea3932f6ad1b2036
  Fix some proofs [Jun 27 01:15:13]
HOL:718b3aaabc70079271693d5540ba16669c2e7ad2
  fix EVERY_CASE_TAC proof [Jun 24 17:29:02]
Machine:lammmington

Jun 28 13:41:38 Claimed job
Jun 28 13:41:43 Reusing HOL
Jun 28 13:41:54 Starting developers
Jun 28 13:41:58 Finished developers                                               3s 209MB
Jun 28 13:41:59 Starting developers/bin
Jun 28 13:42:05 Finished developers/bin                                           4s 592MB
Jun 28 13:42:05 Starting misc
Jun 28 13:42:45 Finished misc                                                    38s   1GB
Jun 28 13:42:46 Starting compiler/proofs
Jun 28 15:17:57 Finished compiler/proofs                                    1h35m10s  39GB
Jun 28 15:17:58 Starting compiler/bootstrap/translation
Jun 28 20:55:26 Finished compiler/bootstrap/translation                     5h37m24s  56GB
Jun 28 20:55:27 Starting semantics/ffi
Jun 28 20:55:36 Finished semantics/ffi                                            8s 557MB
Jun 28 20:55:37 Starting semantics
Jun 28 20:55:38 Finished semantics                                                0s  53MB
Jun 28 20:55:39 Starting semantics/proofs
Jun 28 20:56:01 Finished semantics/proofs                                        21s 745MB
Jun 28 20:56:02 Starting semantics/alt_semantics
Jun 28 20:56:23 Finished semantics/alt_semantics                                 20s 892MB
Jun 28 20:56:24 Starting semantics/alt_semantics/proofs
Jun 28 21:06:44 Finished semantics/alt_semantics/proofs                       10m18s   2GB
Jun 28 21:06:45 Starting basis/pure
Jun 28 21:06:46 Finished basis/pure                                               0s  95MB
Jun 28 21:06:47 Starting translator
Jun 28 21:08:23 Finished translator                                            1m34s   2GB
Jun 28 21:08:24 Starting compiler/parsing
Jun 28 21:08:25 Finished compiler/parsing                                         0s  61MB
Jun 28 21:08:26 Starting characteristic
Jun 28 21:08:28 Finished characteristic                                           1s 123MB
Jun 28 21:08:29 Starting translator/monadic
Jun 28 21:08:31 Finished translator/monadic                                       1s 115MB
Jun 28 21:08:32 Starting translator/monadic/monad_base
Jun 28 21:08:33 Finished translator/monadic/monad_base                            0s  51MB
Jun 28 21:08:34 Starting basis
Jun 28 21:11:00 Finished basis                                                 2m24s   4GB
Jun 28 21:11:00 Starting compiler
Jun 28 21:11:03 Finished compiler                                                 1s 211MB
Jun 28 21:11:04 Starting compiler/inference
Jun 28 21:11:06 Finished compiler/inference                                       1s 109MB
Jun 28 21:11:07 Starting compiler/backend/reg_alloc
Jun 28 21:11:08 Finished compiler/backend/reg_alloc                               0s  55MB
Jun 28 21:11:09 Starting compiler/backend/gc
Jun 28 21:11:11 Finished compiler/backend/gc                                      1s 140MB
Jun 28 21:11:12 Starting compiler/backend
Jun 28 21:11:17 Finished compiler/backend                                         4s 242MB
Jun 28 21:11:18 Starting compiler/encoders/asm
Jun 28 21:11:20 Finished compiler/encoders/asm                                    0s  77MB
Jun 28 21:11:21 Starting compiler/encoders/x64
Jun 28 21:11:22 Finished compiler/encoders/x64                                    0s  83MB
Jun 28 21:11:23 Starting compiler/encoders/arm7
Jun 28 21:11:25 Finished compiler/encoders/arm7                                   0s  90MB
Jun 28 21:11:26 Starting compiler/encoders/arm8
Jun 28 21:11:27 Finished compiler/encoders/arm8                                   0s  84MB
Jun 28 21:11:28 Starting compiler/encoders/arm8_asl
Jun 28 23:17:31 Finished compiler/encoders/arm8_asl                         2h06m01s  32GB
Jun 28 23:17:32 Starting compiler/encoders/mips
Jun 28 23:17:34 Finished compiler/encoders/mips                                   0s  82MB
Jun 28 23:17:34 Starting compiler/encoders/riscv
Jun 28 23:17:36 Finished compiler/encoders/riscv                                  0s  84MB
Jun 28 23:17:37 Starting compiler/encoders/ag32
Jun 28 23:17:39 Finished compiler/encoders/ag32                                   0s  88MB
Jun 28 23:17:40 Starting compiler/encoders/tests
Jun 28 23:17:41 Finished compiler/encoders/tests                                  0s 112MB
Jun 28 23:17:42 Starting compiler/encoders/monadic_enc
Jun 28 23:17:44 Finished compiler/encoders/monadic_enc                            1s 133MB
Jun 28 23:17:45 Starting compiler/backend/x64
Jun 28 23:17:47 Finished compiler/backend/x64                                     1s 130MB
Jun 28 23:17:48 Starting compiler/backend/arm7
Jun 28 23:17:50 Finished compiler/backend/arm7                                    1s 134MB
Jun 28 23:17:51 Starting compiler/backend/arm8
Jun 28 23:17:53 Finished compiler/backend/arm8                                    1s 134MB
Jun 28 23:17:54 Starting compiler/backend/mips
Jun 28 23:17:56 Finished compiler/backend/mips                                    1s 135MB
Jun 28 23:17:57 Starting compiler/backend/riscv
Jun 28 23:17:59 Finished compiler/backend/riscv                                   1s 130MB
Jun 28 23:18:00 Starting compiler/backend/ag32
Jun 28 23:19:06 Finished compiler/backend/ag32                                 1m04s   3GB
Jun 28 23:19:07 Starting compiler/backend/pattern_matching
Jun 28 23:19:08 Finished compiler/backend/pattern_matching                        0s  56MB
Jun 28 23:19:09 Starting compiler/parsing/ocaml
Jun 28 23:20:51 Finished compiler/parsing/ocaml                                1m40s   1GB
Jun 28 23:20:52 Starting compiler/printing
Jun 28 23:20:54 Finished compiler/printing                                        1s 108MB
Jun 28 23:20:55 Starting compiler/parsing/proofs
Jun 28 23:20:56 Finished compiler/parsing/proofs                                  0s  63MB
Jun 28 23:20:57 Starting compiler/inference/proofs
Jun 28 23:20:59 Finished compiler/inference/proofs                                1s 117MB
Jun 28 23:21:00 Starting compiler/backend/semantics
Jun 28 23:24:06 Finished compiler/backend/semantics                            3m04s   3GB
Jun 28 23:24:07 Starting compiler/backend/reg_alloc/proofs
Jun 28 23:24:09 Finished compiler/backend/reg_alloc/proofs                        1s 121MB
Jun 28 23:24:09 Starting compiler/backend/proofs
Jun 28 23:24:54 Finished compiler/backend/proofs                                 43s   1GB
Jun 28 23:24:55 Starting compiler/backend/serialiser
Jun 28 23:24:57 Finished compiler/backend/serialiser                              1s 148MB
Jun 28 23:24:58 Starting compiler/encoders/x64/proofs
Jun 28 23:35:17 Finished compiler/encoders/x64/proofs                         10m18s   4GB
Jun 28 23:35:18 Starting compiler/encoders/arm7/proofs
Jun 28 23:48:13 Finished compiler/encoders/arm7/proofs                        12m53s   5GB
Jun 28 23:48:14 Starting compiler/encoders/arm8/proofs
Jun 28 23:55:12 Finished compiler/encoders/arm8/proofs                         6m57s   4GB
Jun 28 23:55:13 Starting compiler/encoders/arm8_asl/proofs
Jun 29 00:45:00 Finished compiler/encoders/arm8_asl/proofs                    49m44s  20GB
Jun 29 00:45:01 Starting compiler/encoders/mips/proofs
Jun 29 00:54:55 Finished compiler/encoders/mips/proofs                         9m53s   6GB
Jun 29 00:54:56 Starting compiler/encoders/riscv/proofs
Jun 29 01:03:05 Finished compiler/encoders/riscv/proofs                        8m08s   4GB
Jun 29 01:03:06 Starting compiler/encoders/ag32/proofs
Jun 29 01:05:57 Finished compiler/encoders/ag32/proofs                         2m50s   1GB
Jun 29 01:05:58 Starting compiler/backend/x64/proofs
Jun 29 01:06:28 Finished compiler/backend/x64/proofs                             28s   2GB
Jun 29 01:06:29 Starting compiler/backend/arm7/proofs
Jun 29 01:06:58 Finished compiler/backend/arm7/proofs                            28s   2GB
Jun 29 01:06:59 Starting compiler/backend/arm8/proofs
Jun 29 01:07:27 Finished compiler/backend/arm8/proofs                            27s   1GB
Jun 29 01:07:28 Starting compiler/backend/arm8_asl
Jun 29 01:07:48 Finished compiler/backend/arm8_asl                               19s   1GB
Jun 29 01:07:49 Starting compiler/backend/mips/proofs
Jun 29 01:08:19 Finished compiler/backend/mips/proofs                            28s   1GB
Jun 29 01:08:20 Starting compiler/backend/riscv/proofs
Jun 29 01:08:52 Finished compiler/backend/riscv/proofs                           31s   2GB
Jun 29 01:08:53 Starting compiler/backend/ag32/proofs
Jun 29 01:22:30 Finished compiler/backend/ag32/proofs                         13m36s   4GB
Jun 29 01:22:30 Starting compiler/backend/cv_compute
Jun 29 01:23:40 Finished compiler/backend/cv_compute                           1m08s   2GB
Jun 29 01:23:41 Starting cv_translator
Jun 29 01:41:38 Finished cv_translator                                        17m56s   7GB
Jun 29 01:41:39 Starting candle
Jun 29 01:41:40 Finished candle                                                   0s  11MB
Jun 29 01:41:41 Starting candle/set-theory
Jun 29 01:42:14 Finished candle/set-theory                                       31s   1GB
Jun 29 01:42:15 Starting candle/syntax-lib
Jun 29 01:42:17 Finished candle/syntax-lib                                        0s  91MB
Jun 29 01:42:18 Starting candle/standard
Jun 29 01:42:18 Finished candle/standard                                          0s  10MB
Jun 29 01:42:19 Starting candle/standard/syntax
Jun 29 01:42:31 Finished candle/standard/syntax                                  10s 744MB
Jun 29 01:42:32 Starting candle/standard/semantics
Jun 29 01:44:27 Finished candle/standard/semantics                             1m53s   1GB
Jun 29 01:44:27 Starting candle/standard/monadic
Jun 29 01:44:29 Finished candle/standard/monadic                                  1s 124MB
Jun 29 01:44:30 Starting candle/standard/ml_kernel
Jun 29 01:46:15 Finished candle/standard/ml_kernel                             1m42s   4GB
Jun 29 01:46:16 Starting candle/standard/ml_kernel/lisp
Jun 29 01:46:17 Finished candle/standard/ml_kernel/lisp                           0s  51MB
Jun 29 01:46:18 Starting candle/overloading
Jun 29 01:46:19 Finished candle/overloading                                       0s  12MB
Jun 29 01:46:20 Starting candle/overloading/syntax
Jun 29 01:49:30 Finished candle/overloading/syntax                             3m09s   1GB
Jun 29 01:49:31 Starting candle/overloading/semantics
Jun 29 02:00:27 Finished candle/overloading/semantics                         10m54s   5GB
Jun 29 02:00:28 Starting candle/overloading/monadic
Jun 29 02:02:48 Finished candle/overloading/monadic                            2m19s   2GB
Jun 29 02:02:49 Starting candle/overloading/ml_kernel
Jun 29 02:09:57 Finished candle/overloading/ml_kernel                          7m06s   5GB
Jun 29 02:09:58 Starting candle/overloading/ml_checker
Jun 29 02:12:10 Finished candle/overloading/ml_checker                         2m11s   6GB
Jun 29 02:12:11 Starting candle/prover
Jun 29 02:21:42 Finished candle/prover                                         9m29s   5GB
Jun 29 02:21:43 Starting candle/prover/compute
Jun 29 02:21:45 Finished candle/prover/compute                                    1s 138MB
Jun 29 02:21:46 Starting pancake
Jun 29 02:21:48 Finished pancake                                                  1s 139MB
Jun 29 02:21:49 Starting pancake/semantics
Jun 29 02:23:56 Finished pancake/semantics                                     2m06s   2GB
Jun 29 02:23:57 Starting pancake/parser
Jun 29 02:24:23 Finished pancake/parser                                          24s 629MB
Jun 29 02:24:24 Starting pancake/static_checker
Jun 29 02:25:01 Finished pancake/static_checker                                  35s   1GB
Jun 29 02:25:02 Starting pancake/proofs
Jun 29 02:41:06 Finished pancake/proofs                                       16m03s   7GB
Jun 29 02:41:07 Starting compiler/dafny
Jun 29 02:44:08 Finished compiler/dafny                                        3m00s   9GB
Jun 29 02:44:09 Starting compiler/dafny/translation
Jun 29 03:03:31 Finished compiler/dafny/translation                           19m20s  21GB
Jun 29 03:03:32 Starting compiler/dafny/compilation
Jun 29 03:06:28 Finished compiler/dafny/compilation                            2m54s  11GB
Jun 29 03:06:29 Starting compiler/dafny/semantics
Jun 29 03:07:07 Finished compiler/dafny/semantics                                36s   1GB
Jun 29 03:07:08 Starting compiler/scheme
Jun 29 03:07:15 FAILED: compiler/scheme
Scanning $(HOLDIR)/src/bag
Scanning $(HOLDIR)/src/sort
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/algebra/base
Scanning $(HOLDIR)/src/algebra/construction
Scanning $(HOLDIR)/src/algebra
Scanning $(HOLDIR)/src/hol88
Scanning $(HOLDIR)/src/rational
Scanning $(HOLDIR)/src/real
Scanning $(HOLDIR)/src/real/analysis
Scanning $(HOLDIR)/examples/misc
Scanning $(HOLDIR)/examples/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/src/search
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/basis
Scanned 39 directories
Starting work on README.md
Starting work on scheme_astTheory
Starting work on scheme_valuesTheory
README.md                                                           (0s)     OK
scheme_valuesTheory                                                 (1s)     OK
scheme_astTheory                                                    (4s)FAIL<1>
 Saved theorem _______ "datatype_prim"
 Saved theorem _______ "prim_distinct"
 Saved theorem _______ "prim_nchotomy"
 Saved theorem _______ "prim_Axiom"
 Saved theorem _______ "prim_induction"
 Saved theorem _______ "prim_case_cong"
 Saved theorem _______ "prim_case_eq"
 <<HOL message: Defined type: "prim">>
 Saved theorem _______ "datatype_lit"
 Saved theorem _______ "lit_11"
 Saved theorem _______ "lit_distinct"
 Saved theorem _______ "lit_nchotomy"
 Saved theorem _______ "lit_Axiom"
 Saved theorem _______ "lit_induction"
 Saved theorem _______ "lit_case_cong"
 Saved theorem _______ "lit_case_eq"
 <<HOL message: Defined type: "lit">>
 Saved theorem _______ "datatype_exp"
 Saved theorem _______ "exp_11"
 Saved theorem _______ "exp_distinct"
 Saved theorem _______ "exp_nchotomy"
 Saved theorem _______ "exp_Axiom"
 Saved theorem _______ "exp_induction"
 Saved theorem _______ "exp_case_cong"
 Saved theorem _______ "exp_case_eq"
 <<HOL message: Defined type: "exp">>
 Saved theorem _______ "datatype_cont"
 Saved theorem _______ "cont_11"
 Saved theorem _______ "cont_distinct"
 Saved theorem _______ "cont_nchotomy"
 Saved theorem _______ "cont_Axiom"
 Saved theorem _______ "cont_induction"
 Saved theorem _______ "cont_case_cong"
 Saved theorem _______ "cont_case_eq"
 Saved theorem _______ "val_11"
 Saved theorem _______ "val_distinct"
 Saved theorem _______ "val_nchotomy"
 Saved theorem _______ "val_Axiom"
 Saved theorem _______ "val_induction"
 Saved theorem _______ "val_case_cong"
 Saved theorem _______ "val_case_eq"
 <<HOL message: Defined types: "cont", "val">>
 Saved definition ____ "lit_to_val_def"
 
 Exception raised at BasicProvers.Induct_on:
 at BasicProvers.find_subterm:
 No var with name "bs" free in goal, or in outer universal quantifiers
 error in quse /scratch/cakeml/regression3/cakeml-2878/compiler/scheme/scheme_astScript.sml : HOL_ERR {message = "at BasicProvers.Induct_on:\nat BasicProvers.find_subterm:\nNo var with name \"bs\" free in goal, or in outer universal quantifiers", origin_function = "tprove", origin_structure = "Defn", source_location = Loc_Unknown}
 error in load /scratch/cakeml/regression3/cakeml-2878/compiler/scheme/scheme_astScript : HOL_ERR {message = "at BasicProvers.Induct_on:\nat BasicProvers.find_subterm:\nNo var with name \"bs\" free in goal, or in outer universal quantifiers", origin_function = "tprove", origin_structure = "Defn", source_location = Loc_Unknown}
 Uncaught exception at /scratch/cakeml/regression3/HOL-718b3aaabc70079271693d5540ba16669c2e7ad2/src/num/termination/TotalDefn.sml:37: HOL_ERR {message = "at BasicProvers.Induct_on:\nat BasicProvers.find_subterm:\nNo var with name \"bs\" free in goal, or in outer universal quantifiers", origin_function = "tprove", origin_structure = "Defn", source_location = Loc_Unknown}