Job 290

CakeML:cd2ef4b34456062cd42214d952b282abf6126e72
  Update to_wordXXProg translations [Apr 10 13:29:08]
#481 (install-and-run)
Merging into:31c27782fd9fd62e0acfe9275cfe1587d12f71b1
  Make debug output print to stderr [Apr 06 18:23:23]
HOL:870538db577bb24113398b378cbe04d3d7055ffa
  Merge branch 'master' of https://github.com/HOL-Theorem-Prover/HOL [Apr 10 11:31:55]
Machine:oven1 4.15.9-300.fc27.x86_64 x86_64 GNU/Linux

Apr 10 14:28:17 Claimed job
Apr 10 14:28:22 Building HOL
Apr 10 14:36:30 Starting developers/bin
Apr 10 14:36:40 Finished developers/bin                                           8s 923MB
Apr 10 14:36:40 Starting semantics/ffi
Apr 10 14:37:21 Finished semantics/ffi                                           40s 436MB
Apr 10 14:37:22 Starting semantics
Apr 10 14:38:50 Finished semantics                                             1m26s 880MB
Apr 10 14:38:50 Starting semantics/proofs
Apr 10 14:40:40 Finished semantics/proofs                                      1m49s   1GB
Apr 10 14:40:41 Starting basis/pure
Apr 10 14:44:04 Finished basis/pure                                            3m22s 720MB
Apr 10 14:44:05 Starting translator
Apr 10 14:48:00 Finished translator                                            3m55s 928MB
Apr 10 14:48:01 Starting compiler/parsing
Apr 10 14:49:29 Finished compiler/parsing                                      1m27s   1GB
Apr 10 14:49:29 Starting characteristic
Apr 10 14:51:57 Finished characteristic                                        2m27s   1GB
Apr 10 14:51:58 Starting basis
Apr 10 15:10:09 Finished basis                                                18m10s   3GB
Apr 10 15:10:10 Starting translator/monadic
Apr 10 15:10:12 Finished translator/monadic                                       1s  15MB
Apr 10 15:10:12 Starting compiler/inference
Apr 10 15:11:48 Finished compiler/inference                                    1m35s   1GB
Apr 10 15:11:49 Starting compiler/backend/reg_alloc
Apr 10 15:12:17 Finished compiler/backend/reg_alloc                              27s 817MB
Apr 10 15:12:17 Starting compiler/backend/gc
Apr 10 15:21:17 Finished compiler/backend/gc                                   8m59s   3GB
Apr 10 15:21:18 Starting compiler/backend
Apr 10 15:21:21 Finished compiler/backend                                         2s  19MB
Apr 10 15:21:22 Starting compiler/encoders/asm
Apr 10 15:21:23 Finished compiler/encoders/asm                                    1s  11MB
Apr 10 15:21:24 Starting compiler/encoders/x64
Apr 10 15:22:18 Finished compiler/encoders/x64                                   53s 612MB
Apr 10 15:22:19 Starting compiler/encoders/arm6
Apr 10 15:23:57 Finished compiler/encoders/arm6                                1m37s   1GB
Apr 10 15:23:57 Starting compiler/encoders/arm8
Apr 10 15:24:24 Finished compiler/encoders/arm8                                  26s 515MB
Apr 10 15:24:25 Starting compiler/encoders/mips
Apr 10 15:25:12 Finished compiler/encoders/mips                                  46s 869MB
Apr 10 15:25:12 Starting compiler/encoders/riscv
Apr 10 15:26:06 Finished compiler/encoders/riscv                                 53s 665MB
Apr 10 15:26:07 Starting compiler/backend/x64
Apr 10 15:26:32 Finished compiler/backend/x64                                    24s   1GB
Apr 10 15:26:33 Starting compiler/backend/arm6
Apr 10 15:27:00 Finished compiler/backend/arm6                                   27s   1GB
Apr 10 15:27:01 Starting compiler/backend/arm8
Apr 10 15:27:27 Finished compiler/backend/arm8                                   25s   1GB
Apr 10 15:27:27 Starting compiler/backend/mips
Apr 10 15:27:53 Finished compiler/backend/mips                                   24s   1GB
Apr 10 15:27:53 Starting compiler/backend/riscv
Apr 10 15:28:19 Finished compiler/backend/riscv                                  25s   1GB
Apr 10 15:28:19 Starting compiler/parsing/proofs
Apr 10 15:34:28 Finished compiler/parsing/proofs                               6m07s 807MB
Apr 10 15:34:28 Starting compiler/inference/proofs
Apr 10 15:36:47 Finished compiler/inference/proofs                             2m18s   1GB
Apr 10 15:36:48 Starting compiler/backend/semantics
Apr 10 15:48:25 Finished compiler/backend/semantics                           11m35s   2GB
Apr 10 15:48:25 Starting compiler/backend/reg_alloc/proofs
Apr 10 15:49:06 Finished compiler/backend/reg_alloc/proofs                       39s 495MB
Apr 10 15:49:06 Starting compiler/backend/proofs
Apr 10 16:24:57 Finished compiler/backend/proofs                              35m49s   4GB
Apr 10 16:24:57 Starting compiler/encoders/x64/proofs
Apr 10 16:32:44 Finished compiler/encoders/x64/proofs                          7m45s   5GB
Apr 10 16:32:44 Starting compiler/encoders/arm6/proofs
Apr 10 16:40:23 Finished compiler/encoders/arm6/proofs                         7m38s   2GB
Apr 10 16:40:24 Starting compiler/encoders/arm8/proofs
Apr 10 16:45:52 Finished compiler/encoders/arm8/proofs                         5m27s   1GB
Apr 10 16:45:52 Starting compiler/encoders/mips/proofs
Apr 10 16:53:11 Finished compiler/encoders/mips/proofs                         7m18s   2GB
Apr 10 16:53:12 Starting compiler/encoders/riscv/proofs
Apr 10 17:01:17 Finished compiler/encoders/riscv/proofs                        8m04s 807MB
Apr 10 17:01:17 Starting compiler/backend/x64/proofs
Apr 10 17:01:48 Finished compiler/backend/x64/proofs                             30s   1GB
Apr 10 17:01:49 Starting compiler/backend/arm6/proofs
Apr 10 17:02:22 Finished compiler/backend/arm6/proofs                            33s   1GB
Apr 10 17:02:23 Starting compiler/backend/arm8/proofs
Apr 10 17:02:54 Finished compiler/backend/arm8/proofs                            30s   1GB
Apr 10 17:02:55 Starting compiler/backend/mips/proofs
Apr 10 17:03:27 Finished compiler/backend/mips/proofs                            31s   1GB
Apr 10 17:03:28 Starting compiler/backend/riscv/proofs
Apr 10 17:04:00 Finished compiler/backend/riscv/proofs                           31s   1GB
Apr 10 17:04:01 Starting compiler/proofs
Apr 10 17:05:28 Finished compiler/proofs                                       1m26s   2GB
Apr 10 17:05:28 Starting candle/set-theory
Apr 10 17:06:25 Finished candle/set-theory                                       55s 572MB
Apr 10 17:06:25 Starting candle/syntax-lib
Apr 10 17:06:36 Finished candle/syntax-lib                                       10s 606MB
Apr 10 17:06:37 Starting candle/standard/syntax
Apr 10 17:08:11 Finished candle/standard/syntax                                1m33s 623MB
Apr 10 17:08:11 Starting candle/standard/semantics
Apr 10 17:09:31 Finished candle/standard/semantics                             1m18s 996MB
Apr 10 17:09:31 Starting candle/standard/monadic
Apr 10 17:10:59 Finished candle/standard/monadic                               1m27s   1GB
Apr 10 17:11:00 Starting candle/standard/ml_kernel
Apr 10 17:16:58 Finished candle/standard/ml_kernel                             5m57s   1GB
Apr 10 17:16:58 Starting candle/standard/opentheory
Apr 10 17:17:16 Finished candle/standard/opentheory                              16s 769MB
Apr 10 17:17:16 Starting characteristic/examples
Apr 10 17:18:41 Finished characteristic/examples                               1m24s   1GB
Apr 10 17:18:42 Starting tutorial/solutions
Apr 10 17:43:50 Finished tutorial/solutions                                   25m07s   9GB
Apr 10 17:43:51 Starting translator/monadic/examples
Apr 10 17:45:45 Finished translator/monadic/examples                           1m53s   2GB
Apr 10 17:45:45 Starting examples
Apr 10 17:51:08 Finished examples                                              5m22s   2GB
Apr 10 17:51:09 Starting examples/compilation
Apr 10 21:58:36 Finished examples/compilation                               4h07m26s  22GB
Apr 10 21:58:37 Starting examples/compilation/proofs
Apr 10 22:02:26 Finished examples/compilation/proofs                           3m48s   6GB
Apr 10 22:02:26 Starting compiler/benchmarks
Apr 10 22:02:27 Finished compiler/benchmarks                                      0s   4MB
Apr 10 22:02:28 Starting translator/okasaki-examples
Apr 10 22:06:00 Finished translator/okasaki-examples                           3m31s   1GB
Apr 10 22:06:01 Starting translator/other-examples
Apr 10 22:09:32 Finished translator/other-examples                             3m30s 713MB
Apr 10 22:09:33 Starting compiler/parsing/tests
Apr 10 22:09:57 Finished compiler/parsing/tests                                  23s 307MB
Apr 10 22:09:57 Starting compiler/bootstrap/translation
Apr 11 02:43:27 FAILED: compiler/bootstrap/translation
]0;Holmake: .]0;Holmake: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/examples/l3-machine-code/arm/model]0;Holmake: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/examples/l3-machine-code/common]0;Holmake: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/examples/machine-code/hoare-tripleWorking in $(HOLDIR)/examples/machine-code/hoare-triple
]0;Holmake: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/examples/l3-machine-code/common]0;Holmake: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/examples/l3-machine-code/commonWorking in $(HOLDIR)/examples/l3-machine-code/common
]0;Holmake: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/examples/l3-machine-code/arm/model]0;Holmake: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/examples/l3-machine-code/lib]0;Holmake: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/examples/l3-machine-code/libWorking in $(HOLDIR)/examples/l3-machine-code/lib
]0;Holmake: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/examples/l3-machine-code/arm/model]0;Holmake: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/examples/l3-machine-code/arm/modelWorking in $(HOLDIR)/examples/l3-machine-code/arm/model
]0;Holmake: .]0;Holmake: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/examples/l3-machine-code/arm8/model]0;Holmake: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/examples/l3-machine-code/arm8/modelWorking in $(HOLDIR)/examples/l3-machine-code/arm8/model
]0;Holmake: .]0;Holmake: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/examples/l3-machine-code/mips/model]0;Holmake: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/examples/l3-machine-code/mips/modelWorking in $(HOLDIR)/examples/l3-machine-code/mips/model
]0;Holmake: .]0;Holmake: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/examples/l3-machine-code/riscv/model]0;Holmake: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/examples/l3-machine-code/riscv/modelWorking in $(HOLDIR)/examples/l3-machine-code/riscv/model
]0;Holmake: .]0;Holmake: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/examples/l3-machine-code/x64/model]0;Holmake: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/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: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/examples/balanced_bst]0;Holmake: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/examples/balanced_bstWorking in $(HOLDIR)/examples/balanced_bst
]0;Holmake: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/examples/formal-languages]0;Holmake: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../misc]0;Holmake: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/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: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/examples/machine-code/multiword]0;Holmake: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/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]0;Holmake: ../../encodersWorking in $(CAKEMLDIR)/compiler/encoders
]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: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/examples/l3-machine-code/arm/step]0;Holmake: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/examples/l3-machine-code]0;Holmake: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/examples/machine-code/decompiler]0;Holmake: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/examples/machine-code/decompilerWorking in $(HOLDIR)/examples/machine-code/decompiler
]0;Holmake: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/examples/l3-machine-code]0;Holmake: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/examples/l3-machine-codeWorking in $(HOLDIR)/examples/l3-machine-code
]0;Holmake: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/examples/l3-machine-code/arm/step]0;Holmake: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/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: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/examples/l3-machine-code/arm8/step]0;Holmake: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/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: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/examples/l3-machine-code/mips/step]0;Holmake: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/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: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/examples/l3-machine-code/riscv/step]0;Holmake: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/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: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/examples/l3-machine-code/x64/step]0;Holmake: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/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: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/examples/unification/triangular/first-order]0;Holmake: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/examples/unification/triangular]0;Holmake: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/examples/unification/triangularWorking in $(HOLDIR)/examples/unification/triangular
]0;Holmake: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/examples/unification/triangular/first-order]0;Holmake: ~/regression/HOL-870538db577bb24113398b378cbe04d3d7055ffa/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_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>
 Uncaught exception: HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 235) (THEN1 on line 240)", origin_function = "THEN1", origin_structure = "Tactical"}
 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