Job 821

CakeML:ca20e4907cd991f00c093a18bf2a240da7cf6d0f
  Merge branch 'master' into vstte18 [Apr 29 10:15:10]
#629 (vstte18)
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 29 11:12:07 Claimed job
Apr 29 11:12:29 Building HOL
Apr 29 11:20:18 Starting developers
Apr 29 11:20:19 Finished developers                                               0s  35MB
Apr 29 11:20:19 Starting developers/bin
Apr 29 11:20:53 Finished developers/bin                                          33s 141MB
Apr 29 11:20:53 Starting semantics/ffi
Apr 29 11:21:26 Finished semantics/ffi                                           33s 569MB
Apr 29 11:21:27 Starting semantics
Apr 29 11:22:58 Finished semantics                                             1m30s   1GB
Apr 29 11:22:59 Starting semantics/proofs
Apr 29 11:25:50 Finished semantics/proofs                                      2m51s   1GB
Apr 29 11:25:51 Starting basis/pure
Apr 29 11:29:19 Finished basis/pure                                            3m28s 579MB
Apr 29 11:29:20 Starting translator
Apr 29 11:30:56 Finished translator                                            1m36s   1GB
Apr 29 11:30:57 Starting compiler/parsing
Apr 29 11:31:54 Finished compiler/parsing                                        56s   2GB
Apr 29 11:31:54 Starting characteristic
Apr 29 11:36:58 Finished characteristic                                        5m03s   1GB
Apr 29 11:36:59 Starting translator/monadic
Apr 29 11:38:24 Finished translator/monadic                                    1m24s   1GB
Apr 29 11:38:24 Starting basis
Apr 29 11:55:01 Finished basis                                                16m36s   2GB
Apr 29 11:55:01 Starting compiler/inference
Apr 29 11:56:46 Finished compiler/inference                                    1m44s   1GB
Apr 29 11:56:47 Starting compiler/backend/reg_alloc
Apr 29 11:57:44 Finished compiler/backend/reg_alloc                              56s   1GB
Apr 29 11:57:44 Starting compiler/backend/gc
Apr 29 12:06:38 Finished compiler/backend/gc                                   8m53s   2GB
Apr 29 12:06:38 Starting compiler/backend
Apr 29 12:06:39 Finished compiler/backend                                         0s  42MB
Apr 29 12:06:39 Starting compiler/encoders/asm
Apr 29 12:06:40 Finished compiler/encoders/asm                                    0s  32MB
Apr 29 12:06:40 Starting compiler/encoders/x64
Apr 29 12:07:37 Finished compiler/encoders/x64                                   56s 778MB
Apr 29 12:07:37 Starting compiler/encoders/arm6
Apr 29 12:09:12 Finished compiler/encoders/arm6                                1m34s   1GB
Apr 29 12:09:12 Starting compiler/encoders/arm8
Apr 29 12:09:41 Finished compiler/encoders/arm8                                  28s 638MB
Apr 29 12:09:41 Starting compiler/encoders/mips
Apr 29 12:10:44 Finished compiler/encoders/mips                                1m01s 865MB
Apr 29 12:10:44 Starting compiler/encoders/riscv
Apr 29 12:12:01 Finished compiler/encoders/riscv                               1m16s   1GB
Apr 29 12:12:01 Starting compiler/encoders/ag32
Apr 29 12:12:16 Finished compiler/encoders/ag32                                  14s 782MB
Apr 29 12:12:16 Starting compiler/backend/x64
Apr 29 12:12:32 Finished compiler/backend/x64                                    15s   1GB
Apr 29 12:12:32 Starting compiler/backend/arm6
Apr 29 12:12:50 Finished compiler/backend/arm6                                   17s   1GB
Apr 29 12:12:50 Starting compiler/backend/arm8
Apr 29 12:13:06 Finished compiler/backend/arm8                                   15s 960MB
Apr 29 12:13:06 Starting compiler/backend/mips
Apr 29 12:13:23 Finished compiler/backend/mips                                   16s   1GB
Apr 29 12:13:23 Starting compiler/backend/riscv
Apr 29 12:13:40 Finished compiler/backend/riscv                                  16s   1GB
Apr 29 12:13:40 Starting compiler/backend/ag32
Apr 29 12:14:45 Finished compiler/backend/ag32                                 1m04s   1GB
Apr 29 12:14:46 Starting compiler/parsing/proofs
Apr 29 12:20:14 Finished compiler/parsing/proofs                               5m28s   1GB
Apr 29 12:20:15 Starting compiler/inference/proofs
Apr 29 12:22:51 Finished compiler/inference/proofs                             2m35s   1GB
Apr 29 12:22:51 Starting compiler/backend/semantics
Apr 29 12:29:43 Finished compiler/backend/semantics                            6m51s   2GB
Apr 29 12:29:44 Starting compiler/backend/reg_alloc/proofs
Apr 29 12:32:58 Finished compiler/backend/reg_alloc/proofs                     3m14s 810MB
Apr 29 12:32:59 Starting compiler/backend/proofs
Apr 29 13:09:44 Finished compiler/backend/proofs                              36m45s   4GB
Apr 29 13:09:45 Starting compiler/encoders/x64/proofs
Apr 29 13:19:47 Finished compiler/encoders/x64/proofs                         10m01s   4GB
Apr 29 13:19:48 Starting compiler/encoders/arm6/proofs
Apr 29 13:33:29 Finished compiler/encoders/arm6/proofs                        13m41s   3GB
Apr 29 13:33:29 Starting compiler/encoders/arm8/proofs
Apr 29 13:40:08 Finished compiler/encoders/arm8/proofs                         6m38s   1GB
Apr 29 13:40:09 Starting compiler/encoders/mips/proofs
Apr 29 13:50:07 Finished compiler/encoders/mips/proofs                         9m57s   1GB
Apr 29 13:50:07 Starting compiler/encoders/riscv/proofs
Apr 29 13:58:22 Finished compiler/encoders/riscv/proofs                        8m15s   1GB
Apr 29 13:58:23 Starting compiler/encoders/ag32/proofs
Apr 29 14:00:50 Finished compiler/encoders/ag32/proofs                         2m27s 666MB
Apr 29 14:00:51 Starting compiler/backend/x64/proofs
Apr 29 14:01:07 Finished compiler/backend/x64/proofs                             16s 980MB
Apr 29 14:01:08 Starting compiler/backend/arm6/proofs
Apr 29 14:01:26 Finished compiler/backend/arm6/proofs                            18s   1GB
Apr 29 14:01:27 Starting compiler/backend/arm8/proofs
Apr 29 14:01:43 Finished compiler/backend/arm8/proofs                            15s   1GB
Apr 29 14:01:43 Starting compiler/backend/mips/proofs
Apr 29 14:02:00 Finished compiler/backend/mips/proofs                            16s   1GB
Apr 29 14:02:01 Starting compiler/backend/riscv/proofs
Apr 29 14:02:19 Finished compiler/backend/riscv/proofs                           17s 930MB
Apr 29 14:02:19 Starting compiler/backend/ag32/proofs
Apr 29 14:11:19 Finished compiler/backend/ag32/proofs                          8m59s   1GB
Apr 29 14:11:19 Starting compiler/proofs
Apr 29 14:12:30 Finished compiler/proofs                                       1m10s   2GB
Apr 29 14:12:30 Starting candle/set-theory
Apr 29 14:12:55 Finished candle/set-theory                                       24s 677MB
Apr 29 14:12:55 Starting candle/syntax-lib
Apr 29 14:13:04 Finished candle/syntax-lib                                        9s 655MB
Apr 29 14:13:05 Starting candle/standard/syntax
Apr 29 14:14:45 Finished candle/standard/syntax                                1m39s   1GB
Apr 29 14:14:46 Starting candle/standard/semantics
Apr 29 14:16:17 Finished candle/standard/semantics                             1m31s   1GB
Apr 29 14:16:18 Starting candle/standard/monadic
Apr 29 14:17:48 Finished candle/standard/monadic                               1m29s   1GB
Apr 29 14:17:48 Starting candle/standard/ml_kernel
Apr 29 14:21:29 Finished candle/standard/ml_kernel                             3m40s   4GB
Apr 29 14:21:29 Starting candle/standard/opentheory
Apr 29 14:29:45 Finished candle/standard/opentheory                            8m15s   4GB
Apr 29 14:29:46 Starting candle/standard/opentheory/compilation
Apr 29 14:58:30 Finished candle/standard/opentheory/compilation               28m43s  22GB
Apr 29 14:58:30 Starting candle/standard/opentheory/compilation/proofs
Apr 29 14:59:02 Finished candle/standard/opentheory/compilation/proofs           31s   2GB
Apr 29 14:59:03 Starting characteristic/examples
Apr 29 15:00:24 Finished characteristic/examples                               1m20s   2GB
Apr 29 15:00:24 Starting tutorial/solutions
Apr 29 15:13:38 FAILED: tutorial/solutions
]0;Holmake: .]0;Holmake: ~/regression/cakeml-821/basis]0;Holmake: ~/regression/cakeml-821/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/context-free]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[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-821/basis/pure]0;Holmake: ~/regression/cakeml-821/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-821/misc]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/cakeml-821/misc]0;Holmake: ~/regression/cakeml-821/developers]0;Holmake: ~/regression/cakeml-821/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-821/misc]0;Holmake: ~/regression/cakeml-821/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-821/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-821/misc]0;Holmake: ~/regression/cakeml-821/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression/cakeml-821/basis/pure]0;Holmake: ~/regression/cakeml-821/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ~/regression/cakeml-821/basis]0;Holmake: ~/regression/cakeml-821/characteristic]0;Holmake: ~/regression/cakeml-821/compiler/parsing]0;Holmake: ~/regression/cakeml-821/semantics]0;Holmake: ~/regression/cakeml-821/semantics/ffi]0;Holmake: ~/regression/cakeml-821/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-821/semantics]0;Holmake: ~/regression/cakeml-821/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression/cakeml-821/compiler/parsing]0;Holmake: ~/regression/cakeml-821/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/regression/cakeml-821/characteristic]0;Holmake: ~/regression/cakeml-821/semantics/proofs]0;Holmake: ~/regression/cakeml-821/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ~/regression/cakeml-821/characteristic]0;Holmake: ~/regression/cakeml-821/translator]0;Holmake: ~/regression/cakeml-821/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/regression/cakeml-821/characteristic]0;Holmake: ~/regression/cakeml-821/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ~/regression/cakeml-821/basis]0;Holmake: ~/regression/cakeml-821/translator/monadic]0;Holmake: ~/regression/cakeml-821/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-821/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ~/regression/cakeml-821/translator/monadic]0;Holmake: ~/regression/cakeml-821/translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ~/regression/cakeml-821/basis]0;Holmake: ~/regression/cakeml-821/basis[1mWorking in $(CAKEMLDIR)/basis[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-821/compiler]0;Holmake: ~/regression/cakeml-821/compiler/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: ~/regression/cakeml-821/compiler/backend]0;Holmake: ~/regression/cakeml-821/compiler/backend/reg_alloc]0;Holmake: ~/regression/cakeml-821/unverified/reg_alloc]0;Holmake: ~/regression/cakeml-821/unverified/reg_alloc[1mWorking in $(CAKEMLDIR)/unverified/reg_alloc[0m
]0;Holmake: ~/regression/cakeml-821/compiler/backend/reg_alloc]0;Holmake: ~/regression/cakeml-821/compiler/backend/reg_alloc[1mWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc[0m
]0;Holmake: ~/regression/cakeml-821/compiler/backend]0;Holmake: ~/regression/cakeml-821/compiler/encoders/asm]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/cakeml-821/compiler/encoders/asm]0;Holmake: ~/regression/cakeml-821/compiler/encoders/asm[1mWorking in $(CAKEMLDIR)/compiler/encoders/asm[0m
]0;Holmake: ~/regression/cakeml-821/compiler/backend]0;Holmake: ~/regression/cakeml-821/compiler/backend[1mWorking in $(CAKEMLDIR)/compiler/backend[0m
]0;Holmake: ~/regression/cakeml-821/compiler]0;Holmake: ~/regression/cakeml-821/compiler/backend/ag32]0;Holmake: ~/regression/cakeml-821/compiler/encoders/ag32]0;Holmake: ~/regression/cakeml-821/compiler/encoders/ag32[1mWorking in $(CAKEMLDIR)/compiler/encoders/ag32[0m
]0;Holmake: ~/regression/cakeml-821/compiler/backend/ag32]0;Holmake: ~/regression/cakeml-821/compiler/backend/ag32[1mWorking in $(CAKEMLDIR)/compiler/backend/ag32[0m
]0;Holmake: ~/regression/cakeml-821/compiler]0;Holmake: ~/regression/cakeml-821/compiler/backend/arm6]0;Holmake: ~/regression/cakeml-821/compiler/encoders/arm6]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: ~/regression/cakeml-821/compiler/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: ~/regression/cakeml-821/compiler/encoders/arm6]0;Holmake: ~/regression/cakeml-821/compiler/encoders/arm6[1mWorking in $(CAKEMLDIR)/compiler/encoders/arm6[0m
]0;Holmake: ~/regression/cakeml-821/compiler/backend/arm6]0;Holmake: ~/regression/cakeml-821/compiler/backend/arm6[1mWorking in $(CAKEMLDIR)/compiler/backend/arm6[0m
]0;Holmake: ~/regression/cakeml-821/compiler]0;Holmake: ~/regression/cakeml-821/compiler/backend/arm8]0;Holmake: ~/regression/cakeml-821/compiler/encoders/arm8]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: ~/regression/cakeml-821/compiler/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: ~/regression/cakeml-821/compiler/encoders/arm8]0;Holmake: ~/regression/cakeml-821/compiler/encoders/arm8[1mWorking in $(CAKEMLDIR)/compiler/encoders/arm8[0m
]0;Holmake: ~/regression/cakeml-821/compiler/backend/arm8]0;Holmake: ~/regression/cakeml-821/compiler/backend/arm8[1mWorking in $(CAKEMLDIR)/compiler/backend/arm8[0m
]0;Holmake: ~/regression/cakeml-821/compiler]0;Holmake: ~/regression/cakeml-821/compiler/backend/mips]0;Holmake: ~/regression/cakeml-821/compiler/encoders/mips]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: ~/regression/cakeml-821/compiler/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: ~/regression/cakeml-821/compiler/encoders/mips]0;Holmake: ~/regression/cakeml-821/compiler/encoders/mips[1mWorking in $(CAKEMLDIR)/compiler/encoders/mips[0m
]0;Holmake: ~/regression/cakeml-821/compiler/backend/mips]0;Holmake: ~/regression/cakeml-821/compiler/backend/mips[1mWorking in $(CAKEMLDIR)/compiler/backend/mips[0m
]0;Holmake: ~/regression/cakeml-821/compiler]0;Holmake: ~/regression/cakeml-821/compiler/backend/riscv]0;Holmake: ~/regression/cakeml-821/compiler/encoders/riscv]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: ~/regression/cakeml-821/compiler/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: ~/regression/cakeml-821/compiler/encoders/riscv]0;Holmake: ~/regression/cakeml-821/compiler/encoders/riscv[1mWorking in $(CAKEMLDIR)/compiler/encoders/riscv[0m
]0;Holmake: ~/regression/cakeml-821/compiler/backend/riscv]0;Holmake: ~/regression/cakeml-821/compiler/backend/riscv[1mWorking in $(CAKEMLDIR)/compiler/backend/riscv[0m
]0;Holmake: ~/regression/cakeml-821/compiler]0;Holmake: ~/regression/cakeml-821/compiler/backend/x64]0;Holmake: ~/regression/cakeml-821/compiler/encoders/x64]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: ~/regression/cakeml-821/compiler/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: ~/regression/cakeml-821/compiler/encoders/x64]0;Holmake: ~/regression/cakeml-821/compiler/encoders/x64[1mWorking in $(CAKEMLDIR)/compiler/encoders/x64[0m
]0;Holmake: ~/regression/cakeml-821/compiler/backend/x64]0;Holmake: ~/regression/cakeml-821/compiler/backend/x64[1mWorking in $(CAKEMLDIR)/compiler/backend/x64[0m
]0;Holmake: ~/regression/cakeml-821/compiler]0;Holmake: ~/regression/cakeml-821/compiler/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: ~/regression/cakeml-821/compiler/inference]0;Holmake: ~/regression/cakeml-821/compiler/inference[1mWorking in $(CAKEMLDIR)/compiler/inference[0m
]0;Holmake: ~/regression/cakeml-821/compiler]0;Holmake: ~/regression/cakeml-821/compiler[1mWorking in $(CAKEMLDIR)/compiler[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-821/compiler/backend/proofs]0;Holmake: ~/regression/cakeml-821/compiler/backend/gc]0;Holmake: ~/regression/cakeml-821/compiler/backend/gc[1mWorking in $(CAKEMLDIR)/compiler/backend/gc[0m
]0;Holmake: ~/regression/cakeml-821/compiler/backend/proofs]0;Holmake: ~/regression/cakeml-821/compiler/backend/reg_alloc/proofs]0;Holmake: ~/regression/cakeml-821/compiler/backend/reg_alloc/proofs[1mWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
]0;Holmake: ~/regression/cakeml-821/compiler/backend/proofs]0;Holmake: ~/regression/cakeml-821/compiler/backend/semantics]0;Holmake: ~/regression/cakeml-821/compiler/backend/semantics[1mWorking in $(CAKEMLDIR)/compiler/backend/semantics[0m
]0;Holmake: ~/regression/cakeml-821/compiler/backend/proofs]0;Holmake: ~/regression/cakeml-821/compiler/backend/proofs[1mWorking in $(CAKEMLDIR)/compiler/backend/proofs[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-821/compiler/backend/x64/proofs]0;Holmake: ~/regression/cakeml-821/compiler/encoders/x64/proofs]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/x64/prog]0;Holmake: ~/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/x64/prog[1mWorking in $(HOLDIR)/examples/l3-machine-code/x64/prog[0m
]0;Holmake: ~/regression/cakeml-821/compiler/encoders/x64/proofs]0;Holmake: ~/regression/cakeml-821/compiler/encoders/x64/proofs[1mWorking in $(CAKEMLDIR)/compiler/encoders/x64/proofs[0m
]0;Holmake: ~/regression/cakeml-821/compiler/backend/x64/proofs]0;Holmake: ~/regression/cakeml-821/compiler/backend/x64/proofs[1mWorking in $(CAKEMLDIR)/compiler/backend/x64/proofs[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/tutorial/solutions[0m
Starting work on simple_bstTheory
Starting work on splitwordsTheory
Starting work on README.md
Starting work on make_ex
README.md                                           OK
make_ex                                             OK
Starting work on exercises
exercises                                           OK
splitwordsTheory                                    OK
Starting work on wordfreqProgTheory
simple_bstTheory                                    OK
wordfreqProgTheory                                  OK
Starting work on wordfreqCompileTheory
wordfreqCompileTheory                               OK
Starting work on wordfreqProofTheory
wordfreqProofTheory                        FAILED! <1>
 
 which has type
 
 :inode
 
 unification failure message: Attempt to unify different type operators: mlstring$mlstring and fsFFI$inode
 
 error in quse /home/myreen/regression/cakeml-821/tutorial/solutions/wordfreqProofScript.sml : HOL_ERR {message = "on line 42, characters 22-31:\n\nType inference failure: unable to infer a type for the application of\n\ninFS_fname (fs :IO_fs)\n\non line 42, characters 7-32\n\nwhich has type\n\n:mlstring -> bool\n\nto\n\nFile (fname :mlstring)\n\non line 42, characters 22-31\n\nwhich has type\n\n:inode\n\nunification failure message: Attempt to unify different type operators: mlstring$mlstring and fsFFI$inode\n", origin_function = "type-analysis", origin_structure = "Preterm"}
 error in load wordfreqProofScript : HOL_ERR {message = "on line 42, characters 22-31:\n\nType inference failure: unable to infer a type for the application of\n\ninFS_fname (fs :IO_fs)\n\non line 42, characters 7-32\n\nwhich has type\n\n:mlstring -> bool\n\nto\n\nFile (fname :mlstring)\n\non line 42, characters 22-31\n\nwhich has type\n\n:inode\n\nunification failure message: Attempt to unify different type operators: mlstring$mlstring and fsFFI$inode\n", origin_function = "type-analysis", origin_structure = "Preterm"}
 Uncaught exception: HOL_ERR {message = "on line 42, characters 22-31:\n\nType inference failure: unable to infer a type for the application of\n\ninFS_fname (fs :IO_fs)\n\non line 42, characters 7-32\n\nwhich has type\n\n:mlstring -> bool\n\nto\n\nFile (fname :mlstring)\n\non line 42, characters 22-31\n\nwhich has type\n\n:inode\n\nunification failure message: Attempt to unify different type operators: mlstring$mlstring and fsFFI$inode\n", origin_function = "type-analysis", origin_structure = "Preterm"}