Job 828

CakeML:0a1d60de5801cc53e17a621e3615279e88e7c790
  Fix backend proofs broken by adding FMA instruction [Apr 30 11:13:42]
#633 (FMA_support)
Merging into:62c51fa831d455390795c47c53f56b050a23f7ad
  Merge pull request #627 from CakeML/monadic-trans-cleanup [Apr 27 07:20:55]
HOL:8e183cc626814e8bfbee46abcbf51798ee1c69b6
  Emacs mode: fix dumb bug in M-h H [Apr 29 06:05:42]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Apr 30 13:03:42 Claimed job
Apr 30 13:03:46 Reusing HOL
Apr 30 13:03:50 Starting developers
Apr 30 13:03:51 Finished developers                                               0s  21MB
Apr 30 13:03:51 Starting developers/bin
Apr 30 13:04:21 Finished developers/bin                                          29s 207MB
Apr 30 13:04:22 Starting semantics/ffi
Apr 30 13:04:29 Finished semantics/ffi                                            7s 227MB
Apr 30 13:04:30 Starting semantics
Apr 30 13:05:47 Finished semantics                                             1m17s   1GB
Apr 30 13:05:48 Starting semantics/proofs
Apr 30 13:08:43 Finished semantics/proofs                                      2m54s 971MB
Apr 30 13:08:43 Starting basis/pure
Apr 30 13:09:27 Finished basis/pure                                              43s 572MB
Apr 30 13:09:28 Starting translator
Apr 30 13:11:03 Finished translator                                            1m35s   1GB
Apr 30 13:11:03 Starting compiler/parsing
Apr 30 13:12:00 Finished compiler/parsing                                        56s   1GB
Apr 30 13:12:01 Starting characteristic
Apr 30 13:17:03 Finished characteristic                                        5m02s   2GB
Apr 30 13:17:04 Starting translator/monadic
Apr 30 13:18:27 Finished translator/monadic                                    1m23s   1GB
Apr 30 13:18:28 Starting basis
Apr 30 13:34:50 Finished basis                                                16m22s   2GB
Apr 30 13:34:50 Starting compiler/inference
Apr 30 13:36:24 Finished compiler/inference                                    1m32s   1GB
Apr 30 13:36:24 Starting compiler/backend/reg_alloc
Apr 30 13:37:21 Finished compiler/backend/reg_alloc                              56s   1GB
Apr 30 13:37:21 Starting compiler/backend/gc
Apr 30 13:45:19 Finished compiler/backend/gc                                   7m57s   1GB
Apr 30 13:45:20 Starting compiler/backend
Apr 30 13:45:21 Finished compiler/backend                                         0s  43MB
Apr 30 13:45:21 Starting compiler/encoders/asm
Apr 30 13:45:22 Finished compiler/encoders/asm                                    0s  32MB
Apr 30 13:45:22 Starting compiler/encoders/x64
Apr 30 13:45:45 Finished compiler/encoders/x64                                   22s 940MB
Apr 30 13:45:45 Starting compiler/encoders/arm6
Apr 30 13:46:29 Finished compiler/encoders/arm6                                  43s 720MB
Apr 30 13:46:29 Starting compiler/encoders/arm8
Apr 30 13:46:41 Finished compiler/encoders/arm8                                  11s 538MB
Apr 30 13:46:41 Starting compiler/encoders/mips
Apr 30 13:46:59 Finished compiler/encoders/mips                                  16s 865MB
Apr 30 13:46:59 Starting compiler/encoders/riscv
Apr 30 13:47:12 Finished compiler/encoders/riscv                                 12s 800MB
Apr 30 13:47:12 Starting compiler/encoders/ag32
Apr 30 13:47:27 Finished compiler/encoders/ag32                                  14s 801MB
Apr 30 13:47:28 Starting compiler/backend/x64
Apr 30 13:47:43 Finished compiler/backend/x64                                    15s   1GB
Apr 30 13:47:44 Starting compiler/backend/arm6
Apr 30 13:48:00 Finished compiler/backend/arm6                                   16s   1GB
Apr 30 13:48:01 Starting compiler/backend/arm8
Apr 30 13:48:17 Finished compiler/backend/arm8                                   15s   1GB
Apr 30 13:48:17 Starting compiler/backend/mips
Apr 30 13:48:34 Finished compiler/backend/mips                                   16s   1GB
Apr 30 13:48:35 Starting compiler/backend/riscv
Apr 30 13:48:51 Finished compiler/backend/riscv                                  16s   1GB
Apr 30 13:48:52 Starting compiler/backend/ag32
Apr 30 13:49:59 Finished compiler/backend/ag32                                 1m06s   1GB
Apr 30 13:49:59 Starting compiler/parsing/proofs
Apr 30 13:55:29 Finished compiler/parsing/proofs                               5m28s   1GB
Apr 30 13:55:29 Starting compiler/inference/proofs
Apr 30 13:58:07 Finished compiler/inference/proofs                             2m37s   1GB
Apr 30 13:58:08 Starting compiler/backend/semantics
Apr 30 14:05:09 Finished compiler/backend/semantics                            7m00s   1GB
Apr 30 14:05:09 Starting compiler/backend/reg_alloc/proofs
Apr 30 14:08:22 Finished compiler/backend/reg_alloc/proofs                     3m12s   1GB
Apr 30 14:08:23 Starting compiler/backend/proofs
Apr 30 14:46:32 Finished compiler/backend/proofs                              38m07s   4GB
Apr 30 14:46:32 Starting compiler/encoders/x64/proofs
Apr 30 14:55:34 Finished compiler/encoders/x64/proofs                          9m01s   7GB
Apr 30 14:55:35 Starting compiler/encoders/arm6/proofs
Apr 30 15:07:44 Finished compiler/encoders/arm6/proofs                        12m08s   3GB
Apr 30 15:07:44 Starting compiler/encoders/arm8/proofs
Apr 30 15:14:16 Finished compiler/encoders/arm8/proofs                         6m31s   1GB
Apr 30 15:14:17 Starting compiler/encoders/mips/proofs
Apr 30 15:23:34 Finished compiler/encoders/mips/proofs                         9m17s   2GB
Apr 30 15:23:35 Starting compiler/encoders/riscv/proofs
Apr 30 15:31:51 Finished compiler/encoders/riscv/proofs                        8m15s   1GB
Apr 30 15:31:51 Starting compiler/encoders/ag32/proofs
Apr 30 15:34:19 Finished compiler/encoders/ag32/proofs                         2m27s 855MB
Apr 30 15:34:19 Starting compiler/backend/x64/proofs
Apr 30 15:34:35 Finished compiler/backend/x64/proofs                             16s   1GB
Apr 30 15:34:36 Starting compiler/backend/arm6/proofs
Apr 30 15:34:54 Finished compiler/backend/arm6/proofs                            18s   1GB
Apr 30 15:34:54 Starting compiler/backend/arm8/proofs
Apr 30 15:35:10 Finished compiler/backend/arm8/proofs                            15s   1GB
Apr 30 15:35:11 Starting compiler/backend/mips/proofs
Apr 30 15:35:27 Finished compiler/backend/mips/proofs                            16s 986MB
Apr 30 15:35:28 Starting compiler/backend/riscv/proofs
Apr 30 15:35:45 Finished compiler/backend/riscv/proofs                           16s   1GB
Apr 30 15:35:45 Starting compiler/backend/ag32/proofs
Apr 30 15:44:36 Finished compiler/backend/ag32/proofs                          8m50s   2GB
Apr 30 15:44:37 Starting compiler/proofs
Apr 30 15:46:48 Finished compiler/proofs                                       2m10s   2GB
Apr 30 15:46:49 Starting candle/set-theory
Apr 30 15:47:13 Finished candle/set-theory                                       24s 656MB
Apr 30 15:47:14 Starting candle/syntax-lib
Apr 30 15:47:23 Finished candle/syntax-lib                                        8s 667MB
Apr 30 15:47:23 Starting candle/standard/syntax
Apr 30 15:49:04 Finished candle/standard/syntax                                1m39s   1GB
Apr 30 15:49:04 Starting candle/standard/semantics
Apr 30 15:50:37 Finished candle/standard/semantics                             1m32s   1GB
Apr 30 15:50:37 Starting candle/standard/monadic
Apr 30 15:52:08 Finished candle/standard/monadic                               1m30s   1GB
Apr 30 15:52:08 Starting candle/standard/ml_kernel
Apr 30 15:55:57 Finished candle/standard/ml_kernel                             3m48s   4GB
Apr 30 15:55:57 Starting candle/standard/opentheory
Apr 30 16:04:25 Finished candle/standard/opentheory                            8m27s   3GB
Apr 30 16:04:26 Starting candle/standard/opentheory/compilation
Apr 30 16:33:27 Finished candle/standard/opentheory/compilation               29m00s  12GB
Apr 30 16:33:27 Starting candle/standard/opentheory/compilation/proofs
Apr 30 16:34:02 Finished candle/standard/opentheory/compilation/proofs           34s   3GB
Apr 30 16:34:02 Starting characteristic/examples
Apr 30 16:35:24 Finished characteristic/examples                               1m21s   2GB
Apr 30 16:35:25 Starting tutorial/solutions
Apr 30 16:48:17 Finished tutorial/solutions                                   12m51s   6GB
Apr 30 16:48:18 Starting translator/monadic/examples
Apr 30 16:51:01 Finished translator/monadic/examples                           2m43s   2GB
Apr 30 16:51:01 Starting examples
Apr 30 16:59:14 Finished examples                                              8m12s   3GB
Apr 30 16:59:15 Starting examples/compilation/x64
Apr 30 18:51:25 Finished examples/compilation/x64                           1h52m09s  13GB
Apr 30 18:51:25 Starting examples/compilation/x64/proofs
Apr 30 18:52:47 Finished examples/compilation/x64/proofs                       1m21s   2GB
Apr 30 18:52:47 Starting examples/compilation/ag32
Apr 30 19:20:23 Finished examples/compilation/ag32                            27m35s   5GB
Apr 30 19:20:23 Starting examples/compilation/ag32/proofs
Apr 30 19:21:04 Finished examples/compilation/ag32/proofs                        40s   3GB
Apr 30 19:21:05 Starting translator/okasaki-examples
Apr 30 19:25:08 Finished translator/okasaki-examples                           4m03s   1GB
Apr 30 19:25:09 Starting translator/other-examples
Apr 30 19:28:42 Finished translator/other-examples                             3m32s   1GB
Apr 30 19:28:42 Starting compiler/parsing/tests
Apr 30 19:29:07 Finished compiler/parsing/tests                                  24s 498MB
Apr 30 19:29:07 Starting compiler/inference/tests
Apr 30 19:33:13 Finished compiler/inference/tests                              4m04s   2GB
Apr 30 19:33:13 Starting compiler/bootstrap/translation
Apr 30 21:25:43 FAILED: compiler/bootstrap/translation
]0;Holmake: .]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/arm/model]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/common]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/common]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/common[1mWorking in $(HOLDIR)/examples/l3-machine-code/common[0m
]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/arm/model]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/lib]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/lib[1mWorking in $(HOLDIR)/examples/l3-machine-code/lib[0m
]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/arm/model]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/arm/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm/model[0m
]0;Holmake: .]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/arm8/model]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/arm8/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/arm8/model[0m
]0;Holmake: .]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/mips/model]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/mips/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/mips/model[0m
]0;Holmake: .]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/riscv/model]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/riscv/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/riscv/model[0m
]0;Holmake: .]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/x64/model]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/x64/model[1mWorking in $(HOLDIR)/examples/l3-machine-code/x64/model[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-828/basis]0;Holmake: ~/regression/cakeml-828/basis/pure]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/balanced_bst]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/balanced_bst[1mWorking in $(HOLDIR)/examples/balanced_bst[0m
]0;Holmake: ~/regression/cakeml-828/basis/pure]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/formal-languages]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ~/regression/cakeml-828/basis/pure]0;Holmake: ~/regression/cakeml-828/misc]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-828/misc]0;Holmake: ~/regression/cakeml-828/developers]0;Holmake: ~/regression/cakeml-828/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-828/misc]0;Holmake: ~/regression/cakeml-828/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-828/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-828/misc]0;Holmake: ~/regression/cakeml-828/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression/cakeml-828/basis/pure]0;Holmake: ~/regression/cakeml-828/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ~/regression/cakeml-828/basis]0;Holmake: ~/regression/cakeml-828/characteristic]0;Holmake: ~/regression/cakeml-828/compiler/parsing]0;Holmake: ~/regression/cakeml-828/semantics]0;Holmake: ~/regression/cakeml-828/semantics/ffi]0;Holmake: ~/regression/cakeml-828/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-828/semantics]0;Holmake: ~/regression/cakeml-828/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression/cakeml-828/compiler/parsing]0;Holmake: ~/regression/cakeml-828/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/regression/cakeml-828/characteristic]0;Holmake: ~/regression/cakeml-828/semantics/proofs]0;Holmake: ~/regression/cakeml-828/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ~/regression/cakeml-828/characteristic]0;Holmake: ~/regression/cakeml-828/translator]0;Holmake: ~/regression/cakeml-828/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/regression/cakeml-828/characteristic]0;Holmake: ~/regression/cakeml-828/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ~/regression/cakeml-828/basis]0;Holmake: ~/regression/cakeml-828/translator/monadic]0;Holmake: ~/regression/cakeml-828/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-828/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ~/regression/cakeml-828/translator/monadic]0;Holmake: ~/regression/cakeml-828/translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ~/regression/cakeml-828/basis]0;Holmake: ~/regression/cakeml-828/basis[1mWorking in $(CAKEMLDIR)/basis[0m
]0;Holmake: .]0;Holmake: ../..]0;Holmake: ../../backend]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/machine-code/multiword]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/machine-code/multiword[1mWorking in $(HOLDIR)/examples/machine-code/multiword[0m
]0;Holmake: ../../backend]0;Holmake: ../../backend/reg_alloc]0;Holmake: ~/regression/cakeml-828/unverified/reg_alloc]0;Holmake: ~/regression/cakeml-828/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-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/arm/step]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/machine-code/decompiler]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/machine-code/decompiler[1mWorking in $(HOLDIR)/examples/machine-code/decompiler[0m
]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code[1mWorking in $(HOLDIR)/examples/l3-machine-code[0m
]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/arm/step]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/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-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/arm8/step]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/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-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/mips/step]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/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-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/riscv/step]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/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-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/x64/step]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/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-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/unification/triangular/first-order]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/unification/triangular]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/unification/triangular[1mWorking in $(HOLDIR)/examples/unification/triangular[0m
]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/unification/triangular/first-order]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/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
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
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_word64ProgTheory                                                                                        OK
Starting work on to_target64ProgTheory
to_word32ProgTheory                                                                                        OK
Starting work on to_target32ProgTheory
to_target32ProgTheory                                                                             FAILED! <1>
 (r f1 f2. v9 = FPEqual r f1 f2)  (f1 f2. v9 = FPAbs f1 f2) 
 (f1 f2. v9 = FPNeg f1 f2)  (f1 f2. v9 = FPSqrt f1 f2) 
 (f1 f2 f3. v9 = FPAdd f1 f2 f3)  (f1 f2 f3. v9 = FPSub f1 f2 f3) 
 (f1 f2 f3. v9 = FPMul f1 f2 f3)  (f1 f2 f3. v9 = ... ... f2 f3) 
 (f1 f2. v9 = ... ... f2)  (r1 r2 f. v9 = ... ... ) 
 (f r1 r2. ... = ... )  (... ... . ... )  ... ... . ...
 
 error in quse /home/myreen/regression/cakeml-828/compiler/bootstrap/translation/to_target32ProgScript.sml : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
 error in load to_target32ProgScript : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
 Uncaught exception: HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
to_target64ProgTheory                                                                                M-KILLED