Job 873

CakeML:494ff482b4d0a1cf9bc89b8d5708c38f1e51994c
  Extirpate intermediate theorem syntax [May 13 01:26:57]
#635 (thm)
Merging into:8f8560b3414274dcffa62719ba224df92d8cb039
  Merge pull request #651 from talsewell/translator_messages [May 15 03:55:41]
HOL:1557f72fc9a7a80bc5ce2e4df30afd51803c8b75
  Get formal-languages/regular to pass src tests again [May 09 11:06:43]
Machine:te1

May 15 10:10:41 Claimed job
May 15 10:10:45 Reusing HOL
May 15 10:11:34 Starting developers
May 15 10:11:37 Finished developers                                               2s  31MB
May 15 10:11:37 Starting developers/bin
May 15 10:11:43 Finished developers/bin                                           6s 931MB
May 15 10:11:43 Starting semantics/ffi
May 15 10:11:58 Finished semantics/ffi                                           13s 264MB
May 15 10:11:58 Starting semantics
May 15 10:13:50 Finished semantics                                             1m51s   1GB
May 15 10:13:50 Starting semantics/proofs
May 15 10:18:01 Finished semantics/proofs                                      4m11s   1GB
May 15 10:18:01 Starting basis/pure
May 15 10:19:07 Finished basis/pure                                            1m05s 687MB
May 15 10:19:07 Starting translator
May 15 10:21:27 Finished translator                                            2m19s   1GB
May 15 10:21:27 Starting compiler/parsing
May 15 10:22:49 Finished compiler/parsing                                      1m21s   2GB
May 15 10:22:49 Starting characteristic
May 15 10:30:08 Finished characteristic                                        7m19s   1GB
May 15 10:30:09 Starting translator/monadic
May 15 10:32:15 Finished translator/monadic                                    2m05s   1GB
May 15 10:32:15 Starting basis
May 15 10:55:11 Finished basis                                                22m56s   3GB
May 15 10:55:12 Starting compiler/inference
May 15 10:57:19 Finished compiler/inference                                    2m07s   1GB
May 15 10:57:19 Starting compiler/backend/reg_alloc
May 15 10:58:37 Finished compiler/backend/reg_alloc                            1m17s   1GB
May 15 10:58:37 Starting compiler/backend/gc
May 15 11:09:31 Finished compiler/backend/gc                                  10m53s   1GB
May 15 11:09:31 Starting compiler/backend
May 15 11:09:33 Finished compiler/backend                                         2s  33MB
May 15 11:09:33 Starting compiler/encoders/asm
May 15 11:09:34 Finished compiler/encoders/asm                                    1s  31MB
May 15 11:09:35 Starting compiler/encoders/x64
May 15 11:10:10 Finished compiler/encoders/x64                                   35s 714MB
May 15 11:10:10 Starting compiler/encoders/arm6
May 15 11:11:13 Finished compiler/encoders/arm6                                1m03s 776MB
May 15 11:11:13 Starting compiler/encoders/arm8
May 15 11:11:31 Finished compiler/encoders/arm8                                  17s 571MB
May 15 11:11:31 Starting compiler/encoders/mips
May 15 11:11:56 Finished compiler/encoders/mips                                  24s 988MB
May 15 11:11:56 Starting compiler/encoders/riscv
May 15 11:12:16 Finished compiler/encoders/riscv                                 19s 821MB
May 15 11:12:16 Starting compiler/encoders/ag32
May 15 11:12:41 Finished compiler/encoders/ag32                                  24s 735MB
May 15 11:12:41 Starting compiler/backend/x64
May 15 11:13:07 Finished compiler/backend/x64                                    25s 846MB
May 15 11:13:07 Starting compiler/backend/arm6
May 15 11:13:34 Finished compiler/backend/arm6                                   27s   1GB
May 15 11:13:34 Starting compiler/backend/arm8
May 15 11:13:59 Finished compiler/backend/arm8                                   24s 963MB
May 15 11:13:59 Starting compiler/backend/mips
May 15 11:14:24 Finished compiler/backend/mips                                   24s   1GB
May 15 11:14:24 Starting compiler/backend/riscv
May 15 11:14:49 Finished compiler/backend/riscv                                  25s   1GB
May 15 11:14:49 Starting compiler/backend/ag32
May 15 11:16:20 Finished compiler/backend/ag32                                 1m30s   1GB
May 15 11:16:20 Starting compiler/parsing/proofs
May 15 11:25:00 Finished compiler/parsing/proofs                               8m39s   1GB
May 15 11:25:00 Starting compiler/inference/proofs
May 15 11:28:52 Finished compiler/inference/proofs                             3m51s   1GB
May 15 11:28:52 Starting compiler/backend/semantics
May 15 11:38:04 Finished compiler/backend/semantics                            9m12s   2GB
May 15 11:38:04 Starting compiler/backend/reg_alloc/proofs
May 15 11:42:51 Finished compiler/backend/reg_alloc/proofs                     4m47s 908MB
May 15 11:42:52 Starting compiler/backend/proofs
May 15 12:33:09 Finished compiler/backend/proofs                              50m16s   5GB
May 15 12:33:09 Starting compiler/encoders/x64/proofs
May 15 12:45:24 Finished compiler/encoders/x64/proofs                         12m15s   4GB
May 15 12:45:24 Starting compiler/encoders/arm6/proofs
May 15 13:01:52 Finished compiler/encoders/arm6/proofs                        16m28s   3GB
May 15 13:01:52 Starting compiler/encoders/arm8/proofs
May 15 13:10:42 Finished compiler/encoders/arm8/proofs                         8m49s   1GB
May 15 13:10:42 Starting compiler/encoders/mips/proofs
May 15 13:23:02 Finished compiler/encoders/mips/proofs                        12m20s   3GB
May 15 13:23:02 Starting compiler/encoders/riscv/proofs
May 15 13:34:11 Finished compiler/encoders/riscv/proofs                       11m08s   1GB
May 15 13:34:11 Starting compiler/encoders/ag32/proofs
May 15 13:37:26 Finished compiler/encoders/ag32/proofs                         3m14s   1GB
May 15 13:37:26 Starting compiler/backend/x64/proofs
May 15 13:37:52 Finished compiler/backend/x64/proofs                             25s   1GB
May 15 13:37:52 Starting compiler/backend/arm6/proofs
May 15 13:38:19 Finished compiler/backend/arm6/proofs                            27s   1GB
May 15 13:38:19 Starting compiler/backend/arm8/proofs
May 15 13:38:46 Finished compiler/backend/arm8/proofs                            26s   1GB
May 15 13:38:46 Starting compiler/backend/mips/proofs
May 15 13:39:14 Finished compiler/backend/mips/proofs                            27s   1GB
May 15 13:39:14 Starting compiler/backend/riscv/proofs
May 15 13:39:40 Finished compiler/backend/riscv/proofs                           26s   1GB
May 15 13:39:41 Starting compiler/backend/ag32/proofs
May 15 13:51:48 Finished compiler/backend/ag32/proofs                         12m06s   2GB
May 15 13:51:48 Starting compiler/proofs
May 15 13:53:34 Finished compiler/proofs                                       1m46s   3GB
May 15 13:53:34 Starting candle/set-theory
May 15 13:54:11 Finished candle/set-theory                                       36s 785MB
May 15 13:54:11 Starting candle/syntax-lib
May 15 13:54:25 Finished candle/syntax-lib                                       13s 679MB
May 15 13:54:25 Starting candle/standard/syntax
May 15 13:56:47 Finished candle/standard/syntax                                2m22s   1GB
May 15 13:56:48 Starting candle/standard/semantics
May 15 13:59:04 Finished candle/standard/semantics                             2m16s   2GB
May 15 13:59:04 Starting candle/standard/monadic
May 15 14:01:15 Finished candle/standard/monadic                               2m10s   1GB
May 15 14:01:15 Starting candle/standard/ml_kernel
May 15 14:06:23 Finished candle/standard/ml_kernel                             5m07s   3GB
May 15 14:06:23 Starting candle/standard/opentheory
May 15 14:17:43 Finished candle/standard/opentheory                           11m19s   4GB
May 15 14:17:43 Starting candle/standard/opentheory/compilation
May 15 14:54:07 Finished candle/standard/opentheory/compilation               36m23s  16GB
May 15 14:54:07 Starting candle/standard/opentheory/compilation/proofs
May 15 14:54:57 Finished candle/standard/opentheory/compilation/proofs           49s   2GB
May 15 14:54:57 Starting characteristic/examples
May 15 14:56:46 Finished characteristic/examples                               1m49s   2GB
May 15 14:56:46 Starting tutorial/solutions
May 15 15:13:44 Finished tutorial/solutions                                   16m57s   7GB
May 15 15:13:45 Starting translator/monadic/examples
May 15 15:17:22 Finished translator/monadic/examples                           3m37s   2GB
May 15 15:17:22 Starting examples
May 15 15:27:26 Finished examples                                             10m03s   4GB
May 15 15:27:26 Starting examples/compilation/x64
May 15 18:07:17 Finished examples/compilation/x64                           2h39m50s  10GB
May 15 18:07:17 Starting examples/compilation/x64/proofs
May 15 18:09:16 Finished examples/compilation/x64/proofs                       1m59s   2GB
May 15 18:09:17 Starting examples/compilation/ag32
May 15 18:47:18 Finished examples/compilation/ag32                            38m01s   4GB
May 15 18:47:18 Starting examples/compilation/ag32/proofs
May 15 18:48:32 Finished examples/compilation/ag32/proofs                      1m13s   2GB
May 15 18:48:32 Starting translator/okasaki-examples
May 15 18:53:56 Finished translator/okasaki-examples                           5m24s   1GB
May 15 18:53:57 Starting translator/other-examples
May 15 18:54:51 Finished translator/other-examples                               54s   1GB
May 15 18:54:51 Starting compiler/parsing/tests
May 15 18:55:26 Finished compiler/parsing/tests                                  35s 630MB
May 15 18:55:26 Starting compiler/inference/tests
May 15 19:00:42 Finished compiler/inference/tests                              5m15s   3GB
May 15 19:00:42 Starting compiler/bootstrap/translation
May 15 19:19:10 FAILED: compiler/bootstrap/translation
]0;Holmake: .]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/arm/model]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/common]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/machine-code/hoare-triple]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/common]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/common[1mWorking in $(HOLDIR)/examples/l3-machine-code/common[0m
]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/arm/model]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/lib]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/lib[1mWorking in $(HOLDIR)/examples/l3-machine-code/lib[0m
]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/arm/model]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/arm/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/model[0m
]0;Holmake: .]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/arm8/model]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/arm8/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm8/model[0m
]0;Holmake: .]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/mips/model]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/mips/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/mips/model[0m
]0;Holmake: .]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/riscv/model]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/riscv/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/riscv/model[0m
]0;Holmake: .]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/x64/model]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/x64/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/x64/model[0m
]0;Holmake: .]0;Holmake: ~/regression-worker/cakeml-873/basis]0;Holmake: ~/regression-worker/cakeml-873/basis/pure]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/balanced_bst]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: ~/regression-worker/cakeml-873/basis/pure]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/formal-languages/regular]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/formal-languages]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/formal-languages/regular]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ~/regression-worker/cakeml-873/basis/pure]0;Holmake: ~/regression-worker/cakeml-873/misc]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression-worker/cakeml-873/misc]0;Holmake: ~/regression-worker/cakeml-873/developers]0;Holmake: ~/regression-worker/cakeml-873/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression-worker/cakeml-873/misc]0;Holmake: ~/regression-worker/cakeml-873/misc/lem_lib_stub]0;Holmake: ~/regression-worker/cakeml-873/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression-worker/cakeml-873/misc]0;Holmake: ~/regression-worker/cakeml-873/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression-worker/cakeml-873/basis/pure]0;Holmake: ~/regression-worker/cakeml-873/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ~/regression-worker/cakeml-873/basis]0;Holmake: ~/regression-worker/cakeml-873/characteristic]0;Holmake: ~/regression-worker/cakeml-873/compiler/parsing]0;Holmake: ~/regression-worker/cakeml-873/semantics]0;Holmake: ~/regression-worker/cakeml-873/semantics/ffi]0;Holmake: ~/regression-worker/cakeml-873/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression-worker/cakeml-873/semantics]0;Holmake: ~/regression-worker/cakeml-873/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression-worker/cakeml-873/compiler/parsing]0;Holmake: ~/regression-worker/cakeml-873/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/regression-worker/cakeml-873/characteristic]0;Holmake: ~/regression-worker/cakeml-873/semantics/proofs]0;Holmake: ~/regression-worker/cakeml-873/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ~/regression-worker/cakeml-873/characteristic]0;Holmake: ~/regression-worker/cakeml-873/translator]0;Holmake: ~/regression-worker/cakeml-873/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/regression-worker/cakeml-873/characteristic]0;Holmake: ~/regression-worker/cakeml-873/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ~/regression-worker/cakeml-873/basis]0;Holmake: ~/regression-worker/cakeml-873/translator/monadic]0;Holmake: ~/regression-worker/cakeml-873/translator/monadic/monad_base]0;Holmake: ~/regression-worker/cakeml-873/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ~/regression-worker/cakeml-873/translator/monadic]0;Holmake: ~/regression-worker/cakeml-873/translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ~/regression-worker/cakeml-873/basis]0;Holmake: ~/regression-worker/cakeml-873/basis[1mWorking in $(CAKEMLDIR)/basis[0m
]0;Holmake: .]0;Holmake: ../..]0;Holmake: ../../backend]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/machine-code/multiword]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/machine-code/multiword[1mWorking in $(HOLDIR)/examples/machine-code/multiword[0m
]0;Holmake: ../../backend]0;Holmake: ../../backend/reg_alloc]0;Holmake: ~/regression-worker/cakeml-873/unverified/reg_alloc]0;Holmake: ~/regression-worker/cakeml-873/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-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/arm/step]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/machine-code/decompiler]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/machine-code/decompiler[1mWorking in $(HOLDIR)/examples/machine-code/decompiler[0m
]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code[1mWorking in $(HOLDIR)/examples/l3-machine-code[0m
]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/arm/step]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/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-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/arm8/step]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/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-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/mips/step]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/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-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/riscv/step]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/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-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/l3-machine-code/x64/step]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/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-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/unification/triangular/first-order]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/unification/triangular]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/unification/triangular[1mWorking in $(HOLDIR)/examples/unification/triangular[0m
]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/examples/unification/triangular/first-order]0;Holmake: ~/regression-worker/HOL-1557f72fc9a7a80bc5ce2e4df30afd51803c8b75/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: ../../encoders/monadic_enc]0;Holmake: ../../encoders/monadic_enc[1mWorking in $(CAKEMLDIR)/compiler/encoders/monadic_enc[0m
Starting work on monadic_encTheory
Starting work on README.md
README.md                                                                    OK
monadic_encTheory                                                            OK
Starting work on monadic_enc32Theory
Starting work on monadic_enc64Theory
monadic_enc32Theory                                                          OK
monadic_enc64Theory                                                          OK
]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 to_flatProgTheory
Starting work on README.md
README.md                                                                    OK
to_flatProgTheory                                                            OK
Starting work on to_patProgTheory
to_patProgTheory                                                             OK
Starting work on to_closProgTheory
to_closProgTheory                                                   FAILED! <1>
 
 Saved theorem _____ "clos_annotate_shift_v_thm"
 error in quse /usr/local/google/home/ramanakumar/regression-worker/cakeml-873/compiler/bootstrap/translation/to_closProgScript.sml : HOL_ERR {message = "by's tactic failed to prove subgoal on line 257", origin_function = "by", origin_structure = "BasicProvers"}
 error in load to_closProgScript : HOL_ERR {message = "by's tactic failed to prove subgoal on line 257", origin_function = "by", origin_structure = "BasicProvers"}
 Proof of 
 
 a b c d. clos_annotate_shift_side a b c d  T
 
 failed.
 Uncaught exception: HOL_ERR {message = "by's tactic failed to prove subgoal on line 257", origin_function = "by", origin_structure = "BasicProvers"}