Job 865

CakeML:9ed0c210909badb4103863a87bab3ec3613d10f1
  Move arm6->arm7 in build-sequence [May 09 14:21:50]
#633 (FMA_support)
Merging into:d12bf8c081357963887ad183f2f09e395105cdf6
  renaming for Isabelle (resurrect 7fbd3c0) [May 13 08:52:17]
HOL:1557f72fc9a7a80bc5ce2e4df30afd51803c8b75
  Get formal-languages/regular to pass src tests again [May 09 11:06:43]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

May 13 10:15:02 Claimed job
May 13 10:15:06 Reusing HOL
May 13 10:15:53 Starting developers
May 13 10:15:56 Finished developers                                               2s  20MB
May 13 10:15:56 Starting developers/bin
May 13 10:17:08 Finished developers/bin                                        1m11s 919MB
May 13 10:17:08 Starting semantics/ffi
May 13 10:17:18 Finished semantics/ffi                                            9s 222MB
May 13 10:17:18 Starting semantics
May 13 10:18:40 Finished semantics                                             1m21s   1GB
May 13 10:18:40 Starting semantics/proofs
May 13 10:21:40 Finished semantics/proofs                                      2m59s   1GB
May 13 10:21:40 Starting basis/pure
May 13 10:22:27 Finished basis/pure                                              47s 829MB
May 13 10:22:27 Starting translator
May 13 10:24:08 Finished translator                                            1m40s   1GB
May 13 10:24:08 Starting compiler/parsing
May 13 10:25:07 Finished compiler/parsing                                        58s   1GB
May 13 10:25:07 Starting characteristic
May 13 10:30:22 Finished characteristic                                        5m14s   2GB
May 13 10:30:22 Starting translator/monadic
May 13 10:31:52 Finished translator/monadic                                    1m30s   1GB
May 13 10:31:52 Starting basis
May 13 10:48:52 Finished basis                                                16m59s   2GB
May 13 10:48:53 Starting compiler/inference
May 13 10:50:27 Finished compiler/inference                                    1m34s   1GB
May 13 10:50:27 Starting compiler/backend/reg_alloc
May 13 10:51:28 Finished compiler/backend/reg_alloc                              59s   1GB
May 13 10:51:28 Starting compiler/backend/gc
May 13 10:59:33 Finished compiler/backend/gc                                   8m04s   2GB
May 13 10:59:33 Starting compiler/backend
May 13 10:59:35 Finished compiler/backend                                         2s  20MB
May 13 10:59:36 Starting compiler/encoders/asm
May 13 10:59:37 Finished compiler/encoders/asm                                    1s  21MB
May 13 10:59:37 Starting compiler/encoders/x64
May 13 11:00:02 Finished compiler/encoders/x64                                   24s 814MB
May 13 11:00:02 Starting compiler/encoders/arm7
May 13 11:00:49 Finished compiler/encoders/arm7                                  46s 734MB
May 13 11:00:49 Starting compiler/encoders/arm8
May 13 11:01:03 Finished compiler/encoders/arm8                                  13s 559MB
May 13 11:01:03 Starting compiler/encoders/mips
May 13 11:01:21 Finished compiler/encoders/mips                                  18s 966MB
May 13 11:01:22 Starting compiler/encoders/riscv
May 13 11:01:37 Finished compiler/encoders/riscv                                 14s 837MB
May 13 11:01:37 Starting compiler/encoders/ag32
May 13 11:01:54 Finished compiler/encoders/ag32                                  17s 811MB
May 13 11:01:55 Starting compiler/backend/x64
May 13 11:02:13 Finished compiler/backend/x64                                    18s 956MB
May 13 11:02:13 Starting compiler/backend/arm7
May 13 11:02:33 Finished compiler/backend/arm7                                   19s   1GB
May 13 11:02:34 Starting compiler/backend/arm8
May 13 11:02:53 Finished compiler/backend/arm8                                   18s   1GB
May 13 11:02:53 Starting compiler/backend/mips
May 13 11:03:13 Finished compiler/backend/mips                                   19s   1GB
May 13 11:03:13 Starting compiler/backend/riscv
May 13 11:03:32 Finished compiler/backend/riscv                                  19s   1GB
May 13 11:03:32 Starting compiler/backend/ag32
May 13 11:04:40 Finished compiler/backend/ag32                                 1m07s 906MB
May 13 11:04:40 Starting compiler/parsing/proofs
May 13 11:10:12 Finished compiler/parsing/proofs                               5m31s   1GB
May 13 11:10:12 Starting compiler/inference/proofs
May 13 11:12:58 Finished compiler/inference/proofs                             2m45s   1GB
May 13 11:12:58 Starting compiler/backend/semantics
May 13 11:20:02 Finished compiler/backend/semantics                            7m04s   1GB
May 13 11:20:03 Starting compiler/backend/reg_alloc/proofs
May 13 11:23:19 Finished compiler/backend/reg_alloc/proofs                     3m16s 898MB
May 13 11:23:20 Starting compiler/backend/proofs
May 13 12:01:47 Finished compiler/backend/proofs                              38m27s   4GB
May 13 12:01:47 Starting compiler/encoders/x64/proofs
May 13 12:10:38 Finished compiler/encoders/x64/proofs                          8m50s   5GB
May 13 12:10:38 Starting compiler/encoders/arm7/proofs
May 13 12:12:19 FAILED: compiler/encoders/arm7/proofs
]0;Holmake: ~/oven/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/common]0;Holmake: ~/oven/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/commonWorking in $(HOLDIR)/examples/l3-machine-code/common
]0;Holmake: ~/oven/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code]0;Holmake: ~/oven/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/machine-code/decompiler]0;Holmake: ~/oven/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/machine-code/decompilerWorking in $(HOLDIR)/examples/machine-code/decompiler
]0;Holmake: ~/oven/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code]0;Holmake: ~/oven/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-codeWorking in $(HOLDIR)/examples/l3-machine-code
]0;Holmake: ~/oven/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/arm/step]0;Holmake: ~/oven/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/arm/model]0;Holmake: ~/oven/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/lib]0;Holmake: ~/oven/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/libWorking in $(HOLDIR)/examples/l3-machine-code/lib
]0;Holmake: ~/oven/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/arm/model]0;Holmake: ~/oven/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/arm/modelWorking in $(HOLDIR)/examples/l3-machine-code/arm/model
]0;Holmake: ~/oven/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/arm/step]0;Holmake: ~/oven/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/arm/stepWorking in $(HOLDIR)/examples/l3-machine-code/arm/step
]0;Holmake: ~/oven/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/arm/prog]0;Holmake: ~/oven/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/arm/progWorking in $(HOLDIR)/examples/l3-machine-code/arm/prog
]0;Holmake: .]0;Holmake: ..]0;Holmake: ../../asm]0;Holmake: ~/oven/regression/cakeml-865/misc]0;Holmake: ~/oven/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/oven/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ~/oven/regression/cakeml-865/misc]0;Holmake: ~/oven/regression/cakeml-865/developers]0;Holmake: ~/oven/regression/cakeml-865/developersWorking in $(CAKEMLDIR)/developers
]0;Holmake: ~/oven/regression/cakeml-865/misc]0;Holmake: ~/oven/regression/cakeml-865/misc/lem_lib_stub]0;Holmake: ~/oven/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/formal-languages/context-free]0;Holmake: ~/oven/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: ~/oven/regression/cakeml-865/misc/lem_lib_stub]0;Holmake: ~/oven/regression/cakeml-865/misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ~/oven/regression/cakeml-865/misc]0;Holmake: ~/oven/regression/cakeml-865/miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: ../../asm]0;Holmake: ~/oven/regression/cakeml-865/semantics]0;Holmake: ~/oven/regression/cakeml-865/semantics/ffi]0;Holmake: ~/oven/regression/cakeml-865/semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: ~/oven/regression/cakeml-865/semantics]0;Holmake: ~/oven/regression/cakeml-865/semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: ../../asm]0;Holmake: ../../asmWorking in $(CAKEMLDIR)/compiler/encoders/asm
]0;Holmake: ..]0;Holmake: ..Working in $(CAKEMLDIR)/compiler/encoders/arm7
]0;Holmake: .]0;Holmake: .Working in $(CAKEMLDIR)/compiler/encoders/arm7/proofs
Starting work on arm7_targetProofTheory
Starting work on README.md
README.md                                                                    OK
arm7_targetProofTheory                                              FAILED! <1>
  s.pc  state.REG RName_PC  (a. a  s.mem_domain  s.mem a  state.MEM a) 
  (i.
       (i < 16  i  13  i  15) 
       s.regs i  state.REG (R_mode state.CPSR.M (n2w i))) 
  i. i < 32  s.fp_regs i  state.FP.REG (n2w i))  s.mem s.pc  a 
 s.pc  s.mem_domain  s.mem (s.pc + 1w)  b  s.pc + 1w  s.mem_domain 
 s.mem (s.pc + 2w)  c  s.pc + 2w  s.mem_domain  s.mem (s.pc + 3w)  d 
 s.pc + 3w  s.mem_domain
 
 Uncaught exception: HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}