Job 850

CakeML:3b2a4f472fafe48b96ec0bf9a69914bfab51a081
  Attempt fixes after 45a84e07ec595193a2d3bacd455722f180ec814c [May 08 18:45:33]
#629 (vstte18)
Merging into:331972bc323d7886b60ecbab12195ee6999bcdeb
  Merge pull request #634 from CakeML/cleanup [May 08 15:37:32]
HOL:544f92fea1905436f7a85854eed6dcb089568063
  Emacs mode: key-bindings for  [May 05 04:49:45]
Machine:te1

May 08 18:47:03 Claimed job
May 08 18:47:07 Reusing HOL
May 08 18:48:03 Starting developers
May 08 18:48:06 Finished developers                                               2s  34MB
May 08 18:48:06 Starting developers/bin
May 08 18:48:12 Finished developers/bin                                           6s 933MB
May 08 18:48:12 Starting semantics/ffi
May 08 18:48:26 Finished semantics/ffi                                           13s 245MB
May 08 18:48:26 Starting semantics
May 08 18:50:21 Finished semantics                                             1m54s   1GB
May 08 18:50:21 Starting semantics/proofs
May 08 18:54:37 Finished semantics/proofs                                      4m15s   1GB
May 08 18:54:37 Starting basis/pure
May 08 18:55:42 Finished basis/pure                                            1m05s 646MB
May 08 18:55:42 Starting translator
May 08 18:57:59 Finished translator                                            2m16s   1GB
May 08 18:57:59 Starting compiler/parsing
May 08 18:59:18 Finished compiler/parsing                                      1m18s   2GB
May 08 18:59:18 Starting characteristic
May 08 19:06:43 Finished characteristic                                        7m25s   2GB
May 08 19:06:43 Starting translator/monadic
May 08 19:08:50 Finished translator/monadic                                    2m06s   1GB
May 08 19:08:50 Starting basis
May 08 19:31:55 Finished basis                                                23m04s   3GB
May 08 19:31:55 Starting compiler/inference
May 08 19:34:28 Finished compiler/inference                                    2m33s   1GB
May 08 19:34:28 Starting compiler/backend/reg_alloc
May 08 19:35:49 Finished compiler/backend/reg_alloc                            1m20s   1GB
May 08 19:35:49 Starting compiler/backend/gc
May 08 19:48:24 Finished compiler/backend/gc                                  12m32s   1GB
May 08 19:48:24 Starting compiler/backend
May 08 19:48:27 Finished compiler/backend                                         2s  34MB
May 08 19:48:27 Starting compiler/encoders/asm
May 08 19:48:28 Finished compiler/encoders/asm                                    1s  31MB
May 08 19:48:28 Starting compiler/encoders/x64
May 08 19:49:56 Finished compiler/encoders/x64                                 1m28s 726MB
May 08 19:49:57 Starting compiler/encoders/arm6
May 08 19:52:18 Finished compiler/encoders/arm6                                2m21s   1GB
May 08 19:52:18 Starting compiler/encoders/arm8
May 08 19:53:04 Finished compiler/encoders/arm8                                  45s 553MB
May 08 19:53:04 Starting compiler/encoders/mips
May 08 19:54:44 Finished compiler/encoders/mips                                1m38s 938MB
May 08 19:54:44 Starting compiler/encoders/riscv
May 08 19:56:34 Finished compiler/encoders/riscv                               1m50s   1GB
May 08 19:56:34 Starting compiler/encoders/ag32
May 08 19:56:58 Finished compiler/encoders/ag32                                  23s 660MB
May 08 19:56:58 Starting compiler/backend/x64
May 08 19:57:22 Finished compiler/backend/x64                                    24s   1GB
May 08 19:57:23 Starting compiler/backend/arm6
May 08 19:57:49 Finished compiler/backend/arm6                                   26s   1GB
May 08 19:57:49 Starting compiler/backend/arm8
May 08 19:58:13 Finished compiler/backend/arm8                                   23s   1GB
May 08 19:58:13 Starting compiler/backend/mips
May 08 19:58:40 Finished compiler/backend/mips                                   26s   1GB
May 08 19:58:40 Starting compiler/backend/riscv
May 08 19:59:06 Finished compiler/backend/riscv                                  26s   1GB
May 08 19:59:06 Starting compiler/backend/ag32
May 08 20:00:36 Finished compiler/backend/ag32                                 1m30s   1GB
May 08 20:00:36 Starting compiler/parsing/proofs
May 08 20:09:14 Finished compiler/parsing/proofs                               8m38s   1GB
May 08 20:09:15 Starting compiler/inference/proofs
May 08 20:13:03 Finished compiler/inference/proofs                             3m48s 984MB
May 08 20:13:03 Starting compiler/backend/semantics
May 08 20:22:09 Finished compiler/backend/semantics                            9m06s   1GB
May 08 20:22:09 Starting compiler/backend/reg_alloc/proofs
May 09 06:39:49 Resuming compiler/backend/reg_alloc/proofs
May 09 06:39:51 Finished compiler/backend/reg_alloc/proofs                        1s  34MB
May 09 06:39:51 Starting compiler/backend/proofs
May 09 07:30:45 Finished compiler/backend/proofs                              50m53s   4GB
May 09 07:30:45 Starting compiler/encoders/x64/proofs
May 09 07:44:24 Finished compiler/encoders/x64/proofs                         13m38s   4GB
May 09 07:44:24 Starting compiler/encoders/arm6/proofs
May 09 08:02:18 Finished compiler/encoders/arm6/proofs                        17m53s   4GB
May 09 08:02:18 Starting compiler/encoders/arm8/proofs
May 09 08:11:35 Finished compiler/encoders/arm8/proofs                         9m16s   1GB
May 09 08:11:35 Starting compiler/encoders/mips/proofs
May 09 08:25:14 Finished compiler/encoders/mips/proofs                        13m39s   2GB
May 09 08:25:14 Starting compiler/encoders/riscv/proofs
May 09 08:36:37 Finished compiler/encoders/riscv/proofs                       11m22s   1GB
May 09 08:36:37 Starting compiler/encoders/ag32/proofs
May 09 08:39:51 Finished compiler/encoders/ag32/proofs                         3m14s   1GB
May 09 08:39:51 Starting compiler/backend/x64/proofs
May 09 08:40:17 Finished compiler/backend/x64/proofs                             25s   1GB
May 09 08:40:17 Starting compiler/backend/arm6/proofs
May 09 08:40:45 Finished compiler/backend/arm6/proofs                            28s   1GB
May 09 08:40:45 Starting compiler/backend/arm8/proofs
May 09 08:41:12 Finished compiler/backend/arm8/proofs                            26s   1GB
May 09 08:41:12 Starting compiler/backend/mips/proofs
May 09 08:41:38 Finished compiler/backend/mips/proofs                            26s 905MB
May 09 08:41:38 Starting compiler/backend/riscv/proofs
May 09 08:42:06 Finished compiler/backend/riscv/proofs                           27s   1GB
May 09 08:42:06 Starting compiler/backend/ag32/proofs
May 09 08:54:08 Finished compiler/backend/ag32/proofs                         12m02s   2GB
May 09 08:54:08 Starting compiler/proofs
May 09 08:55:53 Finished compiler/proofs                                       1m45s   3GB
May 09 08:55:54 Starting candle/set-theory
May 09 08:56:31 Finished candle/set-theory                                       37s 727MB
May 09 08:56:31 Starting candle/syntax-lib
May 09 08:56:46 Finished candle/syntax-lib                                       14s 653MB
May 09 08:56:46 Starting candle/standard/syntax
May 09 08:59:14 Finished candle/standard/syntax                                2m27s 848MB
May 09 08:59:14 Starting candle/standard/semantics
May 09 09:01:34 Finished candle/standard/semantics                             2m19s   1GB
May 09 09:01:34 Starting candle/standard/monadic
May 09 09:03:43 Finished candle/standard/monadic                               2m08s   1GB
May 09 09:03:43 Starting candle/standard/ml_kernel
May 09 09:08:44 Finished candle/standard/ml_kernel                             5m01s   5GB
May 09 09:08:44 Starting candle/standard/opentheory
May 09 09:20:23 Finished candle/standard/opentheory                           11m38s   3GB
May 09 09:20:23 Starting candle/standard/opentheory/compilation
May 09 09:57:03 Finished candle/standard/opentheory/compilation               36m39s  20GB
May 09 09:57:03 Starting candle/standard/opentheory/compilation/proofs
May 09 09:58:04 Finished candle/standard/opentheory/compilation/proofs         1m00s   2GB
May 09 09:58:04 Starting characteristic/examples
May 09 09:59:56 Finished characteristic/examples                               1m51s   2GB
May 09 09:59:56 Starting tutorial/solutions
May 09 10:17:13 Finished tutorial/solutions                                   17m17s   7GB
May 09 10:17:13 Starting translator/monadic/examples
May 09 10:20:49 Finished translator/monadic/examples                           3m35s   2GB
May 09 10:20:49 Starting examples
May 09 10:26:56 FAILED: examples
]0;Holmake: ~/regression-worker/HOL-544f92fea1905436f7a85854eed6dcb089568063/examples/formal-languages/regular]0;Holmake: ~/regression-worker/HOL-544f92fea1905436f7a85854eed6dcb089568063/examples/formal-languages]0;Holmake: ~/regression-worker/HOL-544f92fea1905436f7a85854eed6dcb089568063/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression-worker/HOL-544f92fea1905436f7a85854eed6dcb089568063/examples/formal-languages/regular]0;Holmake: ~/regression-worker/HOL-544f92fea1905436f7a85854eed6dcb089568063/examples/formal-languages/context-free]0;Holmake: ~/regression-worker/HOL-544f92fea1905436f7a85854eed6dcb089568063/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression-worker/HOL-544f92fea1905436f7a85854eed6dcb089568063/examples/formal-languages/regular]0;Holmake: ~/regression-worker/HOL-544f92fea1905436f7a85854eed6dcb089568063/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: .]0;Holmake: ~/regression-worker/cakeml-850/basis]0;Holmake: ~/regression-worker/cakeml-850/basis/pure]0;Holmake: ~/regression-worker/cakeml-850/misc]0;Holmake: ~/regression-worker/HOL-544f92fea1905436f7a85854eed6dcb089568063/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression-worker/HOL-544f92fea1905436f7a85854eed6dcb089568063/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression-worker/cakeml-850/misc]0;Holmake: ~/regression-worker/HOL-544f92fea1905436f7a85854eed6dcb089568063/examples/machine-code/hoare-triple]0;Holmake: ~/regression-worker/HOL-544f92fea1905436f7a85854eed6dcb089568063/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/regression-worker/cakeml-850/misc]0;Holmake: ~/regression-worker/cakeml-850/developers]0;Holmake: ~/regression-worker/cakeml-850/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression-worker/cakeml-850/misc]0;Holmake: ~/regression-worker/cakeml-850/misc/lem_lib_stub]0;Holmake: ~/regression-worker/cakeml-850/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression-worker/cakeml-850/misc]0;Holmake: ~/regression-worker/cakeml-850/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression-worker/cakeml-850/basis/pure]0;Holmake: ~/regression-worker/cakeml-850/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ~/regression-worker/cakeml-850/basis]0;Holmake: ~/regression-worker/cakeml-850/characteristic]0;Holmake: ~/regression-worker/cakeml-850/compiler/parsing]0;Holmake: ~/regression-worker/cakeml-850/semantics]0;Holmake: ~/regression-worker/cakeml-850/semantics/ffi]0;Holmake: ~/regression-worker/cakeml-850/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression-worker/cakeml-850/semantics]0;Holmake: ~/regression-worker/cakeml-850/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression-worker/cakeml-850/compiler/parsing]0;Holmake: ~/regression-worker/cakeml-850/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/regression-worker/cakeml-850/characteristic]0;Holmake: ~/regression-worker/cakeml-850/semantics/proofs]0;Holmake: ~/regression-worker/cakeml-850/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ~/regression-worker/cakeml-850/characteristic]0;Holmake: ~/regression-worker/cakeml-850/translator]0;Holmake: ~/regression-worker/cakeml-850/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/regression-worker/cakeml-850/characteristic]0;Holmake: ~/regression-worker/cakeml-850/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ~/regression-worker/cakeml-850/basis]0;Holmake: ~/regression-worker/cakeml-850/translator/monadic]0;Holmake: ~/regression-worker/cakeml-850/translator/monadic/monad_base]0;Holmake: ~/regression-worker/cakeml-850/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ~/regression-worker/cakeml-850/translator/monadic]0;Holmake: ~/regression-worker/cakeml-850/translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ~/regression-worker/cakeml-850/basis]0;Holmake: ~/regression-worker/cakeml-850/basis[1mWorking in $(CAKEMLDIR)/basis[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/examples[0m
Starting work on quicksortProgTheory
Starting work on catProgTheory
Starting work on lcsTheory
Starting work on divTheory
lcsTheory                                                                    OK
Starting work on diffTheory
diffTheory                                                                   OK
Starting work on diffProgTheory
catProgTheory                                                                OK
Starting work on doubleProgTheory
quicksortProgTheory                                                          OK
Starting work on array_searchProgTheory
divTheory                                                                    OK
Starting work on echoProgTheory
diffProgTheory                                                               OK
Starting work on filterProgTheory
doubleProgTheory                                                             OK
Starting work on grepProgTheory
echoProgTheory                                                               OK
Starting work on helloErrProgTheory
array_searchProgTheory                                                       OK
Starting work on helloProgTheory
filterProgTheory                                                             OK
Starting work on insertSortProgTheory
helloErrProgTheory                                                           OK
Starting work on iocatProgTheory
helloProgTheory                                                              OK
Starting work on patchProgTheory
iocatProgTheory                                                     FAILED! <1>
 Found near
   [
      Abbr [QUOTE " (*#loc 105 13*)fs'"],
      up_stdo_def,
      IO_fs_component_equality,
      fsupdate_def,
      openFileFS_numchars,
      ...
      ]
 Uncaught exception: Fail "Static Errors"
grepProgTheory                                                         M-KILLED
insertSortProgTheory                                                   M-KILLED
patchProgTheory                                                        M-KILLED