Job 573

CakeML:d61774f4ad5a99f551ead6c65d317f563b27de8b
  Fix parsing issue in BottomUpMergeSort [Nov 21 15:17:14]
#554 (tiny)
Merging into:9b491cb24bd22174a6c514574e4bb6c057eafe2f
  Rename "backend_correct" to "encoder_correct" [Nov 20 18:08:31]
HOL:57ef4df497757f622a7fe2bfeda16116585da6d4
  Update experimental kernel for world free of Globals.priming [Nov 20 05:59:15]
Machine:oven2 4.13.0-37-generic x86_64 GNU/Linux

Nov 21 20:56:16 Claimed job
Nov 21 20:56:20 Reusing HOL
Nov 21 20:56:30 Starting developers/bin
Nov 21 20:57:04 Finished developers/bin                                          33s 202MB
Nov 21 20:57:05 Starting semantics/ffi
Nov 21 20:57:15 Finished semantics/ffi                                            9s 256MB
Nov 21 20:57:16 Starting semantics
Nov 21 20:58:30 Finished semantics                                             1m13s 965MB
Nov 21 20:58:31 Starting semantics/proofs
Nov 21 21:01:21 Finished semantics/proofs                                      2m49s   1GB
Nov 21 21:01:22 Starting basis/pure
Nov 21 21:02:11 Finished basis/pure                                              48s 648MB
Nov 21 21:02:12 Starting translator
Nov 21 21:05:16 Finished translator                                            3m03s 965MB
Nov 21 21:05:17 Starting compiler/parsing
Nov 21 21:06:33 Finished compiler/parsing                                      1m15s   1GB
Nov 21 21:06:34 Starting characteristic
Nov 21 21:09:01 Finished characteristic                                        2m26s   1GB
Nov 21 21:09:01 Starting translator/monadic
Nov 21 21:10:28 Finished translator/monadic                                    1m25s   1GB
Nov 21 21:10:29 Starting basis
Nov 21 21:26:49 Finished basis                                                16m19s   3GB
Nov 21 21:26:50 Starting compiler/inference
Nov 21 21:28:13 Finished compiler/inference                                    1m22s   1GB
Nov 21 21:28:14 Starting compiler/backend/reg_alloc
Nov 21 21:29:00 Finished compiler/backend/reg_alloc                              45s 929MB
Nov 21 21:29:01 Starting compiler/backend/gc
Nov 21 21:35:24 Finished compiler/backend/gc                                   6m22s   1GB
Nov 21 21:35:25 Starting compiler/backend
Nov 21 21:35:28 Finished compiler/backend                                         2s  22MB
Nov 21 21:35:29 Starting compiler/encoders/asm
Nov 21 21:35:30 Finished compiler/encoders/asm                                    0s  14MB
Nov 21 21:35:31 Starting compiler/encoders/x64
Nov 21 21:35:47 Finished compiler/encoders/x64                                   14s 416MB
Nov 21 21:35:48 Starting compiler/encoders/arm6
Nov 21 21:36:32 Finished compiler/encoders/arm6                                  43s 497MB
Nov 21 21:36:33 Starting compiler/encoders/arm8
Nov 21 21:36:41 Finished compiler/encoders/arm8                                   7s 328MB
Nov 21 21:36:42 Starting compiler/encoders/mips
Nov 21 21:36:51 Finished compiler/encoders/mips                                   8s 427MB
Nov 21 21:36:52 Starting compiler/encoders/riscv
Nov 21 21:37:00 Finished compiler/encoders/riscv                                  7s 380MB
Nov 21 21:37:01 Starting compiler/encoders/ag32
Nov 21 21:37:18 Finished compiler/encoders/ag32                                  15s 500MB
Nov 21 21:37:18 Starting compiler/backend/x64
Nov 21 21:37:35 Finished compiler/backend/x64                                    15s 741MB
Nov 21 21:37:36 Starting compiler/backend/arm6
Nov 21 21:37:55 Finished compiler/backend/arm6                                   18s   1GB
Nov 21 21:37:56 Starting compiler/backend/arm8
Nov 21 21:38:14 Finished compiler/backend/arm8                                   17s   1GB
Nov 21 21:38:15 Starting compiler/backend/mips
Nov 21 21:38:34 Finished compiler/backend/mips                                   18s   1GB
Nov 21 21:38:35 Starting compiler/backend/riscv
Nov 21 21:38:53 Finished compiler/backend/riscv                                  17s   1GB
Nov 21 21:38:54 Starting compiler/backend/ag32
Nov 21 21:40:08 Finished compiler/backend/ag32                                 1m12s 968MB
Nov 21 21:40:09 Starting compiler/parsing/proofs
Nov 21 21:46:14 Finished compiler/parsing/proofs                               6m04s 853MB
Nov 21 21:46:14 Starting compiler/inference/proofs
Nov 21 21:49:07 Finished compiler/inference/proofs                             2m52s   1GB
Nov 21 21:49:08 Starting compiler/backend/semantics
Nov 21 21:58:12 Finished compiler/backend/semantics                            9m03s   2GB
Nov 21 21:58:13 Starting compiler/backend/reg_alloc/proofs
Nov 21 22:00:56 Finished compiler/backend/reg_alloc/proofs                     2m42s 491MB
Nov 21 22:00:57 Starting compiler/backend/proofs
Nov 21 22:45:06 Finished compiler/backend/proofs                              44m07s   3GB
Nov 21 22:45:06 Starting compiler/encoders/x64/proofs
Nov 21 22:54:25 Finished compiler/encoders/x64/proofs                          9m18s 975MB
Nov 21 22:54:26 Starting compiler/encoders/arm6/proofs
Nov 21 23:08:32 Finished compiler/encoders/arm6/proofs                        14m04s   1GB
Nov 21 23:08:32 Starting compiler/encoders/arm8/proofs
Nov 21 23:14:29 Finished compiler/encoders/arm8/proofs                         5m56s   1GB
Nov 21 23:14:30 Starting compiler/encoders/mips/proofs
Nov 21 23:24:33 Finished compiler/encoders/mips/proofs                        10m02s   2GB
Nov 21 23:24:34 Starting compiler/encoders/riscv/proofs
Nov 21 23:32:33 Finished compiler/encoders/riscv/proofs                        7m58s 766MB
Nov 21 23:32:34 Starting compiler/encoders/ag32/proofs
Nov 21 23:35:20 Finished compiler/encoders/ag32/proofs                         2m45s 624MB
Nov 21 23:35:21 Starting compiler/backend/x64/proofs
Nov 21 23:35:41 Finished compiler/backend/x64/proofs                             19s   1GB
Nov 21 23:35:42 Starting compiler/backend/arm6/proofs
Nov 21 23:36:04 Finished compiler/backend/arm6/proofs                            20s   1GB
Nov 21 23:36:04 Starting compiler/backend/arm8/proofs
Nov 21 23:36:24 Finished compiler/backend/arm8/proofs                            19s   1GB
Nov 21 23:36:25 Starting compiler/backend/mips/proofs
Nov 21 23:36:46 Finished compiler/backend/mips/proofs                            19s   1GB
Nov 21 23:36:47 Starting compiler/backend/riscv/proofs
Nov 21 23:37:07 Finished compiler/backend/riscv/proofs                           19s   1GB
Nov 21 23:37:07 Starting compiler/backend/ag32/proofs
Nov 21 23:46:55 Finished compiler/backend/ag32/proofs                          9m46s   2GB
Nov 21 23:46:56 Starting compiler/proofs
Nov 21 23:48:16 Finished compiler/proofs                                       1m19s   2GB
Nov 21 23:48:16 Starting candle/set-theory
Nov 21 23:48:42 Finished candle/set-theory                                       24s 602MB
Nov 21 23:48:42 Starting candle/syntax-lib
Nov 21 23:48:52 Finished candle/syntax-lib                                        9s 670MB
Nov 21 23:48:53 Starting candle/standard/syntax
Nov 21 23:50:25 Finished candle/standard/syntax                                1m31s 537MB
Nov 21 23:50:25 Starting candle/standard/semantics
Nov 21 23:51:43 Finished candle/standard/semantics                             1m17s 811MB
Nov 21 23:51:44 Starting candle/standard/monadic
Nov 21 23:53:18 Finished candle/standard/monadic                               1m33s   1GB
Nov 21 23:53:19 Starting candle/standard/ml_kernel
Nov 22 00:08:53 Finished candle/standard/ml_kernel                            15m33s   3GB
Nov 22 00:08:53 Starting candle/standard/opentheory
Nov 22 00:16:45 Finished candle/standard/opentheory                            7m50s   2GB
Nov 22 00:16:46 Starting candle/standard/opentheory/compilation
Nov 22 00:46:48 Finished candle/standard/opentheory/compilation               30m01s  12GB
Nov 22 00:46:49 Starting candle/standard/opentheory/compilation/proofs
Nov 22 00:47:26 Finished candle/standard/opentheory/compilation/proofs           35s   4GB
Nov 22 00:47:27 Starting characteristic/examples
Nov 22 00:48:55 Finished characteristic/examples                               1m27s   1GB
Nov 22 00:48:56 Starting tutorial/solutions
Nov 22 01:02:26 Finished tutorial/solutions                                   13m28s   7GB
Nov 22 01:02:26 Starting translator/monadic/examples
Nov 22 01:04:12 Finished translator/monadic/examples                           1m44s   2GB
Nov 22 01:04:13 Starting examples
Nov 22 01:10:15 Finished examples                                              6m01s   2GB
Nov 22 01:10:15 Starting examples/compilation/x64
Nov 22 03:15:15 Finished examples/compilation/x64                           2h04m59s  10GB
Nov 22 03:15:16 Starting examples/compilation/x64/proofs
Nov 22 03:17:09 Finished examples/compilation/x64/proofs                       1m51s   3GB
Nov 22 03:17:10 Starting examples/compilation/ag32
Nov 22 03:44:05 Finished examples/compilation/ag32                            26m54s   3GB
Nov 22 03:44:05 Starting examples/compilation/ag32/proofs
Nov 22 03:44:30 Finished examples/compilation/ag32/proofs                        24s   2GB
Nov 22 03:44:31 Starting compiler/benchmarks
Nov 22 03:44:32 Finished compiler/benchmarks                                      0s   4MB
Nov 22 03:44:33 Starting translator/okasaki-examples
Nov 22 03:48:06 Finished translator/okasaki-examples                           3m32s   1GB
Nov 22 03:48:07 Starting translator/other-examples
Nov 22 03:51:26 Finished translator/other-examples                             3m18s 817MB
Nov 22 03:51:27 Starting compiler/parsing/tests
Nov 22 03:51:52 Finished compiler/parsing/tests                                  24s 312MB
Nov 22 03:51:53 Starting compiler/inference/tests
Nov 22 03:55:52 Finished compiler/inference/tests                              3m58s   4GB
Nov 22 03:55:53 Starting compiler/bootstrap/translation
Nov 22 07:04:37 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