Job 363

CakeML:bacdfd84c86ee6dd48ef9740a9cc3e5246e3ac48
  Use symbolic names for word shift funs [Jul 12 04:31:41]
#498 (basis-word-ops)
Merging into:ec623912b1a55939bceccd7ad699b2bc29780c08
  Fix stack_to_labProof: shadowed binding [Jul 12 23:31:29]
HOL:4b35dc7ed787300dd46581edc75094d74e067924
  Document mp_then [Jul 13 14:16:44]
Machine:cakeml1797 4.4.0-22-generic x86_64 GNU/Linux

Jul 14 15:31:18 Claimed job
Jul 14 15:31:28 Building HOL
Jul 14 15:43:57 Starting developers/bin
Jul 14 15:44:08 Finished developers/bin                                           8s 224MB
Jul 14 15:44:10 Starting semantics/ffi
Jul 14 15:45:14 Finished semantics/ffi                                         1m02s 405MB
Jul 14 15:45:16 Starting semantics
Jul 14 15:47:41 Finished semantics                                             2m23s   1GB
Jul 14 15:47:43 Starting semantics/proofs
Jul 14 15:51:01 Finished semantics/proofs                                      3m15s   1GB
Jul 14 15:51:03 Starting basis/pure
Jul 14 15:56:50 Finished basis/pure                                            5m45s 781MB
Jul 14 15:56:52 Starting translator
Jul 14 16:03:32 Finished translator                                            6m37s   1GB
Jul 14 16:03:34 Starting compiler/parsing
Jul 14 16:05:43 Finished compiler/parsing                                      2m06s   2GB
Jul 14 16:05:45 Starting characteristic
Jul 14 16:10:06 Finished characteristic                                        4m19s   1GB
Jul 14 16:10:08 Starting basis
Jul 14 16:38:46 Finished basis                                                28m36s   2GB
Jul 14 16:38:48 Starting translator/monadic
Jul 14 16:38:52 Finished translator/monadic                                       2s  14MB
Jul 14 16:38:54 Starting compiler/inference
Jul 14 16:41:35 Finished compiler/inference                                    2m38s   1GB
Jul 14 16:41:37 Starting compiler/backend/reg_alloc
Jul 14 16:42:34 Finished compiler/backend/reg_alloc                              54s   1GB
Jul 14 16:42:36 Starting compiler/backend/gc
Jul 14 16:57:26 Finished compiler/backend/gc                                  14m48s   3GB
Jul 14 16:57:28 Starting compiler/backend
Jul 14 16:57:34 Finished compiler/backend                                         3s  14MB
Jul 14 16:57:36 Starting compiler/encoders/asm
Jul 14 16:57:39 Finished compiler/encoders/asm                                    0s  22MB
Jul 14 16:57:40 Starting compiler/encoders/x64
Jul 14 16:59:09 Finished compiler/encoders/x64                                 1m26s 606MB
Jul 14 16:59:11 Starting compiler/encoders/arm6
Jul 14 17:02:10 Finished compiler/encoders/arm6                                2m56s   1GB
Jul 14 17:02:12 Starting compiler/encoders/arm8
Jul 14 17:02:56 Finished compiler/encoders/arm8                                  42s 392MB
Jul 14 17:02:58 Starting compiler/encoders/mips
Jul 14 17:04:35 Finished compiler/encoders/mips                                1m34s 669MB
Jul 14 17:04:37 Starting compiler/encoders/riscv
Jul 14 17:06:10 Finished compiler/encoders/riscv                               1m31s 486MB
Jul 14 17:06:12 Starting compiler/backend/x64
Jul 14 17:06:46 Finished compiler/backend/x64                                    32s   1GB
Jul 14 17:06:48 Starting compiler/backend/arm6
Jul 14 17:07:25 Finished compiler/backend/arm6                                   35s   1GB
Jul 14 17:07:27 Starting compiler/backend/arm8
Jul 14 17:08:00 Finished compiler/backend/arm8                                   30s 875MB
Jul 14 17:08:02 Starting compiler/backend/mips
Jul 14 17:08:37 Finished compiler/backend/mips                                   32s 878MB
Jul 14 17:08:39 Starting compiler/backend/riscv
Jul 14 17:09:14 Finished compiler/backend/riscv                                  32s   1GB
Jul 14 17:09:16 Starting compiler/parsing/proofs
Jul 14 17:13:16 Finished compiler/parsing/proofs                               3m58s 780MB
Jul 14 17:13:18 Starting compiler/inference/proofs
Jul 14 17:17:18 Finished compiler/inference/proofs                             3m57s   1GB
Jul 14 17:17:20 Starting compiler/backend/semantics
Jul 14 17:31:23 Finished compiler/backend/semantics                           14m01s   2GB
Jul 14 17:31:25 Starting compiler/backend/reg_alloc/proofs
Jul 14 17:32:50 Finished compiler/backend/reg_alloc/proofs                     1m23s 383MB
Jul 14 17:32:52 Starting compiler/backend/proofs
Jul 14 18:28:28 Finished compiler/backend/proofs                              55m33s   5GB
Jul 14 18:28:30 Starting compiler/encoders/x64/proofs
Jul 14 18:39:58 Finished compiler/encoders/x64/proofs                         11m25s   1GB
Jul 14 18:40:00 Starting compiler/encoders/arm6/proofs
Jul 14 18:51:47 Finished compiler/encoders/arm6/proofs                        11m44s   3GB
Jul 14 18:51:49 Starting compiler/encoders/arm8/proofs
Jul 14 19:00:06 Finished compiler/encoders/arm8/proofs                         8m15s   1GB
Jul 14 19:00:08 Starting compiler/encoders/mips/proofs
Jul 14 19:11:43 Finished compiler/encoders/mips/proofs                        11m32s   1GB
Jul 14 19:11:45 Starting compiler/encoders/riscv/proofs
Jul 14 19:24:12 Finished compiler/encoders/riscv/proofs                       12m24s   1GB
Jul 14 19:24:14 Starting compiler/backend/x64/proofs
Jul 14 19:24:51 Finished compiler/backend/x64/proofs                             35s   1GB
Jul 14 19:24:53 Starting compiler/backend/arm6/proofs
Jul 14 19:25:34 Finished compiler/backend/arm6/proofs                            38s   1GB
Jul 14 19:25:36 Starting compiler/backend/arm8/proofs
Jul 14 19:26:13 Finished compiler/backend/arm8/proofs                            35s   1GB
Jul 14 19:26:15 Starting compiler/backend/mips/proofs
Jul 14 19:26:51 Finished compiler/backend/mips/proofs                            34s   1GB
Jul 14 19:26:53 Starting compiler/backend/riscv/proofs
Jul 14 19:27:31 Finished compiler/backend/riscv/proofs                           35s   1GB
Jul 14 19:27:33 Starting compiler/proofs
Jul 14 19:29:57 Finished compiler/proofs                                       2m22s   2GB
Jul 14 19:29:59 Starting candle/set-theory
Jul 14 19:30:54 Finished candle/set-theory                                       53s 554MB
Jul 14 19:30:57 Starting candle/syntax-lib
Jul 14 19:31:17 Finished candle/syntax-lib                                       18s 448MB
Jul 14 19:31:19 Starting candle/standard/syntax
Jul 14 19:34:01 Finished candle/standard/syntax                                2m40s 679MB
Jul 14 19:34:03 Starting candle/standard/semantics
Jul 14 19:36:19 Finished candle/standard/semantics                             2m14s 796MB
Jul 14 19:36:21 Starting candle/standard/monadic
Jul 14 19:38:44 Finished candle/standard/monadic                               2m20s 930MB
Jul 14 19:38:46 Starting candle/standard/ml_kernel
Jul 14 19:49:14 Finished candle/standard/ml_kernel                            10m26s   2GB
Jul 14 19:49:16 Starting candle/standard/opentheory
Jul 14 19:49:43 Finished candle/standard/opentheory                              24s 560MB
Jul 14 19:49:45 Starting characteristic/examples
Jul 14 19:52:11 Finished characteristic/examples                               2m24s   2GB
Jul 14 19:52:13 Starting tutorial/solutions
Jul 14 20:27:30 Finished tutorial/solutions                                   35m15s  15GB
Jul 14 20:27:32 Starting translator/monadic/examples
Jul 14 20:30:28 Finished translator/monadic/examples                           2m53s   2GB
Jul 14 20:30:30 Starting examples
Jul 14 20:38:34 Finished examples                                              8m01s   2GB
Jul 14 20:38:36 Starting examples/compilation
Jul 15 02:28:50 Finished examples/compilation                               5h50m11s  19GB
Jul 15 02:28:52 Starting examples/compilation/proofs
Jul 15 02:34:10 Finished examples/compilation/proofs                           5m16s   5GB
Jul 15 02:34:12 Starting compiler/benchmarks
Jul 15 02:34:14 Finished compiler/benchmarks                                      0s   4MB
Jul 15 02:34:16 Starting translator/okasaki-examples
Jul 15 02:40:56 Finished translator/okasaki-examples                           6m37s   1GB
Jul 15 02:40:58 Starting translator/other-examples
Jul 15 02:47:41 Finished translator/other-examples                             6m40s   1GB
Jul 15 02:47:43 Starting compiler/parsing/tests
Jul 15 02:48:25 Finished compiler/parsing/tests                                  40s 351MB
Jul 15 02:48:27 Starting compiler/bootstrap/translation
Jul 15 10:30:27 FAILED: compiler/bootstrap/translation
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/l3-machine-code/arm/model]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/l3-machine-code/common]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/machine-code/hoare-triple]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/machine-code/hoare-tripleWorking in $(HOLDIR)/examples/machine-code/hoare-triple
]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/l3-machine-code/common]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/l3-machine-code/commonWorking in $(HOLDIR)/examples/l3-machine-code/common
]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/l3-machine-code/arm/model]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/l3-machine-code/lib]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/l3-machine-code/libWorking in $(HOLDIR)/examples/l3-machine-code/lib
]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/l3-machine-code/arm/model]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/l3-machine-code/arm/modelWorking in $(HOLDIR)/examples/l3-machine-code/arm/model
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/l3-machine-code/arm8/model]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/l3-machine-code/arm8/modelWorking in $(HOLDIR)/examples/l3-machine-code/arm8/model
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/l3-machine-code/mips/model]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/l3-machine-code/mips/modelWorking in $(HOLDIR)/examples/l3-machine-code/mips/model
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/l3-machine-code/riscv/model]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/l3-machine-code/riscv/modelWorking in $(HOLDIR)/examples/l3-machine-code/riscv/model
]0;Holmake: .]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/l3-machine-code/x64/model]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/l3-machine-code/x64/modelWorking in $(HOLDIR)/examples/l3-machine-code/x64/model
]0;Holmake: .]0;Holmake: ../../../basis]0;Holmake: ../../../basis/pure]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/balanced_bst]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/balanced_bstWorking in $(HOLDIR)/examples/balanced_bst
]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/formal-languages]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/formal-languages/regular]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../misc]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/fun-op-sem/lprefix_lub]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: ../../../misc]0;Holmake: ../../../developers]0;Holmake: ../../../developersWorking in ../../../developers
]0;Holmake: ../../../misc]0;Holmake: ../../../misc/lem_lib_stub]0;Holmake: ../../../misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: ../../../misc]0;Holmake: ../../../miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../basis/pureWorking in $(CAKEMLDIR)/basis/pure
]0;Holmake: ../../../basis]0;Holmake: ../../../characteristic]0;Holmake: ../../../compiler/parsing]0;Holmake: ../../../semantics]0;Holmake: ../../../semantics/ffi]0;Holmake: ../../../semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: ../../../semantics]0;Holmake: ../../../semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: ../../../compiler/parsing]0;Holmake: ../../../compiler/parsingWorking in $(CAKEMLDIR)/compiler/parsing
]0;Holmake: ../../../characteristic]0;Holmake: ../../../semantics/alt_semantics/proofs]0;Holmake: ../../../semantics/alt_semantics]0;Holmake: ../../../semantics/alt_semanticsWorking in $(CAKEMLDIR)/semantics/alt_semantics
]0;Holmake: ../../../semantics/alt_semantics/proofs]0;Holmake: ../../../semantics/proofs]0;Holmake: ../../../semantics/proofsWorking in $(CAKEMLDIR)/semantics/proofs
]0;Holmake: ../../../semantics/alt_semantics/proofs]0;Holmake: ../../../semantics/alt_semantics/proofsWorking in $(CAKEMLDIR)/semantics/alt_semantics/proofs
]0;Holmake: ../../../characteristic]0;Holmake: ../../../translator]0;Holmake: ../../../translatorWorking in $(CAKEMLDIR)/translator
]0;Holmake: ../../../characteristic]0;Holmake: ../../../characteristicWorking in $(CAKEMLDIR)/characteristic
]0;Holmake: ../../../basis]0;Holmake: ../../../translator/monadic]0;Holmake: ../../../translator/monadicWorking in $(CAKEMLDIR)/translator/monadic
]0;Holmake: ../../../basis]0;Holmake: ../../../basisWorking in $(CAKEMLDIR)/basis
]0;Holmake: .]0;Holmake: ../..]0;Holmake: ../../backend]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/machine-code/multiword]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/machine-code/multiwordWorking in $(HOLDIR)/examples/machine-code/multiword
]0;Holmake: ../../backend]0;Holmake: ../../backend/reg_alloc]0;Holmake: ../../../unverified/reg_alloc]0;Holmake: ../../../unverified/reg_allocWorking in $(CAKEMLDIR)/unverified/reg_alloc
]0;Holmake: ../../backend/reg_alloc]0;Holmake: ../../backend/reg_allocWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc
]0;Holmake: ../../backend]0;Holmake: ../../encoders/asm]0;Holmake: ../../encoders/asmWorking in $(CAKEMLDIR)/compiler/encoders/asm
]0;Holmake: ../../backend]0;Holmake: ../../backendWorking in $(CAKEMLDIR)/compiler/backend
]0;Holmake: ../..]0;Holmake: ../../backend/arm6]0;Holmake: ../../encoders/arm6]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/l3-machine-code/arm/step]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/l3-machine-code]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/machine-code/decompiler]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/machine-code/decompilerWorking in $(HOLDIR)/examples/machine-code/decompiler
]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/l3-machine-code]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/l3-machine-codeWorking in $(HOLDIR)/examples/l3-machine-code
]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/l3-machine-code/arm/step]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/l3-machine-code/arm/stepWorking in $(HOLDIR)/examples/l3-machine-code/arm/step
]0;Holmake: ../../encoders/arm6]0;Holmake: ../../encoders/arm6Working in $(CAKEMLDIR)/compiler/encoders/arm6
]0;Holmake: ../../backend/arm6]0;Holmake: ../../backend/arm6Working in $(CAKEMLDIR)/compiler/backend/arm6
]0;Holmake: ../..]0;Holmake: ../../backend/arm8]0;Holmake: ../../encoders/arm8]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/l3-machine-code/arm8/step]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/l3-machine-code/arm8/stepWorking in $(HOLDIR)/examples/l3-machine-code/arm8/step
]0;Holmake: ../../encoders/arm8]0;Holmake: ../../encoders/arm8Working in $(CAKEMLDIR)/compiler/encoders/arm8
]0;Holmake: ../../backend/arm8]0;Holmake: ../../backend/arm8Working in $(CAKEMLDIR)/compiler/backend/arm8
]0;Holmake: ../..]0;Holmake: ../../backend/mips]0;Holmake: ../../encoders/mips]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/l3-machine-code/mips/step]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/l3-machine-code/mips/stepWorking in $(HOLDIR)/examples/l3-machine-code/mips/step
]0;Holmake: ../../encoders/mips]0;Holmake: ../../encoders/mipsWorking in $(CAKEMLDIR)/compiler/encoders/mips
]0;Holmake: ../../backend/mips]0;Holmake: ../../backend/mipsWorking in $(CAKEMLDIR)/compiler/backend/mips
]0;Holmake: ../..]0;Holmake: ../../backend/riscv]0;Holmake: ../../encoders/riscv]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/l3-machine-code/riscv/step]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/l3-machine-code/riscv/stepWorking in $(HOLDIR)/examples/l3-machine-code/riscv/step
]0;Holmake: ../../encoders/riscv]0;Holmake: ../../encoders/riscvWorking in $(CAKEMLDIR)/compiler/encoders/riscv
]0;Holmake: ../../backend/riscv]0;Holmake: ../../backend/riscvWorking in $(CAKEMLDIR)/compiler/backend/riscv
]0;Holmake: ../..]0;Holmake: ../../backend/x64]0;Holmake: ../../encoders/x64]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/l3-machine-code/x64/step]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/l3-machine-code/x64/stepWorking in $(HOLDIR)/examples/l3-machine-code/x64/step
]0;Holmake: ../../encoders/x64]0;Holmake: ../../encoders/x64Working in $(CAKEMLDIR)/compiler/encoders/x64
]0;Holmake: ../../backend/x64]0;Holmake: ../../backend/x64Working in $(CAKEMLDIR)/compiler/backend/x64
]0;Holmake: ../..]0;Holmake: ../../inference]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/unification/triangular/first-order]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/unification/triangular]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/unification/triangularWorking in $(HOLDIR)/examples/unification/triangular
]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/unification/triangular/first-order]0;Holmake: /scratch/cakeml/regression/HOL-4b35dc7ed787300dd46581edc75094d74e067924/examples/unification/triangular/first-orderWorking in $(HOLDIR)/examples/unification/triangular/first-order
]0;Holmake: ../../inference]0;Holmake: ../../inferenceWorking in $(CAKEMLDIR)/compiler/inference
]0;Holmake: ../..]0;Holmake: ../..Working in $(CAKEMLDIR)/compiler
]0;Holmake: .]0;Holmake: ../../backend/reg_alloc/proofs]0;Holmake: ../../backend/reg_alloc/proofsWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
]0;Holmake: .]0;Holmake: ../../inference/proofs]0;Holmake: ../../inference/proofsWorking in $(CAKEMLDIR)/compiler/inference/proofs
]0;Holmake: .]0;Holmake: .Working in $(CAKEMLDIR)/compiler/bootstrap/translation
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! <Signal 9>
 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"
 Saved definition __ "compiler32_prog_def"
 Saved theorem _____ "semantics_compiler32_prog"
 Saved theorem _____ "compiler32Prog_translator_state_thm"
 Saved theorem _____ "compiler32Prog_monad_translator_state_thm"
 Exporting theory "compiler32Prog" ... 
compiler64ProgTheory                                                                                                                                M-KILLED