CakeML Regression Test

Job 112

CakeML:bfcbe761e28b4bf09d1ea1e7e03629fce6ad29d3
  Merge remote-tracking branch 'origin/master' into monad-infer [Dec 26 23:59:52]
#409 (monad-infer)
Merging into:37176c66e6292c8902944ddcb5608c5b58462b61
  Merge pull request #416 from CakeML/mlton_benchmarks [Dec 25 08:16:36]
HOL:17dce4e3a0065d55ecb638375ec7790674a33b73
  Prove more theorems about real_of_int connection [Dec 23 08:55:23]
Machine:cakeml1852 4.4.0-22-generic x86_64 GNU/Linux

Dec 27 10:15:43 Claimed job
Dec 27 10:15:52 Building HOL
Dec 27 10:28:52 Starting semantics/ffi
Dec 27 10:30:03 Finished semantics/ffi                                         1m09s 452MB
Dec 27 10:30:05 Starting semantics
Dec 27 10:32:52 Finished semantics                                             2m44s 874MB
Dec 27 10:32:54 Starting semantics/proofs
Dec 27 10:36:38 Finished semantics/proofs                                      3m41s   1GB
Dec 27 10:36:40 Starting basis/pure
Dec 27 10:42:54 Finished basis/pure                                            6m12s 709MB
Dec 27 10:42:56 Starting translator
Dec 27 10:50:11 Finished translator                                            7m13s   1GB
Dec 27 10:50:13 Starting compiler/parsing
Dec 27 10:52:41 Finished compiler/parsing                                      2m26s   2GB
Dec 27 10:52:43 Starting characteristic
Dec 27 10:57:26 Finished characteristic                                        4m40s   1GB
Dec 27 10:57:28 Starting basis
Dec 27 11:24:10 Finished basis                                                26m39s   2GB
Dec 27 11:24:12 Starting translator/monadic
Dec 27 11:27:40 Finished translator/monadic                                    3m25s   1GB
Dec 27 11:27:42 Starting compiler/inference
Dec 27 11:30:33 Finished compiler/inference                                    2m48s   1GB
Dec 27 11:30:35 Starting compiler/backend/reg_alloc
Dec 27 11:31:24 Finished compiler/backend/reg_alloc                              47s 879MB
Dec 27 11:31:26 Starting compiler/backend/gc
Dec 27 11:47:52 Finished compiler/backend/gc                                  16m24s   2GB
Dec 27 11:47:54 Starting compiler/backend
Dec 27 11:47:58 Finished compiler/backend                                         1s  15MB
Dec 27 11:48:00 Starting compiler/encoders/asm
Dec 27 11:48:02 Finished compiler/encoders/asm                                    0s  13MB
Dec 27 11:48:04 Starting compiler/encoders/x64
Dec 27 11:49:19 Finished compiler/encoders/x64                                 1m12s 433MB
Dec 27 11:49:20 Starting compiler/encoders/arm6
Dec 27 11:52:31 Finished compiler/encoders/arm6                                3m08s   1GB
Dec 27 11:52:33 Starting compiler/encoders/arm8
Dec 27 11:53:25 Finished compiler/encoders/arm8                                  50s 408MB
Dec 27 11:53:27 Starting compiler/encoders/mips
Dec 27 11:54:54 Finished compiler/encoders/mips                                1m24s 733MB
Dec 27 11:54:56 Starting compiler/encoders/riscv
Dec 27 11:56:29 Finished compiler/encoders/riscv                               1m31s 464MB
Dec 27 11:56:31 Starting compiler/backend/x64
Dec 27 11:57:12 Finished compiler/backend/x64                                    39s   1GB
Dec 27 11:57:14 Starting compiler/backend/arm6
Dec 27 11:58:00 Finished compiler/backend/arm6                                   44s   1GB
Dec 27 11:58:02 Starting compiler/backend/arm8
Dec 27 11:58:44 Finished compiler/backend/arm8                                   40s 936MB
Dec 27 11:58:46 Starting compiler/backend/mips
Dec 27 11:59:33 Finished compiler/backend/mips                                   44s   1GB
Dec 27 11:59:35 Starting compiler/backend/riscv
Dec 27 12:00:19 Finished compiler/backend/riscv                                  41s 852MB
Dec 27 12:00:21 Starting compiler/parsing/proofs
Dec 27 12:05:07 Finished compiler/parsing/proofs                               4m44s 601MB
Dec 27 12:05:09 Starting compiler/inference/proofs
Dec 27 12:09:33 Finished compiler/inference/proofs                             4m22s   1GB
Dec 27 12:09:35 Starting compiler/backend/semantics
Dec 27 12:28:52 Finished compiler/backend/semantics                           19m14s   3GB
Dec 27 12:28:54 Starting compiler/backend/reg_alloc/proofs
Dec 27 12:30:10 Finished compiler/backend/reg_alloc/proofs                     1m14s 401MB
Dec 27 12:30:12 Starting compiler/backend/proofs
Dec 27 13:41:24 Finished compiler/backend/proofs                            1h11m09s   6GB
Dec 27 13:41:26 Starting compiler/encoders/x64/proofs
Dec 27 13:52:59 Finished compiler/encoders/x64/proofs                         11m31s   1GB
Dec 27 13:53:01 Starting compiler/encoders/arm6/proofs
Dec 27 14:06:39 Finished compiler/encoders/arm6/proofs                        13m35s   2GB
Dec 27 14:06:41 Starting compiler/encoders/arm8/proofs
Dec 27 14:16:05 Finished compiler/encoders/arm8/proofs                         9m22s   1GB
Dec 27 14:16:07 Starting compiler/encoders/mips/proofs
Dec 27 14:29:05 Finished compiler/encoders/mips/proofs                        12m56s   3GB
Dec 27 14:29:07 Starting compiler/encoders/riscv/proofs
Dec 27 14:43:10 Finished compiler/encoders/riscv/proofs                       13m59s 934MB
Dec 27 14:43:12 Starting compiler/backend/x64/proofs
Dec 27 14:44:07 Finished compiler/backend/x64/proofs                             52s   1GB
Dec 27 14:44:09 Starting compiler/backend/arm6/proofs
Dec 27 14:45:10 Finished compiler/backend/arm6/proofs                            59s   1GB
Dec 27 14:45:12 Starting compiler/backend/arm8/proofs
Dec 27 14:46:06 Finished compiler/backend/arm8/proofs                            52s   1GB
Dec 27 14:46:08 Starting compiler/backend/mips/proofs
Dec 27 14:47:03 Finished compiler/backend/mips/proofs                            52s   1GB
Dec 27 14:47:05 Starting compiler/backend/riscv/proofs
Dec 27 14:48:00 Finished compiler/backend/riscv/proofs                           53s   1GB
Dec 27 14:48:02 Starting compiler/proofs
Dec 27 14:50:36 Finished compiler/proofs                                       2m31s   1GB
Dec 27 14:50:38 Starting candle/set-theory
Dec 27 14:52:24 Finished candle/set-theory                                     1m44s 543MB
Dec 27 14:52:26 Starting candle/syntax-lib
Dec 27 14:52:48 Finished candle/syntax-lib                                       19s 559MB
Dec 27 14:52:50 Starting candle/standard/syntax
Dec 27 14:55:52 Finished candle/standard/syntax                                3m00s 598MB
Dec 27 14:55:54 Starting candle/standard/semantics
Dec 27 14:58:24 Finished candle/standard/semantics                             2m28s 976MB
Dec 27 14:58:26 Starting candle/standard/monadic
Dec 27 15:01:12 Finished candle/standard/monadic                               2m44s   1GB
Dec 27 15:01:14 Starting candle/standard/ml_kernel
Dec 27 15:12:32 Finished candle/standard/ml_kernel                            11m16s   1GB
Dec 27 15:12:34 Starting candle/standard/opentheory
Dec 27 15:13:07 Finished candle/standard/opentheory                              31s 682MB
Dec 27 15:13:09 Starting characteristic/examples
Dec 27 15:15:26 Finished characteristic/examples                               2m15s   1GB
Dec 27 15:15:28 Starting tutorial/solutions
Dec 27 15:48:05 Finished tutorial/solutions                                   32m34s   9GB
Dec 27 15:48:07 Starting examples
Dec 27 15:55:48 Finished examples                                              7m38s   1GB
Dec 27 15:55:50 Starting examples/compilation
Dec 27 20:40:12 Finished examples/compilation                               4h44m18s  12GB
Dec 27 20:40:14 Starting examples/compilation/proofs
Dec 27 20:45:55 Finished examples/compilation/proofs                           5m39s   4GB
Dec 27 20:45:57 Starting compiler/benchmarks
Dec 27 20:45:59 Finished compiler/benchmarks                                      0s   4MB
Dec 27 20:46:01 Starting translator/okasaki-examples
Dec 27 20:53:29 Finished translator/okasaki-examples                           7m26s   1GB
Dec 27 20:53:31 Starting translator/other-examples
Dec 27 21:00:19 Finished translator/other-examples                             6m45s   1GB
Dec 27 21:00:21 Starting compiler/parsing/tests
Dec 27 21:01:01 Finished compiler/parsing/tests                                  38s 355MB
Dec 27 21:01:03 Starting compiler/bootstrap/translation
Dec 28 05:13:41 FAILED: compiler/bootstrap/translation
]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/formal-languages/context-freeFinished recursive invocation in /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/formal-languages/context-free
]0;Holmake: .Recursively calling Holmake in /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code/arm/model
]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code/arm/modelRecursively calling Holmake in /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code/common
]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code/commonRecursively calling Holmake in /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/machine-code/hoare-triple
]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/machine-code/hoare-tripleFinished recursive invocation in /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/machine-code/hoare-triple
]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code/common]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code/commonFinished recursive invocation in /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code/common
]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code/arm/modelRecursively calling Holmake in /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code/lib
]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code/lib]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code/libFinished recursive invocation in /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code/lib
]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code/arm/model]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code/arm/modelFinished recursive invocation in /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code/arm/model
]0;Holmake: .Recursively calling Holmake in /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code/arm8/model
]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code/arm8/model]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code/arm8/modelFinished recursive invocation in /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code/arm8/model
]0;Holmake: .Recursively calling Holmake in /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code/mips/model
]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code/mips/model]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code/mips/modelFinished recursive invocation in /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code/mips/model
]0;Holmake: .Recursively calling Holmake in /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code/riscv/model
]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code/riscv/model]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code/riscv/modelFinished recursive invocation in /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code/riscv/model
]0;Holmake: .Recursively calling Holmake in /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code/x64/model
]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code/x64/model]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code/x64/modelFinished recursive invocation in /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/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-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/formal-languages/regular
]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/balanced_bstFinished recursive invocation in /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/formal-languagesFinished recursive invocation in /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/formal-languages/regularFinished recursive invocation in /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/formal-languages/regular
]0;Holmake: ../../../basis/pureRecursively calling Holmake in ../../../misc
]0;Holmake: ../../../miscRecursively calling Holmake in /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/fun-op-sem/lprefix_lub
]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/fun-op-sem/lprefix_lubFinished recursive invocation in /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/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-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/machine-code/multiword
]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/machine-code/multiword]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/machine-code/multiwordFinished recursive invocation in /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/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-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code/arm/step
]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code/arm/stepRecursively calling Holmake in /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code
]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-codeRecursively calling Holmake in /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/machine-code/decompiler
]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/machine-code/decompiler]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/machine-code/decompilerFinished recursive invocation in /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/machine-code/decompiler
]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-codeFinished recursive invocation in /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code
]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code/arm/step]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code/arm/stepFinished recursive invocation in /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/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-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code/arm8/step
]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code/arm8/step]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code/arm8/stepFinished recursive invocation in /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/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-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code/mips/step
]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code/mips/step]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code/mips/stepFinished recursive invocation in /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/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-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code/riscv/step
]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code/riscv/step]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code/riscv/stepFinished recursive invocation in /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/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-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code/x64/step
]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code/x64/step]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/l3-machine-code/x64/stepFinished recursive invocation in /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/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-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/unification/triangular/first-order
]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/unification/triangular/first-orderRecursively calling Holmake in /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/unification/triangular
]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/unification/triangular]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/unification/triangularFinished recursive invocation in /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/unification/triangular
]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/unification/triangular/first-order]0;Holmake: /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/examples/unification/triangular/first-orderFinished recursive invocation in /scratch/cakeml/regression/HOL-17dce4e3a0065d55ecb638375ec7790674a33b73/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_word32ProgTheory                                                          OK
Starting work on to_target32ProgTheory
to_word64ProgTheory                                                          OK
Starting work on to_target64ProgTheory
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! <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