Job 1235

CakeML: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 23 15:05:18 Claimed job
May 23 15:05:25 Building HOL
May 23 15:18:26 Starting developers
May 23 15:18:31 Finished developers                                               4s  91MB
May 23 15:18:31 Starting developers/bin
May 23 15:18:39 Finished developers/bin                                           7s   1GB
May 23 15:18:39 Starting semantics/ffi
May 23 15:18:49 Finished semantics/ffi                                           10s 228MB
May 23 15:18:49 Starting semantics
May 23 15:20:21 Finished semantics                                             1m31s   1GB
May 23 15:20:21 Starting semantics/proofs
May 23 15:23:52 Finished semantics/proofs                                      3m30s   1GB
May 23 15:23:52 Starting semantics/alt_semantics
May 23 15:24:00 Finished semantics/alt_semantics                                  8s 298MB
May 23 15:24:00 Starting semantics/alt_semantics/proofs
May 23 15:26:14 Finished semantics/alt_semantics/proofs                        2m13s 785MB
May 23 15:26:14 Starting basis/pure
May 23 15:29:15 Finished basis/pure                                            3m00s 985MB
May 23 15:29:15 Starting translator
May 23 15:31:54 Finished translator                                            2m39s   1GB
May 23 15:31:55 Starting compiler/parsing
May 23 15:33:07 Finished compiler/parsing                                      1m12s   2GB
May 23 15:33:08 Starting characteristic
May 23 15:39:10 Finished characteristic                                        6m02s   2GB
May 23 15:39:10 Starting translator/monadic
May 23 15:40:47 Finished translator/monadic                                    1m36s   1GB
May 23 15:40:47 Starting basis
May 23 16:14:37 Finished basis                                                33m49s  16GB
May 23 16:14:37 Starting compiler/inference
May 23 16:15:48 Finished compiler/inference                                    1m10s   1GB
May 23 16:15:48 Starting compiler/backend/reg_alloc
May 23 16:16:52 Finished compiler/backend/reg_alloc                            1m03s   1GB
May 23 16:16:52 Starting compiler/backend/gc
May 23 16:20:28 Finished compiler/backend/gc                                   3m35s   2GB
May 23 16:20:28 Starting compiler/backend
May 23 16:25:11 Finished compiler/backend                                      4m43s   4GB
May 23 16:25:11 Starting compiler/encoders/asm
May 23 16:25:34 Finished compiler/encoders/asm                                   22s 880MB
May 23 16:25:34 Starting compiler/encoders/x64
May 23 16:26:33 Finished compiler/encoders/x64                                   59s 915MB
May 23 16:26:33 Starting compiler/encoders/arm7
May 23 16:28:29 Finished compiler/encoders/arm7                                1m55s   1GB
May 23 16:28:30 Starting compiler/encoders/arm8
May 23 16:29:03 Finished compiler/encoders/arm8                                  33s 875MB
May 23 16:29:04 Starting compiler/encoders/mips
May 23 16:30:15 Finished compiler/encoders/mips                                1m11s   1GB
May 23 16:30:15 Starting compiler/encoders/riscv
May 23 16:31:41 Finished compiler/encoders/riscv                               1m25s   1GB
May 23 16:31:41 Starting compiler/encoders/ag32
May 23 16:31:59 Finished compiler/encoders/ag32                                  17s 778MB
May 23 16:32:00 Starting compiler/backend/x64
May 23 16:32:19 Finished compiler/backend/x64                                    18s   1GB
May 23 16:32:19 Starting compiler/backend/arm7
May 23 16:32:40 Finished compiler/backend/arm7                                   20s   1GB
May 23 16:32:40 Starting compiler/backend/arm8
May 23 16:32:59 Finished compiler/backend/arm8                                   18s   1GB
May 23 16:32:59 Starting compiler/backend/mips
May 23 16:33:19 Finished compiler/backend/mips                                   19s   1GB
May 23 16:33:19 Starting compiler/backend/riscv
May 23 16:33:39 Finished compiler/backend/riscv                                  19s   1GB
May 23 16:33:39 Starting compiler/backend/ag32
May 23 16:34:05 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:   17s  user:   16s     OK
ag32_memoryTheory                               real:   24s  user:   22sFAIL<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"}