Job 856

CakeML:9ed0c210909badb4103863a87bab3ec3613d10f1
  Move arm6->arm7 in build-sequence [May 09 14:21:50]
#633 (FMA_support)
Merging into:53fd12a2f3ee14927097506986b55a5d2bcf1b97
  Merge pull request #641 from CakeML/issue465 [May 10 05:54:52]
HOL:1557f72fc9a7a80bc5ce2e4df30afd51803c8b75
  Get formal-languages/regular to pass src tests again [May 09 11:06:43]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

May 10 13:46:26 Claimed job
May 10 13:46:33 Building HOL
May 10 13:54:20 Starting developers
May 10 13:54:21 Finished developers                                               0s  22MB
May 10 13:54:21 Starting developers/bin
May 10 13:54:24 Finished developers/bin                                           2s 144MB
May 10 13:54:24 Starting semantics/ffi
May 10 13:54:58 Finished semantics/ffi                                           32s 539MB
May 10 13:54:58 Starting semantics
May 10 13:56:28 Finished semantics                                             1m29s   1GB
May 10 13:56:28 Starting semantics/proofs
May 10 13:59:27 Finished semantics/proofs                                      2m58s   1GB
May 10 13:59:27 Starting basis/pure
May 10 14:03:01 Finished basis/pure                                            3m33s 779MB
May 10 14:03:01 Starting translator
May 10 14:04:38 Finished translator                                            1m36s   1GB
May 10 14:04:38 Starting compiler/parsing
May 10 14:05:36 Finished compiler/parsing                                        57s   2GB
May 10 14:05:36 Starting characteristic
May 10 14:10:42 Finished characteristic                                        5m05s   1GB
May 10 14:10:42 Starting translator/monadic
May 10 14:12:05 Finished translator/monadic                                    1m22s   1GB
May 10 14:12:05 Starting basis
May 10 14:28:49 Finished basis                                                16m43s   2GB
May 10 14:28:49 Starting compiler/inference
May 10 14:30:37 Finished compiler/inference                                    1m47s   1GB
May 10 14:30:37 Starting compiler/backend/reg_alloc
May 10 14:31:35 Finished compiler/backend/reg_alloc                              57s   1GB
May 10 14:31:36 Starting compiler/backend/gc
May 10 14:40:34 Finished compiler/backend/gc                                   8m58s   1GB
May 10 14:40:35 Starting compiler/backend
May 10 14:40:36 Finished compiler/backend                                         0s  42MB
May 10 14:40:36 Starting compiler/encoders/asm
May 10 14:40:36 Finished compiler/encoders/asm                                    0s  32MB
May 10 14:40:37 Starting compiler/encoders/x64
May 10 14:41:33 Finished compiler/encoders/x64                                   55s 917MB
May 10 14:41:33 Starting compiler/encoders/arm7
May 10 14:43:09 Finished compiler/encoders/arm7                                1m35s   1GB
May 10 14:43:09 Starting compiler/encoders/arm8
May 10 14:43:38 Finished compiler/encoders/arm8                                  28s 866MB
May 10 14:43:38 Starting compiler/encoders/mips
May 10 14:44:42 Finished compiler/encoders/mips                                1m03s   1GB
May 10 14:44:42 Starting compiler/encoders/riscv
May 10 14:46:00 Finished compiler/encoders/riscv                               1m16s   1GB
May 10 14:46:00 Starting compiler/encoders/ag32
May 10 14:46:15 Finished compiler/encoders/ag32                                  14s 768MB
May 10 14:46:15 Starting compiler/backend/x64
May 10 14:46:31 Finished compiler/backend/x64                                    15s   1GB
May 10 14:46:31 Starting compiler/backend/arm7
May 10 14:46:48 Finished compiler/backend/arm7                                   16s   1GB
May 10 14:46:48 Starting compiler/backend/arm8
May 10 14:47:05 Finished compiler/backend/arm8                                   16s 910MB
May 10 14:47:05 Starting compiler/backend/mips
May 10 14:47:21 Finished compiler/backend/mips                                   15s 831MB
May 10 14:47:21 Starting compiler/backend/riscv
May 10 14:47:38 Finished compiler/backend/riscv                                  16s   1GB
May 10 14:47:38 Starting compiler/backend/ag32
May 10 14:48:43 Finished compiler/backend/ag32                                 1m04s   1GB
May 10 14:48:44 Starting compiler/parsing/proofs
May 10 14:54:15 Finished compiler/parsing/proofs                               5m30s   1GB
May 10 14:54:15 Starting compiler/inference/proofs
May 10 14:56:53 Finished compiler/inference/proofs                             2m37s 942MB
May 10 14:56:53 Starting compiler/backend/semantics
May 10 15:03:55 Finished compiler/backend/semantics                            7m01s   1GB
May 10 15:03:55 Starting compiler/backend/reg_alloc/proofs
May 10 15:07:14 Finished compiler/backend/reg_alloc/proofs                     3m18s 744MB
May 10 15:07:14 Starting compiler/backend/proofs
May 10 15:45:32 Finished compiler/backend/proofs                              38m16s   4GB
May 10 15:45:32 Starting compiler/encoders/x64/proofs
May 10 15:55:29 Finished compiler/encoders/x64/proofs                          9m56s   5GB
May 10 15:55:29 Starting compiler/encoders/arm7/proofs
May 10 15:58:27 FAILED: compiler/encoders/arm7/proofs
]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/common]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/common[1mWorking in $(HOLDIR)/examples/l3-machine-code/common[0m
]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/machine-code/decompiler]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/machine-code/decompiler[1mWorking in $(HOLDIR)/examples/machine-code/decompiler[0m
]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code[1mWorking in $(HOLDIR)/examples/l3-machine-code[0m
]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/arm/step]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/arm/model]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/lib]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/lib[1mWorking in $(HOLDIR)/examples/l3-machine-code/lib[0m
]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/arm/model]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/arm/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/model[0m
]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/arm/step]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/arm/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/step[0m
]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/arm/prog]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/arm/prog[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/prog[0m
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: ~/regression/cakeml-856/misc]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-856/misc]0;Holmake: ~/regression/cakeml-856/developers]0;Holmake: ~/regression/cakeml-856/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-856/misc]0;Holmake: ~/regression/cakeml-856/misc/lem_lib_stub]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/cakeml-856/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-856/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-856/misc]0;Holmake: ~/regression/cakeml-856/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ../../asm]0;Holmake: ~/regression/cakeml-856/semantics]0;Holmake: ~/regression/cakeml-856/semantics/ffi]0;Holmake: ~/regression/cakeml-856/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-856/semantics]0;Holmake: ~/regression/cakeml-856/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ../../asm]0;Holmake: ../../asm[1mWorking in $(CAKEMLDIR)/compiler/encoders/asm[0m
]0;Holmake: ..]0;Holmake: ..[1mWorking in $(CAKEMLDIR)/compiler/encoders/arm7[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/compiler/encoders/arm7/proofs[0m
Starting work on arm7_targetProofTheory
arm7_targetProofTheory                                                                                                   FAILED! <1>
       (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
 
 error in quse /home/myreen/regression/cakeml-856/compiler/encoders/arm7/proofs/arm7_targetProofScript.sml : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
 error in load arm7_targetProofScript : 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"}