Job 1004

CakeML:349c6adc73366d9c689a0c8bd11d85c75fd0f71b
  Fix drule breakages in compiler/inference/proofs [Aug 16 00:47:59]
HOL:ea47c77c31d0bce19dc95254ee42d589d1ef0bea
  Provide Triviality syntax as alias for Theorem[local] [Aug 14 06:42:27]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Aug 16 00:55:15 Claimed job
Aug 16 00:55:21 Reusing HOL
Aug 16 00:56:08 Starting developers
Aug 16 00:56:10 Finished developers                                               2s  21MB
Aug 16 00:56:10 Starting developers/bin
Aug 16 00:56:17 Finished developers/bin                                           6s 961MB
Aug 16 00:56:17 Starting semantics/ffi
Aug 16 00:56:27 Finished semantics/ffi                                            9s 230MB
Aug 16 00:56:27 Starting semantics
Aug 16 00:57:48 Finished semantics                                             1m20s 959MB
Aug 16 00:57:48 Starting semantics/proofs
Aug 16 01:00:48 Finished semantics/proofs                                      2m59s   1GB
Aug 16 01:00:48 Starting semantics/alt_semantics
Aug 16 01:00:56 Finished semantics/alt_semantics                                  7s 299MB
Aug 16 01:00:56 Starting semantics/alt_semantics/proofs
Aug 16 01:02:43 Finished semantics/alt_semantics/proofs                        1m46s 777MB
Aug 16 01:02:43 Starting basis/pure
Aug 16 01:03:30 Finished basis/pure                                              47s 766MB
Aug 16 01:03:31 Starting translator
Aug 16 01:05:16 Finished translator                                            1m45s   1GB
Aug 16 01:05:16 Starting compiler/parsing
Aug 16 01:06:13 Finished compiler/parsing                                        57s   2GB
Aug 16 01:06:14 Starting characteristic
Aug 16 01:11:29 Finished characteristic                                        5m14s   1GB
Aug 16 01:11:29 Starting translator/monadic
Aug 16 01:12:57 Finished translator/monadic                                    1m28s   1GB
Aug 16 01:12:57 Starting basis
Aug 16 01:30:32 Finished basis                                                17m34s   2GB
Aug 16 01:30:32 Starting compiler/inference
Aug 16 01:32:10 Finished compiler/inference                                    1m37s   1GB
Aug 16 01:32:10 Starting compiler/backend/reg_alloc
Aug 16 01:33:10 Finished compiler/backend/reg_alloc                            1m00s   1GB
Aug 16 01:33:10 Starting compiler/backend/gc
Aug 16 01:41:23 Finished compiler/backend/gc                                   8m12s   2GB
Aug 16 01:41:23 Starting compiler/backend
Aug 16 01:41:25 Finished compiler/backend                                         2s  15MB
Aug 16 01:41:25 Starting compiler/encoders/asm
Aug 16 01:41:27 Finished compiler/encoders/asm                                    1s  13MB
Aug 16 01:41:27 Starting compiler/encoders/x64
Aug 16 01:41:52 Finished compiler/encoders/x64                                   24s 957MB
Aug 16 01:41:52 Starting compiler/encoders/arm7
Aug 16 01:42:39 Finished compiler/encoders/arm7                                  46s 781MB
Aug 16 01:42:39 Starting compiler/encoders/arm8
Aug 16 01:42:52 Finished compiler/encoders/arm8                                  13s 606MB
Aug 16 01:42:52 Starting compiler/encoders/mips
Aug 16 01:43:10 Finished compiler/encoders/mips                                  17s 937MB
Aug 16 01:43:10 Starting compiler/encoders/riscv
Aug 16 01:43:26 Finished compiler/encoders/riscv                                 16s 700MB
Aug 16 01:43:26 Starting compiler/encoders/ag32
Aug 16 01:43:43 Finished compiler/encoders/ag32                                  16s 737MB
Aug 16 01:43:43 Starting compiler/backend/x64
Aug 16 01:44:02 Finished compiler/backend/x64                                    18s   1GB
Aug 16 01:44:02 Starting compiler/backend/arm7
Aug 16 01:44:23 Finished compiler/backend/arm7                                   20s   1GB
Aug 16 01:44:23 Starting compiler/backend/arm8
Aug 16 01:44:42 Finished compiler/backend/arm8                                   18s   1GB
Aug 16 01:44:42 Starting compiler/backend/mips
Aug 16 01:45:01 Finished compiler/backend/mips                                   18s   1GB
Aug 16 01:45:01 Starting compiler/backend/riscv
Aug 16 01:45:20 Finished compiler/backend/riscv                                  18s   1GB
Aug 16 01:45:20 Starting compiler/backend/ag32
Aug 16 01:46:28 Finished compiler/backend/ag32                                 1m07s 912MB
Aug 16 01:46:28 Starting compiler/parsing/proofs
Aug 16 01:52:05 Finished compiler/parsing/proofs                               5m36s   1GB
Aug 16 01:52:05 Starting compiler/inference/proofs
Aug 16 01:54:51 Finished compiler/inference/proofs                             2m45s   1GB
Aug 16 01:54:51 Starting compiler/backend/semantics
Aug 16 02:02:04 Finished compiler/backend/semantics                            7m12s   1GB
Aug 16 02:02:04 Starting compiler/backend/reg_alloc/proofs
Aug 16 02:05:20 Finished compiler/backend/reg_alloc/proofs                     3m15s 746MB
Aug 16 02:05:20 Starting compiler/backend/proofs
Aug 16 02:43:54 Finished compiler/backend/proofs                              38m33s   4GB
Aug 16 02:43:54 Starting compiler/encoders/x64/proofs
Aug 16 02:53:50 Finished compiler/encoders/x64/proofs                          9m55s   5GB
Aug 16 02:53:50 Starting compiler/encoders/arm7/proofs
Aug 16 03:07:02 Finished compiler/encoders/arm7/proofs                        13m11s   7GB
Aug 16 03:07:02 Starting compiler/encoders/arm8/proofs
Aug 16 03:13:40 Finished compiler/encoders/arm8/proofs                         6m37s   1GB
Aug 16 03:13:40 Starting compiler/encoders/mips/proofs
Aug 16 03:23:56 Finished compiler/encoders/mips/proofs                        10m16s   2GB
Aug 16 03:23:56 Starting compiler/encoders/riscv/proofs
Aug 16 03:32:12 Finished compiler/encoders/riscv/proofs                        8m15s   1GB
Aug 16 03:32:12 Starting compiler/encoders/ag32/proofs
Aug 16 03:34:39 Finished compiler/encoders/ag32/proofs                         2m27s 706MB
Aug 16 03:34:39 Starting compiler/backend/x64/proofs
Aug 16 03:34:59 Finished compiler/backend/x64/proofs                             19s 769MB
Aug 16 03:34:59 Starting compiler/backend/arm7/proofs
Aug 16 03:35:20 Finished compiler/backend/arm7/proofs                            20s   1GB
Aug 16 03:35:21 Starting compiler/backend/arm8/proofs
Aug 16 03:35:40 Finished compiler/backend/arm8/proofs                            19s   1GB
Aug 16 03:35:40 Starting compiler/backend/mips/proofs
Aug 16 03:36:02 Finished compiler/backend/mips/proofs                            21s   1GB
Aug 16 03:36:02 Starting compiler/backend/riscv/proofs
Aug 16 03:36:22 Finished compiler/backend/riscv/proofs                           19s   1GB
Aug 16 03:36:22 Starting compiler/backend/ag32/proofs
Aug 16 03:37:44 FAILED: compiler/backend/ag32/proofs
]0;Holmake: ~/oven/regression/HOL-ea47c77c31d0bce19dc95254ee42d589d1ef0bea/examples/l3-machine-code/common]0;Holmake: ~/oven/regression/HOL-ea47c77c31d0bce19dc95254ee42d589d1ef0bea/examples/l3-machine-code/commonWorking in $(HOLDIR)/examples/l3-machine-code/common
]0;Holmake: .]0;Holmake: ~/oven/regression/HOL-ea47c77c31d0bce19dc95254ee42d589d1ef0bea/examples/machine-code/decompiler]0;Holmake: ~/oven/regression/HOL-ea47c77c31d0bce19dc95254ee42d589d1ef0bea/examples/machine-code/decompilerWorking in $(HOLDIR)/examples/machine-code/decompiler
]0;Holmake: .]0;Holmake: ~/oven/regression/cakeml-1004/basis]0;Holmake: ~/oven/regression/cakeml-1004/basis/pure]0;Holmake: ~/oven/regression/HOL-ea47c77c31d0bce19dc95254ee42d589d1ef0bea/examples/balanced_bst]0;Holmake: ~/oven/regression/HOL-ea47c77c31d0bce19dc95254ee42d589d1ef0bea/examples/balanced_bstWorking in $(HOLDIR)/examples/balanced_bst
]0;Holmake: ~/oven/regression/cakeml-1004/basis/pure]0;Holmake: ~/oven/regression/HOL-ea47c77c31d0bce19dc95254ee42d589d1ef0bea/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-ea47c77c31d0bce19dc95254ee42d589d1ef0bea/examples/formal-languages]0;Holmake: ~/oven/regression/HOL-ea47c77c31d0bce19dc95254ee42d589d1ef0bea/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: ~/oven/regression/HOL-ea47c77c31d0bce19dc95254ee42d589d1ef0bea/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-ea47c77c31d0bce19dc95254ee42d589d1ef0bea/examples/formal-languages/context-free]0;Holmake: ~/oven/regression/HOL-ea47c77c31d0bce19dc95254ee42d589d1ef0bea/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: ~/oven/regression/HOL-ea47c77c31d0bce19dc95254ee42d589d1ef0bea/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-ea47c77c31d0bce19dc95254ee42d589d1ef0bea/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: ~/oven/regression/cakeml-1004/basis/pure]0;Holmake: ~/oven/regression/cakeml-1004/misc]0;Holmake: ~/oven/regression/HOL-ea47c77c31d0bce19dc95254ee42d589d1ef0bea/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/oven/regression/HOL-ea47c77c31d0bce19dc95254ee42d589d1ef0bea/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ~/oven/regression/cakeml-1004/misc]0;Holmake: ~/oven/regression/cakeml-1004/developers]0;Holmake: ~/oven/regression/cakeml-1004/developersWorking in $(CAKEMLDIR)/developers
]0;Holmake: ~/oven/regression/cakeml-1004/misc]0;Holmake: ~/oven/regression/cakeml-1004/misc/lem_lib_stub]0;Holmake: ~/oven/regression/cakeml-1004/misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ~/oven/regression/cakeml-1004/misc]0;Holmake: ~/oven/regression/cakeml-1004/miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: ~/oven/regression/cakeml-1004/basis/pure]0;Holmake: ~/oven/regression/cakeml-1004/basis/pureWorking in $(CAKEMLDIR)/basis/pure
]0;Holmake: ~/oven/regression/cakeml-1004/basis]0;Holmake: ~/oven/regression/cakeml-1004/characteristic]0;Holmake: ~/oven/regression/cakeml-1004/compiler/parsing]0;Holmake: ~/oven/regression/cakeml-1004/semantics]0;Holmake: ~/oven/regression/cakeml-1004/semantics/ffi]0;Holmake: ~/oven/regression/cakeml-1004/semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: ~/oven/regression/cakeml-1004/semantics]0;Holmake: ~/oven/regression/cakeml-1004/semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: ~/oven/regression/cakeml-1004/compiler/parsing]0;Holmake: ~/oven/regression/cakeml-1004/compiler/parsingWorking in $(CAKEMLDIR)/compiler/parsing
]0;Holmake: ~/oven/regression/cakeml-1004/characteristic]0;Holmake: ~/oven/regression/cakeml-1004/semantics/proofs]0;Holmake: ~/oven/regression/cakeml-1004/semantics/proofsWorking in $(CAKEMLDIR)/semantics/proofs
]0;Holmake: ~/oven/regression/cakeml-1004/characteristic]0;Holmake: ~/oven/regression/cakeml-1004/translator]0;Holmake: ~/oven/regression/cakeml-1004/translatorWorking in $(CAKEMLDIR)/translator
]0;Holmake: ~/oven/regression/cakeml-1004/characteristic]0;Holmake: ~/oven/regression/cakeml-1004/characteristicWorking in $(CAKEMLDIR)/characteristic
]0;Holmake: ~/oven/regression/cakeml-1004/basis]0;Holmake: ~/oven/regression/cakeml-1004/translator/monadic]0;Holmake: ~/oven/regression/cakeml-1004/translator/monadic/monad_base]0;Holmake: ~/oven/regression/cakeml-1004/translator/monadic/monad_baseWorking in $(CAKEMLDIR)/translator/monadic/monad_base
]0;Holmake: ~/oven/regression/cakeml-1004/translator/monadic]0;Holmake: ~/oven/regression/cakeml-1004/translator/monadicWorking in $(CAKEMLDIR)/translator/monadic
]0;Holmake: ~/oven/regression/cakeml-1004/basis]0;Holmake: ~/oven/regression/cakeml-1004/basisWorking in $(CAKEMLDIR)/basis
]0;Holmake: .]0;Holmake: ..]0;Holmake: ../..]0;Holmake: ~/oven/regression/HOL-ea47c77c31d0bce19dc95254ee42d589d1ef0bea/examples/machine-code/multiword]0;Holmake: ~/oven/regression/HOL-ea47c77c31d0bce19dc95254ee42d589d1ef0bea/examples/machine-code/multiwordWorking in $(HOLDIR)/examples/machine-code/multiword
]0;Holmake: ../..]0;Holmake: ../../reg_alloc]0;Holmake: ~/oven/regression/cakeml-1004/unverified/reg_alloc]0;Holmake: ~/oven/regression/cakeml-1004/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