Job 3214

CakeML:ba73c51089c061c53a95857d8ebc8afa8bfdd751
  Merge remote-tracking branch 'origin/master' into string_cmp [Feb 10 21:37:10]
#1331 (string_cmp)
Merging into:c98da7fc904c5d6d0e9a75a18fac1796a9bfb1f9
  Adds simple optimization of store reads/writes in wordLang (#1327) [Feb 09 04:44:26]
HOL:b725f6e8834462a5b4bb2fb67b35e36f368cb8b6
  Tweak regular Holmakefile to clean selftest's log [Jan 30 05:30:27]
Machine:timtam

Feb 10 21:51:23 Claimed job
Feb 10 21:51:28 Reusing HOL
Feb 10 21:51:36 Starting developers
Feb 10 21:51:41 Finished developers                                               4s 188MB
Feb 10 21:51:42 Starting developers/bin
Feb 10 21:51:47 Finished developers/bin                                           4s  90MB
Feb 10 21:51:48 Starting misc
Feb 10 21:52:30 Finished misc                                                    40s   1GB
Feb 10 21:52:30 Starting compiler/proofs
Feb 10 22:52:07 Finished compiler/proofs                                      59m36s  10GB
Feb 10 22:52:08 Starting compiler/bootstrap/compilation/x64/64/proofs
Feb 11 04:51:33 Finished compiler/bootstrap/compilation/x64/64/proofs       5h59m24s  65GB
Feb 11 04:51:34 Starting semantics/ffi
Feb 11 04:51:45 Finished semantics/ffi                                           10s 538MB
Feb 11 04:51:46 Starting semantics
Feb 11 04:51:48 Finished semantics                                                1s  89MB
Feb 11 04:51:49 Starting semantics/proofs
Feb 11 04:52:12 Finished semantics/proofs                                        22s 954MB
Feb 11 04:52:13 Starting semantics/alt_semantics
Feb 11 04:52:32 Finished semantics/alt_semantics                                 18s 710MB
Feb 11 04:52:33 Starting semantics/alt_semantics/proofs
Feb 11 04:55:59 Finished semantics/alt_semantics/proofs                        3m24s   1GB
Feb 11 04:56:00 Starting basis/pure
Feb 11 04:56:01 Finished basis/pure                                               0s  92MB
Feb 11 04:56:02 Starting translator
Feb 11 04:57:08 Finished translator                                            1m04s   3GB
Feb 11 04:57:09 Starting compiler/parsing
Feb 11 04:57:11 Finished compiler/parsing                                         1s 101MB
Feb 11 04:57:12 Starting characteristic
Feb 11 04:57:14 Finished characteristic                                           1s 127MB
Feb 11 04:57:15 Starting translator/monadic
Feb 11 04:57:17 Finished translator/monadic                                       1s 116MB
Feb 11 04:57:18 Starting translator/monadic/monad_base
Feb 11 04:57:20 Finished translator/monadic/monad_base                            0s  97MB
Feb 11 04:57:21 Starting profiler
Feb 11 04:57:51 Finished profiler                                                29s   1GB
Feb 11 04:57:52 Starting basis
Feb 11 04:59:28 Finished basis                                                 1m35s   4GB
Feb 11 04:59:29 Starting compiler
Feb 11 04:59:32 Finished compiler                                                 2s 219MB
Feb 11 04:59:33 Starting compiler/inference
Feb 11 04:59:35 Finished compiler/inference                                       1s 119MB
Feb 11 04:59:36 Starting compiler/backend/reg_alloc
Feb 11 04:59:38 Finished compiler/backend/reg_alloc                               1s  94MB
Feb 11 04:59:39 Starting compiler/backend/gc
Feb 11 04:59:41 Finished compiler/backend/gc                                      1s 145MB
Feb 11 04:59:42 Starting compiler/backend
Feb 11 04:59:48 Finished compiler/backend                                         4s 246MB
Feb 11 04:59:49 Starting compiler/encoders/asm
Feb 11 04:59:51 Finished compiler/encoders/asm                                    1s  98MB
Feb 11 04:59:52 Starting compiler/encoders/x64
Feb 11 04:59:54 Finished compiler/encoders/x64                                    1s 107MB
Feb 11 04:59:54 Starting compiler/encoders/arm7
Feb 11 04:59:56 Finished compiler/encoders/arm7                                   1s 111MB
Feb 11 04:59:57 Starting compiler/encoders/arm8
Feb 11 04:59:59 Finished compiler/encoders/arm8                                   1s 105MB
Feb 11 05:00:00 Starting compiler/encoders/arm8_asl
Feb 11 05:00:15 Finished compiler/encoders/arm8_asl                              13s   1GB
Feb 11 05:00:15 Starting compiler/encoders/mips
Feb 11 05:00:17 Finished compiler/encoders/mips                                   1s 110MB
Feb 11 05:00:18 Starting compiler/encoders/riscv
Feb 11 05:00:20 Finished compiler/encoders/riscv                                  1s 106MB
Feb 11 05:00:21 Starting compiler/encoders/ag32
Feb 11 05:00:23 Finished compiler/encoders/ag32                                   1s 105MB
Feb 11 05:00:24 Starting compiler/encoders/tests
Feb 11 05:00:26 Finished compiler/encoders/tests                                  1s 120MB
Feb 11 05:00:27 Starting compiler/encoders/monadic_enc
Feb 11 05:00:51 Finished compiler/encoders/monadic_enc                           23s   1GB
Feb 11 05:00:52 Starting compiler/backend/x64
Feb 11 05:00:55 Finished compiler/backend/x64                                     1s 147MB
Feb 11 05:00:56 Starting compiler/backend/arm7
Feb 11 05:00:58 Finished compiler/backend/arm7                                    1s 145MB
Feb 11 05:00:59 Starting compiler/backend/arm8
Feb 11 05:01:01 Finished compiler/backend/arm8                                    1s 146MB
Feb 11 05:01:02 Starting compiler/backend/mips
Feb 11 05:01:05 Finished compiler/backend/mips                                    1s 145MB
Feb 11 05:01:05 Starting compiler/backend/riscv
Feb 11 05:01:08 Finished compiler/backend/riscv                                   1s 146MB
Feb 11 05:01:09 Starting compiler/backend/ag32
Feb 11 05:02:11 Finished compiler/backend/ag32                                 1m01s   3GB
Feb 11 05:02:11 Starting compiler/backend/pattern_matching
Feb 11 05:02:13 Finished compiler/backend/pattern_matching                        1s  90MB
Feb 11 05:02:14 Starting compiler/parsing/ocaml
Feb 11 05:03:58 Finished compiler/parsing/ocaml                                1m42s   1GB
Feb 11 05:03:59 Starting compiler/printing
Feb 11 05:04:53 Finished compiler/printing                                       54s   1GB
Feb 11 05:04:54 Starting compiler/parsing/proofs
Feb 11 05:04:56 Finished compiler/parsing/proofs                                  1s 103MB
Feb 11 05:04:57 Starting compiler/inference/proofs
Feb 11 05:04:59 Finished compiler/inference/proofs                                1s 120MB
Feb 11 05:05:00 Starting compiler/backend/semantics
Feb 11 05:06:59 Finished compiler/backend/semantics                            1m57s   2GB
Feb 11 05:06:59 Starting compiler/backend/reg_alloc/proofs
Feb 11 05:07:02 Finished compiler/backend/reg_alloc/proofs                        1s 119MB
Feb 11 05:07:02 Starting compiler/backend/proofs
Feb 11 05:07:43 Finished compiler/backend/proofs                                 39s   2GB
Feb 11 05:07:44 Starting compiler/backend/serialiser
Feb 11 05:07:47 Finished compiler/backend/serialiser                              1s 150MB
Feb 11 05:07:48 Starting compiler/encoders/x64/proofs
Feb 11 05:07:50 Finished compiler/encoders/x64/proofs                             1s 106MB
Feb 11 05:07:50 Starting compiler/encoders/arm7/proofs
Feb 11 05:18:27 Finished compiler/encoders/arm7/proofs                        10m35s   9GB
Feb 11 05:18:28 Starting compiler/encoders/arm8/proofs
Feb 11 05:25:00 Finished compiler/encoders/arm8/proofs                         6m30s   4GB
Feb 11 05:25:00 Starting compiler/encoders/arm8_asl/proofs
Feb 11 05:39:29 Finished compiler/encoders/arm8_asl/proofs                    14m27s   4GB
Feb 11 05:39:30 Starting compiler/encoders/mips/proofs
Feb 11 05:48:04 Finished compiler/encoders/mips/proofs                         8m33s  12GB
Feb 11 05:48:05 Starting compiler/encoders/riscv/proofs
Feb 11 05:55:55 Finished compiler/encoders/riscv/proofs                        7m48s   5GB
Feb 11 05:55:55 Starting compiler/encoders/ag32/proofs
Feb 11 05:58:30 Finished compiler/encoders/ag32/proofs                         2m34s   2GB
Feb 11 05:58:31 Starting compiler/backend/x64/proofs
Feb 11 05:58:35 Finished compiler/backend/x64/proofs                              2s 208MB
Feb 11 05:58:35 Starting compiler/backend/arm7/proofs
Feb 11 05:59:11 Finished compiler/backend/arm7/proofs                            34s   2GB
Feb 11 05:59:12 Starting compiler/backend/arm8/proofs
Feb 11 05:59:46 Finished compiler/backend/arm8/proofs                            33s   1GB
Feb 11 05:59:47 Starting compiler/backend/arm8_asl
Feb 11 06:00:11 Finished compiler/backend/arm8_asl                               23s   1GB
Feb 11 06:00:11 Starting compiler/backend/mips/proofs
Feb 11 06:00:47 Finished compiler/backend/mips/proofs                            35s   2GB
Feb 11 06:00:48 Starting compiler/backend/riscv/proofs
Feb 11 06:01:26 Finished compiler/backend/riscv/proofs                           36s   2GB
Feb 11 06:01:27 Starting compiler/backend/ag32/proofs
Feb 11 06:12:28 Finished compiler/backend/ag32/proofs                         11m00s   4GB
Feb 11 06:12:29 Starting compiler/backend/cv_compute
Feb 11 06:12:58 Finished compiler/backend/cv_compute                             27s   1GB
Feb 11 06:12:59 Starting cv_translator
Feb 11 06:18:25 Finished cv_translator                                         5m25s   4GB
Feb 11 06:18:26 Starting candle
Feb 11 06:18:26 Finished candle                                                   0s  15MB
Feb 11 06:18:27 Starting candle/set-theory
Feb 11 06:18:57 Finished candle/set-theory                                       28s 958MB
Feb 11 06:18:58 Starting candle/syntax-lib
Feb 11 06:18:59 Finished candle/syntax-lib                                        0s  87MB
Feb 11 06:19:00 Starting candle/standard
Feb 11 06:19:01 Finished candle/standard                                          0s  17MB
Feb 11 06:19:02 Starting candle/standard/syntax
Feb 11 06:19:16 Finished candle/standard/syntax                                  13s 777MB
Feb 11 06:19:17 Starting candle/standard/semantics
Feb 11 06:21:25 Finished candle/standard/semantics                             2m07s   3GB
Feb 11 06:21:26 Starting candle/standard/monadic
Feb 11 06:21:28 Finished candle/standard/monadic                                  1s 121MB
Feb 11 06:21:29 Starting candle/standard/ml_kernel
Feb 11 06:23:24 Finished candle/standard/ml_kernel                             1m54s   4GB
Feb 11 06:23:25 Starting candle/overloading
Feb 11 06:23:26 Finished candle/overloading                                       0s  15MB
Feb 11 06:23:27 Starting candle/overloading/syntax
Feb 11 06:26:31 Finished candle/overloading/syntax                             3m03s   2GB
Feb 11 06:26:32 Starting candle/overloading/semantics
Feb 11 06:36:50 Finished candle/overloading/semantics                         10m17s   6GB
Feb 11 06:36:51 Starting candle/overloading/monadic
Feb 11 06:38:56 Finished candle/overloading/monadic                            2m04s   1GB
Feb 11 06:38:57 Starting candle/overloading/ml_kernel
Feb 11 06:45:04 Finished candle/overloading/ml_kernel                          6m06s   7GB
Feb 11 06:45:05 Starting candle/overloading/ml_checker
Feb 11 06:47:24 Finished candle/overloading/ml_checker                         2m17s   6GB
Feb 11 06:47:25 Starting candle/prover
Feb 11 06:47:28 Finished candle/prover                                            2s 174MB
Feb 11 06:47:28 Starting candle/prover/compute
Feb 11 06:47:31 Finished candle/prover/compute                                    1s 163MB
Feb 11 06:47:32 Starting pancake
Feb 11 06:47:34 Finished pancake                                                  1s 149MB
Feb 11 06:47:35 Starting pancake/semantics
Feb 11 06:50:18 Finished pancake/semantics                                     2m41s   1GB
Feb 11 06:50:19 Starting pancake/parser
Feb 11 06:50:49 Finished pancake/parser                                          29s 745MB
Feb 11 06:50:50 Starting pancake/static_checker
Feb 11 06:51:55 Finished pancake/static_checker                                1m04s   1GB
Feb 11 06:51:56 Starting pancake/proofs
Feb 11 07:03:41 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/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)/examples/data-structures/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/pl-semantics/lprefix_lub
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(HOLDIR)/examples/algorithms
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
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 55 directories
Starting work on README.md
Starting work on crep_arithProofTheory
Starting work on crep_inlineProofTheory
Starting work on loop_callProofTheory
README.md                                                           (0s)     OK
Starting work on loop_removeProofTheory
crep_arithProofTheory                                               (6s)     OK
Starting work on pan_globalsProofTheory
loop_callProofTheory                                               (13s)     OK
Starting work on loop_liveProofTheory
loop_liveProofTheory                                               (16s)     OK
Starting work on crep_to_loopProofTheory
pan_globalsProofTheory                                             (52s)     OK
Starting work on pan_itreeEquivProofTheory
loop_removeProofTheory                                             (66s)     OK
Starting work on loop_to_wordProofTheory
crep_to_loopProofTheory                                            (42s)     OK
Starting work on pan_simpProofTheory
crep_inlineProofTheory                                            (110s)     OK
Starting work on pan_to_crepProofTheory
loop_to_wordProofTheory                                            (45s)     OK
pan_simpProofTheory                                                (36s)     OK
pan_to_crepProofTheory                                            (108s)     OK
Starting work on pan_to_wordProofTheory
pan_to_wordProofTheory                                             (85s)     OK
Starting work on pan_to_targetProofTheory
pan_itreeEquivProofTheory                                         (338s)     OK
pan_to_targetProofTheory                                          (377s)FAIL<1>
 
 compile_prog_max c mc pan_code = (SOME (bytes,bitmaps,c'),stack_max) 
 pancake_good_code pan_code  distinct_params (functions pan_code) 
 ALL_DISTINCT (MAP FST (functions pan_code))  s.code = FEMPTY 
 s.locals = FEMPTY  s.globals = FEMPTY 
 size_of_eids pan_code < dimword (:) 
 FDOM s.eshapes = FDOM (get_eids (functions pan_code))  backend_config_ok c 
 mc_conf_ok mc  mc_init_ok c mc  mc.target.config.ISA  Ag32 
 0w < mc.target.get_reg ms mc.len_reg 
 globals_size = SUM (MAP size_of_shape (dec_shapes (compile_prog pan_code))) 
 mc.target.get_reg ms mc.len_reg < mc.target.get_reg ms mc.ptr2_reg 
 mc.target.get_reg ms mc.len_reg = s.base_addr 
 globals_allocatable s pan_code 
 heap_len =
 w2n (mc.target.get_reg ms mc.ptr2_reg + -1w * s.base_addr) DIV
 (dimindex (:) DIV 8) 
 s.top_addr =
 s.base_addr + bytes_in_word * n2w heap_len 
 n2w (globals_size * dimindex (:) DIV 8)  globals_size  heap_len 
 s.memaddrs =
 addresses (mc.target.get_reg ms mc.len_reg) (heap_len  globals_size) 
 aligned (shift (:) + 1)
   (mc.target.get_reg ms mc.ptr2_reg + -1w * mc.target.get_reg ms mc.len_reg) 
 adj_ptr2 =
 mc.target.get_reg ms mc.len_reg + bytes_in_word * n2w max_stack_alloc 
 adj_ptr4 =
 mc.target.get_reg ms mc.len2_reg  bytes_in_word * n2w max_stack_alloc 
 adj_ptr2  mc.target.get_reg ms mc.ptr2_reg 
 mc.target.get_reg ms mc.ptr2_reg  adj_ptr4 
 w2n
   (mc.target.get_reg ms mc.ptr2_reg + -1w * mc.target.get_reg ms mc.len_reg) 
 w2n bytes_in_word * (2 * max_heap_limit (:) c.data_conf  1) 
 w2n bytes_in_word * (2 * max_heap_limit (:) c.data_conf  1) < dimword (:) 
 s.ffi = ffi  (mc.target.config.big_endian  s.be) 
 OPTION_ALL (EVERY (x. s. x = ExtCall s)) c.lab_conf.ffi_names 
 pan_installed bytes cbspace bitmaps data_sp c'.lab_conf.ffi_names
   (heap_regs c.stack_conf.reg_names) mc c'.lab_conf.shmem_extra ms
   (wlab_wloc  s.memory) s.memaddrs s.sh_memaddrs  start = main 
 semantics_decls s start pan_code  Fail 
 machine_sem mc ffi ms 
 extend_with_resource_limit'
   (option_lt stack_max (SOME (FST (read_limits c mc ms))))
   {semantics_decls s start pan_code}
 
 failed.
 
 Exception raised at boolLib.store_thm_at:
 at Tactical.THEN1:
   Failed to prove theorem "pan_to_target_compile_semantics":
 first subgoal not solved by second tactic
 Full log: /scratch/cakeml/regression2/cakeml-3214/pancake/proofs/.hol/logs/pan_to_targetProofTheory