Job 854

CakeML:9ed0c210909badb4103863a87bab3ec3613d10f1
  Move arm6->arm7 in build-sequence [May 09 14:21:50]
#633 (FMA_support)
Merging into:331972bc323d7886b60ecbab12195ee6999bcdeb
  Merge pull request #634 from CakeML/cleanup [May 08 15:37:32]
HOL:818ca782a5ea727abaa821f259ded153f08a6f18
  Give up on sending Travis notifications to hol-builds [May 08 01:08:45]
Machine:brain08 4.14.89.1.amd64-smp x86_64 GNU/Linux

May 09 15:19:38 Claimed job
May 09 15:19:44 Building HOL
May 09 15:34:59 Starting developers
May 09 15:35:00 Finished developers                                               1s  36MB
May 09 15:35:00 Starting developers/bin
May 09 15:35:10 Finished developers/bin                                           8s 927MB
May 09 15:35:10 Starting semantics/ffi
May 09 15:36:21 Finished semantics/ffi                                         1m11s 623MB
May 09 15:36:21 Starting semantics
May 09 15:39:15 Finished semantics                                             2m53s   1GB
May 09 15:39:16 Starting semantics/proofs
May 09 15:45:17 Finished semantics/proofs                                      6m00s   1GB
May 09 15:45:17 Starting basis/pure
May 09 15:52:02 Finished basis/pure                                            6m44s 674MB
May 09 15:52:02 Starting translator
May 09 15:55:10 Finished translator                                            3m07s   1GB
May 09 15:55:10 Starting compiler/parsing
May 09 15:57:04 Finished compiler/parsing                                      1m53s   1GB
May 09 15:57:04 Starting characteristic
May 09 16:07:16 Finished characteristic                                       10m11s   1GB
May 09 16:07:17 Starting translator/monadic
May 09 16:10:05 Finished translator/monadic                                    2m48s   1GB
May 09 16:10:06 Starting basis
May 09 16:42:18 Finished basis                                                32m11s   2GB
May 09 16:42:18 Starting compiler/inference
May 09 16:46:03 Finished compiler/inference                                    3m44s   1GB
May 09 16:46:03 Starting compiler/backend/reg_alloc
May 09 16:47:41 Finished compiler/backend/reg_alloc                            1m37s   1GB
May 09 16:47:41 Starting compiler/backend/gc
May 09 17:04:21 Finished compiler/backend/gc                                  16m39s   2GB
May 09 17:04:22 Starting compiler/backend
May 09 17:04:30 Finished compiler/backend                                         8s 302MB
May 09 17:04:30 Starting compiler/encoders/asm
May 09 17:04:31 Finished compiler/encoders/asm                                    0s  28MB
May 09 17:04:32 Starting compiler/encoders/x64
May 09 17:06:26 Finished compiler/encoders/x64                                 1m54s 828MB
May 09 17:06:26 Starting compiler/encoders/arm7
May 09 17:10:06 Finished compiler/encoders/arm7                                3m39s   3GB
May 09 17:10:06 Starting compiler/encoders/arm8
May 09 17:11:09 Finished compiler/encoders/arm8                                1m02s 863MB
May 09 17:11:09 Starting compiler/encoders/mips
May 09 17:13:21 Finished compiler/encoders/mips                                2m12s   1GB
May 09 17:13:22 Starting compiler/encoders/riscv
May 09 17:16:00 Finished compiler/encoders/riscv                               2m38s   1GB
May 09 17:16:00 Starting compiler/encoders/ag32
May 09 17:16:30 Finished compiler/encoders/ag32                                  29s 798MB
May 09 17:16:30 Starting compiler/backend/x64
May 09 17:17:11 Finished compiler/backend/x64                                    40s   1GB
May 09 17:17:11 Starting compiler/backend/arm7
May 09 17:17:54 Finished compiler/backend/arm7                                   42s   1GB
May 09 17:17:54 Starting compiler/backend/arm8
May 09 17:18:32 Finished compiler/backend/arm8                                   37s   1GB
May 09 17:18:32 Starting compiler/backend/mips
May 09 17:19:11 Finished compiler/backend/mips                                   39s   1GB
May 09 17:19:12 Starting compiler/backend/riscv
May 09 17:19:52 Finished compiler/backend/riscv                                  39s   1GB
May 09 17:19:52 Starting compiler/backend/ag32
May 09 17:22:10 Finished compiler/backend/ag32                                 2m17s   1GB
May 09 17:22:10 Starting compiler/parsing/proofs
May 09 17:32:39 Finished compiler/parsing/proofs                              10m28s   1GB
May 09 17:32:40 Starting compiler/inference/proofs
May 09 17:38:10 Finished compiler/inference/proofs                             5m30s   1GB
May 09 17:38:10 Starting compiler/backend/semantics
May 09 17:51:54 Finished compiler/backend/semantics                           13m43s   1GB
May 09 17:51:55 Starting compiler/backend/reg_alloc/proofs
May 09 17:58:38 Finished compiler/backend/reg_alloc/proofs                     6m43s   1GB
May 09 17:58:39 Starting compiler/backend/proofs
May 09 19:08:47 Finished compiler/backend/proofs                            1h10m07s   5GB
May 09 19:08:47 Starting compiler/encoders/x64/proofs
May 09 19:29:55 Finished compiler/encoders/x64/proofs                         21m07s   4GB
May 09 19:29:55 Starting compiler/encoders/arm7/proofs
May 09 19:36:00 FAILED: compiler/encoders/arm7/proofs
]0;Holmake: /local/hbecker/regression/HOL-818ca782a5ea727abaa821f259ded153f08a6f18/examples/l3-machine-code/common]0;Holmake: /local/hbecker/regression/HOL-818ca782a5ea727abaa821f259ded153f08a6f18/examples/l3-machine-code/commonWorking in $(HOLDIR)/examples/l3-machine-code/common
]0;Holmake: /local/hbecker/regression/HOL-818ca782a5ea727abaa821f259ded153f08a6f18/examples/l3-machine-code]0;Holmake: /local/hbecker/regression/HOL-818ca782a5ea727abaa821f259ded153f08a6f18/examples/machine-code/decompiler]0;Holmake: /local/hbecker/regression/HOL-818ca782a5ea727abaa821f259ded153f08a6f18/examples/machine-code/decompilerWorking in $(HOLDIR)/examples/machine-code/decompiler
]0;Holmake: /local/hbecker/regression/HOL-818ca782a5ea727abaa821f259ded153f08a6f18/examples/l3-machine-code]0;Holmake: /local/hbecker/regression/HOL-818ca782a5ea727abaa821f259ded153f08a6f18/examples/l3-machine-codeWorking in $(HOLDIR)/examples/l3-machine-code
]0;Holmake: /local/hbecker/regression/HOL-818ca782a5ea727abaa821f259ded153f08a6f18/examples/l3-machine-code/arm/step]0;Holmake: /local/hbecker/regression/HOL-818ca782a5ea727abaa821f259ded153f08a6f18/examples/l3-machine-code/arm/model]0;Holmake: /local/hbecker/regression/HOL-818ca782a5ea727abaa821f259ded153f08a6f18/examples/l3-machine-code/lib]0;Holmake: /local/hbecker/regression/HOL-818ca782a5ea727abaa821f259ded153f08a6f18/examples/l3-machine-code/libWorking in $(HOLDIR)/examples/l3-machine-code/lib
]0;Holmake: /local/hbecker/regression/HOL-818ca782a5ea727abaa821f259ded153f08a6f18/examples/l3-machine-code/arm/model]0;Holmake: /local/hbecker/regression/HOL-818ca782a5ea727abaa821f259ded153f08a6f18/examples/l3-machine-code/arm/modelWorking in $(HOLDIR)/examples/l3-machine-code/arm/model
]0;Holmake: /local/hbecker/regression/HOL-818ca782a5ea727abaa821f259ded153f08a6f18/examples/l3-machine-code/arm/step]0;Holmake: /local/hbecker/regression/HOL-818ca782a5ea727abaa821f259ded153f08a6f18/examples/l3-machine-code/arm/stepWorking in $(HOLDIR)/examples/l3-machine-code/arm/step
]0;Holmake: /local/hbecker/regression/HOL-818ca782a5ea727abaa821f259ded153f08a6f18/examples/l3-machine-code/arm/prog]0;Holmake: /local/hbecker/regression/HOL-818ca782a5ea727abaa821f259ded153f08a6f18/examples/l3-machine-code/arm/progWorking in $(HOLDIR)/examples/l3-machine-code/arm/prog
Starting work on arm-step-heap
arm-step-heap                                                                                                                                                                                                    OK
Starting work on arm_progTheory
arm_progTheory                                                                                                                                                                                                   OK
]0;Holmake: .]0;Holmake: ..]0;Holmake: ../../asm]0;Holmake: /local/hbecker/regression/cakeml-854/misc]0;Holmake: /local/hbecker/regression/HOL-818ca782a5ea727abaa821f259ded153f08a6f18/examples/fun-op-sem/lprefix_lub]0;Holmake: /local/hbecker/regression/HOL-818ca782a5ea727abaa821f259ded153f08a6f18/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: /local/hbecker/regression/cakeml-854/misc]0;Holmake: /local/hbecker/regression/cakeml-854/developers]0;Holmake: /local/hbecker/regression/cakeml-854/developersWorking in $(CAKEMLDIR)/developers
]0;Holmake: /local/hbecker/regression/cakeml-854/misc]0;Holmake: /local/hbecker/regression/cakeml-854/misc/lem_lib_stub]0;Holmake: /local/hbecker/regression/HOL-818ca782a5ea727abaa821f259ded153f08a6f18/examples/formal-languages/context-free]0;Holmake: /local/hbecker/regression/HOL-818ca782a5ea727abaa821f259ded153f08a6f18/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: /local/hbecker/regression/cakeml-854/misc/lem_lib_stub]0;Holmake: /local/hbecker/regression/cakeml-854/misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: /local/hbecker/regression/cakeml-854/misc]0;Holmake: /local/hbecker/regression/cakeml-854/miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: ../../asm]0;Holmake: /local/hbecker/regression/cakeml-854/semantics]0;Holmake: /local/hbecker/regression/cakeml-854/semantics/ffi]0;Holmake: /local/hbecker/regression/cakeml-854/semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: /local/hbecker/regression/cakeml-854/semantics]0;Holmake: /local/hbecker/regression/cakeml-854/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"}