Job 897

CakeML:fd7db02fddc5af0030bd92c78f3e4f3ff535e22b
  Merge remote-tracking branch 'origin/master' into cleanup [May 23 16:40:36]
#653 (cleanup)
Merging into:21975585998034b43aee723e21c7043f250a58fd
  Merge pull request #635 from CakeML/thm [May 22 08:49:19]
HOL:08cf0f71293ee2ed21e3c2667ecbb0a9d211be18
  Add regression tests for find_consts [May 24 06:22:28]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

May 24 07:55:22 Claimed job
May 24 07:55:29 Building HOL
May 24 08:03:21 Starting developers
May 24 08:03:22 Finished developers                                               0s  38MB
May 24 08:03:24 Starting developers/bin
May 24 08:08:06 Finished developers/bin                                        4m41s 207MB
May 24 08:08:07 Starting semantics/ffi
May 24 08:08:42 Finished semantics/ffi                                           33s 398MB
May 24 08:08:43 Starting semantics
May 24 08:10:13 Finished semantics                                             1m29s 827MB
May 24 08:10:16 Starting semantics/proofs
May 24 08:13:12 Finished semantics/proofs                                      2m55s   1GB
May 24 08:13:13 Starting basis/pure
May 24 08:16:46 Finished basis/pure                                            3m27s 710MB
May 24 08:16:49 Starting translator
May 24 08:18:28 Finished translator                                            1m36s   1GB
May 24 08:18:32 Starting compiler/parsing
May 24 08:19:31 Finished compiler/parsing                                        57s   2GB
May 24 08:19:31 Starting characteristic
May 24 08:24:38 Finished characteristic                                        5m07s   1GB
May 24 08:24:39 Starting translator/monadic
May 24 08:26:03 Finished translator/monadic                                    1m23s   1GB
May 24 08:26:03 Starting basis
May 24 08:42:56 Finished basis                                                16m52s   3GB
May 24 08:42:56 Starting compiler/inference
May 24 08:44:41 Finished compiler/inference                                    1m44s   1GB
May 24 08:44:41 Starting compiler/backend/reg_alloc
May 24 08:45:38 Finished compiler/backend/reg_alloc                              57s   1GB
May 24 08:45:39 Starting compiler/backend/gc
May 24 08:54:32 Finished compiler/backend/gc                                   8m52s   2GB
May 24 08:54:32 Starting compiler/backend
May 24 08:54:33 Finished compiler/backend                                         0s  43MB
May 24 08:54:33 Starting compiler/encoders/asm
May 24 08:54:33 Finished compiler/encoders/asm                                    0s  36MB
May 24 08:54:34 Starting compiler/encoders/x64
May 24 08:55:30 Finished compiler/encoders/x64                                   55s 705MB
May 24 08:55:30 Starting compiler/encoders/arm6
May 24 08:57:04 Finished compiler/encoders/arm6                                1m33s   1GB
May 24 08:57:05 Starting compiler/encoders/arm8
May 24 08:57:34 Finished compiler/encoders/arm8                                  29s 654MB
May 24 08:57:34 Starting compiler/encoders/mips
May 24 08:58:38 Finished compiler/encoders/mips                                1m03s 840MB
May 24 08:58:39 Starting compiler/encoders/riscv
May 24 08:59:54 Finished compiler/encoders/riscv                               1m14s 829MB
May 24 08:59:54 Starting compiler/encoders/ag32
May 24 09:00:09 Finished compiler/encoders/ag32                                  14s 611MB
May 24 09:00:09 Starting compiler/backend/x64
May 24 09:00:25 Finished compiler/backend/x64                                    15s   1GB
May 24 09:00:25 Starting compiler/backend/arm6
May 24 09:00:43 Finished compiler/backend/arm6                                   17s   1GB
May 24 09:00:43 Starting compiler/backend/arm8
May 24 09:00:59 Finished compiler/backend/arm8                                   15s   1GB
May 24 09:00:59 Starting compiler/backend/mips
May 24 09:01:16 Finished compiler/backend/mips                                   16s   1GB
May 24 09:01:16 Starting compiler/backend/riscv
May 24 09:01:31 Finished compiler/backend/riscv                                  15s   1GB
May 24 09:01:32 Starting compiler/backend/ag32
May 24 09:02:38 Finished compiler/backend/ag32                                 1m05s   1GB
May 24 09:02:38 Starting compiler/parsing/proofs
May 24 09:08:07 Finished compiler/parsing/proofs                               5m28s 851MB
May 24 09:08:07 Starting compiler/inference/proofs
May 24 09:10:42 Finished compiler/inference/proofs                             2m34s 802MB
May 24 09:10:43 Starting compiler/backend/semantics
May 24 09:17:35 Finished compiler/backend/semantics                            6m52s   2GB
May 24 09:17:36 Starting compiler/backend/reg_alloc/proofs
May 24 09:20:53 Finished compiler/backend/reg_alloc/proofs                     3m16s 766MB
May 24 09:20:53 Starting compiler/backend/proofs
May 24 09:57:59 Finished compiler/backend/proofs                              37m05s   3GB
May 24 09:57:59 Starting compiler/encoders/x64/proofs
May 24 10:07:59 Finished compiler/encoders/x64/proofs                          9m59s   5GB
May 24 10:07:59 Starting compiler/encoders/arm6/proofs
May 24 10:21:29 Finished compiler/encoders/arm6/proofs                        13m29s   3GB
May 24 10:21:29 Starting compiler/encoders/arm8/proofs
May 24 10:28:03 Finished compiler/encoders/arm8/proofs                         6m32s   1GB
May 24 10:28:03 Starting compiler/encoders/mips/proofs
May 24 10:37:46 Finished compiler/encoders/mips/proofs                         9m43s   3GB
May 24 10:37:47 Starting compiler/encoders/riscv/proofs
May 24 10:45:54 Finished compiler/encoders/riscv/proofs                        8m07s   1GB
May 24 10:45:55 Starting compiler/encoders/ag32/proofs
May 24 10:48:21 Finished compiler/encoders/ag32/proofs                         2m26s 713MB
May 24 10:48:22 Starting compiler/backend/x64/proofs
May 24 10:48:38 Finished compiler/backend/x64/proofs                             16s   1GB
May 24 10:48:38 Starting compiler/backend/arm6/proofs
May 24 10:48:58 Finished compiler/backend/arm6/proofs                            19s 824MB
May 24 10:48:58 Starting compiler/backend/arm8/proofs
May 24 10:49:14 Finished compiler/backend/arm8/proofs                            15s   1GB
May 24 10:49:14 Starting compiler/backend/mips/proofs
May 24 10:49:30 Finished compiler/backend/mips/proofs                            16s   1GB
May 24 10:49:31 Starting compiler/backend/riscv/proofs
May 24 10:49:47 Finished compiler/backend/riscv/proofs                           16s   1GB
May 24 10:49:47 Starting compiler/backend/ag32/proofs
May 24 10:58:39 Finished compiler/backend/ag32/proofs                          8m51s   2GB
May 24 10:58:40 Starting compiler/proofs
May 24 11:00:06 Finished compiler/proofs                                       1m26s   2GB
May 24 11:00:07 Starting candle/set-theory
May 24 11:00:31 Finished candle/set-theory                                       24s 767MB
May 24 11:00:32 Starting candle/syntax-lib
May 24 11:00:41 Finished candle/syntax-lib                                        8s 663MB
May 24 11:00:41 Starting candle/standard/syntax
May 24 11:02:21 Finished candle/standard/syntax                                1m39s 877MB
May 24 11:02:21 Starting candle/standard/semantics
May 24 11:03:54 Finished candle/standard/semantics                             1m32s   1GB
May 24 11:03:54 Starting candle/standard/monadic
May 24 11:05:25 Finished candle/standard/monadic                               1m31s   1GB
May 24 11:05:26 Starting candle/standard/ml_kernel
May 24 11:09:10 Finished candle/standard/ml_kernel                             3m43s   5GB
May 24 11:09:10 Starting candle/standard/opentheory
May 24 11:17:30 Finished candle/standard/opentheory                            8m20s   3GB
May 24 11:17:31 Starting candle/standard/opentheory/compilation
May 24 11:45:27 Finished candle/standard/opentheory/compilation               27m56s  13GB
May 24 11:45:28 Starting candle/standard/opentheory/compilation/proofs
May 24 11:46:02 Finished candle/standard/opentheory/compilation/proofs           34s   3GB
May 24 11:46:02 Starting characteristic/examples
May 24 11:47:26 Finished characteristic/examples                               1m22s   1GB
May 24 11:47:26 Starting tutorial/solutions
May 24 12:00:20 Finished tutorial/solutions                                   12m54s   6GB
May 24 12:00:20 Starting translator/monadic/examples
May 24 12:03:07 Finished translator/monadic/examples                           2m45s   2GB
May 24 12:03:07 Starting examples
May 24 12:11:45 Finished examples                                              8m37s   4GB
May 24 12:11:45 Starting examples/compilation/x64
May 24 14:10:45 Finished examples/compilation/x64                           1h58m58s  15GB
May 24 14:10:45 Starting examples/compilation/x64/proofs
May 24 14:12:09 Finished examples/compilation/x64/proofs                       1m23s   2GB
May 24 14:12:09 Starting examples/compilation/ag32
May 24 14:39:50 Finished examples/compilation/ag32                            27m40s   6GB
May 24 14:39:51 Starting examples/compilation/ag32/proofs
May 24 14:40:46 Finished examples/compilation/ag32/proofs                        54s   3GB
May 24 14:40:46 Starting translator/okasaki-examples
May 24 14:44:46 Finished translator/okasaki-examples                           3m59s   1GB
May 24 14:44:46 Starting translator/other-examples
May 24 14:48:03 Finished translator/other-examples                             3m16s   1GB
May 24 14:48:03 Starting compiler/parsing/tests
May 24 14:48:28 Finished compiler/parsing/tests                                  24s 522MB
May 24 14:48:28 Starting compiler/inference/tests
May 24 14:52:35 Finished compiler/inference/tests                              4m06s   4GB
May 24 14:52:35 Starting compiler/bootstrap/translation
May 24 16:50:49 FAILED: compiler/bootstrap/translation
]0;Holmake: .]0;Holmake: ~/regression/HOL-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/examples/l3-machine-code/arm/model]0;Holmake: ~/regression/HOL-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/examples/l3-machine-code/common]0;Holmake: ~/regression/HOL-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/regression/HOL-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/examples/l3-machine-code/common]0;Holmake: ~/regression/HOL-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/examples/l3-machine-code/common[1mWorking in $(HOLDIR)/examples/l3-machine-code/common[0m
]0;Holmake: ~/regression/HOL-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/examples/l3-machine-code/arm/model]0;Holmake: ~/regression/HOL-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/examples/l3-machine-code/lib]0;Holmake: ~/regression/HOL-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/examples/l3-machine-code/lib[1mWorking in $(HOLDIR)/examples/l3-machine-code/lib[0m
]0;Holmake: ~/regression/HOL-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/examples/l3-machine-code/arm/model]0;Holmake: ~/regression/HOL-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/examples/l3-machine-code/arm/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/model[0m
]0;Holmake: .]0;Holmake: ~/regression/HOL-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/examples/l3-machine-code/arm8/model]0;Holmake: ~/regression/HOL-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/examples/l3-machine-code/arm8/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm8/model[0m
]0;Holmake: .]0;Holmake: ~/regression/HOL-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/examples/l3-machine-code/mips/model]0;Holmake: ~/regression/HOL-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/examples/l3-machine-code/mips/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/mips/model[0m
]0;Holmake: .]0;Holmake: ~/regression/HOL-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/examples/l3-machine-code/riscv/model]0;Holmake: ~/regression/HOL-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/examples/l3-machine-code/riscv/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/riscv/model[0m
]0;Holmake: .]0;Holmake: ~/regression/HOL-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/examples/l3-machine-code/x64/model]0;Holmake: ~/regression/HOL-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/examples/l3-machine-code/x64/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/x64/model[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-897/basis]0;Holmake: ~/regression/cakeml-897/basis/pure]0;Holmake: ~/regression/HOL-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/examples/balanced_bst]0;Holmake: ~/regression/HOL-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: ~/regression/cakeml-897/basis/pure]0;Holmake: ~/regression/HOL-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/examples/formal-languages]0;Holmake: ~/regression/HOL-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ~/regression/cakeml-897/basis/pure]0;Holmake: ~/regression/cakeml-897/misc]0;Holmake: ~/regression/HOL-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-897/misc]0;Holmake: ~/regression/cakeml-897/developers]0;Holmake: ~/regression/cakeml-897/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-897/misc]0;Holmake: ~/regression/cakeml-897/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-897/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-897/misc]0;Holmake: ~/regression/cakeml-897/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression/cakeml-897/basis/pure]0;Holmake: ~/regression/cakeml-897/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ~/regression/cakeml-897/basis]0;Holmake: ~/regression/cakeml-897/characteristic]0;Holmake: ~/regression/cakeml-897/compiler/parsing]0;Holmake: ~/regression/cakeml-897/semantics]0;Holmake: ~/regression/cakeml-897/semantics/ffi]0;Holmake: ~/regression/cakeml-897/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-897/semantics]0;Holmake: ~/regression/cakeml-897/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression/cakeml-897/compiler/parsing]0;Holmake: ~/regression/cakeml-897/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/regression/cakeml-897/characteristic]0;Holmake: ~/regression/cakeml-897/semantics/proofs]0;Holmake: ~/regression/cakeml-897/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ~/regression/cakeml-897/characteristic]0;Holmake: ~/regression/cakeml-897/translator]0;Holmake: ~/regression/cakeml-897/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/regression/cakeml-897/characteristic]0;Holmake: ~/regression/cakeml-897/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ~/regression/cakeml-897/basis]0;Holmake: ~/regression/cakeml-897/translator/monadic]0;Holmake: ~/regression/cakeml-897/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-897/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ~/regression/cakeml-897/translator/monadic]0;Holmake: ~/regression/cakeml-897/translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ~/regression/cakeml-897/basis]0;Holmake: ~/regression/cakeml-897/basis[1mWorking in $(CAKEMLDIR)/basis[0m
]0;Holmake: .]0;Holmake: ../..]0;Holmake: ../../backend]0;Holmake: ~/regression/HOL-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/examples/machine-code/multiword]0;Holmake: ~/regression/HOL-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/examples/machine-code/multiword[1mWorking in $(HOLDIR)/examples/machine-code/multiword[0m
]0;Holmake: ../../backend]0;Holmake: ../../backend/reg_alloc]0;Holmake: ~/regression/cakeml-897/unverified/reg_alloc]0;Holmake: ~/regression/cakeml-897/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-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/examples/l3-machine-code/arm/step]0;Holmake: ~/regression/HOL-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/examples/l3-machine-code]0;Holmake: ~/regression/HOL-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/examples/machine-code/decompiler]0;Holmake: ~/regression/HOL-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/examples/machine-code/decompiler[1mWorking in $(HOLDIR)/examples/machine-code/decompiler[0m
]0;Holmake: ~/regression/HOL-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/examples/l3-machine-code]0;Holmake: ~/regression/HOL-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/examples/l3-machine-code[1mWorking in $(HOLDIR)/examples/l3-machine-code[0m
]0;Holmake: ~/regression/HOL-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/examples/l3-machine-code/arm/step]0;Holmake: ~/regression/HOL-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/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-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/examples/l3-machine-code/arm8/step]0;Holmake: ~/regression/HOL-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/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-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/examples/l3-machine-code/mips/step]0;Holmake: ~/regression/HOL-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/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-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/examples/l3-machine-code/riscv/step]0;Holmake: ~/regression/HOL-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/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-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/examples/l3-machine-code/x64/step]0;Holmake: ~/regression/HOL-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/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-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/examples/unification/triangular/first-order]0;Holmake: ~/regression/HOL-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/examples/unification/triangular]0;Holmake: ~/regression/HOL-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/examples/unification/triangular[1mWorking in $(HOLDIR)/examples/unification/triangular[0m
]0;Holmake: ~/regression/HOL-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/examples/unification/triangular/first-order]0;Holmake: ~/regression/HOL-08cf0f71293ee2ed21e3c2667ecbb0a9d211be18/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_enc64Theory                                 OK
monadic_enc32Theory                                 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                                   OK
Starting work on to_bvlProgTheory
to_bvlProgTheory                                    OK
Starting work on to_bviProgTheory
to_bviProgTheory                                    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_target32ProgTheory                               OK
Starting work on arm6ProgTheory
to_target64ProgTheory                               OK
Starting work on x64ProgTheory
x64ProgTheory                                       OK
Starting work on arm8ProgTheory
arm6ProgTheory                                      OK
Starting work on ag32ProgTheory
ag32ProgTheory                             FAILED! <1>
      pred_setTheory.IN_INSERT,
      pred_setTheory.NOT_IN_EMPTY,
      wordsTheory.WORD_LO,
      wordsTheory.word_abs_def,
      wordsTheory.WORD_LE,
      ...
      ]
 error in quse /home/myreen/regression/cakeml-897/compiler/bootstrap/translation/ag32ProgScript.sml : Fail "Static Errors"
 error in load ag32ProgScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"
arm8ProgTheory                                M-KILLED