Job 1316

CakeML:fe62f4e478a1011649a5b16b81e14d9d1ccd9b7a
  Get files to build following changes to HOL [Aug 05 11:41:01]
HOL:a084f49e1bf9a108a354cd01a025118182b72fd5
  emacs-mode: Fix error in detection of end of open declarations [Aug 04 04:40:14]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Aug 05 11:57:44 Claimed job
Aug 05 11:57:55 Building HOL
Aug 05 12:13:10 Starting developers
Aug 05 12:13:15 Finished developers                                               4s 120MB
Aug 05 12:13:15 Starting developers/bin
Aug 05 12:13:22 Finished developers/bin                                           7s   1GB
Aug 05 12:13:22 Starting semantics/ffi
Aug 05 12:13:34 Finished semantics/ffi                                           11s 250MB
Aug 05 12:13:34 Starting semantics
Aug 05 12:15:19 Finished semantics                                             1m44s   1GB
Aug 05 12:15:19 Starting semantics/proofs
Aug 05 12:19:09 Finished semantics/proofs                                      3m49s   1GB
Aug 05 12:19:09 Starting semantics/alt_semantics
Aug 05 12:19:19 Finished semantics/alt_semantics                                 10s 331MB
Aug 05 12:19:19 Starting semantics/alt_semantics/proofs
Aug 05 12:21:44 Finished semantics/alt_semantics/proofs                        2m24s 766MB
Aug 05 12:21:44 Starting basis/pure
Aug 05 12:25:02 Finished basis/pure                                            3m18s 855MB
Aug 05 12:25:03 Starting translator
Aug 05 12:28:01 Finished translator                                            2m58s   1GB
Aug 05 12:28:01 Starting compiler/parsing
Aug 05 12:29:20 Finished compiler/parsing                                      1m19s   2GB
Aug 05 12:29:20 Starting characteristic
Aug 05 12:35:51 Finished characteristic                                        6m30s   1GB
Aug 05 12:35:51 Starting translator/monadic
Aug 05 12:37:38 Finished translator/monadic                                    1m46s   1GB
Aug 05 12:37:38 Starting basis
Aug 05 13:16:40 Finished basis                                                39m01s  12GB
Aug 05 13:16:40 Starting compiler/inference
Aug 05 13:18:00 Finished compiler/inference                                    1m19s 946MB
Aug 05 13:18:00 Starting compiler/backend/reg_alloc
Aug 05 13:19:13 Finished compiler/backend/reg_alloc                            1m12s   1GB
Aug 05 13:19:13 Starting compiler/backend/gc
Aug 05 13:23:23 Finished compiler/backend/gc                                   4m09s   2GB
Aug 05 13:23:23 Starting compiler/backend
Aug 05 13:28:51 Finished compiler/backend                                      5m28s   3GB
Aug 05 13:28:52 Starting compiler/encoders/asm
Aug 05 13:29:18 Finished compiler/encoders/asm                                   26s 791MB
Aug 05 13:29:18 Starting compiler/encoders/x64
Aug 05 13:30:25 Finished compiler/encoders/x64                                 1m06s 976MB
Aug 05 13:30:25 Starting compiler/encoders/arm7
Aug 05 13:32:33 Finished compiler/encoders/arm7                                2m07s   1GB
Aug 05 13:32:33 Starting compiler/encoders/arm8
Aug 05 13:33:14 Finished compiler/encoders/arm8                                  40s 915MB
Aug 05 13:33:14 Starting compiler/encoders/mips
Aug 05 13:34:42 Finished compiler/encoders/mips                                1m27s 933MB
Aug 05 13:34:42 Starting compiler/encoders/riscv
Aug 05 13:36:23 Finished compiler/encoders/riscv                               1m41s   1GB
Aug 05 13:36:24 Starting compiler/encoders/ag32
Aug 05 13:36:43 Finished compiler/encoders/ag32                                  19s 859MB
Aug 05 13:36:43 Starting compiler/backend/x64
Aug 05 13:37:06 Finished compiler/backend/x64                                    22s   1GB
Aug 05 13:37:06 Starting compiler/backend/arm7
Aug 05 13:37:28 Finished compiler/backend/arm7                                   22s   1GB
Aug 05 13:37:28 Starting compiler/backend/arm8
Aug 05 13:37:48 Finished compiler/backend/arm8                                   19s   1GB
Aug 05 13:37:48 Starting compiler/backend/mips
Aug 05 13:38:09 Finished compiler/backend/mips                                   20s   1GB
Aug 05 13:38:09 Starting compiler/backend/riscv
Aug 05 13:38:30 Finished compiler/backend/riscv                                  20s   1GB
Aug 05 13:38:30 Starting compiler/backend/ag32
Aug 05 13:39:48 Finished compiler/backend/ag32                                 1m17s   1GB
Aug 05 13:39:48 Starting compiler/parsing/proofs
Aug 05 13:45:58 Finished compiler/parsing/proofs                               6m10s   1GB
Aug 05 13:45:59 Starting compiler/inference/proofs
Aug 05 13:48:47 Finished compiler/inference/proofs                             2m48s   1GB
Aug 05 13:48:47 Starting compiler/backend/semantics
Aug 05 14:22:45 Finished compiler/backend/semantics                           33m56s   2GB
Aug 05 14:22:45 Starting compiler/backend/reg_alloc/proofs
Aug 05 14:26:45 Finished compiler/backend/reg_alloc/proofs                     4m00s 893MB
Aug 05 14:26:45 Starting compiler/backend/proofs
Aug 05 15:32:25 Finished compiler/backend/proofs                            1h05m39s  15GB
Aug 05 15:32:25 Starting compiler/encoders/x64/proofs
Aug 05 15:44:26 Finished compiler/encoders/x64/proofs                         12m00s   1GB
Aug 05 15:44:26 Starting compiler/encoders/arm7/proofs
Aug 05 15:58:59 Finished compiler/encoders/arm7/proofs                        14m33s   6GB
Aug 05 15:58:59 Starting compiler/encoders/arm8/proofs
Aug 05 16:06:46 Finished compiler/encoders/arm8/proofs                         7m46s 855MB
Aug 05 16:06:46 Starting compiler/encoders/mips/proofs
Aug 05 16:18:03 Finished compiler/encoders/mips/proofs                        11m16s   2GB
Aug 05 16:18:03 Starting compiler/encoders/riscv/proofs
Aug 05 16:27:47 Finished compiler/encoders/riscv/proofs                        9m43s 998MB
Aug 05 16:27:47 Starting compiler/encoders/ag32/proofs
Aug 05 16:30:41 Finished compiler/encoders/ag32/proofs                         2m53s 678MB
Aug 05 16:30:41 Starting compiler/backend/x64/proofs
Aug 05 16:31:03 Finished compiler/backend/x64/proofs                             21s   1GB
Aug 05 16:31:03 Starting compiler/backend/arm7/proofs
Aug 05 16:31:26 Finished compiler/backend/arm7/proofs                            23s   1GB
Aug 05 16:31:27 Starting compiler/backend/arm8/proofs
Aug 05 16:31:49 Finished compiler/backend/arm8/proofs                            21s   1GB
Aug 05 16:31:49 Starting compiler/backend/mips/proofs
Aug 05 16:32:11 Finished compiler/backend/mips/proofs                            22s   1GB
Aug 05 16:32:11 Starting compiler/backend/riscv/proofs
Aug 05 16:32:35 Finished compiler/backend/riscv/proofs                           21s   1GB
Aug 05 16:32:35 Starting compiler/backend/ag32/proofs
Aug 05 16:33:43 FAILED: compiler/backend/ag32/proofs
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)/examples/fun-op-sem/lprefix_lub
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc/lem_lib_stub
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/basis
Scanning $(HOLDIR)/examples/machine-code/multiword
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/compiler/backend/reachability
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/reachability/proofs
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/compiler/backend/semantics
Scanning $(CAKEMLDIR)/compiler/backend/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/ag32/proofs
Starting work on stateTheory
Starting work on README.md
Starting work on ag32_configProofTheory
README.md                                       real:    0s  user:    0s     OK
stateTheory                                     real:    4s  user:    3s     OK
Starting work on temporal_stateTheory
temporal_stateTheory                            real:    3s  user:    3s     OK
Starting work on ag32_progTheory
ag32_configProofTheory                          real:   20s  user:   19s     OK
Starting work on ag32_machine_configTheory
ag32_progTheory                                 real:   17s  user:   16s     OK
Starting work on ag32_ffi_codeProofTheory
ag32_machine_configTheory                       real:   19s  user:   18s     OK
Starting work on ag32_memoryProofTheory
ag32_ffi_codeProofTheory                        real:   40s  user:   38sFAIL<1>
   (ffi_code_start_offset + ag32_ffi_write_entrypoint +
    4 * LENGTH ag32_ffi_write_set_id_code +
    4 * LENGTH ag32_ffi_write_check_conf_code +
    4 * LENGTH ag32_ffi_write_load_noff_code +
    4 * LENGTH ag32_ffi_write_check_lengths_code)  s.R 5w = n2w output_offset 
 k. FUNPOW Next k s = ag32_ffi_write_write_header s
 
 failed.
 Failed to prove theorem ag32_ffi_write_write_header_code_thm.
 Uncaught exception: HOL_ERR {message = "by's tactic failed to prove subgoal on line 752 (THEN1 on line 779) (THEN1 on line 801) (THEN1 on line 806) (THEN1 on line 828) (THEN1 on line 833) (THEN1 on line 896) (THEN1 on line 919) (THEN1 on line 976) (THEN1 on line 998) (THEN1 on line 1055) (THEN1 on line 1079) (THEN1 on line 1101) (THEN1 on line 1167) (THEN1 on line 1189) (THEN1 on line 1249) (THEN1 on line 1273)", origin_function = "by", origin_structure = "BasicProvers"}
ag32_memoryProofTheory                                                  M-KILLED