Job 2766

CakeML:777e7d300886ba28ac955d2e036c5efc83eefff3
  Minor work towards #1122 [Jan 25 08:59:29]
#1123 (remove_list_max)
Merging into:7a0bcc6c0345d8f4081aa961bbab662d063864f0
  Merge pull request #1119 from CakeML/ordinarymath-patch-1 [Jan 23 05:26:11]
HOL:5c113170525b75be2ec405b1079ec20d2008f2c4
  Remove some more adjoin_to* (from pairScript.sml) [Jan 20 23:55:48]
Machine:lammmington

Jan 25 09:21:47 Claimed job
Jan 25 09:21:52 Reusing HOL
Jan 25 09:22:03 Starting developers
Jan 25 09:22:07 Finished developers                                               2s 107MB
Jan 25 09:22:08 Starting developers/bin
Jan 25 09:22:14 Finished developers/bin                                           5s 745MB
Jan 25 09:22:15 Starting misc
Jan 25 09:22:58 Finished misc                                                    42s   2GB
Jan 25 09:22:59 Starting compiler/proofs
Jan 25 11:01:37 Finished compiler/proofs                                    1h38m36s  46GB
Jan 25 11:01:38 Starting compiler/bootstrap/translation
Jan 25 16:52:11 Finished compiler/bootstrap/translation                     5h50m32s  96GB
Jan 25 16:52:12 Starting semantics/ffi
Jan 25 16:52:22 Finished semantics/ffi                                            9s 598MB
Jan 25 16:52:23 Starting semantics
Jan 25 16:52:25 Finished semantics                                                0s  52MB
Jan 25 16:52:25 Starting semantics/proofs
Jan 25 16:52:48 Finished semantics/proofs                                        21s 864MB
Jan 25 16:52:49 Starting semantics/alt_semantics
Jan 25 16:53:10 Finished semantics/alt_semantics                                 19s 891MB
Jan 25 16:53:11 Starting semantics/alt_semantics/proofs
Jan 25 17:03:35 Finished semantics/alt_semantics/proofs                       10m23s   2GB
Jan 25 17:03:36 Starting basis/pure
Jan 25 17:03:37 Finished basis/pure                                               0s  63MB
Jan 25 17:03:38 Starting translator
Jan 25 17:05:13 Finished translator                                            1m33s   3GB
Jan 25 17:05:13 Starting compiler/parsing
Jan 25 17:05:15 Finished compiler/parsing                                         0s  57MB
Jan 25 17:05:16 Starting characteristic
Jan 25 17:05:18 Finished characteristic                                           0s  82MB
Jan 25 17:05:19 Starting translator/monadic
Jan 25 17:05:20 Finished translator/monadic                                       0s  86MB
Jan 25 17:05:21 Starting translator/monadic/monad_base
Jan 25 17:05:22 Finished translator/monadic/monad_base                            0s  53MB
Jan 25 17:05:23 Starting basis
Jan 25 17:07:50 Finished basis                                                 2m25s   3GB
Jan 25 17:07:51 Starting compiler
Jan 25 17:07:53 Finished compiler                                                 1s 197MB
Jan 25 17:07:54 Starting compiler/inference
Jan 25 17:07:56 Finished compiler/inference                                       0s  87MB
Jan 25 17:07:57 Starting compiler/backend/reg_alloc
Jan 25 17:07:58 Finished compiler/backend/reg_alloc                               0s  55MB
Jan 25 17:07:59 Starting compiler/backend/gc
Jan 25 17:08:01 Finished compiler/backend/gc                                      1s 133MB
Jan 25 17:08:02 Starting compiler/backend
Jan 25 17:08:07 Finished compiler/backend                                         4s 245MB
Jan 25 17:08:08 Starting compiler/encoders/asm
Jan 25 17:08:10 Finished compiler/encoders/asm                                    0s  81MB
Jan 25 17:08:11 Starting compiler/encoders/x64
Jan 25 17:08:12 Finished compiler/encoders/x64                                    0s  83MB
Jan 25 17:08:13 Starting compiler/encoders/arm7
Jan 25 17:08:15 Finished compiler/encoders/arm7                                   0s  87MB
Jan 25 17:08:16 Starting compiler/encoders/arm8
Jan 25 17:08:18 Finished compiler/encoders/arm8                                   0s  88MB
Jan 25 17:08:19 Starting compiler/encoders/arm8_asl
Jan 25 17:09:15 Finished compiler/encoders/arm8_asl                              55s  18GB
Jan 25 17:09:16 Starting compiler/encoders/mips
Jan 25 17:09:18 Finished compiler/encoders/mips                                   0s  90MB
Jan 25 17:09:19 Starting compiler/encoders/riscv
Jan 25 17:09:20 Finished compiler/encoders/riscv                                  0s  82MB
Jan 25 17:09:21 Starting compiler/encoders/ag32
Jan 25 17:09:23 Finished compiler/encoders/ag32                                   0s  86MB
Jan 25 17:09:24 Starting compiler/encoders/tests
Jan 25 17:09:26 Finished compiler/encoders/tests                                  1s 111MB
Jan 25 17:09:27 Starting compiler/encoders/monadic_enc
Jan 25 17:09:29 Finished compiler/encoders/monadic_enc                            1s 123MB
Jan 25 17:09:30 Starting compiler/backend/x64
Jan 25 17:09:32 Finished compiler/backend/x64                                     1s 125MB
Jan 25 17:09:33 Starting compiler/backend/arm7
Jan 25 17:09:35 Finished compiler/backend/arm7                                    1s 128MB
Jan 25 17:09:36 Starting compiler/backend/arm8
Jan 25 17:09:38 Finished compiler/backend/arm8                                    1s 123MB
Jan 25 17:09:39 Starting compiler/backend/mips
Jan 25 17:09:41 Finished compiler/backend/mips                                    1s 123MB
Jan 25 17:09:41 Starting compiler/backend/riscv
Jan 25 17:09:44 Finished compiler/backend/riscv                                   1s 125MB
Jan 25 17:09:44 Starting compiler/backend/ag32
Jan 25 17:10:51 Finished compiler/backend/ag32                                 1m05s   2GB
Jan 25 17:10:51 Starting compiler/backend/pattern_matching
Jan 25 17:10:53 Finished compiler/backend/pattern_matching                        0s  55MB
Jan 25 17:10:54 Starting compiler/parsing/ocaml
Jan 25 17:12:36 Finished compiler/parsing/ocaml                                1m41s   1GB
Jan 25 17:12:37 Starting compiler/printing
Jan 25 17:12:39 Finished compiler/printing                                        0s  90MB
Jan 25 17:12:40 Starting compiler/parsing/proofs
Jan 25 17:12:41 Finished compiler/parsing/proofs                                  0s  65MB
Jan 25 17:12:42 Starting compiler/inference/proofs
Jan 25 17:12:44 Finished compiler/inference/proofs                                0s  84MB
Jan 25 17:12:45 Starting compiler/backend/semantics
Jan 25 17:15:51 Finished compiler/backend/semantics                            3m05s   3GB
Jan 25 17:15:52 Starting compiler/backend/reg_alloc/proofs
Jan 25 17:15:54 Finished compiler/backend/reg_alloc/proofs                        0s  93MB
Jan 25 17:15:54 Starting compiler/backend/proofs
Jan 25 17:16:45 Finished compiler/backend/proofs                                 50s   3GB
Jan 25 17:16:46 Starting compiler/backend/serialiser
Jan 25 17:16:48 Finished compiler/backend/serialiser                              1s 137MB
Jan 25 17:16:49 Starting compiler/encoders/x64/proofs
Jan 25 17:27:01 Finished compiler/encoders/x64/proofs                         10m10s   5GB
Jan 25 17:27:02 Starting compiler/encoders/arm7/proofs
Jan 25 17:40:15 Finished compiler/encoders/arm7/proofs                        13m12s  10GB
Jan 25 17:40:16 Starting compiler/encoders/arm8/proofs
Jan 25 17:47:05 Finished compiler/encoders/arm8/proofs                         6m47s   3GB
Jan 25 17:47:05 Starting compiler/encoders/arm8_asl/proofs
Jan 25 18:02:31 Finished compiler/encoders/arm8_asl/proofs                    15m24s   3GB
Jan 25 18:02:32 Starting compiler/encoders/mips/proofs
Jan 25 18:12:44 Finished compiler/encoders/mips/proofs                        10m11s   7GB
Jan 25 18:12:45 Starting compiler/encoders/riscv/proofs
Jan 25 18:20:55 Finished compiler/encoders/riscv/proofs                        8m09s   3GB
Jan 25 18:20:56 Starting compiler/encoders/ag32/proofs
Jan 25 18:23:48 Finished compiler/encoders/ag32/proofs                         2m50s   1GB
Jan 25 18:23:49 Starting compiler/backend/x64/proofs
Jan 25 18:24:21 Finished compiler/backend/x64/proofs                             31s   2GB
Jan 25 18:24:22 Starting compiler/backend/arm7/proofs
Jan 25 18:24:52 Finished compiler/backend/arm7/proofs                            29s   1GB
Jan 25 18:24:53 Starting compiler/backend/arm8/proofs
Jan 25 18:25:25 Finished compiler/backend/arm8/proofs                            30s   2GB
Jan 25 18:25:26 Starting compiler/backend/arm8_asl
Jan 25 18:25:46 Finished compiler/backend/arm8_asl                               19s   1GB
Jan 25 18:25:47 Starting compiler/backend/mips/proofs
Jan 25 18:26:20 Finished compiler/backend/mips/proofs                            32s   2GB
Jan 25 18:26:21 Starting compiler/backend/riscv/proofs
Jan 25 18:26:55 Finished compiler/backend/riscv/proofs                           33s   2GB
Jan 25 18:26:56 Starting compiler/backend/ag32/proofs
Jan 25 18:40:41 Finished compiler/backend/ag32/proofs                         13m44s   5GB
Jan 25 18:40:42 Starting compiler/backend/cv_compute
Jan 25 18:41:53 Finished compiler/backend/cv_compute                           1m09s   2GB
Jan 25 18:41:54 Starting cv_translator
Jan 25 18:44:29 FAILED: cv_translator
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)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(HOLDIR)/src/ring/src
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/src/rational
Scanning $(HOLDIR)/src/num/theories/cv_compute/automation
Scanning $(HOLDIR)/examples/bootstrap
Scanning $(HOLDIR)/examples/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/src/search
Scanning $(HOLDIR)/examples/formal-languages/regular
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 $(HOLDIR)/examples/algorithms
Scanning $(HOLDIR)/examples/machine-code/multiword
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
Scanning $(HOLDIR)/src/algebra/base
Scanning $(HOLDIR)/src/algebra/construction
Scanning $(HOLDIR)/src/algebra
Scanning $(HOLDIR)/src/hol88
Scanning $(HOLDIR)/src/real
Scanning $(HOLDIR)/src/floating-point
Scanning $(HOLDIR)/src/monad/more_monads
Scanning $(HOLDIR)/src/update
Scanning $(HOLDIR)/examples/l3-machine-code/common
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/basis
Scanning $(CAKEMLDIR)/compiler/encoders/ag32
Scanning $(CAKEMLDIR)/compiler/backend/ag32
Scanning $(HOLDIR)/examples/l3-machine-code/lib
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/model
Scanning $(HOLDIR)/examples/machine-code/decompiler
Scanning $(HOLDIR)/examples/l3-machine-code
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm8
Scanning $(CAKEMLDIR)/compiler/backend/arm8
Scanning $(CAKEMLDIR)/compiler/backend/serialiser
Scanning $(HOLDIR)/examples/l3-machine-code/arm/model
Scanning $(HOLDIR)/examples/l3-machine-code/arm/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm7
Scanning $(HOLDIR)/examples/l3-machine-code/mips/model
Scanning $(HOLDIR)/examples/l3-machine-code/mips/step
Scanning $(CAKEMLDIR)/compiler/encoders/mips
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/model
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/step
Scanning $(CAKEMLDIR)/compiler/encoders/riscv
Scanning $(HOLDIR)/examples/l3-machine-code/x64/model
Scanning $(HOLDIR)/examples/l3-machine-code/x64/step
Scanning $(CAKEMLDIR)/compiler/encoders/x64
Scanning $(CAKEMLDIR)/compiler/backend/cv_compute
Scanning $(CAKEMLDIR)/compiler/backend/x64
Scanning $(HOLDIR)/examples/algorithms/unification/triangular
Scanning $(HOLDIR)/src/transfer/examples
Scanning $(HOLDIR)/examples/algorithms/unification/triangular/first-order
Scanning $(HOLDIR)/examples/algorithms/unification/triangular/first-order/compilation
Scanning $(CAKEMLDIR)/compiler/inference
Scanned 80 directories
Starting work on README.md
Starting work on to_data_cvTheory
Starting work on fmap_cvTheory
README.md                                                           (0s)     OK
fmap_cvTheory                                                      (11s)     OK
to_data_cvTheory                                                  (144s)FAIL<1>
 Finished translating max_dec_name, stored in cv_flat_pattern_max_dec_name_thm
 Starting translation of compile_exp_alt, compile_exp_alts_alt, compile_letexps_alt, compile_match_alt from to_data_cvTheory.
 Saved definition ____ "cv_compile_exp_alt_def"
 Saved induction _____ "cv_compile_exp_alt_ind"
 Saved theorem _______ "compile_exp_alt_pre_rules"
 Saved theorem _______ "compile_exp_alt_pre_ind"
 Saved theorem _______ "compile_exp_alt_pre_strongind"
 Saved theorem _______ "compile_exp_alt_pre_cases"
 Saved theorem _______ "cv_compile_exp_alt_thm"
 Finished translating compile_exp_alt, compile_exp_alts_alt, compile_letexps_alt, compile_match_alt, stored in cv_compile_exp_alt_thm
 
 WARNING: definition of cv_compile_exp_alt has a precondition.
 You can set up the precondition proof as follows:
 
 Theorem compile_exp_alt_pre[cv_pre]:
   (cfg v. compile_exp_alt_pre cfg v) 
   (cfg v. compile_exp_alts_alt_pre cfg v) 
   (cfg v. compile_letexps_alt_pre cfg v) 
   (cfg v. compile_match_alt_pre cfg v)
 Proof
   ho_match_mp_tac compile_exp_alt_ind (* for example *)
   ...
 QED
 
 Saved theorem _______ "compile_exp_alt_pre"
 Proof of 
 
 (cfg exp. compile_exp_alt cfg exp = compile_exp cfg exp) 
 (cfg xs. compile_exp_alts_alt cfg xs = compile_exps cfg xs) 
 (cfg xs.
    compile_letexps_alt cfg xs = MAP ((x,y,z). (x,y,compile_exp cfg z)) xs) 
 cfg xs. compile_match_alt cfg xs = compile_match cfg xs
 
 failed.
 First unsolved sub-goal is
 
 MAX i
   (list_max
      (MAP ((_,_,j,_,_). j) (MAP ((x,y,z). (x,y,compile_exp cfg z)) xs))) =
 MAX i
   (MAX_LIST
      (MAP ((_,_,j,_,_). j) (MAP ((a,b,c). (a,b,compile_exp cfg c)) xs)))
 
 Failed to prove theorem compile_exp_alt_thm.
 
 Exception raised at Tactical.TAC_PROOF:
 unsolved goals
 error in quse /scratch/cakeml/regression2/cakeml-2766/cv_translator/to_data_cvScript.sml : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical", source_location = Loc_Unknown}
 error in load /scratch/cakeml/regression2/cakeml-2766/cv_translator/to_data_cvScript : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical", source_location = Loc_Unknown}
 Uncaught exception at /scratch/cakeml/regression2/HOL-5c113170525b75be2ec405b1079ec20d2008f2c4/src/prekernel/Feedback.sml:124: HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical", source_location = Loc_Unknown}