Job 1527

CakeML:e012c3f796e70bc3cafb75aa94ebaf5c300c4492
  Fix another broken proof [May 18 07:46:24]
HOL:1354090035c466ccae632435bb016c0bebf281d7
  Move large_numberTheory to examples/probability [May 13 23:47:06]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

May 18 07:46:40 Claimed job
May 18 07:46:46 Reusing HOL
May 18 07:46:52 Starting developers
May 18 07:46:54 Finished developers                                               2s 120MB
May 18 07:46:55 Starting developers/bin
May 18 07:47:01 Finished developers/bin                                           6s   1GB
May 18 07:47:01 Starting semantics/ffi
May 18 07:47:12 Finished semantics/ffi                                           10s 295MB
May 18 07:47:12 Starting semantics
May 18 07:48:50 Finished semantics                                             1m38s   1GB
May 18 07:48:51 Starting semantics/proofs
May 18 07:52:33 Finished semantics/proofs                                      3m42s   1GB
May 18 07:52:33 Starting semantics/alt_semantics
May 18 07:52:42 Finished semantics/alt_semantics                                  8s 439MB
May 18 07:52:42 Starting semantics/alt_semantics/proofs
May 18 07:55:03 Finished semantics/alt_semantics/proofs                        2m21s   1GB
May 18 07:55:04 Starting basis/pure
May 18 07:57:53 Finished basis/pure                                            2m49s   1GB
May 18 07:57:53 Starting translator
May 18 08:01:41 Finished translator                                            3m47s   2GB
May 18 08:01:41 Starting compiler/parsing
May 18 08:03:00 Finished compiler/parsing                                      1m18s   2GB
May 18 08:03:00 Starting characteristic
May 18 08:09:03 Finished characteristic                                        6m03s   3GB
May 18 08:09:03 Starting translator/monadic
May 18 08:10:57 Finished translator/monadic                                    1m52s   3GB
May 18 08:10:57 Starting basis
May 18 08:55:01 Finished basis                                                44m04s  34GB
May 18 08:55:02 Starting compiler/inference
May 18 08:56:13 Finished compiler/inference                                    1m11s   2GB
May 18 08:56:14 Starting compiler/backend/reg_alloc
May 18 08:57:20 Finished compiler/backend/reg_alloc                            1m05s   1GB
May 18 08:57:20 Starting compiler/backend/gc
May 18 09:00:59 Finished compiler/backend/gc                                   3m39s   3GB
May 18 09:00:59 Starting compiler/backend
May 18 09:06:05 Finished compiler/backend                                      5m05s   5GB
May 18 09:06:05 Starting compiler/encoders/asm
May 18 09:06:28 Finished compiler/encoders/asm                                   22s   1GB
May 18 09:06:28 Starting compiler/encoders/x64
May 18 09:07:31 Finished compiler/encoders/x64                                 1m02s   1GB
May 18 09:07:31 Starting compiler/encoders/arm7
May 18 09:09:34 Finished compiler/encoders/arm7                                2m02s   1GB
May 18 09:09:34 Starting compiler/encoders/arm8
May 18 09:10:13 Finished compiler/encoders/arm8                                  38s   1GB
May 18 09:10:13 Starting compiler/encoders/mips
May 18 09:11:38 Finished compiler/encoders/mips                                1m24s   1GB
May 18 09:11:38 Starting compiler/encoders/riscv
May 18 09:13:18 Finished compiler/encoders/riscv                               1m39s   1GB
May 18 09:13:18 Starting compiler/encoders/ag32
May 18 09:13:36 Finished compiler/encoders/ag32                                  17s 984MB
May 18 09:13:37 Starting compiler/backend/x64
May 18 09:13:57 Finished compiler/backend/x64                                    20s   1GB
May 18 09:13:57 Starting compiler/backend/arm7
May 18 09:14:19 Finished compiler/backend/arm7                                   21s   1GB
May 18 09:14:19 Starting compiler/backend/arm8
May 18 09:14:39 Finished compiler/backend/arm8                                   20s   1GB
May 18 09:14:40 Starting compiler/backend/mips
May 18 09:15:00 Finished compiler/backend/mips                                   20s   1GB
May 18 09:15:00 Starting compiler/backend/riscv
May 18 09:15:22 Finished compiler/backend/riscv                                  21s   1GB
May 18 09:15:22 Starting compiler/backend/ag32
May 18 09:15: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)/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$(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:    8s  user:    8s     OK
ag32_memoryTheory                                                                                                                                    real:   16s  user:   15sFAIL<1>
 
 s.PC + 40w = 40w + s.PC
 
 Failed to prove theorem ag32_ffi_return_thm.
 
 Exception raised at Tactical.TAC_PROOF:
 unsolved goals
 error in quse /home/myreen/regression/cakeml-1527/compiler/backend/ag32/ag32_memoryScript.sml : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
 error in load /home/myreen/regression/cakeml-1527/compiler/backend/ag32/ag32_memoryScript : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
 Uncaught exception: HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
ag32_configTheory                                                                                                                                                            M-KILLED