Job 187

CakeML:572020aeaeb5f7e86c094b072a99edce8bd052d7
  Revert unnecessary w82n conversion for file descriptors [Jan 25 15:06:30]
#443 (marshalling)
Merging into:87d0bbe35db4aa4a8ab36824e2ca9670966b6b9e
  Finish reverting change to inference error msgs [Jan 25 20:20:05]
HOL:8d28b9b85d195e3015b0a050b177021a86263f39
  changed wording waa -> vwaa [Jan 25 20:04:32]
Machine:cakeml1797 4.4.0-22-generic x86_64 GNU/Linux

Jan 26 08:11:21 Claimed job
Jan 26 08:11:29 Building HOL
Jan 26 08:23:30 Starting semantics/ffi
Jan 26 08:24:34 Finished semantics/ffi                                         1m02s 335MB
Jan 26 08:24:36 Starting semantics
Jan 26 08:27:06 Finished semantics                                             2m27s 900MB
Jan 26 08:27:08 Starting semantics/proofs
Jan 26 08:30:34 Finished semantics/proofs                                      3m24s   1GB
Jan 26 08:30:36 Starting basis/pure
Jan 26 08:36:44 Finished basis/pure                                            6m05s 661MB
Jan 26 08:36:46 Starting translator
Jan 26 08:44:06 Finished translator                                            7m18s 858MB
Jan 26 08:44:08 Starting compiler/parsing
Jan 26 08:46:38 Finished compiler/parsing                                      2m27s   2GB
Jan 26 08:46:39 Starting characteristic
Jan 26 08:51:31 Finished characteristic                                        4m50s   1GB
Jan 26 08:51:33 Starting basis
Jan 26 09:27:02 Finished basis                                                35m26s   2GB
Jan 26 09:27:04 Starting translator/monadic
Jan 26 09:27:07 Finished translator/monadic                                       1s  16MB
Jan 26 09:27:09 Starting compiler/inference
Jan 26 09:30:02 Finished compiler/inference                                    2m50s   1GB
Jan 26 09:30:04 Starting compiler/backend/reg_alloc
Jan 26 09:30:56 Finished compiler/backend/reg_alloc                              50s 839MB
Jan 26 09:30:58 Starting compiler/backend/gc
Jan 26 09:47:34 Finished compiler/backend/gc                                  16m34s   2GB
Jan 26 09:47:36 Starting compiler/backend
Jan 26 09:47:41 Finished compiler/backend                                         2s  22MB
Jan 26 09:47:43 Starting compiler/encoders/asm
Jan 26 09:47:45 Finished compiler/encoders/asm                                    0s  13MB
Jan 26 09:47:47 Starting compiler/encoders/x64
Jan 26 09:49:34 Finished compiler/encoders/x64                                 1m44s 447MB
Jan 26 09:49:36 Starting compiler/encoders/arm6
Jan 26 09:52:41 Finished compiler/encoders/arm6                                3m03s   1GB
Jan 26 09:52:43 Starting compiler/encoders/arm8
Jan 26 09:53:33 Finished compiler/encoders/arm8                                  47s 436MB
Jan 26 09:53:34 Starting compiler/encoders/mips
Jan 26 09:54:59 Finished compiler/encoders/mips                                1m22s 598MB
Jan 26 09:55:01 Starting compiler/encoders/riscv
Jan 26 09:56:35 Finished compiler/encoders/riscv                               1m31s 461MB
Jan 26 09:56:37 Starting compiler/backend/x64
Jan 26 09:57:23 Finished compiler/backend/x64                                    44s   1GB
Jan 26 09:57:25 Starting compiler/backend/arm6
Jan 26 09:58:12 Finished compiler/backend/arm6                                   44s   1GB
Jan 26 09:58:13 Starting compiler/backend/arm8
Jan 26 09:59:01 Finished compiler/backend/arm8                                   45s   1GB
Jan 26 09:59:03 Starting compiler/backend/mips
Jan 26 09:59:52 Finished compiler/backend/mips                                   46s   1GB
Jan 26 09:59:54 Starting compiler/backend/riscv
Jan 26 10:00:40 Finished compiler/backend/riscv                                  44s   1GB
Jan 26 10:00:42 Starting compiler/parsing/proofs
Jan 26 10:05:25 Finished compiler/parsing/proofs                               4m41s 787MB
Jan 26 10:05:27 Starting compiler/inference/proofs
Jan 26 10:09:54 Finished compiler/inference/proofs                             4m25s   1GB
Jan 26 10:09:56 Starting compiler/backend/semantics
Jan 26 10:29:53 Finished compiler/backend/semantics                           19m54s   2GB
Jan 26 10:29:55 Starting compiler/backend/reg_alloc/proofs
Jan 26 10:31:15 Finished compiler/backend/reg_alloc/proofs                     1m17s 511MB
Jan 26 10:31:17 Starting compiler/backend/proofs
Jan 26 11:44:05 Finished compiler/backend/proofs                            1h12m45s   5GB
Jan 26 11:44:07 Starting compiler/encoders/x64/proofs
Jan 26 11:58:04 Finished compiler/encoders/x64/proofs                         13m55s   2GB
Jan 26 11:58:06 Starting compiler/encoders/arm6/proofs
Jan 26 12:12:22 Finished compiler/encoders/arm6/proofs                        14m14s   2GB
Jan 26 12:12:24 Starting compiler/encoders/arm8/proofs
Jan 26 12:21:56 Finished compiler/encoders/arm8/proofs                         9m29s   1GB
Jan 26 12:21:58 Starting compiler/encoders/mips/proofs
Jan 26 12:35:04 Finished compiler/encoders/mips/proofs                        13m03s   1GB
Jan 26 12:35:06 Starting compiler/encoders/riscv/proofs
Jan 26 12:49:24 Finished compiler/encoders/riscv/proofs                       14m16s   1GB
Jan 26 12:49:26 Starting compiler/backend/x64/proofs
Jan 26 12:50:21 Finished compiler/backend/x64/proofs                             53s   1GB
Jan 26 12:50:23 Starting compiler/backend/arm6/proofs
Jan 26 12:51:23 Finished compiler/backend/arm6/proofs                            57s   1GB
Jan 26 12:51:25 Starting compiler/backend/arm8/proofs
Jan 26 12:52:20 Finished compiler/backend/arm8/proofs                            53s   1GB
Jan 26 12:52:22 Starting compiler/backend/mips/proofs
Jan 26 12:53:19 Finished compiler/backend/mips/proofs                            55s   1GB
Jan 26 12:53:21 Starting compiler/backend/riscv/proofs
Jan 26 12:54:19 Finished compiler/backend/riscv/proofs                           55s   1GB
Jan 26 12:54:21 Starting compiler/proofs
Jan 26 12:57:15 Finished compiler/proofs                                       2m52s   1GB
Jan 26 12:57:16 Starting candle/set-theory
Jan 26 12:59:01 Finished candle/set-theory                                     1m42s 553MB
Jan 26 12:59:03 Starting candle/syntax-lib
Jan 26 12:59:25 Finished candle/syntax-lib                                       20s 591MB
Jan 26 12:59:27 Starting candle/standard/syntax
Jan 26 13:02:28 Finished candle/standard/syntax                                2m59s 584MB
Jan 26 13:02:30 Starting candle/standard/semantics
Jan 26 13:04:57 Finished candle/standard/semantics                             2m24s 771MB
Jan 26 13:04:58 Starting candle/standard/monadic
Jan 26 13:07:46 Finished candle/standard/monadic                               2m45s 893MB
Jan 26 13:07:48 Starting candle/standard/ml_kernel
Jan 26 13:19:16 Finished candle/standard/ml_kernel                            11m25s   2GB
Jan 26 13:19:18 Starting candle/standard/opentheory
Jan 26 13:19:51 Finished candle/standard/opentheory                              31s 724MB
Jan 26 13:19:53 Starting characteristic/examples
Jan 26 13:22:37 Finished characteristic/examples                               2m41s   1GB
Jan 26 13:22:39 Starting tutorial/solutions
Jan 26 14:03:57 Finished tutorial/solutions                                   41m16s  10GB
Jan 26 14:03:59 Starting examples
Jan 26 14:13:12 Finished examples                                              9m11s   3GB
Jan 26 14:13:14 Starting examples/compilation
Jan 26 20:46:51 Finished examples/compilation                               6h33m34s  18GB
Jan 26 20:46:53 Starting examples/compilation/proofs
Jan 26 20:53:40 Finished examples/compilation/proofs                           6m44s   4GB
Jan 26 20:53:42 Starting compiler/benchmarks
Jan 26 20:53:44 Finished compiler/benchmarks                                      0s   6MB
Jan 26 20:53:46 Starting translator/okasaki-examples
Jan 26 21:01:28 Finished translator/okasaki-examples                           7m40s   1GB
Jan 26 21:01:30 Starting translator/other-examples
Jan 26 21:08:30 Finished translator/other-examples                             6m58s 877MB
Jan 26 21:08:32 Starting compiler/parsing/tests
Jan 26 21:09:14 Finished compiler/parsing/tests                                  39s 362MB
Jan 26 21:09:15 Starting compiler/bootstrap/translation
Jan 27 06:11:44 FAILED: compiler/bootstrap/translation
]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/formal-languages/context-freeFinished recursive invocation in /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/formal-languages/context-free
]0;Holmake: .Recursively calling Holmake in /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code/arm/model
]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code/arm/modelRecursively calling Holmake in /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code/common
]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code/commonRecursively calling Holmake in /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/machine-code/hoare-triple
]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/machine-code/hoare-tripleFinished recursive invocation in /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/machine-code/hoare-triple
]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code/common]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code/commonFinished recursive invocation in /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code/common
]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code/arm/modelRecursively calling Holmake in /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code/lib
]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code/lib]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code/libFinished recursive invocation in /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code/lib
]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code/arm/model]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code/arm/modelFinished recursive invocation in /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code/arm/model
]0;Holmake: .Recursively calling Holmake in /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code/arm8/model
]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code/arm8/model]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code/arm8/modelFinished recursive invocation in /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code/arm8/model
]0;Holmake: .Recursively calling Holmake in /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code/mips/model
]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code/mips/model]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code/mips/modelFinished recursive invocation in /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code/mips/model
]0;Holmake: .Recursively calling Holmake in /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code/riscv/model
]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code/riscv/model]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code/riscv/modelFinished recursive invocation in /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code/riscv/model
]0;Holmake: .Recursively calling Holmake in /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code/x64/model
]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code/x64/model]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code/x64/modelFinished recursive invocation in /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/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-8d28b9b85d195e3015b0a050b177021a86263f39/examples/formal-languages/regular
]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/balanced_bstFinished recursive invocation in /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/formal-languagesFinished recursive invocation in /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/formal-languages/regularFinished recursive invocation in /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/formal-languages/regular
]0;Holmake: ../../../basis/pureRecursively calling Holmake in ../../../misc
]0;Holmake: ../../../miscRecursively calling Holmake in /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/fun-op-sem/lprefix_lub
]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/fun-op-sem/lprefix_lubFinished recursive invocation in /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/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: ../../../basisRecursively calling Holmake in ../../../translator/monadic
]0;Holmake: ../../../translator/monadic]0;Holmake: ../../../translator/monadicFinished recursive invocation in ../../../translator/monadic
]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-8d28b9b85d195e3015b0a050b177021a86263f39/examples/machine-code/multiword
]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/machine-code/multiword]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/machine-code/multiwordFinished recursive invocation in /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/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-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code/arm/step
]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code/arm/stepRecursively calling Holmake in /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code
]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-codeRecursively calling Holmake in /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/machine-code/decompiler
]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/machine-code/decompiler]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/machine-code/decompilerFinished recursive invocation in /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/machine-code/decompiler
]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-codeFinished recursive invocation in /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code
]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code/arm/step]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code/arm/stepFinished recursive invocation in /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/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-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code/arm8/step
]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code/arm8/step]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code/arm8/stepFinished recursive invocation in /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/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-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code/mips/step
]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code/mips/step]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code/mips/stepFinished recursive invocation in /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/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-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code/riscv/step
]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code/riscv/step]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code/riscv/stepFinished recursive invocation in /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/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-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code/x64/step
]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code/x64/step]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/l3-machine-code/x64/stepFinished recursive invocation in /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/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-8d28b9b85d195e3015b0a050b177021a86263f39/examples/unification/triangular/first-order
]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/unification/triangular/first-orderRecursively calling Holmake in /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/unification/triangular
]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/unification/triangular]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/unification/triangularFinished recursive invocation in /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/unification/triangular
]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/unification/triangular/first-order]0;Holmake: /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/unification/triangular/first-orderFinished recursive invocation in /scratch/cakeml/regression/HOL-8d28b9b85d195e3015b0a050b177021a86263f39/examples/unification/triangular/first-order
]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>
 Proof of 
 
 app p main_v [Conv NONE []] (STDIO fs * COMMANDLINE cl)
   (POSTv uv.
           &UNIT_TYPE () uv *
           STDIO (full_compile_32 (TL cl) (get_stdin fs) fs) *
           COMMANDLINE cl)
 
 failed.
 Failed to prove theorem main_spec.
compiler64ProgTheory                                                   M-KILLED