Job 198

CakeML:badc95d1c211cfc09089fc6b12d277e4d8eaa5d4
  Fix more references to word_shift and shift definitions [Jan 30 23:25:45]
#449 (issue171)
Merging into:19c41e5bac090d86a4245e2b6054ef710c42a402
  Remove use of global grammar in encoders/asm/asmLib [Feb 02 12:00:22]
HOL:70896e58b479f639028d997c2b5056958fb5dae5
  Merge pull request #515 from simonjantsch/master [Feb 01 10:59:37]
Machine:cakeml1795 4.4.0-98-generic x86_64 GNU/Linux

Feb 02 19:55:22 Claimed job
Feb 02 19:55:33 Building HOL
Feb 02 20:07:59 Starting semantics/ffi
Feb 02 20:09:06 Finished semantics/ffi                                         1m04s 406MB
Feb 02 20:09:08 Starting semantics
Feb 02 20:11:45 Finished semantics                                             2m35s   1GB
Feb 02 20:11:47 Starting semantics/proofs
Feb 02 20:15:23 Finished semantics/proofs                                      3m34s 911MB
Feb 02 20:15:25 Starting basis/pure
Feb 02 20:21:38 Finished basis/pure                                            6m10s 744MB
Feb 02 20:21:40 Starting translator
Feb 02 20:28:53 Finished translator                                            7m10s 876MB
Feb 02 20:28:55 Starting compiler/parsing
Feb 02 20:31:32 Finished compiler/parsing                                      2m35s   1GB
Feb 02 20:31:34 Starting characteristic
Feb 02 20:36:19 Finished characteristic                                        4m42s   1GB
Feb 02 20:36:21 Starting basis
Feb 02 21:10:59 Finished basis                                                34m35s   2GB
Feb 02 21:11:01 Starting translator/monadic
Feb 02 21:11:04 Finished translator/monadic                                       1s  28MB
Feb 02 21:11:06 Starting compiler/inference
Feb 02 21:13:59 Finished compiler/inference                                    2m51s   1GB
Feb 02 21:14:01 Starting compiler/backend/reg_alloc
Feb 02 21:14:53 Finished compiler/backend/reg_alloc                              49s 896MB
Feb 02 21:14:55 Starting compiler/backend/gc
Feb 02 21:31:10 Finished compiler/backend/gc                                  16m13s   3GB
Feb 02 21:31:12 Starting compiler/backend
Feb 02 21:31:17 Finished compiler/backend                                         2s  16MB
Feb 02 21:31:19 Starting compiler/encoders/asm
Feb 02 21:31:21 Finished compiler/encoders/asm                                    0s  11MB
Feb 02 21:31:23 Starting compiler/encoders/x64
Feb 02 21:33:00 Finished compiler/encoders/x64                                 1m35s 443MB
Feb 02 21:33:02 Starting compiler/encoders/arm6
Feb 02 21:36:03 Finished compiler/encoders/arm6                                2m58s   1GB
Feb 02 21:36:05 Starting compiler/encoders/arm8
Feb 02 21:36:54 Finished compiler/encoders/arm8                                  47s 425MB
Feb 02 21:36:56 Starting compiler/encoders/mips
Feb 02 21:38:21 Finished compiler/encoders/mips                                1m23s 819MB
Feb 02 21:38:23 Starting compiler/encoders/riscv
Feb 02 21:39:56 Finished compiler/encoders/riscv                               1m31s 471MB
Feb 02 21:39:58 Starting compiler/backend/x64
Feb 02 21:40:44 Finished compiler/backend/x64                                    43s   1GB
Feb 02 21:40:46 Starting compiler/backend/arm6
Feb 02 21:41:29 Finished compiler/backend/arm6                                   41s   1GB
Feb 02 21:41:31 Starting compiler/backend/arm8
Feb 02 21:42:17 Finished compiler/backend/arm8                                   43s   1GB
Feb 02 21:42:19 Starting compiler/backend/mips
Feb 02 21:43:03 Finished compiler/backend/mips                                   41s 836MB
Feb 02 21:43:05 Starting compiler/backend/riscv
Feb 02 21:43:51 Finished compiler/backend/riscv                                  44s   1GB
Feb 02 21:43:53 Starting compiler/parsing/proofs
Feb 02 21:48:29 Finished compiler/parsing/proofs                               4m34s 966MB
Feb 02 21:48:31 Starting compiler/inference/proofs
Feb 02 21:52:50 Finished compiler/inference/proofs                             4m16s   1GB
Feb 02 21:52:52 Starting compiler/backend/semantics
Feb 02 22:12:09 Finished compiler/backend/semantics                           19m15s   4GB
Feb 02 22:12:11 Starting compiler/backend/reg_alloc/proofs
Feb 02 22:13:30 Finished compiler/backend/reg_alloc/proofs                     1m17s 531MB
Feb 02 22:13:32 Starting compiler/backend/proofs
Feb 02 23:21:24 Finished compiler/backend/proofs                            1h07m50s   4GB
Feb 02 23:21:26 Starting compiler/encoders/x64/proofs
Feb 02 23:34:51 Finished compiler/encoders/x64/proofs                         13m23s   2GB
Feb 02 23:34:53 Starting compiler/encoders/arm6/proofs
Feb 02 23:48:12 Finished compiler/encoders/arm6/proofs                        13m16s   3GB
Feb 02 23:48:13 Starting compiler/encoders/arm8/proofs
Feb 02 23:57:19 Finished compiler/encoders/arm8/proofs                         9m03s   1GB
Feb 02 23:57:21 Starting compiler/encoders/mips/proofs
Feb 03 00:09:58 Finished compiler/encoders/mips/proofs                        12m35s   2GB
Feb 03 00:10:00 Starting compiler/encoders/riscv/proofs
Feb 03 00:23:28 Finished compiler/encoders/riscv/proofs                       13m26s   1GB
Feb 03 00:23:30 Starting compiler/backend/x64/proofs
Feb 03 00:24:23 Finished compiler/backend/x64/proofs                             50s   1GB
Feb 03 00:24:25 Starting compiler/backend/arm6/proofs
Feb 03 00:25:27 Finished compiler/backend/arm6/proofs                            59s   1GB
Feb 03 00:25:29 Starting compiler/backend/arm8/proofs
Feb 03 00:26:20 Finished compiler/backend/arm8/proofs                            49s   1GB
Feb 03 00:26:22 Starting compiler/backend/mips/proofs
Feb 03 00:27:17 Finished compiler/backend/mips/proofs                            52s   1GB
Feb 03 00:27:18 Starting compiler/backend/riscv/proofs
Feb 03 00:28:11 Finished compiler/backend/riscv/proofs                           50s   1GB
Feb 03 00:28:13 Starting compiler/proofs
Feb 03 00:30:56 Finished compiler/proofs                                       2m40s   2GB
Feb 03 00:30:58 Starting candle/set-theory
Feb 03 00:32:35 Finished candle/set-theory                                     1m35s 610MB
Feb 03 00:32:37 Starting candle/syntax-lib
Feb 03 00:32:58 Finished candle/syntax-lib                                       19s 482MB
Feb 03 00:33:00 Starting candle/standard/syntax
Feb 03 00:35:52 Finished candle/standard/syntax                                2m50s 620MB
Feb 03 00:35:54 Starting candle/standard/semantics
Feb 03 00:38:17 Finished candle/standard/semantics                             2m20s 672MB
Feb 03 00:38:19 Starting candle/standard/monadic
Feb 03 00:40:59 Finished candle/standard/monadic                               2m38s 792MB
Feb 03 00:41:01 Starting candle/standard/ml_kernel
Feb 03 00:51:39 Finished candle/standard/ml_kernel                            10m35s   1GB
Feb 03 00:51:41 Starting candle/standard/opentheory
Feb 03 00:52:11 Finished candle/standard/opentheory                              28s 876MB
Feb 03 00:52:13 Starting characteristic/examples
Feb 03 00:54:47 Finished characteristic/examples                               2m31s   1GB
Feb 03 00:54:49 Starting tutorial/solutions
Feb 03 01:32:51 Finished tutorial/solutions                                   38m00s   9GB
Feb 03 01:32:53 Starting examples
Feb 03 01:41:34 Finished examples                                              8m38s   3GB
Feb 03 01:41:35 Starting examples/compilation
Feb 03 07:45:53 Finished examples/compilation                               6h04m15s  19GB
Feb 03 07:45:55 Starting examples/compilation/proofs
Feb 03 07:52:21 Finished examples/compilation/proofs                           6m23s   5GB
Feb 03 07:52:23 Starting compiler/benchmarks
Feb 03 07:52:25 Finished compiler/benchmarks                                      0s   6MB
Feb 03 07:52:27 Starting translator/okasaki-examples
Feb 03 07:59:39 Finished translator/okasaki-examples                           7m10s   1GB
Feb 03 07:59:41 Starting translator/other-examples
Feb 03 08:06:22 Finished translator/other-examples                             6m39s   1GB
Feb 03 08:06:24 Starting compiler/parsing/tests
Feb 03 08:07:05 Finished compiler/parsing/tests                                  39s 373MB
Feb 03 08:07:07 Starting compiler/bootstrap/translation
Feb 03 16:47:47 FAILED: compiler/bootstrap/translation
]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/formal-languages/context-free]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/formal-languages/context-freeFinished recursive invocation in /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/formal-languages/context-free
]0;Holmake: .Recursively calling Holmake in /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code/arm/model
]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code/arm/modelRecursively calling Holmake in /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code/common
]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code/commonRecursively calling Holmake in /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/machine-code/hoare-triple
]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/machine-code/hoare-tripleFinished recursive invocation in /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/machine-code/hoare-triple
]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code/common]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code/commonFinished recursive invocation in /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code/common
]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code/arm/modelRecursively calling Holmake in /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code/lib
]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code/lib]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code/libFinished recursive invocation in /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code/lib
]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code/arm/model]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code/arm/modelFinished recursive invocation in /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code/arm/model
]0;Holmake: .Recursively calling Holmake in /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code/arm8/model
]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code/arm8/model]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code/arm8/modelFinished recursive invocation in /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code/arm8/model
]0;Holmake: .Recursively calling Holmake in /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code/mips/model
]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code/mips/model]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code/mips/modelFinished recursive invocation in /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code/mips/model
]0;Holmake: .Recursively calling Holmake in /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code/riscv/model
]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code/riscv/model]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code/riscv/modelFinished recursive invocation in /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code/riscv/model
]0;Holmake: .Recursively calling Holmake in /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code/x64/model
]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code/x64/model]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code/x64/modelFinished recursive invocation in /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/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-70896e58b479f639028d997c2b5056958fb5dae5/examples/formal-languages/regular
]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/balanced_bstFinished recursive invocation in /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/formal-languages/regularRecursively calling Holmake in /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/formal-languagesFinished recursive invocation in /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/formal-languages/regularFinished recursive invocation in /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/formal-languages/regular
]0;Holmake: ../../../basis/pureRecursively calling Holmake in ../../../misc
]0;Holmake: ../../../miscRecursively calling Holmake in /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/fun-op-sem/lprefix_lub
]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/fun-op-sem/lprefix_lubFinished recursive invocation in /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/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-70896e58b479f639028d997c2b5056958fb5dae5/examples/machine-code/multiword
]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/machine-code/multiword]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/machine-code/multiwordFinished recursive invocation in /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/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-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code/arm/step
]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code/arm/stepRecursively calling Holmake in /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code
]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-codeRecursively calling Holmake in /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/machine-code/decompiler
]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/machine-code/decompiler]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/machine-code/decompilerFinished recursive invocation in /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/machine-code/decompiler
]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-codeFinished recursive invocation in /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code
]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code/arm/step]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code/arm/stepFinished recursive invocation in /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/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-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code/arm8/step
]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code/arm8/step]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code/arm8/stepFinished recursive invocation in /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/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-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code/mips/step
]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code/mips/step]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code/mips/stepFinished recursive invocation in /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/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-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code/riscv/step
]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code/riscv/step]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code/riscv/stepFinished recursive invocation in /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/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-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code/x64/step
]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code/x64/step]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/l3-machine-code/x64/stepFinished recursive invocation in /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/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-70896e58b479f639028d997c2b5056958fb5dae5/examples/unification/triangular/first-order
]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/unification/triangular/first-orderRecursively calling Holmake in /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/unification/triangular
]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/unification/triangular]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/unification/triangularFinished recursive invocation in /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/unification/triangular
]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/unification/triangular/first-order]0;Holmake: /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/examples/unification/triangular/first-orderFinished recursive invocation in /scratch/cakeml/regression/HOL-70896e58b479f639028d997c2b5056958fb5dae5/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! <Signal 9>
        STDIO (fastForwardFD fs 0) * COMMANDLINE cl *
        &PAIR_TYPE (MISC_APP_LIST_TYPE STRING_TYPE) STRING_TYPE
           (compile_32 (TL cl) (DROP p_2 inp)) v'
 Using CF specification print_app_list_spec from theory basisProg
 xlet_auto : using heuristics
 Post condition: POSTv uv1.
        STDIO (add_stdout (fastForwardFD fs 0) (concat (append out))) *
        COMMANDLINE cl * &UNIT_TYPE () uv1
 Saved theorem _____ "main_spec"
 Saved theorem _____ "main_whole_prog_spec"
compiler64ProgTheory                                                   M-KILLED