Job 860

CakeML:9ed0c210909badb4103863a87bab3ec3613d10f1
  Move arm6->arm7 in build-sequence [May 09 14:21:50]
#633 (FMA_support)
Merging into:96ec9c17d55e54ccc04d7858e8f7a1257f8452ec
  Merge pull request #643 from CakeML/cleanup [May 11 05:53:36]
HOL:1557f72fc9a7a80bc5ce2e4df30afd51803c8b75
  Get formal-languages/regular to pass src tests again [May 09 11:06:43]
Machine:te1

May 11 16:19:07 Claimed job
May 11 16:19:12 Building HOL
May 11 16:32:00 Starting developers
May 11 16:32:03 Finished developers                                               2s  30MB
May 11 16:32:03 Starting developers/bin
May 11 16:32:09 Finished developers/bin                                           6s 929MB
May 11 16:32:09 Starting semantics/ffi
May 11 16:33:05 Finished semantics/ffi                                           55s 538MB
May 11 16:33:05 Starting semantics
May 11 16:35:19 Finished semantics                                             2m14s   1GB
May 11 16:35:19 Starting semantics/proofs
May 11 16:39:37 Finished semantics/proofs                                      4m17s   1GB
May 11 16:39:37 Starting basis/pure
May 11 16:44:31 Finished basis/pure                                            4m54s 756MB
May 11 16:44:31 Starting translator
May 11 16:46:53 Finished translator                                            2m21s   1GB
May 11 16:46:53 Starting compiler/parsing
May 11 16:48:10 Finished compiler/parsing                                      1m17s   1GB
May 11 16:48:10 Starting characteristic
May 11 16:55:33 Finished characteristic                                        7m22s   2GB
May 11 16:55:33 Starting translator/monadic
May 11 16:57:40 Finished translator/monadic                                    2m06s   1GB
May 11 16:57:40 Starting basis
May 11 17:21:15 Finished basis                                                23m35s   3GB
May 11 17:21:15 Starting compiler/inference
May 11 17:23:54 Finished compiler/inference                                    2m38s   1GB
May 11 17:23:54 Starting compiler/backend/reg_alloc
May 11 17:25:12 Finished compiler/backend/reg_alloc                            1m18s   1GB
May 11 17:25:12 Starting compiler/backend/gc
May 11 17:37:40 Finished compiler/backend/gc                                  12m27s   1GB
May 11 17:37:40 Starting compiler/backend
May 11 17:37:43 Finished compiler/backend                                         2s  32MB
May 11 17:37:43 Starting compiler/encoders/asm
May 11 17:37:44 Finished compiler/encoders/asm                                    1s  17MB
May 11 17:37:44 Starting compiler/encoders/x64
May 11 17:39:12 Finished compiler/encoders/x64                                 1m28s 624MB
May 11 17:39:12 Starting compiler/encoders/arm7
May 11 17:41:38 Finished compiler/encoders/arm7                                2m25s   1GB
May 11 17:41:38 Starting compiler/encoders/arm8
May 11 17:42:23 Finished compiler/encoders/arm8                                  44s 635MB
May 11 17:42:23 Starting compiler/encoders/mips
May 11 17:44:01 Finished compiler/encoders/mips                                1m37s 927MB
May 11 17:44:01 Starting compiler/encoders/riscv
May 11 17:45:52 Finished compiler/encoders/riscv                               1m51s   1GB
May 11 17:45:52 Starting compiler/encoders/ag32
May 11 17:46:16 Finished compiler/encoders/ag32                                  23s 520MB
May 11 17:46:16 Starting compiler/backend/x64
May 11 17:46:42 Finished compiler/backend/x64                                    25s   1GB
May 11 17:46:42 Starting compiler/backend/arm7
May 11 17:47:07 Finished compiler/backend/arm7                                   25s   1GB
May 11 17:47:07 Starting compiler/backend/arm8
May 11 17:47:32 Finished compiler/backend/arm8                                   25s   1GB
May 11 17:47:33 Starting compiler/backend/mips
May 11 17:47:57 Finished compiler/backend/mips                                   23s 863MB
May 11 17:47:57 Starting compiler/backend/riscv
May 11 17:48:24 Finished compiler/backend/riscv                                  26s   1GB
May 11 17:48:24 Starting compiler/backend/ag32
May 11 17:49:54 Finished compiler/backend/ag32                                 1m29s   1GB
May 11 17:49:54 Starting compiler/parsing/proofs
May 11 17:58:32 Finished compiler/parsing/proofs                               8m38s   1GB
May 11 17:58:32 Starting compiler/inference/proofs
May 11 18:02:30 Finished compiler/inference/proofs                             3m58s   1GB
May 11 18:02:30 Starting compiler/backend/semantics
May 11 18:11:52 Finished compiler/backend/semantics                            9m21s   1GB
May 11 18:11:52 Starting compiler/backend/reg_alloc/proofs
May 11 18:16:46 Finished compiler/backend/reg_alloc/proofs                     4m53s   1GB
May 11 18:16:46 Starting compiler/backend/proofs
May 11 19:08:29 Finished compiler/backend/proofs                              51m42s   4GB
May 11 19:08:29 Starting compiler/encoders/x64/proofs
May 11 19:22:03 Finished compiler/encoders/x64/proofs                         13m34s   6GB
May 11 19:22:03 Starting compiler/encoders/arm7/proofs
May 11 19:25:53 FAILED: compiler/encoders/arm7/proofs
]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/common]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/common[1mWorking in $(HOLDIR)/examples/l3-machine-code/common[0m
]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/machine-code/decompiler]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/machine-code/decompiler[1mWorking in $(HOLDIR)/examples/machine-code/decompiler[0m
]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code[1mWorking in $(HOLDIR)/examples/l3-machine-code[0m
]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/arm/step]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/arm/model]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/lib]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/lib[1mWorking in $(HOLDIR)/examples/l3-machine-code/lib[0m
]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/arm/model]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/arm/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/model[0m
]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/arm/step]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/arm/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/step[0m
]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/arm/prog]0;Holmake: ~/regression-worker/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-worker/cakeml-860/misc]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression-worker/cakeml-860/misc]0;Holmake: ~/regression-worker/cakeml-860/developers]0;Holmake: ~/regression-worker/cakeml-860/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression-worker/cakeml-860/misc]0;Holmake: ~/regression-worker/cakeml-860/misc/lem_lib_stub]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/formal-languages/context-free]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression-worker/cakeml-860/misc/lem_lib_stub]0;Holmake: ~/regression-worker/cakeml-860/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression-worker/cakeml-860/misc]0;Holmake: ~/regression-worker/cakeml-860/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ../../asm]0;Holmake: ~/regression-worker/cakeml-860/semantics]0;Holmake: ~/regression-worker/cakeml-860/semantics/ffi]0;Holmake: ~/regression-worker/cakeml-860/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression-worker/cakeml-860/semantics]0;Holmake: ~/regression-worker/cakeml-860/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
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"}