CakeML Regression Test

Job 1310

CakeML:d1d432a909d07bc1e7207777adb8827ced0fb173
  Fix {clos_known,clos_mti,reg_alloc}Proof given Abbrev changes in HOL [Jul 30 07:27:19]
HOL:ff3ac4c4c36730c3560764bd9487f22baea5d7a9
  Avoid GC test warnings on low user times, and avoid a MoscowML bug [Jul 29 01:44:39]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Jul 30 08:04:04 Claimed job
Jul 30 08:04:07 Reusing HOL
Jul 30 08:04:15 Starting developers
Jul 30 08:04:15 Finished developers                                               0s  29MB
Jul 30 08:04:15 Starting developers/bin
Jul 30 08:04:21 Finished developers/bin                                           5s   1GB
Jul 30 08:04:22 Starting semantics/ffi
Jul 30 08:04:31 Finished semantics/ffi                                            8s 250MB
Jul 30 08:04:31 Starting semantics
Jul 30 08:05:52 Finished semantics                                             1m21s   1GB
Jul 30 08:05:52 Starting semantics/proofs
Jul 30 08:09:07 Finished semantics/proofs                                      3m14s   1GB
Jul 30 08:09:08 Starting semantics/alt_semantics
Jul 30 08:09:15 Finished semantics/alt_semantics                                  7s 329MB
Jul 30 08:09:15 Starting semantics/alt_semantics/proofs
Jul 30 08:11:20 Finished semantics/alt_semantics/proofs                        2m04s   1GB
Jul 30 08:11:20 Starting basis/pure
Jul 30 08:12:09 Finished basis/pure                                              48s 729MB
Jul 30 08:12:09 Starting translator
Jul 30 08:14:47 Finished translator                                            2m37s   1GB
Jul 30 08:14:47 Starting compiler/parsing
Jul 30 08:15:54 Finished compiler/parsing                                      1m06s   2GB
Jul 30 08:15:54 Starting characteristic
Jul 30 08:21:42 Finished characteristic                                        5m47s   2GB
Jul 30 08:21:42 Starting translator/monadic
Jul 30 08:23:16 Finished translator/monadic                                    1m33s   1GB
Jul 30 08:23:16 Starting basis
Jul 30 08:56:21 Finished basis                                                33m04s  20GB
Jul 30 08:56:21 Starting compiler/inference
Jul 30 08:57:22 Finished compiler/inference                                    1m00s   1GB
Jul 30 08:57:22 Starting compiler/backend/reg_alloc
Jul 30 08:58:26 Finished compiler/backend/reg_alloc                            1m03s   1GB
Jul 30 08:58:26 Starting compiler/backend/gc
Jul 30 09:01:53 Finished compiler/backend/gc                                   3m26s   2GB
Jul 30 09:01:53 Starting compiler/backend
Jul 30 09:06:27 Finished compiler/backend                                      4m33s   3GB
Jul 30 09:06:27 Starting compiler/encoders/asm
Jul 30 09:06:48 Finished compiler/encoders/asm                                   20s 746MB
Jul 30 09:06:48 Starting compiler/encoders/x64
Jul 30 09:07:46 Finished compiler/encoders/x64                                   57s 737MB
Jul 30 09:07:46 Starting compiler/encoders/arm7
Jul 30 09:09:36 Finished compiler/encoders/arm7                                1m49s   1GB
Jul 30 09:09:36 Starting compiler/encoders/arm8
Jul 30 09:10:09 Finished compiler/encoders/arm8                                  33s 641MB
Jul 30 09:10:10 Starting compiler/encoders/mips
Jul 30 09:11:24 Finished compiler/encoders/mips                                1m14s   1GB
Jul 30 09:11:24 Starting compiler/encoders/riscv
Jul 30 09:12:53 Finished compiler/encoders/riscv                               1m28s   1GB
Jul 30 09:12:53 Starting compiler/encoders/ag32
Jul 30 09:13:10 Finished compiler/encoders/ag32                                  16s 889MB
Jul 30 09:13:10 Starting compiler/backend/x64
Jul 30 09:13:28 Finished compiler/backend/x64                                    17s   1GB
Jul 30 09:13:28 Starting compiler/backend/arm7
Jul 30 09:13:48 Finished compiler/backend/arm7                                   19s   1GB
Jul 30 09:13:48 Starting compiler/backend/arm8
Jul 30 09:14:07 Finished compiler/backend/arm8                                   18s 958MB
Jul 30 09:14:07 Starting compiler/backend/mips
Jul 30 09:14:26 Finished compiler/backend/mips                                   18s   1GB
Jul 30 09:14:26 Starting compiler/backend/riscv
Jul 30 09:14:45 Finished compiler/backend/riscv                                  18s   1GB
Jul 30 09:14:45 Starting compiler/backend/ag32
Jul 30 09:15:15 FAILED: compiler/backend/ag32
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$(HOLDIR)/examples/machine-code/hoare-triple[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$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/ag32[0m
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:    7s  user:    7s     OK
ag32_configTheory      real:   16s  user:   16s     OK
ag32_memoryTheory      real:   28s  user:   27sFAIL<1>
           s.MEM|>
 
 failed.
 Failed to prove theorem ag32_ffi_get_arg_store_thm.
 
 Exception raised at BasicProvers.by:
 by's tactic failed to prove subgoal on line 1505 (THEN1 on line 1499) (THEN1 on line 1489) (THEN1 on line 1518) (THEN1 on line 1536) (THEN1 on line 1540) (THEN1 on line 1591)
 error in quse /home/myreen/regression/cakeml-1310/compiler/backend/ag32/ag32_memoryScript.sml : HOL_ERR {message = "by's tactic failed to prove subgoal on line 1505 (THEN1 on line 1499) (THEN1 on line 1489) (THEN1 on line 1518) (THEN1 on line 1536) (THEN1 on line 1540) (THEN1 on line 1591)", origin_function = "by", origin_structure = "BasicProvers"}
 error in load /home/myreen/regression/cakeml-1310/compiler/backend/ag32/ag32_memoryScript : HOL_ERR {message = "by's tactic failed to prove subgoal on line 1505 (THEN1 on line 1499) (THEN1 on line 1489) (THEN1 on line 1518) (THEN1 on line 1536) (THEN1 on line 1540) (THEN1 on line 1591)", origin_function = "by", origin_structure = "BasicProvers"}
 Uncaught exception: HOL_ERR {message = "by's tactic failed to prove subgoal on line 1505 (THEN1 on line 1499) (THEN1 on line 1489) (THEN1 on line 1518) (THEN1 on line 1536) (THEN1 on line 1540) (THEN1 on line 1591)", origin_function = "by", origin_structure = "BasicProvers"}