Job 2816

CakeML:503c0ff7b7832c31a0f7d4ebc5303d4d5c2efc3a
  remove whitespace [Apr 30 13:50:01]
#1165 (pancake_internal32bit)
Merging into:3a32c44c6206176c9170037342ca7969e812114a
  Merge pull request #1166 from CakeML/UNCURRY_CONST_fix [May 02 15:46:26]
HOL:cf4347f8d871d793c021d04fe2bdc677c7149183
  Add UNCURRY_CONST [Apr 21 09:14:13]
Machine:lammmington

May 05 06:09:18 Claimed job
May 05 06:09:25 Reusing HOL
May 05 06:09:35 Starting developers
May 05 06:09:39 Finished developers                                               3s 211MB
May 05 06:09:40 Starting developers/bin
May 05 06:09:45 Finished developers/bin                                           3s 592MB
May 05 06:09:46 Starting misc
May 05 06:10:28 Finished misc                                                    41s   1GB
May 05 06:10:29 Starting compiler/proofs
May 05 07:54:28 Finished compiler/proofs                                    1h43m58s  34GB
May 05 07:54:29 Starting compiler/bootstrap/translation
May 05 13:34:44 Finished compiler/bootstrap/translation                     5h40m13s  86GB
May 05 13:34:45 Starting semantics/ffi
May 05 13:34:54 Finished semantics/ffi                                            8s 557MB
May 05 13:34:55 Starting semantics
May 05 13:34:57 Finished semantics                                                0s  51MB
May 05 13:34:58 Starting semantics/proofs
May 05 13:35:22 Finished semantics/proofs                                        23s   1GB
May 05 13:35:22 Starting semantics/alt_semantics
May 05 13:35:43 Finished semantics/alt_semantics                                 20s 882MB
May 05 13:35:44 Starting semantics/alt_semantics/proofs
May 05 13:45:58 Finished semantics/alt_semantics/proofs                       10m13s   2GB
May 05 13:45:59 Starting basis/pure
May 05 13:46:01 Finished basis/pure                                               0s  90MB
May 05 13:46:02 Starting translator
May 05 13:47:37 Finished translator                                            1m33s   2GB
May 05 13:47:38 Starting compiler/parsing
May 05 13:47:39 Finished compiler/parsing                                         0s  62MB
May 05 13:47:40 Starting characteristic
May 05 13:47:42 Finished characteristic                                           1s 119MB
May 05 13:47:43 Starting translator/monadic
May 05 13:47:45 Finished translator/monadic                                       1s 115MB
May 05 13:47:46 Starting translator/monadic/monad_base
May 05 13:47:47 Finished translator/monadic/monad_base                            0s  53MB
May 05 13:47:48 Starting basis
May 05 13:50:10 Finished basis                                                 2m21s   4GB
May 05 13:50:11 Starting compiler
May 05 13:50:14 Finished compiler                                                 1s 197MB
May 05 13:50:15 Starting compiler/inference
May 05 13:50:17 Finished compiler/inference                                       1s 112MB
May 05 13:50:18 Starting compiler/backend/reg_alloc
May 05 13:50:19 Finished compiler/backend/reg_alloc                               0s  59MB
May 05 13:50:20 Starting compiler/backend/gc
May 05 13:50:22 Finished compiler/backend/gc                                      1s 137MB
May 05 13:50:23 Starting compiler/backend
May 05 13:50:28 Finished compiler/backend                                         3s 271MB
May 05 13:50:29 Starting compiler/encoders/asm
May 05 13:50:31 Finished compiler/encoders/asm                                    0s  79MB
May 05 13:50:31 Starting compiler/encoders/x64
May 05 13:50:33 Finished compiler/encoders/x64                                    0s  86MB
May 05 13:50:34 Starting compiler/encoders/arm7
May 05 13:50:36 Finished compiler/encoders/arm7                                   0s  89MB
May 05 13:50:37 Starting compiler/encoders/arm8
May 05 13:50:38 Finished compiler/encoders/arm8                                   0s  88MB
May 05 13:50:39 Starting compiler/encoders/arm8_asl
May 05 15:52:30 Finished compiler/encoders/arm8_asl                         2h01m49s  41GB
May 05 15:52:31 Starting compiler/encoders/mips
May 05 15:52:32 Finished compiler/encoders/mips                                   0s  86MB
May 05 15:52:33 Starting compiler/encoders/riscv
May 05 15:52:35 Finished compiler/encoders/riscv                                  0s  85MB
May 05 15:52:36 Starting compiler/encoders/ag32
May 05 15:52:37 Finished compiler/encoders/ag32                                   0s  82MB
May 05 15:52:38 Starting compiler/encoders/tests
May 05 15:52:40 Finished compiler/encoders/tests                                  1s 115MB
May 05 15:52:41 Starting compiler/encoders/monadic_enc
May 05 15:52:43 Finished compiler/encoders/monadic_enc                            1s 140MB
May 05 15:52:44 Starting compiler/backend/x64
May 05 15:52:46 Finished compiler/backend/x64                                     1s 142MB
May 05 15:52:47 Starting compiler/backend/arm7
May 05 15:52:49 Finished compiler/backend/arm7                                    1s 142MB
May 05 15:52:50 Starting compiler/backend/arm8
May 05 15:52:52 Finished compiler/backend/arm8                                    1s 142MB
May 05 15:52:53 Starting compiler/backend/mips
May 05 15:52:55 Finished compiler/backend/mips                                    1s 141MB
May 05 15:52:56 Starting compiler/backend/riscv
May 05 15:52:58 Finished compiler/backend/riscv                                   1s 142MB
May 05 15:52:59 Starting compiler/backend/ag32
May 05 15:54:04 Finished compiler/backend/ag32                                 1m04s   2GB
May 05 15:54:05 Starting compiler/backend/pattern_matching
May 05 15:54:07 Finished compiler/backend/pattern_matching                        0s  54MB
May 05 15:54:08 Starting compiler/parsing/ocaml
May 05 15:55:51 Finished compiler/parsing/ocaml                                1m42s   1GB
May 05 15:55:51 Starting compiler/printing
May 05 15:55:53 Finished compiler/printing                                        1s 112MB
May 05 15:55:54 Starting compiler/parsing/proofs
May 05 15:55:56 Finished compiler/parsing/proofs                                  0s  62MB
May 05 15:55:57 Starting compiler/inference/proofs
May 05 15:55:59 Finished compiler/inference/proofs                                1s 113MB
May 05 15:56:00 Starting compiler/backend/semantics
May 05 15:59:07 Finished compiler/backend/semantics                            3m06s   2GB
May 05 15:59:08 Starting compiler/backend/reg_alloc/proofs
May 05 15:59:10 Finished compiler/backend/reg_alloc/proofs                        1s 125MB
May 05 15:59:11 Starting compiler/backend/proofs
May 05 15:59:57 Finished compiler/backend/proofs                                 44s   3GB
May 05 15:59:57 Starting compiler/backend/serialiser
May 05 16:00:00 Finished compiler/backend/serialiser                              1s 141MB
May 05 16:00:01 Starting compiler/encoders/x64/proofs
May 05 16:10:11 Finished compiler/encoders/x64/proofs                         10m09s   5GB
May 05 16:10:12 Starting compiler/encoders/arm7/proofs
May 05 16:23:19 Finished compiler/encoders/arm7/proofs                        13m06s   9GB
May 05 16:23:20 Starting compiler/encoders/arm8/proofs
May 05 16:30:14 Finished compiler/encoders/arm8/proofs                         6m53s   5GB
May 05 16:30:15 Starting compiler/encoders/arm8_asl/proofs
May 05 17:19:35 Finished compiler/encoders/arm8_asl/proofs                    49m19s  20GB
May 05 17:19:36 Starting compiler/encoders/mips/proofs
May 05 17:29:41 Finished compiler/encoders/mips/proofs                        10m03s   6GB
May 05 17:29:41 Starting compiler/encoders/riscv/proofs
May 05 17:37:49 Finished compiler/encoders/riscv/proofs                        8m06s   4GB
May 05 17:37:50 Starting compiler/encoders/ag32/proofs
May 05 17:40:41 Finished compiler/encoders/ag32/proofs                         2m49s   1GB
May 05 17:40:42 Starting compiler/backend/x64/proofs
May 05 17:41:14 Finished compiler/backend/x64/proofs                             31s   2GB
May 05 17:41:15 Starting compiler/backend/arm7/proofs
May 05 17:41:47 Finished compiler/backend/arm7/proofs                            30s   2GB
May 05 17:41:47 Starting compiler/backend/arm8/proofs
May 05 17:42:16 Finished compiler/backend/arm8/proofs                            27s   2GB
May 05 17:42:17 Starting compiler/backend/arm8_asl
May 05 17:42:38 Finished compiler/backend/arm8_asl                               20s   2GB
May 05 17:42:39 Starting compiler/backend/mips/proofs
May 05 17:43:09 Finished compiler/backend/mips/proofs                            29s   2GB
May 05 17:43:10 Starting compiler/backend/riscv/proofs
May 05 17:43:40 Finished compiler/backend/riscv/proofs                           29s   2GB
May 05 17:43:41 Starting compiler/backend/ag32/proofs
May 05 17:57:22 Finished compiler/backend/ag32/proofs                         13m39s   5GB
May 05 17:57:23 Starting compiler/backend/cv_compute
May 05 17:58:31 Finished compiler/backend/cv_compute                           1m07s   1GB
May 05 17:58:32 Starting cv_translator
May 05 18:18:46 Finished cv_translator                                        20m13s  11GB
May 05 18:18:46 Starting candle
May 05 18:18:47 Finished candle                                                   0s  11MB
May 05 18:18:48 Starting candle/set-theory
May 05 18:19:22 Finished candle/set-theory                                       32s   1GB
May 05 18:19:23 Starting candle/syntax-lib
May 05 18:19:24 Finished candle/syntax-lib                                        0s  89MB
May 05 18:19:25 Starting candle/standard
May 05 18:19:26 Finished candle/standard                                          0s  12MB
May 05 18:19:27 Starting candle/standard/syntax
May 05 18:19:40 Finished candle/standard/syntax                                  11s 759MB
May 05 18:19:41 Starting candle/standard/semantics
May 05 18:21:37 Finished candle/standard/semantics                             1m55s   2GB
May 05 18:21:38 Starting candle/standard/monadic
May 05 18:21:40 Finished candle/standard/monadic                                  1s 119MB
May 05 18:21:41 Starting candle/standard/ml_kernel
May 05 18:23:25 Finished candle/standard/ml_kernel                             1m42s   4GB
May 05 18:23:26 Starting candle/standard/ml_kernel/lisp
May 05 18:23:27 Finished candle/standard/ml_kernel/lisp                           0s  47MB
May 05 18:23:28 Starting candle/overloading
May 05 18:23:29 Finished candle/overloading                                       0s  11MB
May 05 18:23:30 Starting candle/overloading/syntax
May 05 18:26:39 Finished candle/overloading/syntax                             3m09s   2GB
May 05 18:26:40 Starting candle/overloading/semantics
May 05 18:37:38 Finished candle/overloading/semantics                         10m56s   8GB
May 05 18:37:38 Starting candle/overloading/monadic
May 05 18:39:59 Finished candle/overloading/monadic                            2m20s   2GB
May 05 18:40:00 Starting candle/overloading/ml_kernel
May 05 18:47:18 Finished candle/overloading/ml_kernel                          7m16s   6GB
May 05 18:47:19 Starting candle/overloading/ml_checker
May 05 18:49:30 Finished candle/overloading/ml_checker                         2m10s   6GB
May 05 18:49:31 Starting candle/prover
May 05 18:59:11 Finished candle/prover                                         9m38s   5GB
May 05 18:59:12 Starting candle/prover/compute
May 05 18:59:14 Finished candle/prover/compute                                    1s 147MB
May 05 18:59:15 Starting pancake
May 05 18:59:37 Finished pancake                                                 21s 803MB
May 05 18:59:38 Starting pancake/semantics
May 05 19:01:49 Finished pancake/semantics                                     2m09s   2GB
May 05 19:01:50 Starting pancake/parser
May 05 19:02:16 Finished pancake/parser                                          25s 442MB
May 05 19:02:17 Starting pancake/static_checker
May 05 19:02:54 Finished pancake/static_checker                                  36s   1GB
May 05 19:02:55 Starting pancake/proofs
May 05 19:04:18 FAILED: pancake/proofs
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(HOLDIR)/src/TeX
Scanning $(HOLDIR)/src/bag
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/src/ring/src
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/examples/machine-code/multiword
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)/examples/formal-languages/context-free
Scanning $(HOLDIR)/src/search
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(HOLDIR)/examples/algorithms
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/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/backend/gc
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/semantics/alt_semantics
Scanning $(CAKEMLDIR)/semantics/alt_semantics/proofs
Scanning $(CAKEMLDIR)/compiler/backend/semantics
Scanning $(CAKEMLDIR)/compiler/backend/proofs
Scanning $(CAKEMLDIR)/pancake
Scanning $(CAKEMLDIR)/pancake/semantics
Scanned 58 directories
Starting work on README.md
Starting work on crep_arithProofTheory
Starting work on loop_callProofTheory
Starting work on loop_removeProofTheory
README.md                                                           (0s)     OK
Starting work on panItreeSemEquivTheory
crep_arithProofTheory                                               (7s)     OK
Starting work on pan_simpProofTheory
loop_callProofTheory                                               (16s)     OK
Starting work on loop_liveProofTheory
loop_liveProofTheory                                               (18s)     OK
Starting work on crep_to_loopProofTheory
pan_simpProofTheory                                                (48s)     OK
Starting work on pan_to_crepProofTheory
pan_to_crepProofTheory                                             (18s)FAIL<1>
 <<HOL message: Created theory "pan_to_crepProof">>
 Saved definition ____ "excp_rel_def"
 Saved definition ____ "ctxt_fc_def"
 Saved definition ____ "code_rel_def"
 Saved definition ____ "state_rel_def"
 Saved definition ____ "locals_rel_def"
 Saved theorem _______ "code_rel_imp"
 Saved theorem _______ "code_rel_empty_locals"
 Saved theorem _______ "cexp_heads_eq"
 Saved theorem _______ "compile_exp_val_rel"
 Saved theorem _______ "mem_comp_field_lem"
 Saved theorem _______ "MEM_compile_exp_vmax"
 Saved definition ____ "globals_lookup_def"
 Saved theorem _______ "compile_Skip_Break_Continue_Annot"
 Saved theorem _______ "compile_Tick"
 Saved theorem _______ "locals_rel_lookup_ctxt"
 Saved theorem _______ "eval_nested_assign_distinct_eq"
 Saved theorem _______ "eval_nested_decs_seq_res_var_eq"
 Saved theorem _______ "mem_comp_field"
 Saved theorem _______ "eval_var_cexp_present_ctxt"
 Saved theorem _______ "compile_Assign"
 Saved theorem _______ "not_mem_context_assigned_mem_gt"
 Saved theorem _______ "rewritten_context_unassigned"
 Saved theorem _______ "ctxt_max_el_leq"
 Saved theorem _______ "compile_Dec"
 Saved theorem _______ "compile_Store"
 Saved theorem _______ "compile_Store32"
 error in quse /scratch/cakeml/regression2/cakeml-2816/pancake/proofs/pan_to_crepProofScript.sml : DUP "compile_Store32"
 error in load /scratch/cakeml/regression2/cakeml-2816/pancake/proofs/pan_to_crepProofScript : DUP "compile_Store32"
 Uncaught exception at /scratch/cakeml/regression2/HOL-cf4347f8d871d793c021d04fe2bdc677c7149183/src/portableML/Table.sml:493: DUP "compile_Store32"
loop_removeProofTheory                                             (77s)MKILLED
panItreeSemEquivTheory                                             (75s)MKILLED
crep_to_loopProofTheory                                            (38s)MKILLED