Overview

Job 573

CakeML:d61774f4ad5a99f551ead6c65d317f563b27de8b
  Fix parsing issue in BottomUpMergeSort
#554 (tiny)
Merging into:9b491cb24bd22174a6c514574e4bb6c057eafe2f
  Rename "backend_correct" to "encoder_correct"
HOL:57ef4df497757f622a7fe2bfeda16116585da6d4
  Update experimental kernel for world free of Globals.priming
Machine:oven2 4.13.0-37-generic x86_64 GNU/Linux

 Claimed job
 Reusing HOL
 Starting developers/bin
 Finished developers/bin                                          33s 202MB
 Starting semantics/ffi
 Finished semantics/ffi                                            9s 256MB
 Starting semantics
 Finished semantics                                             1m13s 965MB
 Starting semantics/proofs
 Finished semantics/proofs                                      2m49s   1GB
 Starting basis/pure
 Finished basis/pure                                              48s 648MB
 Starting translator
 Finished translator                                            3m03s 965MB
 Starting compiler/parsing
 Finished compiler/parsing                                      1m15s   1GB
 Starting characteristic
 Finished characteristic                                        2m26s   1GB
 Starting translator/monadic
 Finished translator/monadic                                    1m25s   1GB
 Starting basis
 Finished basis                                                16m19s   3GB
 Starting compiler/inference
 Finished compiler/inference                                    1m22s   1GB
 Starting compiler/backend/reg_alloc
 Finished compiler/backend/reg_alloc                              45s 929MB
 Starting compiler/backend/gc
 Finished compiler/backend/gc                                   6m22s   1GB
 Starting compiler/backend
 Finished compiler/backend                                         2s  22MB
 Starting compiler/encoders/asm
 Finished compiler/encoders/asm                                    0s  14MB
 Starting compiler/encoders/x64
 Finished compiler/encoders/x64                                   14s 416MB
 Starting compiler/encoders/arm6
 Finished compiler/encoders/arm6                                  43s 497MB
 Starting compiler/encoders/arm8
 Finished compiler/encoders/arm8                                   7s 328MB
 Starting compiler/encoders/mips
 Finished compiler/encoders/mips                                   8s 427MB
 Starting compiler/encoders/riscv
 Finished compiler/encoders/riscv                                  7s 380MB
 Starting compiler/encoders/ag32
 Finished compiler/encoders/ag32                                  15s 500MB
 Starting compiler/backend/x64
 Finished compiler/backend/x64                                    15s 741MB
 Starting compiler/backend/arm6
 Finished compiler/backend/arm6                                   18s   1GB
 Starting compiler/backend/arm8
 Finished compiler/backend/arm8                                   17s   1GB
 Starting compiler/backend/mips
 Finished compiler/backend/mips                                   18s   1GB
 Starting compiler/backend/riscv
 Finished compiler/backend/riscv                                  17s   1GB
 Starting compiler/backend/ag32
 Finished compiler/backend/ag32                                 1m12s 968MB
 Starting compiler/parsing/proofs
 Finished compiler/parsing/proofs                               6m04s 853MB
 Starting compiler/inference/proofs
 Finished compiler/inference/proofs                             2m52s   1GB
 Starting compiler/backend/semantics
 Finished compiler/backend/semantics                            9m03s   2GB
 Starting compiler/backend/reg_alloc/proofs
 Finished compiler/backend/reg_alloc/proofs                     2m42s 491MB
 Starting compiler/backend/proofs
 Finished compiler/backend/proofs                              44m07s   3GB
 Starting compiler/encoders/x64/proofs
 Finished compiler/encoders/x64/proofs                          9m18s 975MB
 Starting compiler/encoders/arm6/proofs
 Finished compiler/encoders/arm6/proofs                        14m04s   1GB
 Starting compiler/encoders/arm8/proofs
 Finished compiler/encoders/arm8/proofs                         5m56s   1GB
 Starting compiler/encoders/mips/proofs
 Finished compiler/encoders/mips/proofs                        10m02s   2GB
 Starting compiler/encoders/riscv/proofs
 Finished compiler/encoders/riscv/proofs                        7m58s 766MB
 Starting compiler/encoders/ag32/proofs
 Finished compiler/encoders/ag32/proofs                         2m45s 624MB
 Starting compiler/backend/x64/proofs
 Finished compiler/backend/x64/proofs                             19s   1GB
 Starting compiler/backend/arm6/proofs
 Finished compiler/backend/arm6/proofs                            20s   1GB
 Starting compiler/backend/arm8/proofs
 Finished compiler/backend/arm8/proofs                            19s   1GB
 Starting compiler/backend/mips/proofs
 Finished compiler/backend/mips/proofs                            19s   1GB
 Starting compiler/backend/riscv/proofs
 Finished compiler/backend/riscv/proofs                           19s   1GB
 Starting compiler/backend/ag32/proofs
 Finished compiler/backend/ag32/proofs                          9m46s   2GB
 Starting compiler/proofs
 Finished compiler/proofs                                       1m19s   2GB
 Starting candle/set-theory
 Finished candle/set-theory                                       24s 602MB
 Starting candle/syntax-lib
 Finished candle/syntax-lib                                        9s 670MB
 Starting candle/standard/syntax
 Finished candle/standard/syntax                                1m31s 537MB
 Starting candle/standard/semantics
 Finished candle/standard/semantics                             1m17s 811MB
 Starting candle/standard/monadic
 Finished candle/standard/monadic                               1m33s   1GB
 Starting candle/standard/ml_kernel
 Finished candle/standard/ml_kernel                            15m33s   3GB
 Starting candle/standard/opentheory
 Finished candle/standard/opentheory                            7m50s   2GB
 Starting candle/standard/opentheory/compilation
 Finished candle/standard/opentheory/compilation               30m01s  12GB
 Starting candle/standard/opentheory/compilation/proofs
 Finished candle/standard/opentheory/compilation/proofs           35s   4GB
 Starting characteristic/examples
 Finished characteristic/examples                               1m27s   1GB
 Starting tutorial/solutions
 Finished tutorial/solutions                                   13m28s   7GB
 Starting translator/monadic/examples
 Finished translator/monadic/examples                           1m44s   2GB
 Starting examples
 Finished examples                                              6m01s   2GB
 Starting examples/compilation/x64
 Finished examples/compilation/x64                           2h04m59s  10GB
 Starting examples/compilation/x64/proofs
 Finished examples/compilation/x64/proofs                       1m51s   3GB
 Starting examples/compilation/ag32
 Finished examples/compilation/ag32                            26m54s   3GB
 Starting examples/compilation/ag32/proofs
 Finished examples/compilation/ag32/proofs                        24s   2GB
 Starting compiler/benchmarks
 Finished compiler/benchmarks                                      0s   4MB
 Starting translator/okasaki-examples
 Finished translator/okasaki-examples                           3m32s   1GB
 Starting translator/other-examples
 Finished translator/other-examples                             3m18s 817MB
 Starting compiler/parsing/tests
 Finished compiler/parsing/tests                                  24s 312MB
 Starting compiler/inference/tests
 Finished compiler/inference/tests                              3m58s   4GB
 Starting compiler/bootstrap/translation
 FAILED: compiler/bootstrap/translation
]0;Holmake: .]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/arm/model]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/common]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/common]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/common[1mWorking in $(HOLDIR)/examples/l3-machine-code/common[0m
]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/arm/model]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/lib]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/lib[1mWorking in $(HOLDIR)/examples/l3-machine-code/lib[0m
]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/arm/model]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/arm/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/model[0m
]0;Holmake: .]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/arm8/model]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/arm8/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm8/model[0m
]0;Holmake: .]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/mips/model]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/mips/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/mips/model[0m
]0;Holmake: .]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/riscv/model]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/riscv/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/riscv/model[0m
]0;Holmake: .]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/x64/model]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/x64/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/x64/model[0m
]0;Holmake: .]0;Holmake: ../../../basis]0;Holmake: ../../../basis/pure]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/balanced_bst]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/formal-languages]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../misc]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ../../../misc]0;Holmake: ../../../developers]0;Holmake: ../../../developers[1mWorking in ../../../developers[0m
]0;Holmake: ../../../misc]0;Holmake: ../../../misc/lem_lib_stub]0;Holmake: ../../../misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ../../../misc]0;Holmake: ../../../misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ../../../basis/pure]0;Holmake: ../../../basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ../../../basis]0;Holmake: ../../../characteristic]0;Holmake: ../../../compiler/parsing]0;Holmake: ../../../semantics]0;Holmake: ../../../semantics/ffi]0;Holmake: ../../../semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ../../../semantics]0;Holmake: ../../../semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ../../../compiler/parsing]0;Holmake: ../../../compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ../../../characteristic]0;Holmake: ../../../semantics/proofs]0;Holmake: ../../../semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ../../../characteristic]0;Holmake: ../../../translator]0;Holmake: ../../../semantics/alt_semantics/proofs]0;Holmake: ../../../semantics/alt_semantics]0;Holmake: ../../../semantics/alt_semantics[1mWorking in $(CAKEMLDIR)/semantics/alt_semantics[0m
]0;Holmake: ../../../semantics/alt_semantics/proofs]0;Holmake: ../../../semantics/alt_semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/alt_semantics/proofs[0m
]0;Holmake: ../../../translator]0;Holmake: ../../../translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ../../../characteristic]0;Holmake: ../../../characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ../../../basis]0;Holmake: ../../../translator/monadic]0;Holmake: ../../../translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ../../../basis]0;Holmake: ../../../basis[1mWorking in $(CAKEMLDIR)/basis[0m
]0;Holmake: .]0;Holmake: ../..]0;Holmake: ../../backend]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/machine-code/multiword]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/machine-code/multiword[1mWorking in $(HOLDIR)/examples/machine-code/multiword[0m
]0;Holmake: ../../backend]0;Holmake: ../../backend/reg_alloc]0;Holmake: ../../../unverified/reg_alloc]0;Holmake: ../../../unverified/reg_alloc[1mWorking in $(CAKEMLDIR)/unverified/reg_alloc[0m
]0;Holmake: ../../backend/reg_alloc]0;Holmake: ../../backend/reg_alloc[1mWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc[0m
]0;Holmake: ../../backend]0;Holmake: ../../encoders/asm]0;Holmake: ../../encoders/asm[1mWorking in $(CAKEMLDIR)/compiler/encoders/asm[0m
]0;Holmake: ../../backend]0;Holmake: ../../backend[1mWorking in $(CAKEMLDIR)/compiler/backend[0m
]0;Holmake: ../..]0;Holmake: ../../backend/ag32]0;Holmake: ../../encoders/ag32]0;Holmake: ../../encoders/ag32[1mWorking in $(CAKEMLDIR)/compiler/encoders/ag32[0m
]0;Holmake: ../../backend/ag32]0;Holmake: ../../backend/ag32[1mWorking in $(CAKEMLDIR)/compiler/backend/ag32[0m
]0;Holmake: ../..]0;Holmake: ../../backend/arm6]0;Holmake: ../../encoders/arm6]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/arm/step]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/machine-code/decompiler]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/machine-code/decompiler[1mWorking in $(HOLDIR)/examples/machine-code/decompiler[0m
]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code[1mWorking in $(HOLDIR)/examples/l3-machine-code[0m
]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/arm/step]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/arm/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/step[0m
]0;Holmake: ../../encoders/arm6]0;Holmake: ../../encoders/arm6[1mWorking in $(CAKEMLDIR)/compiler/encoders/arm6[0m
]0;Holmake: ../../backend/arm6]0;Holmake: ../../backend/arm6[1mWorking in $(CAKEMLDIR)/compiler/backend/arm6[0m
]0;Holmake: ../..]0;Holmake: ../../backend/arm8]0;Holmake: ../../encoders/arm8]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/arm8/step]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/arm8/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm8/step[0m
]0;Holmake: ../../encoders/arm8]0;Holmake: ../../encoders/arm8[1mWorking in $(CAKEMLDIR)/compiler/encoders/arm8[0m
]0;Holmake: ../../backend/arm8]0;Holmake: ../../backend/arm8[1mWorking in $(CAKEMLDIR)/compiler/backend/arm8[0m
]0;Holmake: ../..]0;Holmake: ../../backend/mips]0;Holmake: ../../encoders/mips]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/mips/step]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/mips/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/mips/step[0m
]0;Holmake: ../../encoders/mips]0;Holmake: ../../encoders/mips[1mWorking in $(CAKEMLDIR)/compiler/encoders/mips[0m
]0;Holmake: ../../backend/mips]0;Holmake: ../../backend/mips[1mWorking in $(CAKEMLDIR)/compiler/backend/mips[0m
]0;Holmake: ../..]0;Holmake: ../../backend/riscv]0;Holmake: ../../encoders/riscv]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/riscv/step]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/riscv/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/riscv/step[0m
]0;Holmake: ../../encoders/riscv]0;Holmake: ../../encoders/riscv[1mWorking in $(CAKEMLDIR)/compiler/encoders/riscv[0m
]0;Holmake: ../../backend/riscv]0;Holmake: ../../backend/riscv[1mWorking in $(CAKEMLDIR)/compiler/backend/riscv[0m
]0;Holmake: ../..]0;Holmake: ../../backend/x64]0;Holmake: ../../encoders/x64]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/x64/step]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/l3-machine-code/x64/step[1mWorking in $(HOLDIR)/examples/l3-machine-code/x64/step[0m
]0;Holmake: ../../encoders/x64]0;Holmake: ../../encoders/x64[1mWorking in $(CAKEMLDIR)/compiler/encoders/x64[0m
]0;Holmake: ../../backend/x64]0;Holmake: ../../backend/x64[1mWorking in $(CAKEMLDIR)/compiler/backend/x64[0m
]0;Holmake: ../..]0;Holmake: ../../inference]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/unification/triangular/first-order]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/unification/triangular]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/unification/triangular[1mWorking in $(HOLDIR)/examples/unification/triangular[0m
]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/unification/triangular/first-order]0;Holmake: ~/regression/HOL-57ef4df497757f622a7fe2bfeda16116585da6d4/examples/unification/triangular/first-order[1mWorking in $(HOLDIR)/examples/unification/triangular/first-order[0m
]0;Holmake: ../../inference]0;Holmake: ../../inference[1mWorking in $(CAKEMLDIR)/compiler/inference[0m
]0;Holmake: ../..]0;Holmake: ../..[1mWorking in $(CAKEMLDIR)/compiler[0m
]0;Holmake: .]0;Holmake: ../../backend/reg_alloc/proofs]0;Holmake: ../../backend/reg_alloc/proofs[1mWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
]0;Holmake: .]0;Holmake: ../../inference/proofs]0;Holmake: ../../inference/proofs[1mWorking in $(CAKEMLDIR)/compiler/inference/proofs[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/compiler/bootstrap/translation[0m
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_word32ProgTheory                                                                                        OK
Starting work on to_target32ProgTheory
to_word64ProgTheory                                                                                        OK
Starting work on to_target64ProgTheory
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 ag32ProgTheory
arm8ProgTheory                                                                                             OK
Starting work on riscvProgTheory
ag32ProgTheory                                                                                             OK
Starting work on compiler32ProgTheory
riscvProgTheory                                                                                            OK
Starting work on mipsProgTheory
mipsProgTheory                                                                                             OK
Starting work on compiler64ProgTheory
compiler32ProgTheory                                                                              FAILED! <1>
 Proof of 
 
 app p main_v [Conv NONE []] (STDIO fs * COMMANDLINE cl)
   (POSTv uv.
        &UNIT_TYPE () uv * STDIO (full_compile_32 (TL cl) (get_stdin fs) fs) *
        COMMANDLINE cl)
 
 failed.
 Failed to prove theorem main_spec.
 Uncaught exception: HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 266) (THEN1 on line 271)", origin_function = "THEN1", origin_structure = "Tactical"}
compiler64ProgTheory                                                                                 M-KILLED