Overview

Job 463

CakeML:f6d8ed2ee71091a75c6c7c634490380e8abe11a9
  Fix typo
HOL:98d718b2599e89f71200ee47e9077ea1cfaba444
  Merge pull request #577 from binghe/topology_merge.2
Machine:cakeml1797 4.4.0-22-generic x86_64 GNU/Linux

 Claimed job
 Building HOL
 Starting developers/bin
 Finished developers/bin                                           7s 144MB
 Starting semantics/ffi
 Finished semantics/ffi                                           58s 364MB
 Starting semantics
 Finished semantics                                             2m20s 806MB
 Starting semantics/proofs
 Finished semantics/proofs                                      5m12s 955MB
 Starting basis/pure
 Finished basis/pure                                            5m44s 714MB
 Starting translator
 Finished translator                                            1m54s   1GB
 Starting compiler/parsing
 Finished compiler/parsing                                      2m16s   1GB
 Starting characteristic
 Finished characteristic                                        4m30s   1GB
 Starting translator/monadic
 Finished translator/monadic                                    2m32s   1GB
 Starting basis
 Finished basis                                                28m14s   2GB
 Starting compiler/inference
 Finished compiler/inference                                    2m44s   1GB
 Starting compiler/backend/reg_alloc
 Finished compiler/backend/reg_alloc                            1m18s   1GB
 Starting compiler/backend/gc
 Finished compiler/backend/gc                                  14m39s   3GB
 Starting compiler/backend
 Finished compiler/backend                                         3s  16MB
 Starting compiler/encoders/asm
 Finished compiler/encoders/asm                                    0s  27MB
 Starting compiler/encoders/x64
 Finished compiler/encoders/x64                                 1m25s 598MB
 Starting compiler/encoders/arm6
 Finished compiler/encoders/arm6                                2m56s   1GB
 Starting compiler/encoders/arm8
 Finished compiler/encoders/arm8                                  43s 389MB
 Starting compiler/encoders/mips
 Finished compiler/encoders/mips                                1m36s 904MB
 Starting compiler/encoders/riscv
 Finished compiler/encoders/riscv                               1m32s 699MB
 Starting compiler/backend/x64
 Finished compiler/backend/x64                                    31s   1GB
 Starting compiler/backend/arm6
 Finished compiler/backend/arm6                                   31s   1GB
 Starting compiler/backend/arm8
 Finished compiler/backend/arm8                                   30s   1GB
 Starting compiler/backend/mips
 Finished compiler/backend/mips                                   30s 765MB
 Starting compiler/backend/riscv
 Finished compiler/backend/riscv                                  31s   1GB
 Starting compiler/parsing/proofs
 Finished compiler/parsing/proofs                               4m01s 692MB
 Starting compiler/inference/proofs
 Finished compiler/inference/proofs                             4m47s   1GB
 Starting compiler/backend/semantics
 Finished compiler/backend/semantics                           14m27s   2GB
 Starting compiler/backend/reg_alloc/proofs
 Finished compiler/backend/reg_alloc/proofs                    12m04s 563MB
 Starting compiler/backend/proofs
 Finished compiler/backend/proofs                              54m21s   3GB
 Starting compiler/encoders/x64/proofs
 Finished compiler/encoders/x64/proofs                         11m29s   1GB
 Starting compiler/encoders/arm6/proofs
 Finished compiler/encoders/arm6/proofs                        11m59s   2GB
 Starting compiler/encoders/arm8/proofs
 Finished compiler/encoders/arm8/proofs                         8m18s   1GB
 Starting compiler/encoders/mips/proofs
 Finished compiler/encoders/mips/proofs                        11m35s   1GB
 Starting compiler/encoders/riscv/proofs
 Finished compiler/encoders/riscv/proofs                       12m28s 899MB
 Starting compiler/backend/x64/proofs
 Finished compiler/backend/x64/proofs                             33s   1GB
 Starting compiler/backend/arm6/proofs
 Finished compiler/backend/arm6/proofs                            34s   1GB
 Starting compiler/backend/arm8/proofs
 Finished compiler/backend/arm8/proofs                            33s   1GB
 Starting compiler/backend/mips/proofs
 Finished compiler/backend/mips/proofs                            34s   1GB
 Starting compiler/backend/riscv/proofs
 Finished compiler/backend/riscv/proofs                           33s   1GB
 Starting compiler/proofs
 Finished compiler/proofs                                       2m23s   2GB
 Starting candle/set-theory
 Finished candle/set-theory                                       54s 595MB
 Starting candle/syntax-lib
 Finished candle/syntax-lib                                       16s 547MB
 Starting candle/standard/syntax
 Finished candle/standard/syntax                                2m42s 621MB
 Starting candle/standard/semantics
 Finished candle/standard/semantics                             2m12s 871MB
 Starting candle/standard/monadic
 Finished candle/standard/monadic                               2m35s 929MB
 Starting candle/standard/ml_kernel
 Finished candle/standard/ml_kernel                            24m42s   4GB
 Starting candle/standard/opentheory
 Finished candle/standard/opentheory                           14m43s   4GB
 Starting characteristic/examples
 Finished characteristic/examples                               2m40s   2GB
 Starting tutorial/solutions
 Finished tutorial/solutions                                   21m11s   7GB
 Starting translator/monadic/examples
 Finished translator/monadic/examples                           2m43s   2GB
 Starting examples
 Finished examples                                              8m08s   4GB
 Starting examples/compilation
 Finished examples/compilation                               2h55m56s  15GB
 Starting examples/compilation/proofs
 Finished examples/compilation/proofs                           3m36s   3GB
 Starting compiler/benchmarks
 Finished compiler/benchmarks                                      0s   4MB
 Starting translator/okasaki-examples
 Finished translator/okasaki-examples                           6m17s   1GB
 Starting translator/other-examples
 Finished translator/other-examples                             6m41s 963MB
 Starting compiler/parsing/tests
 Finished compiler/parsing/tests                                  39s 304MB
 Starting compiler/inference/tests
 Finished compiler/inference/tests                              6m22s   5GB
 Starting compiler/bootstrap/translation
 FAILED: compiler/bootstrap/translation
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/arm/model]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/common]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/common]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/common[1mWorking in $(HOLDIR)/examples/l3-machine-code/common[0m
]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/arm/model]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/lib]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/lib[1mWorking in $(HOLDIR)/examples/l3-machine-code/lib[0m
]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/arm/model]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/arm/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/model[0m
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/arm8/model]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/arm8/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm8/model[0m
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/mips/model]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/mips/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/mips/model[0m
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/riscv/model]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/riscv/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/riscv/model[0m
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/x64/model]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/x64/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/x64/model[0m
]0;Holmake: .]0;Holmake: ../../../basis]0;Holmake: ../../../basis/pure]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../misc]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ../../../misc]0;Holmake: ../../../developers]0;Holmake: ../../../developers[1mWorking in ../../../developers[0m
]0;Holmake: ../../../misc]0;Holmake: ../../../misc/lem_lib_stub]0;Holmake: ../../../misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ../../../misc]0;Holmake: ../../../misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ../../../basis]0;Holmake: ../../../characteristic]0;Holmake: ../../../compiler/parsing]0;Holmake: ../../../semantics]0;Holmake: ../../../semantics/ffi]0;Holmake: ../../../semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ../../../semantics]0;Holmake: ../../../semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ../../../compiler/parsing]0;Holmake: ../../../compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ../../../characteristic]0;Holmake: ../../../translator]0;Holmake: ../../../semantics/proofs]0;Holmake: ../../../semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ../../../translator]0;Holmake: ../../../translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ../../../characteristic]0;Holmake: ../../../characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ../../../basis]0;Holmake: ../../../translator/monadic]0;Holmake: ../../../translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ../../../basis]0;Holmake: ../../../basis[1mWorking in $(CAKEMLDIR)/basis[0m
]0;Holmake: .]0;Holmake: ../..]0;Holmake: ../../backend]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/machine-code/multiword]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/machine-code/multiword[1mWorking in $(HOLDIR)/examples/machine-code/multiword[0m
]0;Holmake: ../../backend]0;Holmake: ../../backend/reg_alloc]0;Holmake: ../../../unverified/reg_alloc]0;Holmake: ../../../unverified/reg_alloc[1mWorking in $(CAKEMLDIR)/unverified/reg_alloc[0m
]0;Holmake: ../../backend/reg_alloc]0;Holmake: ../../backend/reg_alloc[1mWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc[0m
]0;Holmake: ../../backend]0;Holmake: ../../encoders/asm]0;Holmake: ../../encoders/asm[1mWorking in $(CAKEMLDIR)/compiler/encoders/asm[0m
]0;Holmake: ../../backend]0;Holmake: ../../backend[1mWorking in $(CAKEMLDIR)/compiler/backend[0m
]0;Holmake: ../..]0;Holmake: ../../backend/arm6]0;Holmake: ../../encoders/arm6]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/arm/step]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/machine-code/decompiler]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/machine-code/decompiler[1mWorking in $(HOLDIR)/examples/machine-code/decompiler[0m
]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code[1mWorking in $(HOLDIR)/examples/l3-machine-code[0m
]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/arm/step]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/arm/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/step[0m
]0;Holmake: ../../encoders/arm6]0;Holmake: ../../encoders/arm6[1mWorking in $(CAKEMLDIR)/compiler/encoders/arm6[0m
]0;Holmake: ../../backend/arm6]0;Holmake: ../../backend/arm6[1mWorking in $(CAKEMLDIR)/compiler/backend/arm6[0m
]0;Holmake: ../..]0;Holmake: ../../backend/arm8]0;Holmake: ../../encoders/arm8]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/arm8/step]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/arm8/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm8/step[0m
]0;Holmake: ../../encoders/arm8]0;Holmake: ../../encoders/arm8[1mWorking in $(CAKEMLDIR)/compiler/encoders/arm8[0m
]0;Holmake: ../../backend/arm8]0;Holmake: ../../backend/arm8[1mWorking in $(CAKEMLDIR)/compiler/backend/arm8[0m
]0;Holmake: ../..]0;Holmake: ../../backend/mips]0;Holmake: ../../encoders/mips]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/mips/step]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/mips/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/mips/step[0m
]0;Holmake: ../../encoders/mips]0;Holmake: ../../encoders/mips[1mWorking in $(CAKEMLDIR)/compiler/encoders/mips[0m
]0;Holmake: ../../backend/mips]0;Holmake: ../../backend/mips[1mWorking in $(CAKEMLDIR)/compiler/backend/mips[0m
]0;Holmake: ../..]0;Holmake: ../../backend/riscv]0;Holmake: ../../encoders/riscv]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/riscv/step]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/riscv/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/riscv/step[0m
]0;Holmake: ../../encoders/riscv]0;Holmake: ../../encoders/riscv[1mWorking in $(CAKEMLDIR)/compiler/encoders/riscv[0m
]0;Holmake: ../../backend/riscv]0;Holmake: ../../backend/riscv[1mWorking in $(CAKEMLDIR)/compiler/backend/riscv[0m
]0;Holmake: ../..]0;Holmake: ../../backend/x64]0;Holmake: ../../encoders/x64]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/x64/step]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/l3-machine-code/x64/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/x64/step[0m
]0;Holmake: ../../encoders/x64]0;Holmake: ../../encoders/x64[1mWorking in $(CAKEMLDIR)/compiler/encoders/x64[0m
]0;Holmake: ../../backend/x64]0;Holmake: ../../backend/x64[1mWorking in $(CAKEMLDIR)/compiler/backend/x64[0m
]0;Holmake: ../..]0;Holmake: ../../inference]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/unification/triangular/first-order]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/unification/triangular]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/unification/triangular[1mWorking in $(HOLDIR)/examples/unification/triangular[0m
]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/unification/triangular/first-order]0;Holmake: /scratch/cakeml/regression/HOL-98d718b2599e89f71200ee47e9077ea1cfaba444/examples/unification/triangular/first-order[1mWorking in $(HOLDIR)/examples/unification/triangular/first-order[0m
]0;Holmake: ../../inference]0;Holmake: ../../inference[1mWorking in $(CAKEMLDIR)/compiler/inference[0m
]0;Holmake: ../..]0;Holmake: ../..[1mWorking in $(CAKEMLDIR)/compiler[0m
]0;Holmake: .]0;Holmake: ../../backend/reg_alloc/proofs]0;Holmake: ../../backend/reg_alloc/proofs[1mWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
]0;Holmake: .]0;Holmake: ../../inference/proofs]0;Holmake: ../../inference/proofs[1mWorking in $(CAKEMLDIR)/compiler/inference/proofs[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/compiler/bootstrap/translation[0m
Starting work on heap
heap                                                                                                                                                      OK
Starting work on to_dataProgTheory
to_dataProgTheory                                                                                                                                         OK
Starting work on lexerProgTheory
lexerProgTheory                                                                                                                                           OK
Starting work on parserProgTheory
parserProgTheory                                                                                                                                          OK
Starting work on reg_allocProgTheory
reg_allocProgTheory                                                                                                                                       OK
Starting work on inferProgTheory
inferProgTheory                                                                                                                                           OK
Starting work on explorerProgTheory
explorerProgTheory                                                                                                                                        OK
Starting work on sexp_parserProgTheory
sexp_parserProgTheory                                                                                                                                     OK
Starting work on to_word32ProgTheory
Starting work on to_word64ProgTheory
to_word64ProgTheory                                                                                                                                       OK
Starting work on to_target64ProgTheory
to_word32ProgTheory                                                                                                                                       OK
Starting work on to_target32ProgTheory
to_target32ProgTheory                                                                                                                                     OK
Starting work on arm6ProgTheory
to_target64ProgTheory                                                                                                                                     OK
Starting work on x64ProgTheory
x64ProgTheory                                                                                                                                             OK
Starting work on arm8ProgTheory
arm6ProgTheory                                                                                                                                            OK
Starting work on compiler32ProgTheory
arm8ProgTheory                                                                                                                                            OK
Starting work on riscvProgTheory
riscvProgTheory                                                                                                                                           OK
Starting work on mipsProgTheory
mipsProgTheory                                                                                                                                            OK
Starting work on compiler64ProgTheory
compiler32ProgTheory                                                                                                                      FAILED! <Signal 9>
 Saved theorem _____ "nsLookup_auto_env_73"
 Saved theorem _____ "compiler_parse_stack_conf_v_thm"
 Translating compiler_parse_top_config
 Saved theorem _____ "nsLookup_auto_env_74"
 Saved theorem _____ "compiler_parse_top_config_v_thm"
 Translating arm6_config_arm6_names
 Saved theorem _____ "nsLookup_auto_env_75"
 Saved theorem _____ "arm6_config_arm6_names_v_thm"
 Translating export_arm6_ffi_asm
 Saved theorem _____ "nsLookup_auto_env_76"
compiler64ProgTheory                                                                                                                                M-KILLED