Overview

Job 1788

CakeML:71680ad5cc7a726b2fbd647ad26a0827a8dc9435
  Prove PEG-completeness for system with more declaration nesting
#862 (gh859)
Merging into:5c8c961383b431e16bfc2c6ba7e13d0e6a8cf7f7
  Fix basis for changes to ZIP and LUPDATE in HOL
HOL:b2236d1e8f18d389921766fcda06075975394e9f
  Fix ZIP_ind test case
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

 Claimed job
 Building HOL
 Starting developers
 Finished developers                                               4s 133MB
 Starting developers/bin
 Finished developers/bin                                           5s 670MB
 Starting semantics/ffi
 Finished semantics/ffi                                           11s 222MB
 Starting semantics
 Finished semantics                                             2m42s   1GB
 Starting semantics/proofs
 Finished semantics/proofs                                      4m26s   1GB
 Starting semantics/alt_semantics
 Finished semantics/alt_semantics                                 19s 459MB
 Starting semantics/alt_semantics/proofs
 Finished semantics/alt_semantics/proofs                        2m55s 774MB
 Starting basis/pure
 Finished basis/pure                                            3m29s 929MB
 Starting translator
 Finished translator                                            3m48s   1GB
 Starting compiler/parsing
 Finished compiler/parsing                                      1m38s   2GB
 Starting characteristic
 Finished characteristic                                        7m33s   2GB
 Starting translator/monadic
 Finished translator/monadic                                    2m24s   1GB
 Starting basis
 Finished basis                                                55m21s   6GB
 Starting compiler/inference
 Finished compiler/inference                                    1m41s   1GB
 Starting compiler/backend/reg_alloc
 Finished compiler/backend/reg_alloc                            2m02s   1GB
 Starting compiler/backend/gc
 Finished compiler/backend/gc                                   5m27s   1GB
 Starting compiler/backend
 Finished compiler/backend                                      6m58s   2GB
 Starting compiler/encoders/asm
 Finished compiler/encoders/asm                                   33s 711MB
 Starting compiler/encoders/x64
 Finished compiler/encoders/x64                                 1m19s   1GB
 Starting compiler/encoders/arm7
 Finished compiler/encoders/arm7                                2m29s   1GB
 Starting compiler/encoders/arm8
 Finished compiler/encoders/arm8                                  49s   1GB
 Starting compiler/encoders/arm8_asl
 Finished compiler/encoders/arm8_asl                         2h38m59s  10GB
 Starting compiler/encoders/mips
 Finished compiler/encoders/mips                                1m50s   1GB
 Starting compiler/encoders/riscv
 Finished compiler/encoders/riscv                               2m12s   1GB
 Starting compiler/encoders/ag32
 Finished compiler/encoders/ag32                                  25s 773MB
 Starting compiler/backend/x64
 Finished compiler/backend/x64                                    26s   1GB
 Starting compiler/backend/arm7
 Finished compiler/backend/arm7                                   28s   1GB
 Starting compiler/backend/arm8
 Finished compiler/backend/arm8                                   26s   1GB
 Starting compiler/backend/mips
 Finished compiler/backend/mips                                   26s   1GB
 Starting compiler/backend/riscv
 Finished compiler/backend/riscv                                  25s   1GB
 Starting compiler/backend/ag32
 Finished compiler/backend/ag32                                 1m36s   1GB
 Starting compiler/parsing/proofs
 Finished compiler/parsing/proofs                               4m13s   1GB
 Starting compiler/inference/proofs
 Finished compiler/inference/proofs                             2m51s   1GB
 Starting compiler/backend/semantics
 Finished compiler/backend/semantics                           37m05s   3GB
 Starting compiler/backend/reg_alloc/proofs
 Finished compiler/backend/reg_alloc/proofs                     4m44s 673MB
 Starting compiler/backend/proofs
 Finished compiler/backend/proofs                            1h21m33s   8GB
 Starting compiler/backend/serialiser
 Finished compiler/backend/serialiser                           1m47s   1GB
 Starting compiler/encoders/x64/proofs
 Finished compiler/encoders/x64/proofs                         11m41s   1GB
 Starting compiler/encoders/arm7/proofs
 Finished compiler/encoders/arm7/proofs                        14m56s   3GB
 Starting compiler/encoders/arm8/proofs
 Finished compiler/encoders/arm8/proofs                         7m59s   1GB
 Starting compiler/encoders/arm8_asl/proofs
 Finished compiler/encoders/arm8_asl/proofs                    58m15s   8GB
 Starting compiler/encoders/mips/proofs
 Finished compiler/encoders/mips/proofs                        12m29s   3GB
 Starting compiler/encoders/riscv/proofs
 Finished compiler/encoders/riscv/proofs                       11m52s 652MB
 Starting compiler/encoders/ag32/proofs
 Finished compiler/encoders/ag32/proofs                         3m17s 662MB
 Starting compiler/backend/x64/proofs
 Finished compiler/backend/x64/proofs                             33s   1GB
 Starting compiler/backend/arm7/proofs
 Finished compiler/backend/arm7/proofs                            38s   1GB
 Starting compiler/backend/arm8/proofs
 Finished compiler/backend/arm8/proofs                            34s   1GB
 Starting compiler/backend/arm8_asl
 Finished compiler/backend/arm8_asl                               28s   1GB
 Starting compiler/backend/mips/proofs
 Finished compiler/backend/mips/proofs                            34s   1GB
 Starting compiler/backend/riscv/proofs
 Finished compiler/backend/riscv/proofs                           34s   1GB
 Starting compiler/backend/ag32/proofs
 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