Job 1790

CakeML:05128e17c334af95da1efdc21b80ff61dc2529b4
  Fix ag32_ffi_codeProof for HOL's new auto rewrite on  [Feb 23 23:58:54]
HOL:b2236d1e8f18d389921766fcda06075975394e9f
  Fix ZIP_ind test case [Feb 23 03:12:26]
Machine:stove 4.15.0-143-generic x86_64 GNU/Linux

Feb 24 00:04:43 Claimed job
Feb 24 00:04:45 Reusing HOL
Feb 24 00:04:58 Starting developers
Feb 24 00:05:03 Finished developers                                               4s 153MB
Feb 24 00:05:03 Starting developers/bin
Feb 24 00:05:07 Finished developers/bin                                           4s 675MB
Feb 24 00:05:07 Starting semantics/ffi
Feb 24 00:05:17 Finished semantics/ffi                                            9s 262MB
Feb 24 00:05:17 Starting semantics
Feb 24 00:07:20 Finished semantics                                             2m02s   1GB
Feb 24 00:07:20 Starting semantics/proofs
Feb 24 00:10:57 Finished semantics/proofs                                      3m37s   1GB
Feb 24 00:10:57 Starting semantics/alt_semantics
Feb 24 00:11:14 Finished semantics/alt_semantics                                 16s 515MB
Feb 24 00:11:14 Starting semantics/alt_semantics/proofs
Feb 24 00:13:41 Finished semantics/alt_semantics/proofs                        2m27s   1GB
Feb 24 00:13:42 Starting basis/pure
Feb 24 00:14:45 Finished basis/pure                                            1m02s 893MB
Feb 24 00:14:45 Starting translator
Feb 24 00:17:45 Finished translator                                            3m00s   1GB
Feb 24 00:17:45 Starting compiler/parsing
Feb 24 00:19:01 Finished compiler/parsing                                      1m15s   2GB
Feb 24 00:19:01 Starting characteristic
Feb 24 00:25:28 Finished characteristic                                        6m24s   1GB
Feb 24 00:25:28 Starting translator/monadic
Feb 24 00:27:24 Finished translator/monadic                                    1m56s   1GB
Feb 24 00:27:24 Starting basis
Feb 24 01:13:43 Finished basis                                                46m18s  19GB
Feb 24 01:13:43 Starting compiler/inference
Feb 24 01:15:05 Finished compiler/inference                                    1m21s   1GB
Feb 24 01:15:05 Starting compiler/backend/reg_alloc
Feb 24 01:16:49 Finished compiler/backend/reg_alloc                            1m43s   1GB
Feb 24 01:16:49 Starting compiler/backend/gc
Feb 24 01:21:13 Finished compiler/backend/gc                                   4m24s   2GB
Feb 24 01:21:13 Starting compiler/backend
Feb 24 01:26:41 Finished compiler/backend                                      5m26s   2GB
Feb 24 01:26:41 Starting compiler/encoders/asm
Feb 24 01:27:11 Finished compiler/encoders/asm                                   30s 968MB
Feb 24 01:27:12 Starting compiler/encoders/x64
Feb 24 01:27:42 Finished compiler/encoders/x64                                   30s 709MB
Feb 24 01:27:42 Starting compiler/encoders/arm7
Feb 24 01:28:36 Finished compiler/encoders/arm7                                  54s 827MB
Feb 24 01:28:36 Starting compiler/encoders/arm8
Feb 24 01:28:53 Finished compiler/encoders/arm8                                  16s 778MB
Feb 24 01:28:53 Starting compiler/encoders/arm8_asl
Feb 24 01:31:25 Finished compiler/encoders/arm8_asl                            2m31s   1GB
Feb 24 01:31:25 Starting compiler/encoders/mips
Feb 24 01:31:46 Finished compiler/encoders/mips                                  20s   1GB
Feb 24 01:31:46 Starting compiler/encoders/riscv
Feb 24 01:32:05 Finished compiler/encoders/riscv                                 19s 808MB
Feb 24 01:32:05 Starting compiler/encoders/ag32
Feb 24 01:32:27 Finished compiler/encoders/ag32                                  21s 690MB
Feb 24 01:32:27 Starting compiler/backend/x64
Feb 24 01:32:49 Finished compiler/backend/x64                                    21s   1GB
Feb 24 01:32:49 Starting compiler/backend/arm7
Feb 24 01:33:10 Finished compiler/backend/arm7                                   21s   1GB
Feb 24 01:33:10 Starting compiler/backend/arm8
Feb 24 01:33:33 Finished compiler/backend/arm8                                   23s   1GB
Feb 24 01:33:33 Starting compiler/backend/mips
Feb 24 01:33:57 Finished compiler/backend/mips                                   23s   1GB
Feb 24 01:33:57 Starting compiler/backend/riscv
Feb 24 01:34:20 Finished compiler/backend/riscv                                  23s   1GB
Feb 24 01:34:20 Starting compiler/backend/ag32
Feb 24 01:35:45 Finished compiler/backend/ag32                                 1m24s   1GB
Feb 24 01:35:45 Starting compiler/parsing/proofs
Feb 24 01:39:29 Finished compiler/parsing/proofs                               3m43s   1GB
Feb 24 01:39:29 Starting compiler/inference/proofs
Feb 24 01:42:00 Finished compiler/inference/proofs                             2m30s 944MB
Feb 24 01:42:00 Starting compiler/backend/semantics
Feb 24 02:10:42 Finished compiler/backend/semantics                           28m41s   3GB
Feb 24 02:10:42 Starting compiler/backend/reg_alloc/proofs
Feb 24 02:14:13 Finished compiler/backend/reg_alloc/proofs                     3m31s   1GB
Feb 24 02:14:14 Starting compiler/backend/proofs
Feb 24 03:06:19 Finished compiler/backend/proofs                              52m04s  15GB
Feb 24 03:06:19 Starting compiler/backend/serialiser
Feb 24 03:07:56 Finished compiler/backend/serialiser                           1m36s   2GB
Feb 24 03:07:56 Starting compiler/encoders/x64/proofs
Feb 24 03:17:24 Finished compiler/encoders/x64/proofs                          9m27s   5GB
Feb 24 03:17:24 Starting compiler/encoders/arm7/proofs
Feb 24 03:30:29 Finished compiler/encoders/arm7/proofs                        13m04s   3GB
Feb 24 03:30:29 Starting compiler/encoders/arm8/proofs
Feb 24 03:37:19 Finished compiler/encoders/arm8/proofs                         6m50s   1GB
Feb 24 03:37:19 Starting compiler/encoders/arm8_asl/proofs
Feb 24 03:52:39 Finished compiler/encoders/arm8_asl/proofs                    15m19s   1GB
Feb 24 03:52:39 Starting compiler/encoders/mips/proofs
Feb 24 04:02:42 Finished compiler/encoders/mips/proofs                        10m02s   2GB
Feb 24 04:02:42 Starting compiler/encoders/riscv/proofs
Feb 24 04:11:18 Finished compiler/encoders/riscv/proofs                        8m35s   1GB
Feb 24 04:11:18 Starting compiler/encoders/ag32/proofs
Feb 24 04:13:53 Finished compiler/encoders/ag32/proofs                         2m35s 639MB
Feb 24 04:13:54 Starting compiler/backend/x64/proofs
Feb 24 04:14:21 Finished compiler/backend/x64/proofs                             27s   1GB
Feb 24 04:14:21 Starting compiler/backend/arm7/proofs
Feb 24 04:14:50 Finished compiler/backend/arm7/proofs                            28s   1GB
Feb 24 04:14:50 Starting compiler/backend/arm8/proofs
Feb 24 04:15:17 Finished compiler/backend/arm8/proofs                            27s   1GB
Feb 24 04:15:17 Starting compiler/backend/arm8_asl
Feb 24 04:15:39 Finished compiler/backend/arm8_asl                               21s   1GB
Feb 24 04:15:39 Starting compiler/backend/mips/proofs
Feb 24 04:16:07 Finished compiler/backend/mips/proofs                            27s   1GB
Feb 24 04:16:07 Starting compiler/backend/riscv/proofs
Feb 24 04:16:35 Finished compiler/backend/riscv/proofs                           28s   1GB
Feb 24 04:16:35 Starting compiler/backend/ag32/proofs
Feb 24 04:18:06 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 README.md
Starting work on ag32_progTheory
Starting work on ag32_configProofTheory
README.md                                                                                                                                                                         (0s)     OK
ag32_progTheory                                                                                                                                                                  (21s)     OK
Starting work on ag32_ffi_codeProofTheory
ag32_configProofTheory                                                                                                                                                           (24s)     OK
Starting work on ag32_machine_configTheory
ag32_machine_configTheory                                                                                                                                                        (23s)     OK
Starting work on ag32_memoryProofTheory
ag32_memoryProofTheory                                                                                                                                                           (34s)FAIL<1>
   bytes_in_memory a ls m md
 
 failed.
 Failed to prove theorem bytes_in_memory_get_byte_words.
 
 Exception raised at Thm_cont.DISCH_THEN:
  (THEN1 on line 261) (THEN1 on line 264) (THEN1 on line 285)
 error in quse /home/cug/hk324/cml-regression/cakeml-1790/compiler/backend/ag32/proofs/ag32_memoryProofScript.sml : HOL_ERR {message = " (THEN1 on line 261) (THEN1 on line 264) (THEN1 on line 285)", origin_function = "DISCH_THEN", origin_structure = "Thm_cont"}
 error in load /home/cug/hk324/cml-regression/cakeml-1790/compiler/backend/ag32/proofs/ag32_memoryProofScript : HOL_ERR {message = " (THEN1 on line 261) (THEN1 on line 264) (THEN1 on line 285)", origin_function = "DISCH_THEN", origin_structure = "Thm_cont"}
 Uncaught exception: HOL_ERR {message = " (THEN1 on line 261) (THEN1 on line 264) (THEN1 on line 285)", origin_function = "DISCH_THEN", origin_structure = "Thm_cont"}
ag32_ffi_codeProofTheory                                                                                                                                                         (64s)MKILLED