Job 515

CakeML:0bca5648f09015518a7629441ff5c3e6174e3731
  Fix some things downstream of the tap changes. [Sep 20 15:16:47]
#526 (explorer)
Merging into:675c1da06454efcef70f62574de96a524820287f
  Merge pull request #532 from CakeML/trans-msg [Oct 03 07:58:05]
HOL:c99b7420019e4deae768b219d3c8e926b43af0b7
  Make buildheap preserve temporary files when --dbg flag is set [Oct 05 01:50:41]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Oct 05 08:49:55 Claimed job
Oct 05 08:50:09 Building HOL
Oct 05 08:59:28 Starting developers/bin
Oct 05 09:00:46 Finished developers/bin                                        1m17s 912MB
Oct 05 09:00:46 Starting semantics/ffi
Oct 05 09:01:26 Finished semantics/ffi                                           38s 381MB
Oct 05 09:01:26 Starting semantics
Oct 05 09:02:52 Finished semantics                                             1m25s   1GB
Oct 05 09:02:53 Starting semantics/proofs
Oct 05 09:05:34 Finished semantics/proofs                                      2m40s   1GB
Oct 05 09:05:35 Starting basis/pure
Oct 05 09:09:08 Finished basis/pure                                            3m32s 824MB
Oct 05 09:09:09 Starting translator
Oct 05 09:10:15 Finished translator                                            1m06s   1GB
Oct 05 09:10:16 Starting compiler/parsing
Oct 05 09:11:49 Finished compiler/parsing                                      1m32s   1GB
Oct 05 09:11:50 Starting characteristic
Oct 05 09:14:18 Finished characteristic                                        2m26s   1GB
Oct 05 09:14:18 Starting translator/monadic
Oct 05 09:15:45 Finished translator/monadic                                    1m26s   1GB
Oct 05 09:15:46 Starting basis
Oct 05 09:32:14 Finished basis                                                16m26s   2GB
Oct 05 09:32:14 Starting compiler/inference
Oct 05 09:33:57 Finished compiler/inference                                    1m41s   1GB
Oct 05 09:33:57 Starting compiler/backend/reg_alloc
Oct 05 09:34:45 Finished compiler/backend/reg_alloc                              47s   1GB
Oct 05 09:34:46 Starting compiler/backend/gc
Oct 05 09:43:37 Finished compiler/backend/gc                                   8m50s   3GB
Oct 05 09:43:38 Starting compiler/backend
Oct 05 09:43:41 Finished compiler/backend                                         2s  14MB
Oct 05 09:43:42 Starting compiler/encoders/asm
Oct 05 09:43:44 Finished compiler/encoders/asm                                    1s  10MB
Oct 05 09:43:44 Starting compiler/encoders/x64
Oct 05 09:44:36 Finished compiler/encoders/x64                                   50s 591MB
Oct 05 09:44:36 Starting compiler/encoders/arm6
Oct 05 09:46:21 Finished compiler/encoders/arm6                                1m44s   1GB
Oct 05 09:46:22 Starting compiler/encoders/arm8
Oct 05 09:46:48 Finished compiler/encoders/arm8                                  25s 480MB
Oct 05 09:46:49 Starting compiler/encoders/mips
Oct 05 09:47:47 Finished compiler/encoders/mips                                  57s 895MB
Oct 05 09:47:47 Starting compiler/encoders/riscv
Oct 05 09:48:48 Finished compiler/encoders/riscv                                 59s 711MB
Oct 05 09:48:49 Starting compiler/backend/x64
Oct 05 09:49:08 Finished compiler/backend/x64                                    19s   1GB
Oct 05 09:49:09 Starting compiler/backend/arm6
Oct 05 09:49:30 Finished compiler/backend/arm6                                   20s   1GB
Oct 05 09:49:31 Starting compiler/backend/arm8
Oct 05 09:49:50 Finished compiler/backend/arm8                                   19s   1GB
Oct 05 09:49:51 Starting compiler/backend/mips
Oct 05 09:50:12 Finished compiler/backend/mips                                   20s   1GB
Oct 05 09:50:13 Starting compiler/backend/riscv
Oct 05 09:50:32 Finished compiler/backend/riscv                                  18s   1GB
Oct 05 09:50:32 Starting compiler/parsing/proofs
Oct 05 09:56:51 Finished compiler/parsing/proofs                               6m17s 777MB
Oct 05 09:56:51 Starting compiler/inference/proofs
Oct 05 09:59:44 Finished compiler/inference/proofs                             2m52s   1GB
Oct 05 09:59:45 Starting compiler/backend/semantics
Oct 05 10:09:51 Finished compiler/backend/semantics                           10m05s   2GB
Oct 05 10:09:52 Starting compiler/backend/reg_alloc/proofs
Oct 05 10:17:23 Finished compiler/backend/reg_alloc/proofs                     7m30s 585MB
Oct 05 10:17:24 Starting compiler/backend/proofs
Oct 05 10:59:53 Finished compiler/backend/proofs                              42m28s   4GB
Oct 05 10:59:53 Starting compiler/encoders/x64/proofs
Oct 05 11:07:07 Finished compiler/encoders/x64/proofs                          7m12s   4GB
Oct 05 11:07:07 Starting compiler/encoders/arm6/proofs
Oct 05 11:15:44 Finished compiler/encoders/arm6/proofs                         8m36s   2GB
Oct 05 11:15:45 Starting compiler/encoders/arm8/proofs
Oct 05 11:21:13 Finished compiler/encoders/arm8/proofs                         5m27s   1GB
Oct 05 11:21:14 Starting compiler/encoders/mips/proofs
Oct 05 11:29:11 Finished compiler/encoders/mips/proofs                         7m55s   2GB
Oct 05 11:29:11 Starting compiler/encoders/riscv/proofs
Oct 05 11:40:33 Finished compiler/encoders/riscv/proofs                       11m21s 911MB
Oct 05 11:40:34 Starting compiler/backend/x64/proofs
Oct 05 11:41:04 Finished compiler/backend/x64/proofs                             29s   1GB
Oct 05 11:41:04 Starting compiler/backend/arm6/proofs
Oct 05 11:41:34 Finished compiler/backend/arm6/proofs                            29s   1GB
Oct 05 11:41:35 Starting compiler/backend/arm8/proofs
Oct 05 11:42:04 Finished compiler/backend/arm8/proofs                            28s 753MB
Oct 05 11:42:05 Starting compiler/backend/mips/proofs
Oct 05 11:42:34 Finished compiler/backend/mips/proofs                            28s   1GB
Oct 05 11:42:34 Starting compiler/backend/riscv/proofs
Oct 05 11:43:01 Finished compiler/backend/riscv/proofs                           26s   1GB
Oct 05 11:43:02 Starting compiler/proofs
Oct 05 11:45:00 Finished compiler/proofs                                       1m57s   1GB
Oct 05 11:45:01 Starting candle/set-theory
Oct 05 11:45:44 Finished candle/set-theory                                       43s 593MB
Oct 05 11:45:45 Starting candle/syntax-lib
Oct 05 11:45:59 Finished candle/syntax-lib                                       13s 604MB
Oct 05 11:46:00 Starting candle/standard/syntax
Oct 05 11:48:11 Finished candle/standard/syntax                                2m10s 690MB
Oct 05 11:48:12 Starting candle/standard/semantics
Oct 05 11:50:01 Finished candle/standard/semantics                             1m48s   1GB
Oct 05 11:50:01 Starting candle/standard/monadic
Oct 05 11:51:47 Finished candle/standard/monadic                               1m45s 808MB
Oct 05 11:51:48 Starting candle/standard/ml_kernel
Oct 05 12:08:43 Finished candle/standard/ml_kernel                            16m54s   4GB
Oct 05 12:08:43 Starting candle/standard/opentheory
Oct 05 12:17:45 Finished candle/standard/opentheory                            9m01s   9GB
Oct 05 12:17:46 Starting candle/standard/opentheory/compilation
Oct 05 12:54:54 Finished candle/standard/opentheory/compilation               37m07s  16GB
Oct 05 12:54:55 Starting characteristic/examples
Oct 05 12:56:36 Finished characteristic/examples                               1m40s   2GB
Oct 05 12:56:37 Starting tutorial/solutions
Oct 05 13:10:44 Finished tutorial/solutions                                   14m06s   6GB
Oct 05 13:10:45 Starting translator/monadic/examples
Oct 05 13:12:47 Finished translator/monadic/examples                           2m01s   2GB
Oct 05 13:12:47 Starting examples
Oct 05 13:19:33 Finished examples                                              6m45s   4GB
Oct 05 13:19:34 Starting examples/compilation
Oct 05 15:33:32 Finished examples/compilation                               2h13m57s   9GB
Oct 05 15:33:33 Starting examples/compilation/proofs
Oct 05 15:35:31 Finished examples/compilation/proofs                           1m58s   3GB
Oct 05 15:35:32 Starting compiler/benchmarks
Oct 05 15:35:33 Finished compiler/benchmarks                                      0s   5MB
Oct 05 15:35:34 Starting translator/okasaki-examples
Oct 05 15:39:16 Finished translator/okasaki-examples                           3m41s   1GB
Oct 05 15:39:17 Starting translator/other-examples
Oct 05 15:43:01 Finished translator/other-examples                             3m43s 870MB
Oct 05 15:43:02 Starting compiler/parsing/tests
Oct 05 15:43:28 Finished compiler/parsing/tests                                  25s 291MB
Oct 05 15:43:29 Starting compiler/inference/tests
Oct 05 15:47:35 Finished compiler/inference/tests                              4m06s   5GB
Oct 05 15:47:36 Starting compiler/bootstrap/translation
Oct 05 21:05:33 FAILED: compiler/bootstrap/translation
]0;Holmake: .]0;Holmake: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/l3-machine-code/arm/model]0;Holmake: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/l3-machine-code/common]0;Holmake: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/machine-code/hoare-triple]0;Holmake: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/machine-code/hoare-tripleWorking in $(HOLDIR)/examples/machine-code/hoare-triple
]0;Holmake: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/l3-machine-code/common]0;Holmake: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/l3-machine-code/commonWorking in $(HOLDIR)/examples/l3-machine-code/common
]0;Holmake: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/l3-machine-code/arm/model]0;Holmake: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/l3-machine-code/lib]0;Holmake: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/l3-machine-code/libWorking in $(HOLDIR)/examples/l3-machine-code/lib
]0;Holmake: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/l3-machine-code/arm/model]0;Holmake: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/l3-machine-code/arm/modelWorking in $(HOLDIR)/examples/l3-machine-code/arm/model
]0;Holmake: .]0;Holmake: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/l3-machine-code/arm8/model]0;Holmake: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/l3-machine-code/arm8/modelWorking in $(HOLDIR)/examples/l3-machine-code/arm8/model
]0;Holmake: .]0;Holmake: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/l3-machine-code/mips/model]0;Holmake: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/l3-machine-code/mips/modelWorking in $(HOLDIR)/examples/l3-machine-code/mips/model
]0;Holmake: .]0;Holmake: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/l3-machine-code/riscv/model]0;Holmake: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/l3-machine-code/riscv/modelWorking in $(HOLDIR)/examples/l3-machine-code/riscv/model
]0;Holmake: .]0;Holmake: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/l3-machine-code/x64/model]0;Holmake: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/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: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/balanced_bst]0;Holmake: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/balanced_bstWorking in $(HOLDIR)/examples/balanced_bst
]0;Holmake: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/formal-languages]0;Holmake: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/formal-languages/regular]0;Holmake: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../misc]0;Holmake: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/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: ../../../translator]0;Holmake: ../../../semantics/proofs]0;Holmake: ../../../semantics/proofsWorking in $(CAKEMLDIR)/semantics/proofs
]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: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/machine-code/multiword]0;Holmake: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/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: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/l3-machine-code/arm/step]0;Holmake: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/l3-machine-code]0;Holmake: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/machine-code/decompiler]0;Holmake: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/machine-code/decompilerWorking in $(HOLDIR)/examples/machine-code/decompiler
]0;Holmake: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/l3-machine-code]0;Holmake: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/l3-machine-codeWorking in $(HOLDIR)/examples/l3-machine-code
]0;Holmake: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/l3-machine-code/arm/step]0;Holmake: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/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: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/l3-machine-code/arm8/step]0;Holmake: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/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: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/l3-machine-code/mips/step]0;Holmake: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/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: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/l3-machine-code/riscv/step]0;Holmake: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/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: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/l3-machine-code/x64/step]0;Holmake: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/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: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/unification/triangular/first-order]0;Holmake: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/unification/triangular]0;Holmake: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/unification/triangularWorking in $(HOLDIR)/examples/unification/triangular
]0;Holmake: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/examples/unification/triangular/first-order]0;Holmake: ~/oven/regression/HOL-c99b7420019e4deae768b219d3c8e926b43af0b7/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 reg_allocProgTheory
reg_allocProgTheory                                                          OK
Starting work on inferProgTheory
inferProgTheory                                                              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
x64ProgTheory                                                                OK
Starting work on arm8ProgTheory
to_target32ProgTheory                                                        OK
Starting work on arm6ProgTheory
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>
 
 
 which has type:
 
 :32 backend$config ->
 ast$dec list ->
 (word8 list # word32 list # 32 lab_to_target$config) option # tap_data list
 
 Failed translation: compile
 Uncaught exception: UnableToTranslate (Const (?, GRND (Tyapp ((?, 2), [Tyapp ((?, 1), [Tyapp ((?, 1), [Tyapp ((?, 1), [Tyapp ((?, 1), [Tyapp ((?, 1), [Tyapp ((?, 1), [Tyapp ((?, 0), [])])])])])])]), Tyapp ((?, 2), [Tyapp ((?, 1), [Tyapp ((?, 0), [])]), Tyapp ((?, 2), [Tyapp ((?, 1), [Tyapp ((?, 2), [Tyapp ((?, 1), [Tyapp ((?, 2), [Tyapp ((?, 0), []), Tyapp ((?, 1), [Tyapp ((?, 1), [Tyapp ((?, 1), [Tyapp ((?, 0), [])])])])])]), Tyapp ((?, 2), [Tyapp ((?, 1), [Tyapp ((?, 2), [Tyapp ((?, 0), []), Tyapp ((?, 1), [Tyapp ((?, 1), [Tyapp ((?, 1), [Tyapp ((?, 1), [Tyapp ((?, 1), [Tyapp ((?, 0), [])])])])])])])]), Tyapp ((?, 1), [Tyapp ((?, 1), [Tyapp ((?, 1), [Tyapp ((?, 1), [Tyapp ((?, 1), [Tyapp ((?, 1), [Tyapp ((?, 0), [])])])])])])])])])]), Tyapp ((?, 1), [Tyapp ((?, 0), [])])])])]))))
compiler64ProgTheory                                                   M-KILLED