Job 1789

CakeML:5c8c961383b431e16bfc2c6ba7e13d0e6a8cf7f7
  Fix basis for changes to ZIP and LUPDATE in HOL [Feb 23 14:31:57]
HOL:b2236d1e8f18d389921766fcda06075975394e9f
  Fix ZIP_ind test case [Feb 23 03:12:26]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Feb 23 14:42:48 Claimed job
Feb 23 14:42:49 Reusing HOL
Feb 23 14:43:02 Starting developers
Feb 23 14:43:06 Finished developers                                               4s 128MB
Feb 23 14:43:06 Starting developers/bin
Feb 23 14:43:10 Finished developers/bin                                           4s 674MB
Feb 23 14:43:11 Starting semantics/ffi
Feb 23 14:43:20 Finished semantics/ffi                                            9s 256MB
Feb 23 14:43:20 Starting semantics
Feb 23 14:45:22 Finished semantics                                             2m01s   1GB
Feb 23 14:45:22 Starting semantics/proofs
Feb 23 14:49:04 Finished semantics/proofs                                      3m41s   1GB
Feb 23 14:49:04 Starting semantics/alt_semantics
Feb 23 14:49:21 Finished semantics/alt_semantics                                 16s 498MB
Feb 23 14:49:21 Starting semantics/alt_semantics/proofs
Feb 23 14:51:50 Finished semantics/alt_semantics/proofs                        2m29s 936MB
Feb 23 14:51:50 Starting basis/pure
Feb 23 14:52:53 Finished basis/pure                                            1m02s 901MB
Feb 23 14:52:53 Starting translator
Feb 23 14:55:56 Finished translator                                            3m03s   2GB
Feb 23 14:55:56 Starting compiler/parsing
Feb 23 14:57:13 Finished compiler/parsing                                      1m16s   2GB
Feb 23 14:57:13 Starting characteristic
Feb 23 15:03:34 Finished characteristic                                        6m20s   1GB
Feb 23 15:03:34 Starting translator/monadic
Feb 23 15:05:28 Finished translator/monadic                                    1m53s   1GB
Feb 23 15:05:28 Starting basis
Feb 23 15:51:40 Finished basis                                                46m09s  21GB
Feb 23 15:51:40 Starting compiler/inference
Feb 23 15:53:07 Finished compiler/inference                                    1m27s   1GB
Feb 23 15:53:08 Starting compiler/backend/reg_alloc
Feb 23 15:54:50 Finished compiler/backend/reg_alloc                            1m42s   1GB
Feb 23 15:54:51 Starting compiler/backend/gc
Feb 23 15:59:15 Finished compiler/backend/gc                                   4m24s   1GB
Feb 23 15:59:16 Starting compiler/backend
Feb 23 16:04:46 Finished compiler/backend                                      5m30s   2GB
Feb 23 16:04:46 Starting compiler/encoders/asm
Feb 23 16:05:16 Finished compiler/encoders/asm                                   30s 969MB
Feb 23 16:05:16 Starting compiler/encoders/x64
Feb 23 16:06:23 Finished compiler/encoders/x64                                 1m07s   1GB
Feb 23 16:06:24 Starting compiler/encoders/arm7
Feb 23 16:08:27 Finished compiler/encoders/arm7                                2m03s   1GB
Feb 23 16:08:27 Starting compiler/encoders/arm8
Feb 23 16:09:08 Finished compiler/encoders/arm8                                  41s   1GB
Feb 23 16:09:09 Starting compiler/encoders/arm8_asl
Feb 23 18:20:32 Finished compiler/encoders/arm8_asl                         2h11m22s  39GB
Feb 23 18:20:33 Starting compiler/encoders/mips
Feb 23 18:22:03 Finished compiler/encoders/mips                                1m30s   1GB
Feb 23 18:22:03 Starting compiler/encoders/riscv
Feb 23 18:23:53 Finished compiler/encoders/riscv                               1m49s   1GB
Feb 23 18:23:53 Starting compiler/encoders/ag32
Feb 23 18:24:15 Finished compiler/encoders/ag32                                  21s 690MB
Feb 23 18:24:15 Starting compiler/backend/x64
Feb 23 18:24:37 Finished compiler/backend/x64                                    21s   1GB
Feb 23 18:24:37 Starting compiler/backend/arm7
Feb 23 18:25:01 Finished compiler/backend/arm7                                   23s   1GB
Feb 23 18:25:01 Starting compiler/backend/arm8
Feb 23 18:25:23 Finished compiler/backend/arm8                                   21s   1GB
Feb 23 18:25:23 Starting compiler/backend/mips
Feb 23 18:25:46 Finished compiler/backend/mips                                   22s   1GB
Feb 23 18:25:46 Starting compiler/backend/riscv
Feb 23 18:26:09 Finished compiler/backend/riscv                                  22s   1GB
Feb 23 18:26:09 Starting compiler/backend/ag32
Feb 23 18:27:34 Finished compiler/backend/ag32                                 1m25s   1GB
Feb 23 18:27:34 Starting compiler/parsing/proofs
Feb 23 18:31:17 Finished compiler/parsing/proofs                               3m42s   1GB
Feb 23 18:31:17 Starting compiler/inference/proofs
Feb 23 18:33:50 Finished compiler/inference/proofs                             2m32s 860MB
Feb 23 18:33:50 Starting compiler/backend/semantics
Feb 23 19:02:26 Finished compiler/backend/semantics                           28m36s   2GB
Feb 23 19:02:26 Starting compiler/backend/reg_alloc/proofs
Feb 23 19:05:51 Finished compiler/backend/reg_alloc/proofs                     3m25s   1GB
Feb 23 19:05:51 Starting compiler/backend/proofs
Feb 23 19:57:47 Finished compiler/backend/proofs                              51m52s  22GB
Feb 23 19:57:47 Starting compiler/backend/serialiser
Feb 23 19:59:23 Finished compiler/backend/serialiser                           1m36s   1GB
Feb 23 19:59:23 Starting compiler/encoders/x64/proofs
Feb 23 20:08:55 Finished compiler/encoders/x64/proofs                          9m31s   4GB
Feb 23 20:08:55 Starting compiler/encoders/arm7/proofs
Feb 23 20:21:58 Finished compiler/encoders/arm7/proofs                        13m03s   3GB
Feb 23 20:21:58 Starting compiler/encoders/arm8/proofs
Feb 23 20:28:45 Finished compiler/encoders/arm8/proofs                         6m46s   1GB
Feb 23 20:28:45 Starting compiler/encoders/arm8_asl/proofs
Feb 23 21:19:24 Finished compiler/encoders/arm8_asl/proofs                    50m38s   8GB
Feb 23 21:19:24 Starting compiler/encoders/mips/proofs
Feb 23 21:29:25 Finished compiler/encoders/mips/proofs                        10m01s   1GB
Feb 23 21:29:26 Starting compiler/encoders/riscv/proofs
Feb 23 21:38:12 Finished compiler/encoders/riscv/proofs                        8m45s   1GB
Feb 23 21:38:12 Starting compiler/encoders/ag32/proofs
Feb 23 21:40:47 Finished compiler/encoders/ag32/proofs                         2m34s 670MB
Feb 23 21:40:47 Starting compiler/backend/x64/proofs
Feb 23 21:41:14 Finished compiler/backend/x64/proofs                             26s   1GB
Feb 23 21:41:14 Starting compiler/backend/arm7/proofs
Feb 23 21:41:42 Finished compiler/backend/arm7/proofs                            28s   1GB
Feb 23 21:41:42 Starting compiler/backend/arm8/proofs
Feb 23 21:42:09 Finished compiler/backend/arm8/proofs                            26s   1GB
Feb 23 21:42:09 Starting compiler/backend/arm8_asl
Feb 23 21:42:32 Finished compiler/backend/arm8_asl                               22s   1GB
Feb 23 21:42:32 Starting compiler/backend/mips/proofs
Feb 23 21:42:59 Finished compiler/backend/mips/proofs                            27s   1GB
Feb 23 21:42:59 Starting compiler/backend/riscv/proofs
Feb 23 21:43:27 Finished compiler/backend/riscv/proofs                           27s   1GB
Feb 23 21:43:27 Starting compiler/backend/ag32/proofs
Feb 23 21:44:38 FAILED: compiler/backend/ag32/proofs
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/quotient/src[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(HOLDIR)/src/bag[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/src/hol88[0m
Scanning [1m$(HOLDIR)/src/real[0m
Scanning [1m$(HOLDIR)/src/floating-point[0m
Scanning [1m$(HOLDIR)/src/monad/more_monads[0m
Scanning [1m$(HOLDIR)/src/update[0m
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)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(CAKEMLDIR)/developers[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)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[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/algorithms[0m
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[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/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
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  (3s)     OK
Starting work on temporal_stateTheory
temporal_stateTheory                                                                                                                             examples/l3-machine-code/common  (3s)     OK
Finished $(HOLDIR)/examples/l3-machine-code/common [#theories: 2]                                                                                                                    (7.110s) 
Starting work on ag32_progTheory
ag32_configProofTheory                                                                                                                              compiler/backend/ag32/proofs (23s)     OK
Starting work on ag32_machine_configTheory
ag32_progTheory                                                                                                                                     compiler/backend/ag32/proofs (20s)     OK
Starting work on ag32_ffi_codeProofTheory
ag32_machine_configTheory                                                                                                                           compiler/backend/ag32/proofs (24s)     OK
Starting work on ag32_memoryProofTheory
ag32_ffi_codeProofTheory                                                                                                                            compiler/backend/ag32/proofs (35s)FAIL<1>
 k. FUNPOW Next k s = ag32_ffi_write_num_written s
 
 failed.
 Failed to prove theorem ag32_ffi_write_num_written_code_thm.
 
 Exception raised at BasicProvers.by:
 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)
 error in quse /home/cug/hk324/cml-regression/cakeml-1789/compiler/backend/ag32/proofs/ag32_ffi_codeProofScript.sml : 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"}
 error in load /home/cug/hk324/cml-regression/cakeml-1789/compiler/backend/ag32/proofs/ag32_ffi_codeProofScript : 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"}
 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 (16s)MKILLED