Job 1005

CakeML:349c6adc73366d9c689a0c8bd11d85c75fd0f71b
  Fix drule breakages in compiler/inference/proofs [Aug 16 00:47:59]
HOL:8cc876e8e492e4f4045670ff53549a04cf1fdc65
  Further document drule breakage by linking to CakeML's old_drule [Aug 16 01:09:50]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Aug 16 11:45:09 Claimed job
Aug 16 11:45:16 Building HOL
Aug 16 11:54:45 Starting developers
Aug 16 11:54:48 Finished developers                                               2s  21MB
Aug 16 11:54:48 Starting developers/bin
Aug 16 11:54:54 Finished developers/bin                                           6s 960MB
Aug 16 11:54:55 Starting semantics/ffi
Aug 16 11:55:33 Finished semantics/ffi                                           38s 489MB
Aug 16 11:55:33 Starting semantics
Aug 16 11:57:09 Finished semantics                                             1m35s 995MB
Aug 16 11:57:09 Starting semantics/proofs
Aug 16 12:00:06 Finished semantics/proofs                                      2m57s 957MB
Aug 16 12:00:06 Starting semantics/alt_semantics
Aug 16 12:00:15 Finished semantics/alt_semantics                                  7s 283MB
Aug 16 12:00:15 Starting semantics/alt_semantics/proofs
Aug 16 12:02:04 Finished semantics/alt_semantics/proofs                        1m49s 779MB
Aug 16 12:02:04 Starting basis/pure
Aug 16 12:05:42 Finished basis/pure                                            3m37s 790MB
Aug 16 12:05:42 Starting translator
Aug 16 12:07:29 Finished translator                                            1m46s   1GB
Aug 16 12:07:29 Starting compiler/parsing
Aug 16 12:08:26 Finished compiler/parsing                                        57s   1GB
Aug 16 12:08:27 Starting characteristic
Aug 16 12:13:40 Finished characteristic                                        5m13s   1GB
Aug 16 12:13:41 Starting translator/monadic
Aug 16 12:15:09 Finished translator/monadic                                    1m28s   1GB
Aug 16 12:15:10 Starting basis
Aug 16 12:32:50 Finished basis                                                17m40s   3GB
Aug 16 12:32:50 Starting compiler/inference
Aug 16 12:34:46 Finished compiler/inference                                    1m55s   1GB
Aug 16 12:34:46 Starting compiler/backend/reg_alloc
Aug 16 12:35:46 Finished compiler/backend/reg_alloc                              59s   1GB
Aug 16 12:35:46 Starting compiler/backend/gc
Aug 16 12:45:03 Finished compiler/backend/gc                                   9m16s   2GB
Aug 16 12:45:03 Starting compiler/backend
Aug 16 12:45:06 Finished compiler/backend                                         2s  18MB
Aug 16 12:45:06 Starting compiler/encoders/asm
Aug 16 12:45:07 Finished compiler/encoders/asm                                    1s  14MB
Aug 16 12:45:07 Starting compiler/encoders/x64
Aug 16 12:46:09 Finished compiler/encoders/x64                                 1m01s 751MB
Aug 16 12:46:09 Starting compiler/encoders/arm7
Aug 16 12:47:50 Finished compiler/encoders/arm7                                1m40s   1GB
Aug 16 12:47:50 Starting compiler/encoders/arm8
Aug 16 12:48:22 Finished compiler/encoders/arm8                                  32s 562MB
Aug 16 12:48:22 Starting compiler/encoders/mips
Aug 16 12:49:29 Finished compiler/encoders/mips                                1m06s 827MB
Aug 16 12:49:29 Starting compiler/encoders/riscv
Aug 16 12:50:50 Finished compiler/encoders/riscv                               1m20s   1GB
Aug 16 12:50:50 Starting compiler/encoders/ag32
Aug 16 12:51:07 Finished compiler/encoders/ag32                                  17s 736MB
Aug 16 12:51:08 Starting compiler/backend/x64
Aug 16 12:51:25 Finished compiler/backend/x64                                    17s 846MB
Aug 16 12:51:25 Starting compiler/backend/arm7
Aug 16 12:51:46 Finished compiler/backend/arm7                                   20s   1GB
Aug 16 12:51:46 Starting compiler/backend/arm8
Aug 16 12:52:05 Finished compiler/backend/arm8                                   18s   1GB
Aug 16 12:52:06 Starting compiler/backend/mips
Aug 16 12:52:25 Finished compiler/backend/mips                                   19s   1GB
Aug 16 12:52:25 Starting compiler/backend/riscv
Aug 16 12:52:45 Finished compiler/backend/riscv                                  19s   1GB
Aug 16 12:52:45 Starting compiler/backend/ag32
Aug 16 12:53:53 Finished compiler/backend/ag32                                 1m07s   1GB
Aug 16 12:53:53 Starting compiler/parsing/proofs
Aug 16 12:59:28 Finished compiler/parsing/proofs                               5m33s   1GB
Aug 16 12:59:28 Starting compiler/inference/proofs
Aug 16 13:02:14 Finished compiler/inference/proofs                             2m46s   1GB
Aug 16 13:02:14 Starting compiler/backend/semantics
Aug 16 13:09:21 Finished compiler/backend/semantics                            7m06s   2GB
Aug 16 13:09:21 Starting compiler/backend/reg_alloc/proofs
Aug 16 13:12:35 Finished compiler/backend/reg_alloc/proofs                     3m13s 761MB
Aug 16 13:12:35 Starting compiler/backend/proofs
Aug 16 13:51:00 Finished compiler/backend/proofs                              38m25s   5GB
Aug 16 13:51:00 Starting compiler/encoders/x64/proofs
Aug 16 14:00:59 Finished compiler/encoders/x64/proofs                          9m58s   4GB
Aug 16 14:00:59 Starting compiler/encoders/arm7/proofs
Aug 16 14:14:23 Finished compiler/encoders/arm7/proofs                        13m23s   3GB
Aug 16 14:14:23 Starting compiler/encoders/arm8/proofs
Aug 16 14:20:57 Finished compiler/encoders/arm8/proofs                         6m33s   1GB
Aug 16 14:20:57 Starting compiler/encoders/mips/proofs
Aug 16 14:30:56 Finished compiler/encoders/mips/proofs                         9m59s   2GB
Aug 16 14:30:57 Starting compiler/encoders/riscv/proofs
Aug 16 14:39:19 Finished compiler/encoders/riscv/proofs                        8m22s   1GB
Aug 16 14:39:20 Starting compiler/encoders/ag32/proofs
Aug 16 14:41:47 Finished compiler/encoders/ag32/proofs                         2m27s 706MB
Aug 16 14:41:48 Starting compiler/backend/x64/proofs
Aug 16 14:42:07 Finished compiler/backend/x64/proofs                             19s   1GB
Aug 16 14:42:07 Starting compiler/backend/arm7/proofs
Aug 16 14:42:28 Finished compiler/backend/arm7/proofs                            20s   1GB
Aug 16 14:42:28 Starting compiler/backend/arm8/proofs
Aug 16 14:42:47 Finished compiler/backend/arm8/proofs                            18s 809MB
Aug 16 14:42:47 Starting compiler/backend/mips/proofs
Aug 16 14:43:07 Finished compiler/backend/mips/proofs                            20s   1GB
Aug 16 14:43:08 Starting compiler/backend/riscv/proofs
Aug 16 14:43:28 Finished compiler/backend/riscv/proofs                           20s 999MB
Aug 16 14:43:29 Starting compiler/backend/ag32/proofs
Aug 16 14:44:52 FAILED: compiler/backend/ag32/proofs
]0;Holmake: ~/oven/regression/HOL-8cc876e8e492e4f4045670ff53549a04cf1fdc65/examples/l3-machine-code/common]0;Holmake: ~/oven/regression/HOL-8cc876e8e492e4f4045670ff53549a04cf1fdc65/examples/l3-machine-code/commonWorking in $(HOLDIR)/examples/l3-machine-code/common
]0;Holmake: .]0;Holmake: ~/oven/regression/HOL-8cc876e8e492e4f4045670ff53549a04cf1fdc65/examples/machine-code/decompiler]0;Holmake: ~/oven/regression/HOL-8cc876e8e492e4f4045670ff53549a04cf1fdc65/examples/machine-code/decompilerWorking in $(HOLDIR)/examples/machine-code/decompiler
]0;Holmake: .]0;Holmake: ~/oven/regression/cakeml-1005/basis]0;Holmake: ~/oven/regression/cakeml-1005/basis/pure]0;Holmake: ~/oven/regression/HOL-8cc876e8e492e4f4045670ff53549a04cf1fdc65/examples/balanced_bst]0;Holmake: ~/oven/regression/HOL-8cc876e8e492e4f4045670ff53549a04cf1fdc65/examples/balanced_bstWorking in $(HOLDIR)/examples/balanced_bst
]0;Holmake: ~/oven/regression/cakeml-1005/basis/pure]0;Holmake: ~/oven/regression/HOL-8cc876e8e492e4f4045670ff53549a04cf1fdc65/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-8cc876e8e492e4f4045670ff53549a04cf1fdc65/examples/formal-languages]0;Holmake: ~/oven/regression/HOL-8cc876e8e492e4f4045670ff53549a04cf1fdc65/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: ~/oven/regression/HOL-8cc876e8e492e4f4045670ff53549a04cf1fdc65/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-8cc876e8e492e4f4045670ff53549a04cf1fdc65/examples/formal-languages/context-free]0;Holmake: ~/oven/regression/HOL-8cc876e8e492e4f4045670ff53549a04cf1fdc65/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: ~/oven/regression/HOL-8cc876e8e492e4f4045670ff53549a04cf1fdc65/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-8cc876e8e492e4f4045670ff53549a04cf1fdc65/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: ~/oven/regression/cakeml-1005/basis/pure]0;Holmake: ~/oven/regression/cakeml-1005/misc]0;Holmake: ~/oven/regression/HOL-8cc876e8e492e4f4045670ff53549a04cf1fdc65/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/oven/regression/HOL-8cc876e8e492e4f4045670ff53549a04cf1fdc65/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ~/oven/regression/cakeml-1005/misc]0;Holmake: ~/oven/regression/cakeml-1005/developers]0;Holmake: ~/oven/regression/cakeml-1005/developersWorking in $(CAKEMLDIR)/developers
]0;Holmake: ~/oven/regression/cakeml-1005/misc]0;Holmake: ~/oven/regression/cakeml-1005/misc/lem_lib_stub]0;Holmake: ~/oven/regression/cakeml-1005/misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ~/oven/regression/cakeml-1005/misc]0;Holmake: ~/oven/regression/cakeml-1005/miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: ~/oven/regression/cakeml-1005/basis/pure]0;Holmake: ~/oven/regression/cakeml-1005/basis/pureWorking in $(CAKEMLDIR)/basis/pure
]0;Holmake: ~/oven/regression/cakeml-1005/basis]0;Holmake: ~/oven/regression/cakeml-1005/characteristic]0;Holmake: ~/oven/regression/cakeml-1005/compiler/parsing]0;Holmake: ~/oven/regression/cakeml-1005/semantics]0;Holmake: ~/oven/regression/cakeml-1005/semantics/ffi]0;Holmake: ~/oven/regression/cakeml-1005/semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: ~/oven/regression/cakeml-1005/semantics]0;Holmake: ~/oven/regression/cakeml-1005/semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: ~/oven/regression/cakeml-1005/compiler/parsing]0;Holmake: ~/oven/regression/cakeml-1005/compiler/parsingWorking in $(CAKEMLDIR)/compiler/parsing
]0;Holmake: ~/oven/regression/cakeml-1005/characteristic]0;Holmake: ~/oven/regression/cakeml-1005/semantics/proofs]0;Holmake: ~/oven/regression/cakeml-1005/semantics/proofsWorking in $(CAKEMLDIR)/semantics/proofs
]0;Holmake: ~/oven/regression/cakeml-1005/characteristic]0;Holmake: ~/oven/regression/cakeml-1005/translator]0;Holmake: ~/oven/regression/cakeml-1005/translatorWorking in $(CAKEMLDIR)/translator
]0;Holmake: ~/oven/regression/cakeml-1005/characteristic]0;Holmake: ~/oven/regression/cakeml-1005/characteristicWorking in $(CAKEMLDIR)/characteristic
]0;Holmake: ~/oven/regression/cakeml-1005/basis]0;Holmake: ~/oven/regression/cakeml-1005/translator/monadic]0;Holmake: ~/oven/regression/cakeml-1005/translator/monadic/monad_base]0;Holmake: ~/oven/regression/cakeml-1005/translator/monadic/monad_baseWorking in $(CAKEMLDIR)/translator/monadic/monad_base
]0;Holmake: ~/oven/regression/cakeml-1005/translator/monadic]0;Holmake: ~/oven/regression/cakeml-1005/translator/monadicWorking in $(CAKEMLDIR)/translator/monadic
]0;Holmake: ~/oven/regression/cakeml-1005/basis]0;Holmake: ~/oven/regression/cakeml-1005/basisWorking in $(CAKEMLDIR)/basis
]0;Holmake: .]0;Holmake: ..]0;Holmake: ../..]0;Holmake: ~/oven/regression/HOL-8cc876e8e492e4f4045670ff53549a04cf1fdc65/examples/machine-code/multiword]0;Holmake: ~/oven/regression/HOL-8cc876e8e492e4f4045670ff53549a04cf1fdc65/examples/machine-code/multiwordWorking in $(HOLDIR)/examples/machine-code/multiword
]0;Holmake: ../..]0;Holmake: ../../reg_alloc]0;Holmake: ~/oven/regression/cakeml-1005/unverified/reg_alloc]0;Holmake: ~/oven/regression/cakeml-1005/unverified/reg_allocWorking in $(CAKEMLDIR)/unverified/reg_alloc
]0;Holmake: ../../reg_alloc]0;Holmake: ../../reg_allocWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc
]0;Holmake: ../..]0;Holmake: ../../../encoders/asm]0;Holmake: ../../../encoders/asmWorking in $(CAKEMLDIR)/compiler/encoders/asm
]0;Holmake: ../..]0;Holmake: ../..Working in $(CAKEMLDIR)/compiler/backend
]0;Holmake: ..]0;Holmake: ../../../encoders/ag32]0;Holmake: ../../../encoders/ag32Working in $(CAKEMLDIR)/compiler/encoders/ag32
]0;Holmake: ..]0;Holmake: ..Working in $(CAKEMLDIR)/compiler/backend/ag32
]0;Holmake: .]0;Holmake: ../../proofs]0;Holmake: ../../gc]0;Holmake: ../../gcWorking in $(CAKEMLDIR)/compiler/backend/gc
]0;Holmake: ../../proofs]0;Holmake: ../../reg_alloc/proofs]0;Holmake: ../../reg_alloc/proofsWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
]0;Holmake: ../../proofs]0;Holmake: ../../semantics]0;Holmake: ../../semanticsWorking in $(CAKEMLDIR)/compiler/backend/semantics
]0;Holmake: ../../proofs]0;Holmake: ../../proofsWorking in $(CAKEMLDIR)/compiler/backend/proofs
]0;Holmake: .]0;Holmake: ../../../encoders/ag32/proofs]0;Holmake: ../../../encoders/ag32/proofsWorking in $(CAKEMLDIR)/compiler/encoders/ag32/proofs
]0;Holmake: .]0;Holmake: .Working in $(CAKEMLDIR)/compiler/backend/ag32/proofs
Starting work on ag32_progTheory
Starting work on ag32_configProofTheory
Starting work on README.md
README.md                                                                    OK
ag32_configProofTheory                                                       OK
Starting work on ag32_machine_configTheory
ag32_progTheory                                                              OK
Starting work on ag32_ffi_codeProofTheory
ag32_machine_configTheory                                                    OK
Starting work on ag32_memoryProofTheory
ag32_ffi_codeProofTheory                                            FAILED! <1>
 w2n (get_mem_word s.MEM (n2w (stdin_offset + 4)))  stdin_size 
 w2n (s.R 3w + 4w) + output_buffer_size + 1 < 4294967296 
 output_buffer_size + stdin_size + stdin_offset + 8  w2n (s.R 3w) 
 DISJOINT md {s.PC + n2w k | k DIV 4 < LENGTH ag32_ffi_read_code} 
 DISJOINT md {w | n2w startup_code_size  w  w < n2w heap_start_offset} 
 k. FUNPOW Next k s = ag32_ffi_read s
 
 failed.
 Failed to prove theorem ag32_ffi_read_code_thm.
 Uncaught exception: HOL_ERR {message = " (THEN1 on line 2671) (THEN1 on line 2733) (THEN1 on line 2756) (THEN1 on line 2768)", origin_function = "DISCH_THEN", origin_structure = "Thm_cont"}
ag32_memoryProofTheory                                                 M-KILLED