Overview

Job 860

CakeML:9ed0c210909badb4103863a87bab3ec3613d10f1
  Move arm6->arm7 in build-sequence
#633 (FMA_support)
Merging into:96ec9c17d55e54ccc04d7858e8f7a1257f8452ec
  Merge pull request #643 from CakeML/cleanup
HOL:1557f72fc9a7a80bc5ce2e4df30afd51803c8b75
  Get formal-languages/regular to pass src tests again
Machine:te1

 Claimed job
 Building HOL
 Starting developers
 Finished developers                                               2s  30MB
 Starting developers/bin
 Finished developers/bin                                           6s 929MB
 Starting semantics/ffi
 Finished semantics/ffi                                           55s 538MB
 Starting semantics
 Finished semantics                                             2m14s   1GB
 Starting semantics/proofs
 Finished semantics/proofs                                      4m17s   1GB
 Starting basis/pure
 Finished basis/pure                                            4m54s 756MB
 Starting translator
 Finished translator                                            2m21s   1GB
 Starting compiler/parsing
 Finished compiler/parsing                                      1m17s   1GB
 Starting characteristic
 Finished characteristic                                        7m22s   2GB
 Starting translator/monadic
 Finished translator/monadic                                    2m06s   1GB
 Starting basis
 Finished basis                                                23m35s   3GB
 Starting compiler/inference
 Finished compiler/inference                                    2m38s   1GB
 Starting compiler/backend/reg_alloc
 Finished compiler/backend/reg_alloc                            1m18s   1GB
 Starting compiler/backend/gc
 Finished compiler/backend/gc                                  12m27s   1GB
 Starting compiler/backend
 Finished compiler/backend                                         2s  32MB
 Starting compiler/encoders/asm
 Finished compiler/encoders/asm                                    1s  17MB
 Starting compiler/encoders/x64
 Finished compiler/encoders/x64                                 1m28s 624MB
 Starting compiler/encoders/arm7
 Finished compiler/encoders/arm7                                2m25s   1GB
 Starting compiler/encoders/arm8
 Finished compiler/encoders/arm8                                  44s 635MB
 Starting compiler/encoders/mips
 Finished compiler/encoders/mips                                1m37s 927MB
 Starting compiler/encoders/riscv
 Finished compiler/encoders/riscv                               1m51s   1GB
 Starting compiler/encoders/ag32
 Finished compiler/encoders/ag32                                  23s 520MB
 Starting compiler/backend/x64
 Finished compiler/backend/x64                                    25s   1GB
 Starting compiler/backend/arm7
 Finished compiler/backend/arm7                                   25s   1GB
 Starting compiler/backend/arm8
 Finished compiler/backend/arm8                                   25s   1GB
 Starting compiler/backend/mips
 Finished compiler/backend/mips                                   23s 863MB
 Starting compiler/backend/riscv
 Finished compiler/backend/riscv                                  26s   1GB
 Starting compiler/backend/ag32
 Finished compiler/backend/ag32                                 1m29s   1GB
 Starting compiler/parsing/proofs
 Finished compiler/parsing/proofs                               8m38s   1GB
 Starting compiler/inference/proofs
 Finished compiler/inference/proofs                             3m58s   1GB
 Starting compiler/backend/semantics
 Finished compiler/backend/semantics                            9m21s   1GB
 Starting compiler/backend/reg_alloc/proofs
 Finished compiler/backend/reg_alloc/proofs                     4m53s   1GB
 Starting compiler/backend/proofs
 Finished compiler/backend/proofs                              51m42s   4GB
 Starting compiler/encoders/x64/proofs
 Finished compiler/encoders/x64/proofs                         13m34s   6GB
 Starting compiler/encoders/arm7/proofs
 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"}