Job 1236

CakeML:a681f0882be171571089b73430ae183a1a088a65
  remove heap/stack arguments [May 25 05:14:54]
#738 (export_update)
Merging into:4bc2df653478adec779906cf1820673fb1751a31
  Merge pull request #736 from CakeML/data-cost [May 20 05:27:48]
HOL:16a774456e43bd29a9b94ee31e24f17e059e771f
  Implement a unification-based version of mp_then with similar API [May 20 07:12:37]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

May 25 08:45:39 Claimed job
May 25 08:45:44 Reusing HOL
May 25 08:46:37 Starting developers
May 25 08:46:41 Finished developers                                               4s  84MB
May 25 08:46:41 Starting developers/bin
May 25 08:46:49 Finished developers/bin                                           7s   1GB
May 25 08:46:49 Starting semantics/ffi
May 25 08:47:00 Finished semantics/ffi                                           10s 230MB
May 25 08:47:00 Starting semantics
May 25 08:48:24 Finished semantics                                             1m23s   1GB
May 25 08:48:24 Starting semantics/proofs
May 25 08:51:57 Finished semantics/proofs                                      3m32s   1GB
May 25 08:51:57 Starting semantics/alt_semantics
May 25 08:52:05 Finished semantics/alt_semantics                                  8s 332MB
May 25 08:52:05 Starting semantics/alt_semantics/proofs
May 25 08:54:19 Finished semantics/alt_semantics/proofs                        2m13s 836MB
May 25 08:54:19 Starting basis/pure
May 25 08:55:10 Finished basis/pure                                              50s 724MB
May 25 08:55:10 Starting translator
May 25 08:57:49 Finished translator                                            2m39s   1GB
May 25 08:57:50 Starting compiler/parsing
May 25 08:59:02 Finished compiler/parsing                                      1m11s   1GB
May 25 08:59:02 Starting characteristic
May 25 09:05:04 Finished characteristic                                        6m02s   1GB
May 25 09:05:05 Starting translator/monadic
May 25 09:06:43 Finished translator/monadic                                    1m37s   1GB
May 25 09:06:43 Starting basis
May 25 09:40:23 Finished basis                                                33m39s  12GB
May 25 09:40:23 Starting compiler/inference
May 25 09:41:25 Finished compiler/inference                                    1m02s   1GB
May 25 09:41:25 Starting compiler/backend/reg_alloc
May 25 09:42:29 Finished compiler/backend/reg_alloc                            1m03s   1GB
May 25 09:42:29 Starting compiler/backend/gc
May 25 09:45:48 Finished compiler/backend/gc                                   3m19s   2GB
May 25 09:45:48 Starting compiler/backend
May 25 09:50:31 Finished compiler/backend                                      4m42s   3GB
May 25 09:50:31 Starting compiler/encoders/asm
May 25 09:50:54 Finished compiler/encoders/asm                                   22s 937MB
May 25 09:50:54 Starting compiler/encoders/x64
May 25 09:51:20 Finished compiler/encoders/x64                                   26s 932MB
May 25 09:51:20 Starting compiler/encoders/arm7
May 25 09:52:11 Finished compiler/encoders/arm7                                  50s 770MB
May 25 09:52:11 Starting compiler/encoders/arm8
May 25 09:52:24 Finished compiler/encoders/arm8                                  13s 746MB
May 25 09:52:25 Starting compiler/encoders/mips
May 25 09:52:42 Finished compiler/encoders/mips                                  17s   1GB
May 25 09:52:43 Starting compiler/encoders/riscv
May 25 09:52:58 Finished compiler/encoders/riscv                                 14s 764MB
May 25 09:52:58 Starting compiler/encoders/ag32
May 25 09:53:17 Finished compiler/encoders/ag32                                  18s 655MB
May 25 09:53:17 Starting compiler/backend/x64
May 25 09:53:36 Finished compiler/backend/x64                                    18s   1GB
May 25 09:53:36 Starting compiler/backend/arm7
May 25 09:53:57 Finished compiler/backend/arm7                                   20s   1GB
May 25 09:53:57 Starting compiler/backend/arm8
May 25 09:54:15 Finished compiler/backend/arm8                                   17s   1GB
May 25 09:54:15 Starting compiler/backend/mips
May 25 09:54:34 Finished compiler/backend/mips                                   19s   1GB
May 25 09:54:34 Starting compiler/backend/riscv
May 25 09:54:54 Finished compiler/backend/riscv                                  19s   1GB
May 25 09:54:54 Starting compiler/backend/ag32
May 25 09:55:21 FAILED: compiler/backend/ag32
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 $(HOLDIR)/examples/machine-code/hoare-triple
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 $(HOLDIR)/examples/l3-machine-code/common
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/encoders/ag32
Starting work on README.md
Starting work on ag32_configTheory
Starting work on ag32_memoryTheory
Starting work on export_ag32Theory
README.md                                       real:    0s  user:    0s     OK
export_ag32Theory                               real:    8s  user:    7s     OK
ag32_configTheory                               real:   16s  user:   15s     OK
ag32_memoryTheory                               real:   24s  user:   23sFAIL<1>
 r4 r3.
     ag32_ffi_get_arg_length_store s =
     s with
     <|PC := s.PC + n2w (4 * LENGTH ag32_ffi_get_arg_length_store_code);
       R := s.R4w  r4; 3w  r3;
       MEM := s.MEMs.R 3w  n2w n; s.R 3w + 1w  n2w (n DIV 256) |>
 
 failed.
 Failed to prove theorem ag32_ffi_get_arg_length_store_thm.
 Uncaught exception: HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 1109) (THEN1 on line 1113)", origin_function = "THEN1", origin_structure = "Tactical"}