Job 827

CakeML:97d18a828eaebf8d279e6bb9b2059b4041759060
  Fix wordfreq proof [Apr 29 15:29:41]
#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:brain08 4.14.89.1.amd64-smp x86_64 GNU/Linux

Apr 30 12:38:37 Claimed job
Apr 30 12:38:39 Reusing HOL
Apr 30 12:53:21 Starting developers
Apr 30 12:53:22 Finished developers                                               1s  34MB
Apr 30 12:53:22 Starting developers/bin
Apr 30 12:53:32 Finished developers/bin                                           9s 937MB
Apr 30 12:53:32 Starting semantics/ffi
Apr 30 12:54:43 Finished semantics/ffi                                         1m10s 514MB
Apr 30 12:54:43 Starting semantics
Apr 30 12:57:39 Finished semantics                                             2m55s   1GB
Apr 30 12:57:40 Starting semantics/proofs
Apr 30 13:03:25 Finished semantics/proofs                                      5m45s 980MB
Apr 30 13:03:25 Starting basis/pure
Apr 30 13:10:13 Finished basis/pure                                            6m47s 699MB
Apr 30 13:10:13 Starting translator
Apr 30 13:13:27 Finished translator                                            3m13s   1GB
Apr 30 13:13:27 Starting compiler/parsing
Apr 30 13:15:20 Finished compiler/parsing                                      1m53s   2GB
Apr 30 13:15:21 Starting characteristic
Apr 30 13:25:33 Finished characteristic                                       10m12s   2GB
Apr 30 13:25:34 Starting translator/monadic
Apr 30 13:28:22 Finished translator/monadic                                    2m48s   1GB
Apr 30 13:28:22 Starting basis
Apr 30 14:00:48 Finished basis                                                32m25s   2GB
Apr 30 14:00:48 Starting compiler/inference
Apr 30 14:04:31 Finished compiler/inference                                    3m42s   1GB
Apr 30 14:04:32 Starting compiler/backend/reg_alloc
Apr 30 14:06:09 Finished compiler/backend/reg_alloc                            1m37s   1GB
Apr 30 14:06:09 Starting compiler/backend/gc
Apr 30 14:22:13 Finished compiler/backend/gc                                  16m04s   2GB
Apr 30 14:22:14 Starting compiler/backend
Apr 30 14:22:22 Finished compiler/backend                                         8s 297MB
Apr 30 14:22:22 Starting compiler/encoders/asm
Apr 30 14:22:23 Finished compiler/encoders/asm                                    0s  27MB
Apr 30 14:22:24 Starting compiler/encoders/x64
Apr 30 14:24:22 Finished compiler/encoders/x64                                 1m57s 931MB
Apr 30 14:24:22 Starting compiler/encoders/arm6
Apr 30 14:27:58 Finished compiler/encoders/arm6                                3m35s   2GB
Apr 30 14:27:58 Starting compiler/encoders/arm8
Apr 30 14:29:02 Finished compiler/encoders/arm8                                1m03s 851MB
Apr 30 14:29:02 Starting compiler/encoders/mips
Apr 30 14:31:16 Finished compiler/encoders/mips                                2m14s   1GB
Apr 30 14:31:16 Starting compiler/encoders/riscv
Apr 30 14:33:48 Finished compiler/encoders/riscv                               2m31s   1GB
Apr 30 14:33:48 Starting compiler/encoders/ag32
Apr 30 14:34:17 Finished compiler/encoders/ag32                                  29s 661MB
Apr 30 14:34:18 Starting compiler/backend/x64
Apr 30 14:34:57 Finished compiler/backend/x64                                    39s 893MB
Apr 30 14:34:57 Starting compiler/backend/arm6
Apr 30 14:35:36 Finished compiler/backend/arm6                                   38s   1GB
Apr 30 14:35:37 Starting compiler/backend/arm8
Apr 30 14:36:16 Finished compiler/backend/arm8                                   38s   1GB
Apr 30 14:36:16 Starting compiler/backend/mips
Apr 30 14:36:56 Finished compiler/backend/mips                                   39s 895MB
Apr 30 14:36:56 Starting compiler/backend/riscv
Apr 30 14:37:32 Finished compiler/backend/riscv                                  35s   1GB
Apr 30 14:37:32 Starting compiler/backend/ag32
Apr 30 14:39:53 Finished compiler/backend/ag32                                 2m20s   1GB
Apr 30 14:39:53 Starting compiler/parsing/proofs
Apr 30 14:50:33 Finished compiler/parsing/proofs                              10m39s   1GB
Apr 30 14:50:33 Starting compiler/inference/proofs
Apr 30 14:55:55 Finished compiler/inference/proofs                             5m22s   1GB
Apr 30 14:55:56 Starting compiler/backend/semantics
Apr 30 15:09:34 Finished compiler/backend/semantics                           13m38s   2GB
Apr 30 15:09:34 Starting compiler/backend/reg_alloc/proofs
Apr 30 15:16:06 Finished compiler/backend/reg_alloc/proofs                     6m31s   1GB
Apr 30 15:16:06 Starting compiler/backend/proofs
Apr 30 16:22:57 Finished compiler/backend/proofs                            1h06m50s   4GB
Apr 30 16:22:57 Starting compiler/encoders/x64/proofs
Apr 30 16:43:36 Finished compiler/encoders/x64/proofs                         20m38s   6GB
Apr 30 16:43:36 Starting compiler/encoders/arm6/proofs
Apr 30 17:11:49 Finished compiler/encoders/arm6/proofs                        28m12s   5GB
Apr 30 17:11:49 Starting compiler/encoders/arm8/proofs
Apr 30 17:24:56 Finished compiler/encoders/arm8/proofs                        13m06s   2GB
Apr 30 17:24:57 Starting compiler/encoders/mips/proofs
Apr 30 17:44:54 Finished compiler/encoders/mips/proofs                        19m57s   2GB
Apr 30 17:44:54 Starting compiler/encoders/riscv/proofs
Apr 30 18:01:36 Finished compiler/encoders/riscv/proofs                       16m41s   1GB
Apr 30 18:01:36 Starting compiler/encoders/ag32/proofs
Apr 30 18:06:36 Finished compiler/encoders/ag32/proofs                         4m59s   1GB
Apr 30 18:06:36 Starting compiler/backend/x64/proofs
Apr 30 18:07:17 Finished compiler/backend/x64/proofs                             40s   1GB
Apr 30 18:07:17 Starting compiler/backend/arm6/proofs
Apr 30 18:08:02 Finished compiler/backend/arm6/proofs                            44s   1GB
Apr 30 18:08:02 Starting compiler/backend/arm8/proofs
Apr 30 18:08:43 Finished compiler/backend/arm8/proofs                            40s   1GB
Apr 30 18:08:43 Starting compiler/backend/mips/proofs
Apr 30 18:09:23 Finished compiler/backend/mips/proofs                            39s 999MB
Apr 30 18:09:24 Starting compiler/backend/riscv/proofs
Apr 30 18:10:04 Finished compiler/backend/riscv/proofs                           40s   1GB
Apr 30 18:10:04 Starting compiler/backend/ag32/proofs
Apr 30 18:28:01 Finished compiler/backend/ag32/proofs                         17m57s   2GB
Apr 30 18:28:02 Starting compiler/proofs
Apr 30 18:30:42 Finished compiler/proofs                                       2m40s   2GB
Apr 30 18:30:42 Starting candle/set-theory
Apr 30 18:31:29 Finished candle/set-theory                                       46s 686MB
Apr 30 18:31:30 Starting candle/syntax-lib
Apr 30 18:31:54 Finished candle/syntax-lib                                       24s 640MB
Apr 30 18:31:54 Starting candle/standard/syntax
Apr 30 18:35:15 Finished candle/standard/syntax                                3m20s   1GB
Apr 30 18:35:15 Starting candle/standard/semantics
Apr 30 18:38:29 Finished candle/standard/semantics                             3m13s   1GB
Apr 30 18:38:29 Starting candle/standard/monadic
Apr 30 18:41:34 Finished candle/standard/monadic                               3m04s   1GB
Apr 30 18:41:34 Starting candle/standard/ml_kernel
Apr 30 18:48:57 Finished candle/standard/ml_kernel                             7m22s   3GB
Apr 30 18:48:58 Starting candle/standard/opentheory
Apr 30 19:05:30 Finished candle/standard/opentheory                           16m32s   3GB
Apr 30 19:05:30 Starting candle/standard/opentheory/compilation
Apr 30 19:58:26 Finished candle/standard/opentheory/compilation               52m55s  13GB
Apr 30 19:58:26 Starting candle/standard/opentheory/compilation/proofs
Apr 30 19:59:53 Finished candle/standard/opentheory/compilation/proofs         1m26s   2GB
Apr 30 19:59:53 Starting characteristic/examples
Apr 30 20:02:46 Finished characteristic/examples                               2m52s   2GB
Apr 30 20:02:46 Starting tutorial/solutions
Apr 30 20:28:08 Finished tutorial/solutions                                   25m22s   4GB
Apr 30 20:28:08 Starting translator/monadic/examples
Apr 30 20:32:30 Finished translator/monadic/examples                           4m20s   2GB
Apr 30 20:32:30 Starting examples
Apr 30 20:45:49 Finished examples                                             13m18s   3GB
Apr 30 20:45:49 Starting examples/compilation/x64
May 01 00:33:11 Finished examples/compilation/x64                           3h47m21s  13GB
May 01 00:33:11 Starting examples/compilation/x64/proofs
May 01 00:35:43 Finished examples/compilation/x64/proofs                       2m32s   2GB
May 01 00:35:44 Starting examples/compilation/ag32
May 01 01:28:08 Finished examples/compilation/ag32                            52m23s   7GB
May 01 01:28:08 Starting examples/compilation/ag32/proofs
May 01 01:29:18 FAILED: examples/compilation/ag32/proofs
]0;Holmake: /local/hbecker/regression/cakeml-827/basis/pure]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/formal-languages/regular]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/formal-languages]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/formal-languagesWorking in $(HOLDIR)/examples/formal-languages
]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/formal-languages/regular]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/formal-languages/context-free]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/formal-languages/context-freeWorking in $(HOLDIR)/examples/formal-languages/context-free
]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/formal-languages/regular]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/formal-languages/regularWorking in $(HOLDIR)/examples/formal-languages/regular
Starting work on regexp2dfa
regexp2dfa                                                                                                                       OK
]0;Holmake: /local/hbecker/regression/cakeml-827/basis/pure]0;Holmake: /local/hbecker/regression/cakeml-827/misc]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/fun-op-sem/lprefix_lub]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/fun-op-sem/lprefix_lubWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub
]0;Holmake: /local/hbecker/regression/cakeml-827/misc]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/machine-code/hoare-triple]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/machine-code/hoare-tripleWorking in $(HOLDIR)/examples/machine-code/hoare-triple
]0;Holmake: /local/hbecker/regression/cakeml-827/misc]0;Holmake: /local/hbecker/regression/cakeml-827/developers]0;Holmake: /local/hbecker/regression/cakeml-827/developersWorking in $(CAKEMLDIR)/developers
]0;Holmake: /local/hbecker/regression/cakeml-827/misc]0;Holmake: /local/hbecker/regression/cakeml-827/misc/lem_lib_stub]0;Holmake: /local/hbecker/regression/cakeml-827/misc/lem_lib_stubWorking in $(CAKEMLDIR)/misc/lem_lib_stub
]0;Holmake: /local/hbecker/regression/cakeml-827/misc]0;Holmake: /local/hbecker/regression/cakeml-827/miscWorking in $(CAKEMLDIR)/misc
]0;Holmake: /local/hbecker/regression/cakeml-827/basis/pure]0;Holmake: /local/hbecker/regression/cakeml-827/basis/pureWorking in $(CAKEMLDIR)/basis/pure
]0;Holmake: /local/hbecker/regression/cakeml-827/basis]0;Holmake: /local/hbecker/regression/cakeml-827/characteristic]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/parsing]0;Holmake: /local/hbecker/regression/cakeml-827/semantics]0;Holmake: /local/hbecker/regression/cakeml-827/semantics/ffi]0;Holmake: /local/hbecker/regression/cakeml-827/semantics/ffiWorking in $(CAKEMLDIR)/semantics/ffi
]0;Holmake: /local/hbecker/regression/cakeml-827/semantics]0;Holmake: /local/hbecker/regression/cakeml-827/semanticsWorking in $(CAKEMLDIR)/semantics
]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/parsing]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/parsingWorking in $(CAKEMLDIR)/compiler/parsing
]0;Holmake: /local/hbecker/regression/cakeml-827/characteristic]0;Holmake: /local/hbecker/regression/cakeml-827/semantics/proofs]0;Holmake: /local/hbecker/regression/cakeml-827/semantics/proofsWorking in $(CAKEMLDIR)/semantics/proofs
]0;Holmake: /local/hbecker/regression/cakeml-827/characteristic]0;Holmake: /local/hbecker/regression/cakeml-827/translator]0;Holmake: /local/hbecker/regression/cakeml-827/translatorWorking in $(CAKEMLDIR)/translator
]0;Holmake: /local/hbecker/regression/cakeml-827/characteristic]0;Holmake: /local/hbecker/regression/cakeml-827/characteristicWorking in $(CAKEMLDIR)/characteristic
]0;Holmake: /local/hbecker/regression/cakeml-827/basis]0;Holmake: /local/hbecker/regression/cakeml-827/translator/monadic]0;Holmake: /local/hbecker/regression/cakeml-827/translator/monadic/monad_base]0;Holmake: /local/hbecker/regression/cakeml-827/translator/monadic/monad_baseWorking in $(CAKEMLDIR)/translator/monadic/monad_base
]0;Holmake: /local/hbecker/regression/cakeml-827/translator/monadic]0;Holmake: /local/hbecker/regression/cakeml-827/translator/monadicWorking in $(CAKEMLDIR)/translator/monadic
]0;Holmake: /local/hbecker/regression/cakeml-827/basis]0;Holmake: /local/hbecker/regression/cakeml-827/basisWorking in $(CAKEMLDIR)/basis
]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/backend/ag32]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/backend]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/machine-code/multiword]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/machine-code/multiwordWorking in $(HOLDIR)/examples/machine-code/multiword
]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/backend]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/backend/reg_alloc]0;Holmake: /local/hbecker/regression/cakeml-827/unverified/reg_alloc]0;Holmake: /local/hbecker/regression/cakeml-827/unverified/reg_allocWorking in $(CAKEMLDIR)/unverified/reg_alloc
]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/backend/reg_alloc]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/backend/reg_allocWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc
]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/backend]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/encoders/asm]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/common]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/commonWorking in $(HOLDIR)/examples/l3-machine-code/common
]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/encoders/asm]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/encoders/asmWorking in $(CAKEMLDIR)/compiler/encoders/asm
]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/backend]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/backendWorking in $(CAKEMLDIR)/compiler/backend
]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/backend/ag32]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/encoders/ag32]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/encoders/ag32Working in $(CAKEMLDIR)/compiler/encoders/ag32
]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/backend/ag32]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/backend/ag32Working in $(CAKEMLDIR)/compiler/backend/ag32
]0;Holmake: .]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/backend/ag32/proofs]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/machine-code/decompiler]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/machine-code/decompilerWorking in $(HOLDIR)/examples/machine-code/decompiler
]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/backend/ag32/proofs]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/backend/proofs]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/backend/gc]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/backend/gcWorking in $(CAKEMLDIR)/compiler/backend/gc
]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/backend/proofs]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/backend/reg_alloc/proofs]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/backend/reg_alloc/proofsWorking in $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/backend/proofs]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/backend/semantics]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/backend/semanticsWorking in $(CAKEMLDIR)/compiler/backend/semantics
]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/backend/proofs]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/backend/proofsWorking in $(CAKEMLDIR)/compiler/backend/proofs
]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/backend/ag32/proofs]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/encoders/ag32/proofs]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/encoders/ag32/proofsWorking in $(CAKEMLDIR)/compiler/encoders/ag32/proofs
]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/backend/ag32/proofs]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/backend/ag32/proofsWorking in $(CAKEMLDIR)/compiler/backend/ag32/proofs
]0;Holmake: .]0;Holmake: ../../..]0;Holmake: ../../..Working in $(CAKEMLDIR)/examples
]0;Holmake: .]0;Holmake: ..]0;Holmake: /local/hbecker/regression/cakeml-827/compiler]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/backend/arm6]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/encoders/arm6]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/arm/model]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/lib]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/libWorking in $(HOLDIR)/examples/l3-machine-code/lib
]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/arm/model]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/arm/modelWorking in $(HOLDIR)/examples/l3-machine-code/arm/model
]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/encoders/arm6]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/arm/step]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-codeWorking in $(HOLDIR)/examples/l3-machine-code
]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/arm/step]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/arm/stepWorking in $(HOLDIR)/examples/l3-machine-code/arm/step
]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/encoders/arm6]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/encoders/arm6Working in $(CAKEMLDIR)/compiler/encoders/arm6
]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/backend/arm6]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/backend/arm6Working in $(CAKEMLDIR)/compiler/backend/arm6
]0;Holmake: /local/hbecker/regression/cakeml-827/compiler]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/backend/arm8]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/encoders/arm8]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/arm8/model]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/arm8/modelWorking in $(HOLDIR)/examples/l3-machine-code/arm8/model
]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/encoders/arm8]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/arm8/step]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/arm8/stepWorking in $(HOLDIR)/examples/l3-machine-code/arm8/step
]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/encoders/arm8]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/encoders/arm8Working in $(CAKEMLDIR)/compiler/encoders/arm8
]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/backend/arm8]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/backend/arm8Working in $(CAKEMLDIR)/compiler/backend/arm8
]0;Holmake: /local/hbecker/regression/cakeml-827/compiler]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/backend/mips]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/encoders/mips]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/mips/model]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/mips/modelWorking in $(HOLDIR)/examples/l3-machine-code/mips/model
]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/encoders/mips]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/mips/step]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/mips/stepWorking in $(HOLDIR)/examples/l3-machine-code/mips/step
]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/encoders/mips]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/encoders/mipsWorking in $(CAKEMLDIR)/compiler/encoders/mips
]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/backend/mips]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/backend/mipsWorking in $(CAKEMLDIR)/compiler/backend/mips
]0;Holmake: /local/hbecker/regression/cakeml-827/compiler]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/backend/riscv]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/encoders/riscv]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/riscv/model]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/riscv/modelWorking in $(HOLDIR)/examples/l3-machine-code/riscv/model
]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/encoders/riscv]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/riscv/step]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/riscv/stepWorking in $(HOLDIR)/examples/l3-machine-code/riscv/step
]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/encoders/riscv]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/encoders/riscvWorking in $(CAKEMLDIR)/compiler/encoders/riscv
]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/backend/riscv]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/backend/riscvWorking in $(CAKEMLDIR)/compiler/backend/riscv
]0;Holmake: /local/hbecker/regression/cakeml-827/compiler]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/backend/x64]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/encoders/x64]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/x64/model]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/x64/modelWorking in $(HOLDIR)/examples/l3-machine-code/x64/model
]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/encoders/x64]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/x64/step]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/l3-machine-code/x64/stepWorking in $(HOLDIR)/examples/l3-machine-code/x64/step
]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/encoders/x64]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/encoders/x64Working in $(CAKEMLDIR)/compiler/encoders/x64
]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/backend/x64]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/backend/x64Working in $(CAKEMLDIR)/compiler/backend/x64
]0;Holmake: /local/hbecker/regression/cakeml-827/compiler]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/inference]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/unification/triangular/first-order]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/unification/triangular]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/unification/triangularWorking in $(HOLDIR)/examples/unification/triangular
]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/unification/triangular/first-order]0;Holmake: /local/hbecker/regression/HOL-8e183cc626814e8bfbee46abcbf51798ee1c69b6/examples/unification/triangular/first-orderWorking in $(HOLDIR)/examples/unification/triangular/first-order
]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/inference]0;Holmake: /local/hbecker/regression/cakeml-827/compiler/inferenceWorking in $(CAKEMLDIR)/compiler/inference
]0;Holmake: /local/hbecker/regression/cakeml-827/compiler]0;Holmake: /local/hbecker/regression/cakeml-827/compilerWorking in $(CAKEMLDIR)/compiler
]0;Holmake: ..]0;Holmake: ..Working in $(CAKEMLDIR)/examples/compilation/ag32
]0;Holmake: .]0;Holmake: .Working in $(CAKEMLDIR)/examples/compilation/ag32/proofs
Starting work on helloProofTheory
Starting work on sortProofTheory
Starting work on wordcountProofTheory
Starting work on README.md
README.md                                                                                                                        OK
helloProofTheory                                                                                                        FAILED! <1>
 Proof of 
 
 wfcl cl 
 extract_writes 1
   (MAP get_output_io_event (hello_io_events cl (stdin_fs inp))) =
 "Hello World!\n"
 
 failed.
 Failed to prove theorem hello_extract_writes_stdout.
 Uncaught exception: HOL_ERR {message = "first subgoal not solved by second tactic (THEN1 on line 134) (THEN1 on line 135) (THEN1 on line 139)", origin_function = "THEN1", origin_structure = "Tactical"}
sortProofTheory                                                                                                            M-KILLED
wordcountProofTheory                                                                                                       M-KILLED