Job 1788

CakeML:71680ad5cc7a726b2fbd647ad26a0827a8dc9435
  Prove PEG-completeness for system with more declaration nesting [Feb 11 00:10:20]
#862 (gh859)
Merging into:5c8c961383b431e16bfc2c6ba7e13d0e6a8cf7f7
  Fix basis for changes to ZIP and LUPDATE in HOL [Feb 23 14:31:57]
HOL:b2236d1e8f18d389921766fcda06075975394e9f
  Fix ZIP_ind test case [Feb 23 03:12:26]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Feb 23 14:35:04 Claimed job
Feb 23 14:35:08 Building HOL
Feb 23 14:46:49 Starting developers
Feb 23 14:46:54 Finished developers                                               4s 133MB
Feb 23 14:46:55 Starting developers/bin
Feb 23 14:47:00 Finished developers/bin                                           5s 670MB
Feb 23 14:47:01 Starting semantics/ffi
Feb 23 14:47:13 Finished semantics/ffi                                           11s 222MB
Feb 23 14:47:13 Starting semantics
Feb 23 14:49:55 Finished semantics                                             2m42s   1GB
Feb 23 14:49:56 Starting semantics/proofs
Feb 23 14:54:22 Finished semantics/proofs                                      4m26s   1GB
Feb 23 14:54:22 Starting semantics/alt_semantics
Feb 23 14:54:42 Finished semantics/alt_semantics                                 19s 459MB
Feb 23 14:54:42 Starting semantics/alt_semantics/proofs
Feb 23 14:57:38 Finished semantics/alt_semantics/proofs                        2m55s 774MB
Feb 23 14:57:38 Starting basis/pure
Feb 23 15:01:07 Finished basis/pure                                            3m29s 929MB
Feb 23 15:01:07 Starting translator
Feb 23 15:04:56 Finished translator                                            3m48s   1GB
Feb 23 15:04:56 Starting compiler/parsing
Feb 23 15:06:35 Finished compiler/parsing                                      1m38s   2GB
Feb 23 15:06:35 Starting characteristic
Feb 23 15:14:08 Finished characteristic                                        7m33s   2GB
Feb 23 15:14:08 Starting translator/monadic
Feb 23 15:16:34 Finished translator/monadic                                    2m24s   1GB
Feb 23 15:16:34 Starting basis
Feb 23 16:11:55 Finished basis                                                55m21s   6GB
Feb 23 16:11:56 Starting compiler/inference
Feb 23 16:13:37 Finished compiler/inference                                    1m41s   1GB
Feb 23 16:13:37 Starting compiler/backend/reg_alloc
Feb 23 16:15:40 Finished compiler/backend/reg_alloc                            2m02s   1GB
Feb 23 16:15:40 Starting compiler/backend/gc
Feb 23 16:21:09 Finished compiler/backend/gc                                   5m27s   1GB
Feb 23 16:21:09 Starting compiler/backend
Feb 23 16:28:08 Finished compiler/backend                                      6m58s   2GB
Feb 23 16:28:08 Starting compiler/encoders/asm
Feb 23 16:28:42 Finished compiler/encoders/asm                                   33s 711MB
Feb 23 16:28:42 Starting compiler/encoders/x64
Feb 23 16:30:02 Finished compiler/encoders/x64                                 1m19s   1GB
Feb 23 16:30:02 Starting compiler/encoders/arm7
Feb 23 16:32:32 Finished compiler/encoders/arm7                                2m29s   1GB
Feb 23 16:32:32 Starting compiler/encoders/arm8
Feb 23 16:33:21 Finished compiler/encoders/arm8                                  49s   1GB
Feb 23 16:33:21 Starting compiler/encoders/arm8_asl
Feb 23 19:12:21 Finished compiler/encoders/arm8_asl                         2h38m59s  10GB
Feb 23 19:12:21 Starting compiler/encoders/mips
Feb 23 19:14:12 Finished compiler/encoders/mips                                1m50s   1GB
Feb 23 19:14:12 Starting compiler/encoders/riscv
Feb 23 19:16:25 Finished compiler/encoders/riscv                               2m12s   1GB
Feb 23 19:16:25 Starting compiler/encoders/ag32
Feb 23 19:16:51 Finished compiler/encoders/ag32                                  25s 773MB
Feb 23 19:16:51 Starting compiler/backend/x64
Feb 23 19:17:18 Finished compiler/backend/x64                                    26s   1GB
Feb 23 19:17:18 Starting compiler/backend/arm7
Feb 23 19:17:46 Finished compiler/backend/arm7                                   28s   1GB
Feb 23 19:17:46 Starting compiler/backend/arm8
Feb 23 19:18:13 Finished compiler/backend/arm8                                   26s   1GB
Feb 23 19:18:13 Starting compiler/backend/mips
Feb 23 19:18:39 Finished compiler/backend/mips                                   26s   1GB
Feb 23 19:18:39 Starting compiler/backend/riscv
Feb 23 19:19:05 Finished compiler/backend/riscv                                  25s   1GB
Feb 23 19:19:05 Starting compiler/backend/ag32
Feb 23 19:20:42 Finished compiler/backend/ag32                                 1m36s   1GB
Feb 23 19:20:43 Starting compiler/parsing/proofs
Feb 23 19:24:57 Finished compiler/parsing/proofs                               4m13s   1GB
Feb 23 19:24:57 Starting compiler/inference/proofs
Feb 23 19:27:49 Finished compiler/inference/proofs                             2m51s   1GB
Feb 23 19:27:49 Starting compiler/backend/semantics
Feb 23 20:04:55 Finished compiler/backend/semantics                           37m05s   3GB
Feb 23 20:04:55 Starting compiler/backend/reg_alloc/proofs
Feb 23 20:09:39 Finished compiler/backend/reg_alloc/proofs                     4m44s 673MB
Feb 23 20:09:40 Starting compiler/backend/proofs
Feb 23 21:31:13 Finished compiler/backend/proofs                            1h21m33s   8GB
Feb 23 21:31:13 Starting compiler/backend/serialiser
Feb 23 21:33:01 Finished compiler/backend/serialiser                           1m47s   1GB
Feb 23 21:33:01 Starting compiler/encoders/x64/proofs
Feb 23 21:44:43 Finished compiler/encoders/x64/proofs                         11m41s   1GB
Feb 23 21:44:43 Starting compiler/encoders/arm7/proofs
Feb 23 21:59:39 Finished compiler/encoders/arm7/proofs                        14m56s   3GB
Feb 23 21:59:39 Starting compiler/encoders/arm8/proofs
Feb 23 22:07:39 Finished compiler/encoders/arm8/proofs                         7m59s   1GB
Feb 23 22:07:39 Starting compiler/encoders/arm8_asl/proofs
Feb 23 23:05:55 Finished compiler/encoders/arm8_asl/proofs                    58m15s   8GB
Feb 23 23:05:55 Starting compiler/encoders/mips/proofs
Feb 23 23:18:25 Finished compiler/encoders/mips/proofs                        12m29s   3GB
Feb 23 23:18:25 Starting compiler/encoders/riscv/proofs
Feb 23 23:30:18 Finished compiler/encoders/riscv/proofs                       11m52s 652MB
Feb 23 23:30:18 Starting compiler/encoders/ag32/proofs
Feb 23 23:33:36 Finished compiler/encoders/ag32/proofs                         3m17s 662MB
Feb 23 23:33:36 Starting compiler/backend/x64/proofs
Feb 23 23:34:11 Finished compiler/backend/x64/proofs                             33s   1GB
Feb 23 23:34:11 Starting compiler/backend/arm7/proofs
Feb 23 23:34:49 Finished compiler/backend/arm7/proofs                            38s   1GB
Feb 23 23:34:49 Starting compiler/backend/arm8/proofs
Feb 23 23:35:24 Finished compiler/backend/arm8/proofs                            34s   1GB
Feb 23 23:35:24 Starting compiler/backend/arm8_asl
Feb 23 23:35:53 Finished compiler/backend/arm8_asl                               28s   1GB
Feb 23 23:35:53 Starting compiler/backend/mips/proofs
Feb 23 23:36:28 Finished compiler/backend/mips/proofs                            34s   1GB
Feb 23 23:36:28 Starting compiler/backend/riscv/proofs
Feb 23 23:37:02 Finished compiler/backend/riscv/proofs                           34s   1GB
Feb 23 23:37:02 Starting compiler/backend/ag32/proofs
Feb 23 23:38:40 FAILED: compiler/backend/ag32/proofs
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/quotient/src
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(HOLDIR)/src/bag
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/src/ring/src
Scanning $(HOLDIR)/src/integer
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 $(HOLDIR)/examples/machine-code/decompiler
Scanning $(HOLDIR)/examples/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
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)/basis/pure
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
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
Scanning $(HOLDIR)/examples/algorithms
Scanning $(HOLDIR)/examples/machine-code/multiword
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/encoders/ag32
Scanning $(CAKEMLDIR)/compiler/backend/ag32
Scanning $(CAKEMLDIR)/compiler/backend/gc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/compiler/backend/semantics
Scanning $(CAKEMLDIR)/compiler/backend/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/ag32/proofs
Scanned 52 directories
Starting work on stateTheory
Starting work on README.md
Starting work on ag32_configProofTheory
README.md                             compiler/backend/ag32/proofs  (0s)     OK
stateTheory                        examples/l3-machine-code/common  (5s)     OK
Starting work on temporal_stateTheory
temporal_stateTheory               examples/l3-machine-code/common  (4s)     OK
Finished $(HOLDIR)/examples/l3-machine-code/common [#theories: 2]      (9.869s) 
Starting work on ag32_progTheory
ag32_configProofTheory                compiler/backend/ag32/proofs (30s)     OK
Starting work on ag32_machine_configTheory
ag32_progTheory                       compiler/backend/ag32/proofs (28s)     OK
Starting work on ag32_ffi_codeProofTheory
ag32_machine_configTheory             compiler/backend/ag32/proofs (34s)     OK
Starting work on ag32_memoryProofTheory
ag32_ffi_codeProofTheory              compiler/backend/ag32/proofs (50s)FAIL<1>
 w2n s.PC + 4 * LENGTH ag32_ffi_write_num_written_code < dimword (:32) 
 (k. k DIV 4 < LENGTH ag32_ffi_write_num_written_code 
      s.R 3w + 1w  s.PC + n2w k) 
 (k. k DIV 4 < LENGTH ag32_ffi_write_num_written_code 
      s.R 3w + 2w  s.PC + n2w k) 
 k. FUNPOW Next k s = ag32_ffi_write_num_written s
 
 failed.
 Failed to prove theorem ag32_ffi_write_num_written_code_thm.
 Uncaught exception: HOL_ERR {message = "by's tactic failed to prove subgoal on line 1403 (THEN1 on line 1424) (THEN1 on line 1436) (THEN1 on line 1442) (THEN1 on line 1445) (THEN1 on line 1463) (THEN1 on line 1494) (THEN1 on line 1510) (THEN1 on line 1514) (THEN1 on line 1530) (THEN1 on line 1534)", origin_function = "by", origin_structure = "BasicProvers"}
ag32_memoryProofTheory                compiler/backend/ag32/proofs (22s)MKILLED