Job 1526

CakeML:b1f30b329070e1f285585dded9c4b0910a48216d
  Fix a diverging proof [May 17 21:25:06]
HOL:1354090035c466ccae632435bb016c0bebf281d7
  Move large_numberTheory to examples/probability [May 13 23:47:06]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

May 17 21:25:45 Claimed job
May 17 21:25:48 Building HOL
May 17 21:41:42 Starting developers
May 17 21:41:46 Finished developers                                               4s  88MB
May 17 21:41:47 Starting developers/bin
May 17 21:41:54 Finished developers/bin                                           6s   1GB
May 17 21:41:54 Starting semantics/ffi
May 17 21:42:05 Finished semantics/ffi                                           11s 235MB
May 17 21:42:06 Starting semantics
May 17 21:43:42 Finished semantics                                             1m36s   1GB
May 17 21:43:43 Starting semantics/proofs
May 17 21:47:31 Finished semantics/proofs                                      3m47s   1GB
May 17 21:47:31 Starting semantics/alt_semantics
May 17 21:47:41 Finished semantics/alt_semantics                                  9s 301MB
May 17 21:47:41 Starting semantics/alt_semantics/proofs
May 17 21:50:01 Finished semantics/alt_semantics/proofs                        2m20s   1GB
May 17 21:50:01 Starting basis/pure
May 17 21:53:06 Finished basis/pure                                            3m04s 906MB
May 17 21:53:06 Starting translator
May 17 21:56:43 Finished translator                                            3m36s   1GB
May 17 21:56:43 Starting compiler/parsing
May 17 21:58:00 Finished compiler/parsing                                      1m15s   2GB
May 17 21:58:00 Starting characteristic
May 17 22:03:54 Finished characteristic                                        5m53s   2GB
May 17 22:03:54 Starting translator/monadic
May 17 22:05:33 Finished translator/monadic                                    1m38s   2GB
May 17 22:05:33 Starting basis
May 17 22:52:32 Finished basis                                                46m58s  11GB
May 17 22:52:32 Starting compiler/inference
May 17 22:53:50 Finished compiler/inference                                    1m17s   1GB
May 17 22:53:50 Starting compiler/backend/reg_alloc
May 17 22:54:59 Finished compiler/backend/reg_alloc                            1m09s   1GB
May 17 22:55:00 Starting compiler/backend/gc
May 17 22:58:53 Finished compiler/backend/gc                                   3m53s   2GB
May 17 22:58:53 Starting compiler/backend
May 17 23:04:05 Finished compiler/backend                                      5m11s   4GB
May 17 23:04:05 Starting compiler/encoders/asm
May 17 23:04:29 Finished compiler/encoders/asm                                   23s 667MB
May 17 23:04:29 Starting compiler/encoders/x64
May 17 23:05:34 Finished compiler/encoders/x64                                 1m05s   1GB
May 17 23:05:34 Starting compiler/encoders/arm7
May 17 23:07:48 Finished compiler/encoders/arm7                                2m13s   1GB
May 17 23:07:48 Starting compiler/encoders/arm8
May 17 23:08:28 Finished compiler/encoders/arm8                                  40s 577MB
May 17 23:08:28 Starting compiler/encoders/mips
May 17 23:10:06 Finished compiler/encoders/mips                                1m36s   1GB
May 17 23:10:06 Starting compiler/encoders/riscv
May 17 23:12:00 Finished compiler/encoders/riscv                               1m53s   1GB
May 17 23:12:00 Starting compiler/encoders/ag32
May 17 23:12:19 Finished compiler/encoders/ag32                                  18s 821MB
May 17 23:12:19 Starting compiler/backend/x64
May 17 23:12:40 Finished compiler/backend/x64                                    20s   1GB
May 17 23:12:40 Starting compiler/backend/arm7
May 17 23:13:00 Finished compiler/backend/arm7                                   20s   1GB
May 17 23:13:01 Starting compiler/backend/arm8
May 17 23:13:21 Finished compiler/backend/arm8                                   19s   1GB
May 17 23:13:21 Starting compiler/backend/mips
May 17 23:13:41 Finished compiler/backend/mips                                   20s   1GB
May 17 23:13:41 Starting compiler/backend/riscv
May 17 23:14:02 Finished compiler/backend/riscv                                  19s   1GB
May 17 23:14:02 Starting compiler/backend/ag32
May 17 23:14:20 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:    7s     OK
ag32_memoryTheory                               real:   16s  user:   15sFAIL<1>
 Exception raised at Tactical.TAC_PROOF:
 unsolved goals
 error in quse /home/cake/oven/regression/cakeml-1526/compiler/backend/ag32/ag32_memoryScript.sml : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
 error in load /home/cake/oven/regression/cakeml-1526/compiler/backend/ag32/ag32_memoryScript : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
 First unsolved sub-goal is
 
 s.PC + 40w = 40w + s.PC
 
 Failed to prove theorem ag32_ffi_return_thm.
 Uncaught exception: HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
ag32_configTheory                                                       M-KILLED