CakeML Regression Test

Job 1253

CakeML:15638fd543c6aacfe48a113d4b8c1227fb46954d
  Fix a bunch of files [Jun 06 20:09:35]
HOL:ac7497223d5845f2709250fa8fdcb566cbc2e1ae
  emacs-mode: make regexp searching case-sensitive; SOME not a q'fier [Jun 03 04:25:22]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Jun 06 20:10:15 Claimed job
Jun 06 20:10:17 Reusing HOL
Jun 06 20:10:27 Starting developers
Jun 06 20:10:27 Finished developers                                               0s  29MB
Jun 06 20:10:27 Starting developers/bin
Jun 06 20:10:34 Finished developers/bin                                           6s   1GB
Jun 06 20:10:34 Starting semantics/ffi
Jun 06 20:10:43 Finished semantics/ffi                                            9s 258MB
Jun 06 20:10:43 Starting semantics
Jun 06 20:12:04 Finished semantics                                             1m20s   1GB
Jun 06 20:12:04 Starting semantics/proofs
Jun 06 20:15:15 Finished semantics/proofs                                      3m10s   1GB
Jun 06 20:15:15 Starting semantics/alt_semantics
Jun 06 20:15:23 Finished semantics/alt_semantics                                  7s 349MB
Jun 06 20:15:23 Starting semantics/alt_semantics/proofs
Jun 06 20:17:25 Finished semantics/alt_semantics/proofs                        2m01s 841MB
Jun 06 20:17:25 Starting basis/pure
Jun 06 20:18:13 Finished basis/pure                                              48s 856MB
Jun 06 20:18:13 Starting translator
Jun 06 20:20:50 Finished translator                                            2m36s   1GB
Jun 06 20:20:50 Starting compiler/parsing
Jun 06 20:21:57 Finished compiler/parsing                                      1m07s   2GB
Jun 06 20:21:58 Starting characteristic
Jun 06 20:27:39 Finished characteristic                                        5m40s   1GB
Jun 06 20:27:39 Starting translator/monadic
Jun 06 20:29:13 Finished translator/monadic                                    1m33s   1GB
Jun 06 20:29:13 Starting basis
Jun 06 21:00:11 Finished basis                                                30m58s  14GB
Jun 06 21:00:11 Starting compiler/inference
Jun 06 21:01:16 Finished compiler/inference                                    1m05s   1GB
Jun 06 21:01:17 Starting compiler/backend/reg_alloc
Jun 06 21:02:20 Finished compiler/backend/reg_alloc                            1m03s   1GB
Jun 06 21:02:20 Starting compiler/backend/gc
Jun 06 21:05:42 Finished compiler/backend/gc                                   3m22s   2GB
Jun 06 21:05:43 Starting compiler/backend
Jun 06 21:10:13 Finished compiler/backend                                      4m29s   3GB
Jun 06 21:10:13 Starting compiler/encoders/asm
Jun 06 21:10:34 Finished compiler/encoders/asm                                   20s 710MB
Jun 06 21:10:34 Starting compiler/encoders/x64
Jun 06 21:11:32 Finished compiler/encoders/x64                                   57s 988MB
Jun 06 21:11:32 Starting compiler/encoders/arm7
Jun 06 21:13:20 Finished compiler/encoders/arm7                                1m47s   1GB
Jun 06 21:13:20 Starting compiler/encoders/arm8
Jun 06 21:13:53 Finished compiler/encoders/arm8                                  33s 648MB
Jun 06 21:13:54 Starting compiler/encoders/mips
Jun 06 21:15:08 Finished compiler/encoders/mips                                1m14s   1GB
Jun 06 21:15:09 Starting compiler/encoders/riscv
Jun 06 21:16:37 Finished compiler/encoders/riscv                               1m27s   1GB
Jun 06 21:16:37 Starting compiler/encoders/ag32
Jun 06 21:16:53 Finished compiler/encoders/ag32                                  16s 688MB
Jun 06 21:16:53 Starting compiler/backend/x64
Jun 06 21:17:10 Finished compiler/backend/x64                                    16s 978MB
Jun 06 21:17:10 Starting compiler/backend/arm7
Jun 06 21:17:30 Finished compiler/backend/arm7                                   19s   1GB
Jun 06 21:17:30 Starting compiler/backend/arm8
Jun 06 21:17:48 Finished compiler/backend/arm8                                   18s   1GB
Jun 06 21:17:48 Starting compiler/backend/mips
Jun 06 21:18:06 Finished compiler/backend/mips                                   17s   1GB
Jun 06 21:18:06 Starting compiler/backend/riscv
Jun 06 21:18:23 Finished compiler/backend/riscv                                  16s   1GB
Jun 06 21:18:23 Starting compiler/backend/ag32
Jun 06 21:18:40 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 ag32_configTheory
Starting work on ag32_memoryTheory
Starting work on export_ag32Theory
export_ag32Theory                                                                                                                                   real:    8s  user:    7s     OK
ag32_memoryTheory                                                                                                                                   real:   15s  user:   15sFAIL<1>
           MEM := asm_write_bytearray (s.R 5w) written s.MEM|>
 
 failed.
 Failed to prove theorem ag32_ffi_copy_thm.
 
 Exception raised at Tactical.Q_TAC:
 No parse of quotation leads to success (THEN1 on line 476) (THEN1 on line 507) (THEN1 on line 514) (THEN1 on line 555) (THEN1 on line 557)
 error in quse /home/myreen/regression/cakeml-1253/compiler/backend/ag32/ag32_memoryScript.sml : HOL_ERR {message = "No parse of quotation leads to success (THEN1 on line 476) (THEN1 on line 507) (THEN1 on line 514) (THEN1 on line 555) (THEN1 on line 557)", origin_function = "Q_TAC", origin_structure = "Tactical"}
 error in load /home/myreen/regression/cakeml-1253/compiler/backend/ag32/ag32_memoryScript : HOL_ERR {message = "No parse of quotation leads to success (THEN1 on line 476) (THEN1 on line 507) (THEN1 on line 514) (THEN1 on line 555) (THEN1 on line 557)", origin_function = "Q_TAC", origin_structure = "Tactical"}
 Uncaught exception: HOL_ERR {message = "No parse of quotation leads to success (THEN1 on line 476) (THEN1 on line 507) (THEN1 on line 514) (THEN1 on line 555) (THEN1 on line 557)", origin_function = "Q_TAC", origin_structure = "Tactical"}
ag32_configTheory                                                                                                                                                           M-KILLED