Job 1317

CakeML:e6cb43fb0a02ea76505e35753fb50d36c1e3d10c
  Merge pull request #744 from CakeML/fix_build_instrs [Aug 05 12:13:13]
HOL:a084f49e1bf9a108a354cd01a025118182b72fd5
  emacs-mode: Fix error in detection of end of open declarations [Aug 04 04:40:14]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Aug 05 12:20:28 Claimed job
Aug 05 12:20:31 Reusing HOL
Aug 05 12:20:42 Starting developers
Aug 05 12:20:44 Finished developers                                               2s 133MB
Aug 05 12:20:44 Starting developers/bin
Aug 05 12:20:51 Finished developers/bin                                           6s   1GB
Aug 05 12:20:51 Starting semantics/ffi
Aug 05 12:21:01 Finished semantics/ffi                                           10s 296MB
Aug 05 12:21:01 Starting semantics
Aug 05 12:22:26 Finished semantics                                             1m24s   1GB
Aug 05 12:22:26 Starting semantics/proofs
Aug 05 12:25:42 Finished semantics/proofs                                      3m16s   1GB
Aug 05 12:25:42 Starting semantics/alt_semantics
Aug 05 12:25:51 Finished semantics/alt_semantics                                  8s 434MB
Aug 05 12:25:51 Starting semantics/alt_semantics/proofs
Aug 05 12:27:53 Finished semantics/alt_semantics/proofs                        2m01s   1GB
Aug 05 12:27:53 Starting basis/pure
Aug 05 12:28:47 Finished basis/pure                                              53s   1GB
Aug 05 12:28:47 Starting translator
Aug 05 12:31:25 Finished translator                                            2m37s   2GB
Aug 05 12:31:25 Starting compiler/parsing
Aug 05 12:32:35 Finished compiler/parsing                                      1m10s   3GB
Aug 05 12:32:36 Starting characteristic
Aug 05 12:38:26 Finished characteristic                                        5m49s   3GB
Aug 05 12:38:26 Starting translator/monadic
Aug 05 12:40:04 Finished translator/monadic                                    1m38s   3GB
Aug 05 12:40:04 Starting basis
Aug 05 13:12:45 Finished basis                                                32m40s  30GB
Aug 05 13:12:45 Starting compiler/inference
Aug 05 13:13:50 Finished compiler/inference                                    1m04s   2GB
Aug 05 13:13:50 Starting compiler/backend/reg_alloc
Aug 05 13:14:58 Finished compiler/backend/reg_alloc                            1m07s   2GB
Aug 05 13:14:58 Starting compiler/backend/gc
Aug 05 13:18:20 Finished compiler/backend/gc                                   3m21s   3GB
Aug 05 13:18:20 Starting compiler/backend
Aug 05 13:23:08 Finished compiler/backend                                      4m47s   4GB
Aug 05 13:23:08 Starting compiler/encoders/asm
Aug 05 13:23:31 Finished compiler/encoders/asm                                   22s   1GB
Aug 05 13:23:31 Starting compiler/encoders/x64
Aug 05 13:23:58 Finished compiler/encoders/x64                                   26s   1GB
Aug 05 13:23:58 Starting compiler/encoders/arm7
Aug 05 13:24:49 Finished compiler/encoders/arm7                                  51s   1GB
Aug 05 13:24:49 Starting compiler/encoders/arm8
Aug 05 13:25:04 Finished compiler/encoders/arm8                                  14s   1GB
Aug 05 13:25:04 Starting compiler/encoders/mips
Aug 05 13:25:21 Finished compiler/encoders/mips                                  17s   1GB
Aug 05 13:25:21 Starting compiler/encoders/riscv
Aug 05 13:25:37 Finished compiler/encoders/riscv                                 15s 916MB
Aug 05 13:25:37 Starting compiler/encoders/ag32
Aug 05 13:25:56 Finished compiler/encoders/ag32                                  18s 998MB
Aug 05 13:25:56 Starting compiler/backend/x64
Aug 05 13:26:15 Finished compiler/backend/x64                                    18s   1GB
Aug 05 13:26:15 Starting compiler/backend/arm7
Aug 05 13:26:36 Finished compiler/backend/arm7                                   20s   1GB
Aug 05 13:26:36 Starting compiler/backend/arm8
Aug 05 13:26:56 Finished compiler/backend/arm8                                   19s   1GB
Aug 05 13:26:56 Starting compiler/backend/mips
Aug 05 13:27:16 Finished compiler/backend/mips                                   19s   1GB
Aug 05 13:27:16 Starting compiler/backend/riscv
Aug 05 13:27:36 Finished compiler/backend/riscv                                  20s   1GB
Aug 05 13:27:36 Starting compiler/backend/ag32
Aug 05 13:28:47 Finished compiler/backend/ag32                                 1m11s   2GB
Aug 05 13:28:48 Starting compiler/parsing/proofs
Aug 05 13:31:00 Finished compiler/parsing/proofs                               2m12s   3GB
Aug 05 13:31:01 Starting compiler/inference/proofs
Aug 05 13:33:19 Finished compiler/inference/proofs                             2m18s   1GB
Aug 05 13:33:19 Starting compiler/backend/semantics
Aug 05 13:59:21 Finished compiler/backend/semantics                           26m01s   4GB
Aug 05 13:59:21 Starting compiler/backend/reg_alloc/proofs
Aug 05 14:02:34 Finished compiler/backend/reg_alloc/proofs                     3m12s   1GB
Aug 05 14:02:34 Starting compiler/backend/proofs
Aug 05 14:53:14 Finished compiler/backend/proofs                              50m39s  17GB
Aug 05 14:53:14 Starting compiler/encoders/x64/proofs
Aug 05 15:02:29 Finished compiler/encoders/x64/proofs                          9m14s   4GB
Aug 05 15:02:29 Starting compiler/encoders/arm7/proofs
Aug 05 15:14:50 Finished compiler/encoders/arm7/proofs                        12m21s  11GB
Aug 05 15:14:50 Starting compiler/encoders/arm8/proofs
Aug 05 15:21:03 Finished compiler/encoders/arm8/proofs                         6m12s   3GB
Aug 05 15:21:03 Starting compiler/encoders/mips/proofs
Aug 05 15:30:46 Finished compiler/encoders/mips/proofs                         9m43s   5GB
Aug 05 15:30:47 Starting compiler/encoders/riscv/proofs
Aug 05 15:38:51 Finished compiler/encoders/riscv/proofs                        8m04s   3GB
Aug 05 15:38:51 Starting compiler/encoders/ag32/proofs
Aug 05 15:41:13 Finished compiler/encoders/ag32/proofs                         2m21s   1GB
Aug 05 15:41:13 Starting compiler/backend/x64/proofs
Aug 05 15:41:33 Finished compiler/backend/x64/proofs                             19s   1GB
Aug 05 15:41:33 Starting compiler/backend/arm7/proofs
Aug 05 15:41:54 Finished compiler/backend/arm7/proofs                            21s   1GB
Aug 05 15:41:55 Starting compiler/backend/arm8/proofs
Aug 05 15:42:14 Finished compiler/backend/arm8/proofs                            18s   1GB
Aug 05 15:42:14 Starting compiler/backend/mips/proofs
Aug 05 15:42:34 Finished compiler/backend/mips/proofs                            19s   1GB
Aug 05 15:42:34 Starting compiler/backend/riscv/proofs
Aug 05 15:42:54 Finished compiler/backend/riscv/proofs                           20s   1GB
Aug 05 15:42:54 Starting compiler/backend/ag32/proofs
Aug 05 15:43:51 FAILED: compiler/backend/ag32/proofs
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(HOLDIR)/examples/machine-code/decompiler[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc/lem_lib_stub[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/basis[0m
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reachability[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/ag32[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/ag32[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/gc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reachability/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/ag32/proofs[0m
Starting work on stateTheory
Starting work on README.md
Starting work on ag32_configProofTheory
README.md                                                                                                                                           real:    0s  user:    0s     OK
stateTheory                                                                                                                                         real:    3s  user:    3s     OK
Starting work on temporal_stateTheory
temporal_stateTheory                                                                                                                                real:    3s  user:    3s     OK
Starting work on ag32_progTheory
ag32_configProofTheory                                                                                                                              real:   19s  user:   18s     OK
Starting work on ag32_machine_configTheory
ag32_progTheory                                                                                                                                     real:   15s  user:   15s     OK
Starting work on ag32_ffi_codeProofTheory
ag32_machine_configTheory                                                                                                                           real:   18s  user:   17s     OK
Starting work on ag32_memoryProofTheory
ag32_ffi_codeProofTheory                                                                                                                            real:   32s  user:   30sFAIL<1>
 k. FUNPOW Next k s = ag32_ffi_write_write_header s
 
 failed.
 Failed to prove theorem ag32_ffi_write_write_header_code_thm.
 
 Exception raised at BasicProvers.by:
 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)
 error in quse /home/myreen/regression/cakeml-1317/compiler/backend/ag32/proofs/ag32_ffi_codeProofScript.sml : 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"}
 error in load /home/myreen/regression/cakeml-1317/compiler/backend/ag32/proofs/ag32_ffi_codeProofScript : 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"}
 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