Overview

Job 118

CakeML:bfcbe761e28b4bf09d1ea1e7e03629fce6ad29d3
  Merge remote-tracking branch 'origin/master' into monad-infer
#409 (monad-infer)
Merging into:4db3cb046e194849b4a45828ef7119c6996b110b
  Remove e_rm_reg_def following HOL (04d2447)
HOL:04d2447ff0be8df9be7b13aa97f422fe9fee5809
  Add some SSE (streaming SIMD extensions) instructions to the x86-64 m
Machine:cakeml1853 4.4.0-22-generic x86_64 GNU/Linux

 Claimed job
 Reusing HOL
 Starting semantics/ffi
 Finished semantics/ffi                                           18s 217MB
 Starting semantics
 Finished semantics                                             2m08s 994MB
 Starting semantics/proofs
 Finished semantics/proofs                                      3m26s   1GB
 Starting basis/pure
 Finished basis/pure                                            1m06s 580MB
 Starting translator
 Finished translator                                            7m06s 909MB
 Starting compiler/parsing
 Finished compiler/parsing                                      2m22s   2GB
 Starting characteristic
 Finished characteristic                                        4m41s   1GB
 Starting basis
 Finished basis                                                26m44s   2GB
 Starting translator/monadic
 Finished translator/monadic                                    3m29s   1GB
 Starting compiler/inference
 Finished compiler/inference                                    2m18s   1GB
 Starting compiler/backend/reg_alloc
 Finished compiler/backend/reg_alloc                              47s 679MB
 Starting compiler/backend/gc
 Finished compiler/backend/gc                                  14m22s   3GB
 Starting compiler/backend
 Finished compiler/backend                                         1s  22MB
 Starting compiler/encoders/asm
 Finished compiler/encoders/asm                                    0s  16MB
 Starting compiler/encoders/x64
 Finished compiler/encoders/x64                                   25s 492MB
 Starting compiler/encoders/arm6
 Finished compiler/encoders/arm6                                3m03s   1GB
 Starting compiler/encoders/arm8
 Finished compiler/encoders/arm8                                  44s 514MB
 Starting compiler/encoders/mips
 Finished compiler/encoders/mips                                1m27s 618MB
 Starting compiler/encoders/riscv
 Finished compiler/encoders/riscv                               1m36s 423MB
 Starting compiler/backend/x64
 Finished compiler/backend/x64                                    41s   1GB
 Starting compiler/backend/arm6
 Finished compiler/backend/arm6                                   45s   1GB
 Starting compiler/backend/arm8
 Finished compiler/backend/arm8                                   42s   1GB
 Starting compiler/backend/mips
 Finished compiler/backend/mips                                   44s   1GB
 Starting compiler/backend/riscv
 Finished compiler/backend/riscv                                  44s   1GB
 Starting compiler/parsing/proofs
 Finished compiler/parsing/proofs                               4m45s   1GB
 Starting compiler/inference/proofs
 Finished compiler/inference/proofs                             4m15s   1GB
 Starting compiler/backend/semantics
 Finished compiler/backend/semantics                           18m55s   4GB
 Starting compiler/backend/reg_alloc/proofs
 Finished compiler/backend/reg_alloc/proofs                     1m13s 433MB
 Starting compiler/backend/proofs
 Finished compiler/backend/proofs                            1h10m37s   7GB
 Starting compiler/encoders/x64/proofs
 Finished compiler/encoders/x64/proofs                         12m25s   1GB
 Starting compiler/encoders/arm6/proofs
 Finished compiler/encoders/arm6/proofs                        13m32s   2GB
 Starting compiler/encoders/arm8/proofs
 Finished compiler/encoders/arm8/proofs                         9m08s   1GB
 Starting compiler/encoders/mips/proofs
 Finished compiler/encoders/mips/proofs                        13m03s   2GB
 Starting compiler/encoders/riscv/proofs
 Finished compiler/encoders/riscv/proofs                       13m50s 835MB
 Starting compiler/backend/x64/proofs
 Finished compiler/backend/x64/proofs                             51s   1GB
 Starting compiler/backend/arm6/proofs
 Finished compiler/backend/arm6/proofs                            57s   1GB
 Starting compiler/backend/arm8/proofs
 Finished compiler/backend/arm8/proofs                            50s   1GB
 Starting compiler/backend/mips/proofs
 Finished compiler/backend/mips/proofs                            53s   1GB
 Starting compiler/backend/riscv/proofs
 Finished compiler/backend/riscv/proofs                           51s   1GB
 Starting compiler/proofs
 Finished compiler/proofs                                       2m32s   1GB
 Starting candle/set-theory
 Finished candle/set-theory                                     1m39s 595MB
 Starting candle/syntax-lib
 Finished candle/syntax-lib                                       19s 563MB
 Starting candle/standard/syntax
 Finished candle/standard/syntax                                2m54s 547MB
 Starting candle/standard/semantics
 Finished candle/standard/semantics                             2m20s 818MB
 Starting candle/standard/monadic
 Finished candle/standard/monadic                               2m40s 951MB
 Starting candle/standard/ml_kernel
 Finished candle/standard/ml_kernel                            11m04s   1GB
 Starting candle/standard/opentheory
 Finished candle/standard/opentheory                              29s 673MB
 Starting characteristic/examples
 Finished characteristic/examples                               2m13s   1GB
 Starting tutorial/solutions
 Finished tutorial/solutions                                   33m11s  13GB
 Starting examples
 Finished examples                                              7m37s   2GB
 Starting examples/compilation
 Finished examples/compilation                               4h38m22s  24GB
 Starting examples/compilation/proofs
 Finished examples/compilation/proofs                           5m30s   4GB
 Starting compiler/benchmarks
 Finished compiler/benchmarks                                      0s   4MB
 Starting translator/okasaki-examples
 Finished translator/okasaki-examples                           7m21s   1GB
 Starting translator/other-examples
 Finished translator/other-examples                             6m45s   1GB
 Starting compiler/parsing/tests
 Finished compiler/parsing/tests                                  38s 343MB
 Starting compiler/bootstrap/translation
 FAILED: compiler/bootstrap/translation
]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/formal-languages/context-freeFinished recursive invocation in /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/formal-languages/context-free
]0;Holmake: .Recursively calling Holmake in /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/arm/model
]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/arm/modelRecursively calling Holmake in /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/common
]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/commonRecursively calling Holmake in /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/machine-code/hoare-triple
]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/machine-code/hoare-tripleFinished recursive invocation in /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/machine-code/hoare-triple
]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/common]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/commonFinished recursive invocation in /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/common
]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/arm/modelRecursively calling Holmake in /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/lib
]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/lib]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/libFinished recursive invocation in /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/lib
]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/arm/model]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/arm/modelFinished recursive invocation in /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/arm/model
]0;Holmake: .Recursively calling Holmake in /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/arm8/model
]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/arm8/model]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/arm8/modelFinished recursive invocation in /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/arm8/model
]0;Holmake: .Recursively calling Holmake in /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/mips/model
]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/mips/model]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/mips/modelFinished recursive invocation in /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/mips/model
]0;Holmake: .Recursively calling Holmake in /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/riscv/model
]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/riscv/model]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/riscv/modelFinished recursive invocation in /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/riscv/model
]0;Holmake: .Recursively calling Holmake in /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/x64/model
]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/x64/model]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/x64/modelFinished recursive invocation in /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/x64/model
]0;Holmake: .Recursively calling Holmake in ../../../basis
]0;Holmake: ../../../basisRecursively calling Holmake in ../../../basis/pure
]0;Holmake: ../../../basis/pureRecursively calling Holmake in /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/formal-languages/regular
]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/balanced_bstFinished recursive invocation in /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/formal-languagesFinished recursive invocation in /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/formal-languages/regularFinished recursive invocation in /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/formal-languages/regular
]0;Holmake: ../../../basis/pureRecursively calling Holmake in ../../../misc
]0;Holmake: ../../../miscRecursively calling Holmake in /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/fun-op-sem/lprefix_lub
]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/fun-op-sem/lprefix_lubFinished recursive invocation in /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../../../miscRecursively calling Holmake in ../../../developers
]0;Holmake: ../../../developers]0;Holmake: ../../../developersFinished recursive invocation in ../../../developers
]0;Holmake: ../../../miscRecursively calling Holmake in ../../../misc/lem_lib_stub
]0;Holmake: ../../../misc/lem_lib_stub]0;Holmake: ../../../misc/lem_lib_stubFinished recursive invocation in ../../../misc/lem_lib_stub
]0;Holmake: ../../../misc]0;Holmake: ../../../miscFinished recursive invocation in ../../../misc
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../basis/pureFinished recursive invocation in ../../../basis/pure
]0;Holmake: ../../../basisRecursively calling Holmake in ../../../characteristic
]0;Holmake: ../../../characteristicRecursively calling Holmake in ../../../compiler/parsing
]0;Holmake: ../../../compiler/parsingRecursively calling Holmake in ../../../semantics
]0;Holmake: ../../../semanticsRecursively calling Holmake in ../../../semantics/ffi
]0;Holmake: ../../../semantics/ffi]0;Holmake: ../../../semantics/ffiFinished recursive invocation in ../../../semantics/ffi
]0;Holmake: ../../../semantics]0;Holmake: ../../../semanticsFinished recursive invocation in ../../../semantics
]0;Holmake: ../../../compiler/parsing]0;Holmake: ../../../compiler/parsingFinished recursive invocation in ../../../compiler/parsing
]0;Holmake: ../../../characteristicRecursively calling Holmake in ../../../semantics/alt_semantics/proofs
]0;Holmake: ../../../semantics/alt_semantics/proofsRecursively calling Holmake in ../../../semantics/alt_semantics
]0;Holmake: ../../../semantics/alt_semantics]0;Holmake: ../../../semantics/alt_semanticsFinished recursive invocation in ../../../semantics/alt_semantics
]0;Holmake: ../../../semantics/alt_semantics/proofsRecursively calling Holmake in ../../../semantics/proofs
]0;Holmake: ../../../semantics/proofs]0;Holmake: ../../../semantics/proofsFinished recursive invocation in ../../../semantics/proofs
]0;Holmake: ../../../semantics/alt_semantics/proofs]0;Holmake: ../../../semantics/alt_semantics/proofsFinished recursive invocation in ../../../semantics/alt_semantics/proofs
]0;Holmake: ../../../characteristicRecursively calling Holmake in ../../../translator
]0;Holmake: ../../../translator]0;Holmake: ../../../translatorFinished recursive invocation in ../../../translator
]0;Holmake: ../../../characteristic]0;Holmake: ../../../characteristicFinished recursive invocation in ../../../characteristic
]0;Holmake: ../../../basis]0;Holmake: ../../../basisFinished recursive invocation in ../../../basis
]0;Holmake: .Recursively calling Holmake in ../..
]0;Holmake: ../..Recursively calling Holmake in ../../backend
]0;Holmake: ../../backendRecursively calling Holmake in /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/machine-code/multiword
]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/machine-code/multiword]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/machine-code/multiwordFinished recursive invocation in /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/machine-code/multiword
]0;Holmake: ../../backendRecursively calling Holmake in ../../backend/reg_alloc
]0;Holmake: ../../backend/reg_allocRecursively calling Holmake in ../../../unverified/reg_alloc
]0;Holmake: ../../../unverified/reg_alloc]0;Holmake: ../../../unverified/reg_allocFinished recursive invocation in ../../../unverified/reg_alloc
]0;Holmake: ../../backend/reg_alloc]0;Holmake: ../../backend/reg_allocFinished recursive invocation in ../../backend/reg_alloc
]0;Holmake: ../../backendRecursively calling Holmake in ../../encoders
]0;Holmake: ../../encoders]0;Holmake: ../../encodersFinished recursive invocation in ../../encoders
]0;Holmake: ../../backendRecursively calling Holmake in ../../encoders/asm
]0;Holmake: ../../encoders/asm]0;Holmake: ../../encoders/asmFinished recursive invocation in ../../encoders/asm
]0;Holmake: ../../backend]0;Holmake: ../../backendFinished recursive invocation in ../../backend
]0;Holmake: ../..Recursively calling Holmake in ../../backend/arm6
]0;Holmake: ../../backend/arm6Recursively calling Holmake in ../../encoders/arm6
]0;Holmake: ../../encoders/arm6Recursively calling Holmake in /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/arm/step
]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/arm/stepRecursively calling Holmake in /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code
]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-codeRecursively calling Holmake in /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/machine-code/decompiler
]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/machine-code/decompiler]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/machine-code/decompilerFinished recursive invocation in /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/machine-code/decompiler
]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-codeFinished recursive invocation in /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code
]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/arm/step]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/arm/stepFinished recursive invocation in /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/arm/step
]0;Holmake: ../../encoders/arm6]0;Holmake: ../../encoders/arm6Finished recursive invocation in ../../encoders/arm6
]0;Holmake: ../../backend/arm6]0;Holmake: ../../backend/arm6Finished recursive invocation in ../../backend/arm6
]0;Holmake: ../..Recursively calling Holmake in ../../backend/arm8
]0;Holmake: ../../backend/arm8Recursively calling Holmake in ../../encoders/arm8
]0;Holmake: ../../encoders/arm8Recursively calling Holmake in /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/arm8/step
]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/arm8/step]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/arm8/stepFinished recursive invocation in /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/arm8/step
]0;Holmake: ../../encoders/arm8]0;Holmake: ../../encoders/arm8Finished recursive invocation in ../../encoders/arm8
]0;Holmake: ../../backend/arm8]0;Holmake: ../../backend/arm8Finished recursive invocation in ../../backend/arm8
]0;Holmake: ../..Recursively calling Holmake in ../../backend/mips
]0;Holmake: ../../backend/mipsRecursively calling Holmake in ../../encoders/mips
]0;Holmake: ../../encoders/mipsRecursively calling Holmake in /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/mips/step
]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/mips/step]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/mips/stepFinished recursive invocation in /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/mips/step
]0;Holmake: ../../encoders/mips]0;Holmake: ../../encoders/mipsFinished recursive invocation in ../../encoders/mips
]0;Holmake: ../../backend/mips]0;Holmake: ../../backend/mipsFinished recursive invocation in ../../backend/mips
]0;Holmake: ../..Recursively calling Holmake in ../../backend/riscv
]0;Holmake: ../../backend/riscvRecursively calling Holmake in ../../encoders/riscv
]0;Holmake: ../../encoders/riscvRecursively calling Holmake in /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/riscv/step
]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/riscv/step]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/riscv/stepFinished recursive invocation in /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/riscv/step
]0;Holmake: ../../encoders/riscv]0;Holmake: ../../encoders/riscvFinished recursive invocation in ../../encoders/riscv
]0;Holmake: ../../backend/riscv]0;Holmake: ../../backend/riscvFinished recursive invocation in ../../backend/riscv
]0;Holmake: ../..Recursively calling Holmake in ../../backend/x64
]0;Holmake: ../../backend/x64Recursively calling Holmake in ../../encoders/x64
]0;Holmake: ../../encoders/x64Recursively calling Holmake in /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/x64/step
]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/x64/step]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/x64/stepFinished recursive invocation in /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/l3-machine-code/x64/step
]0;Holmake: ../../encoders/x64]0;Holmake: ../../encoders/x64Finished recursive invocation in ../../encoders/x64
]0;Holmake: ../../backend/x64]0;Holmake: ../../backend/x64Finished recursive invocation in ../../backend/x64
]0;Holmake: ../..Recursively calling Holmake in ../../inference
]0;Holmake: ../../inferenceRecursively calling Holmake in /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/unification/triangular/first-order
]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/unification/triangular/first-orderRecursively calling Holmake in /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/unification/triangular
]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/unification/triangular]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/unification/triangularFinished recursive invocation in /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/unification/triangular
]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/unification/triangular/first-order]0;Holmake: /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/unification/triangular/first-orderFinished recursive invocation in /scratch/cakeml/regression/HOL-04d2447ff0be8df9be7b13aa97f422fe9fee5809/examples/unification/triangular/first-order
]0;Holmake: ../../inferenceRecursively calling Holmake in ../../../translator/monadic
]0;Holmake: ../../../translator/monadic]0;Holmake: ../../../translator/monadicFinished recursive invocation in ../../../translator/monadic
]0;Holmake: ../../inference]0;Holmake: ../../inferenceFinished recursive invocation in ../../inference
]0;Holmake: ../..]0;Holmake: ../..Finished recursive invocation in ../..
]0;Holmake: .Recursively calling Holmake in ../../backend/reg_alloc/proofs
]0;Holmake: ../../backend/reg_alloc/proofs]0;Holmake: ../../backend/reg_alloc/proofsFinished recursive invocation in ../../backend/reg_alloc/proofs
]0;Holmake: .Recursively calling Holmake in ../../inference/proofs
]0;Holmake: ../../inference/proofs]0;Holmake: ../../inference/proofsFinished recursive invocation in ../../inference/proofs
]0;Holmake: .]0;Holmake: .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 inferProgTheory
inferProgTheory                                                              OK
Starting work on reg_allocProgTheory
reg_allocProgTheory                                                          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_target64ProgTheory                                                        OK
Starting work on x64ProgTheory
to_target32ProgTheory                                                        OK
Starting work on arm6ProgTheory
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! <1>
      &UNIT_TYPE () uv *
      (let
         (out,err,b) = full_compile_32 (TL cl) (get_stdin fs) ;
         fs' = if b then fastForwardFD fs 0 else fs
       in
         STDIO (add_stderr (add_stdout fs' (concat (append out))) err)) *
      COMMANDLINE cl)
 
 failed.
 Failed to prove theorem main_spec.
compiler64ProgTheory                                                   M-KILLED