Job 832

CakeML:e7f489f382b8a8555eb803037b368a9a8c7621a0
  Fix monadic encoder hash function to include FMA instruction [May 02 13:25:22]
#633 (FMA_support)
Merging into:62c51fa831d455390795c47c53f56b050a23f7ad
  Merge pull request #627 from CakeML/monadic-trans-cleanup [Apr 27 07:20:55]
HOL:6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed
  Make hol-horizontal (M-h 3 or M-h H w/horizontal) have 80 col window [May 01 23:38:18]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

May 02 13:35:09 Claimed job
May 02 13:35:14 Reusing HOL
May 02 13:35:18 Starting developers
May 02 13:35:19 Finished developers                                               0s  22MB
May 02 13:35:20 Starting developers/bin
May 02 13:35:54 Finished developers/bin                                          34s 144MB
May 02 13:35:55 Starting semantics/ffi
May 02 13:36:02 Finished semantics/ffi                                            7s 232MB
May 02 13:36:03 Starting semantics
May 02 13:37:20 Finished semantics                                             1m17s   1GB
May 02 13:37:21 Starting semantics/proofs
May 02 13:40:18 Finished semantics/proofs                                      2m56s   1GB
May 02 13:40:18 Starting basis/pure
May 02 13:41:02 Finished basis/pure                                              44s 647MB
May 02 13:41:03 Starting translator
May 02 13:42:39 Finished translator                                            1m35s   1GB
May 02 13:42:39 Starting compiler/parsing
May 02 13:43:36 Finished compiler/parsing                                        56s   2GB
May 02 13:43:37 Starting characteristic
May 02 13:48:44 Finished characteristic                                        5m06s   1GB
May 02 13:48:44 Starting translator/monadic
May 02 13:50:11 Finished translator/monadic                                    1m25s   1GB
May 02 13:50:11 Starting basis
May 02 14:06:45 Finished basis                                                16m33s   3GB
May 02 14:06:45 Starting compiler/inference
May 02 14:08:18 Finished compiler/inference                                    1m31s   1GB
May 02 14:08:18 Starting compiler/backend/reg_alloc
May 02 14:09:16 Finished compiler/backend/reg_alloc                              57s   1GB
May 02 14:09:16 Starting compiler/backend/gc
May 02 14:17:08 Finished compiler/backend/gc                                   7m51s   1GB
May 02 14:17:08 Starting compiler/backend
May 02 14:17:09 Finished compiler/backend                                         0s  43MB
May 02 14:17:10 Starting compiler/encoders/asm
May 02 14:17:10 Finished compiler/encoders/asm                                    0s  32MB
May 02 14:17:11 Starting compiler/encoders/x64
May 02 14:17:33 Finished compiler/encoders/x64                                   21s 948MB
May 02 14:17:33 Starting compiler/encoders/arm6
May 02 14:18:16 Finished compiler/encoders/arm6                                  42s 695MB
May 02 14:18:16 Starting compiler/encoders/arm8
May 02 14:18:28 Finished compiler/encoders/arm8                                  11s 569MB
May 02 14:18:29 Starting compiler/encoders/mips
May 02 14:18:44 Finished compiler/encoders/mips                                  15s 842MB
May 02 14:18:45 Starting compiler/encoders/riscv
May 02 14:18:58 Finished compiler/encoders/riscv                                 12s 796MB
May 02 14:18:58 Starting compiler/encoders/ag32
May 02 14:19:13 Finished compiler/encoders/ag32                                  14s 496MB
May 02 14:19:13 Starting compiler/backend/x64
May 02 14:19:29 Finished compiler/backend/x64                                    15s   1GB
May 02 14:19:29 Starting compiler/backend/arm6
May 02 14:19:46 Finished compiler/backend/arm6                                   16s   1GB
May 02 14:19:46 Starting compiler/backend/arm8
May 02 14:20:03 Finished compiler/backend/arm8                                   16s   1GB
May 02 14:20:03 Starting compiler/backend/mips
May 02 14:20:20 Finished compiler/backend/mips                                   16s   1GB
May 02 14:20:21 Starting compiler/backend/riscv
May 02 14:20:38 Finished compiler/backend/riscv                                  16s   1GB
May 02 14:20:38 Starting compiler/backend/ag32
May 02 14:21:44 Finished compiler/backend/ag32                                 1m05s   1GB
May 02 14:21:44 Starting compiler/parsing/proofs
May 02 14:27:16 Finished compiler/parsing/proofs                               5m31s   1GB
May 02 14:27:16 Starting compiler/inference/proofs
May 02 14:29:55 Finished compiler/inference/proofs                             2m38s   1GB
May 02 14:29:56 Starting compiler/backend/semantics
May 02 14:36:56 Finished compiler/backend/semantics                            6m59s   1GB
May 02 14:36:56 Starting compiler/backend/reg_alloc/proofs
May 02 14:40:07 Finished compiler/backend/reg_alloc/proofs                     3m11s 724MB
May 02 14:40:08 Starting compiler/backend/proofs
May 02 15:18:16 Finished compiler/backend/proofs                              38m07s   4GB
May 02 15:18:16 Starting compiler/encoders/x64/proofs
May 02 15:27:17 Finished compiler/encoders/x64/proofs                          9m00s   4GB
May 02 15:27:17 Starting compiler/encoders/arm6/proofs
May 02 15:39:29 Finished compiler/encoders/arm6/proofs                        12m11s   3GB
May 02 15:39:30 Starting compiler/encoders/arm8/proofs
May 02 15:45:57 Finished compiler/encoders/arm8/proofs                         6m26s   1GB
May 02 15:45:57 Starting compiler/encoders/mips/proofs
May 02 15:55:06 Finished compiler/encoders/mips/proofs                         9m08s   3GB
May 02 15:55:06 Starting compiler/encoders/riscv/proofs
May 02 16:03:25 Finished compiler/encoders/riscv/proofs                        8m18s 996MB
May 02 16:03:25 Starting compiler/encoders/ag32/proofs
May 02 16:05:53 Finished compiler/encoders/ag32/proofs                         2m26s 618MB
May 02 16:05:53 Starting compiler/backend/x64/proofs
May 02 16:06:09 Finished compiler/backend/x64/proofs                             15s 756MB
May 02 16:06:10 Starting compiler/backend/arm6/proofs
May 02 16:06:30 Finished compiler/backend/arm6/proofs                            19s   1GB
May 02 16:06:30 Starting compiler/backend/arm8/proofs
May 02 16:06:46 Finished compiler/backend/arm8/proofs                            15s   1GB
May 02 16:06:47 Starting compiler/backend/mips/proofs
May 02 16:07:03 Finished compiler/backend/mips/proofs                            16s   1GB
May 02 16:07:04 Starting compiler/backend/riscv/proofs
May 02 16:07:21 Finished compiler/backend/riscv/proofs                           16s   1GB
May 02 16:07:21 Starting compiler/backend/ag32/proofs
May 02 16:16:14 Finished compiler/backend/ag32/proofs                          8m52s   2GB
May 02 16:16:15 Starting compiler/proofs
May 02 16:18:40 Finished compiler/proofs                                       2m24s   3GB
May 02 16:18:40 Starting candle/set-theory
May 02 16:19:05 Finished candle/set-theory                                       24s 660MB
May 02 16:19:05 Starting candle/syntax-lib
May 02 16:19:15 Finished candle/syntax-lib                                        9s 631MB
May 02 16:19:15 Starting candle/standard/syntax
May 02 16:20:54 Finished candle/standard/syntax                                1m38s   1GB
May 02 16:20:54 Starting candle/standard/semantics
May 02 16:22:27 Finished candle/standard/semantics                             1m32s   1GB
May 02 16:22:27 Starting candle/standard/monadic
May 02 16:23:59 Finished candle/standard/monadic                               1m31s   1GB
May 02 16:23:59 Starting candle/standard/ml_kernel
May 02 16:27:41 Finished candle/standard/ml_kernel                             3m41s   5GB
May 02 16:27:41 Starting candle/standard/opentheory
May 02 16:36:10 Finished candle/standard/opentheory                            8m28s   3GB
May 02 16:36:11 Starting candle/standard/opentheory/compilation
May 02 17:05:39 Finished candle/standard/opentheory/compilation               29m28s  11GB
May 02 17:05:40 Starting candle/standard/opentheory/compilation/proofs
May 02 17:06:40 Finished candle/standard/opentheory/compilation/proofs           59s   2GB
May 02 17:06:40 Starting characteristic/examples
May 02 17:08:01 Finished characteristic/examples                               1m20s   2GB
May 02 17:08:01 Starting tutorial/solutions
May 02 17:20:42 Finished tutorial/solutions                                   12m39s   6GB
May 02 17:20:42 Starting translator/monadic/examples
May 02 17:23:30 Finished translator/monadic/examples                           2m47s   2GB
May 02 17:23:30 Starting examples
May 02 17:31:44 Finished examples                                              8m13s   3GB
May 02 17:31:44 Starting examples/compilation/x64
May 02 19:23:57 Finished examples/compilation/x64                           1h52m12s  10GB
May 02 19:23:58 Starting examples/compilation/x64/proofs
May 02 19:25:20 Finished examples/compilation/x64/proofs                       1m21s   2GB
May 02 19:25:20 Starting examples/compilation/ag32
May 02 19:53:05 Finished examples/compilation/ag32                            27m45s   5GB
May 02 19:53:06 Starting examples/compilation/ag32/proofs
May 02 19:53:51 Finished examples/compilation/ag32/proofs                        45s   3GB
May 02 19:53:52 Starting translator/okasaki-examples
May 02 19:57:54 Finished translator/okasaki-examples                           4m01s   1GB
May 02 19:57:54 Starting translator/other-examples
May 02 20:01:13 Finished translator/other-examples                             3m18s   1GB
May 02 20:01:13 Starting compiler/parsing/tests
May 02 20:01:37 Finished compiler/parsing/tests                                  23s 545MB
May 02 20:01:38 Starting compiler/inference/tests
May 02 20:05:43 Finished compiler/inference/tests                              4m04s   4GB
May 02 20:05:43 Starting compiler/bootstrap/translation
May 02 22:21:09 FAILED: compiler/bootstrap/translation
]0;Holmake: .]0;Holmake: ~/regression/HOL-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/examples/l3-machine-code/arm/model]0;Holmake: ~/regression/HOL-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/examples/l3-machine-code/common]0;Holmake: ~/regression/HOL-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/regression/HOL-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/examples/l3-machine-code/common]0;Holmake: ~/regression/HOL-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/examples/l3-machine-code/common[1mWorking in $(HOLDIR)/examples/l3-machine-code/common[0m
]0;Holmake: ~/regression/HOL-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/examples/l3-machine-code/arm/model]0;Holmake: ~/regression/HOL-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/examples/l3-machine-code/lib]0;Holmake: ~/regression/HOL-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/examples/l3-machine-code/lib[1mWorking in $(HOLDIR)/examples/l3-machine-code/lib[0m
]0;Holmake: ~/regression/HOL-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/examples/l3-machine-code/arm/model]0;Holmake: ~/regression/HOL-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/examples/l3-machine-code/arm/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/model[0m
]0;Holmake: .]0;Holmake: ~/regression/HOL-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/examples/l3-machine-code/arm8/model]0;Holmake: ~/regression/HOL-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/examples/l3-machine-code/arm8/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm8/model[0m
]0;Holmake: .]0;Holmake: ~/regression/HOL-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/examples/l3-machine-code/mips/model]0;Holmake: ~/regression/HOL-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/examples/l3-machine-code/mips/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/mips/model[0m
]0;Holmake: .]0;Holmake: ~/regression/HOL-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/examples/l3-machine-code/riscv/model]0;Holmake: ~/regression/HOL-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/examples/l3-machine-code/riscv/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/riscv/model[0m
]0;Holmake: .]0;Holmake: ~/regression/HOL-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/examples/l3-machine-code/x64/model]0;Holmake: ~/regression/HOL-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/examples/l3-machine-code/x64/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/x64/model[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-832/basis]0;Holmake: ~/regression/cakeml-832/basis/pure]0;Holmake: ~/regression/HOL-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/examples/balanced_bst]0;Holmake: ~/regression/HOL-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: ~/regression/cakeml-832/basis/pure]0;Holmake: ~/regression/HOL-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/examples/formal-languages]0;Holmake: ~/regression/HOL-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ~/regression/cakeml-832/basis/pure]0;Holmake: ~/regression/cakeml-832/misc]0;Holmake: ~/regression/HOL-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-832/misc]0;Holmake: ~/regression/cakeml-832/developers]0;Holmake: ~/regression/cakeml-832/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-832/misc]0;Holmake: ~/regression/cakeml-832/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-832/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-832/misc]0;Holmake: ~/regression/cakeml-832/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression/cakeml-832/basis/pure]0;Holmake: ~/regression/cakeml-832/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ~/regression/cakeml-832/basis]0;Holmake: ~/regression/cakeml-832/characteristic]0;Holmake: ~/regression/cakeml-832/compiler/parsing]0;Holmake: ~/regression/cakeml-832/semantics]0;Holmake: ~/regression/cakeml-832/semantics/ffi]0;Holmake: ~/regression/cakeml-832/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-832/semantics]0;Holmake: ~/regression/cakeml-832/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression/cakeml-832/compiler/parsing]0;Holmake: ~/regression/cakeml-832/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/regression/cakeml-832/characteristic]0;Holmake: ~/regression/cakeml-832/semantics/proofs]0;Holmake: ~/regression/cakeml-832/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ~/regression/cakeml-832/characteristic]0;Holmake: ~/regression/cakeml-832/translator]0;Holmake: ~/regression/cakeml-832/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/regression/cakeml-832/characteristic]0;Holmake: ~/regression/cakeml-832/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ~/regression/cakeml-832/basis]0;Holmake: ~/regression/cakeml-832/translator/monadic]0;Holmake: ~/regression/cakeml-832/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-832/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ~/regression/cakeml-832/translator/monadic]0;Holmake: ~/regression/cakeml-832/translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ~/regression/cakeml-832/basis]0;Holmake: ~/regression/cakeml-832/basis[1mWorking in $(CAKEMLDIR)/basis[0m
]0;Holmake: .]0;Holmake: ../..]0;Holmake: ../../backend]0;Holmake: ~/regression/HOL-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/examples/machine-code/multiword]0;Holmake: ~/regression/HOL-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/examples/machine-code/multiword[1mWorking in $(HOLDIR)/examples/machine-code/multiword[0m
]0;Holmake: ../../backend]0;Holmake: ../../backend/reg_alloc]0;Holmake: ~/regression/cakeml-832/unverified/reg_alloc]0;Holmake: ~/regression/cakeml-832/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-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/examples/l3-machine-code/arm/step]0;Holmake: ~/regression/HOL-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/examples/l3-machine-code]0;Holmake: ~/regression/HOL-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/examples/machine-code/decompiler]0;Holmake: ~/regression/HOL-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/examples/machine-code/decompiler[1mWorking in $(HOLDIR)/examples/machine-code/decompiler[0m
]0;Holmake: ~/regression/HOL-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/examples/l3-machine-code]0;Holmake: ~/regression/HOL-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/examples/l3-machine-code[1mWorking in $(HOLDIR)/examples/l3-machine-code[0m
]0;Holmake: ~/regression/HOL-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/examples/l3-machine-code/arm/step]0;Holmake: ~/regression/HOL-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/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/arm7]0;Holmake: ../../encoders/arm7]0;Holmake: ../../encoders/arm7[1mWorking in $(CAKEMLDIR)/compiler/encoders/arm7[0m
]0;Holmake: ../../backend/arm7]0;Holmake: ../../backend/arm7[1mWorking in $(CAKEMLDIR)/compiler/backend/arm7[0m
]0;Holmake: ../..]0;Holmake: ../../backend/arm8]0;Holmake: ../../encoders/arm8]0;Holmake: ~/regression/HOL-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/examples/l3-machine-code/arm8/step]0;Holmake: ~/regression/HOL-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/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-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/examples/l3-machine-code/mips/step]0;Holmake: ~/regression/HOL-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/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-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/examples/l3-machine-code/riscv/step]0;Holmake: ~/regression/HOL-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/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-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/examples/l3-machine-code/x64/step]0;Holmake: ~/regression/HOL-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/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-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/examples/unification/triangular/first-order]0;Holmake: ~/regression/HOL-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/examples/unification/triangular]0;Holmake: ~/regression/HOL-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/examples/unification/triangular[1mWorking in $(HOLDIR)/examples/unification/triangular[0m
]0;Holmake: ~/regression/HOL-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/examples/unification/triangular/first-order]0;Holmake: ~/regression/HOL-6d809bfa2ef8cbcb75d63317c4f8f2e1a6a836ed/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 arm7ProgTheory
arm8ProgTheory                                      OK
Starting work on riscvProgTheory
arm7ProgTheory                                      OK
Starting work on ag32ProgTheory
riscvProgTheory                                     OK
Starting work on mipsProgTheory
ag32ProgTheory                                      OK
Starting work on compiler32ProgTheory
mipsProgTheory                                      OK
Starting work on compiler64ProgTheory
compiler32ProgTheory                       FAILED! <1>
        COMMANDLINE cl)
 
 failed.
 Failed to prove theorem main_spec.
 
 Exception raised at Tactical.THEN1:
 first subgoal not solved by second tactic (THEN1 on line 293) (THEN1 on line 298) (THEN1 on line 302)
 error in quse /home/myreen/regression/cakeml-832/compiler/bootstrap/translation/compiler32ProgScript.sml : HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 293) (THEN1 on line 298) (THEN1 on line 302)", origin_function = "THEN1", origin_structure = "Tactical"}
 error in load compiler32ProgScript : HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 293) (THEN1 on line 298) (THEN1 on line 302)", origin_function = "THEN1", origin_structure = "Tactical"}
 Uncaught exception: HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 293) (THEN1 on line 298) (THEN1 on line 302)", origin_function = "THEN1", origin_structure = "Tactical"}
compiler64ProgTheory                          M-KILLED