Job 1043

CakeML:880f818f08f12d69b750c9a9b81af72b37d64d92
  adjust to changes in regexpLib [Sep 28 01:50:23]
#691 (regexp_delta)
Merging into:30193e4df86fc6ee1df59c8baf4b125c84ba01d4
  Merge pull request #690 from CakeML/close-files [Sep 13 07:50:45]
HOL:1fbe26f2ca95a6681d6e2bcc7d28a2eae130fe3a
  Merge commit '51d49' into develop [Sep 23 06:58:50]
Machine:stove 4.15.0-55-generic x86_64 GNU/Linux

Sep 28 08:28:53 Claimed job
Sep 28 08:28:59 Building HOL
Sep 28 08:39:12 Starting developers
Sep 28 08:39:16 Finished developers                                               3s 113MB
Sep 28 08:39:16 Starting developers/bin
Sep 28 08:39:22 Finished developers/bin                                           5s 963MB
Sep 28 08:39:22 Starting semantics/ffi
Sep 28 08:40:00 Finished semantics/ffi                                           37s 385MB
Sep 28 08:40:00 Starting semantics
Sep 28 08:41:31 Finished semantics                                             1m31s   1GB
Sep 28 08:41:31 Starting semantics/proofs
Sep 28 08:44:23 Finished semantics/proofs                                      2m51s   1GB
Sep 28 08:44:23 Starting semantics/alt_semantics
Sep 28 08:44:30 Finished semantics/alt_semantics                                  7s 327MB
Sep 28 08:44:30 Starting semantics/alt_semantics/proofs
Sep 28 08:46:16 Finished semantics/alt_semantics/proofs                        1m45s 777MB
Sep 28 08:46:16 Starting basis/pure
Sep 28 08:49:55 Finished basis/pure                                            3m39s 715MB
Sep 28 08:49:55 Starting translator
Sep 28 08:51:39 Finished translator                                            1m43s   1GB
Sep 28 08:51:39 Starting compiler/parsing
Sep 28 08:52:33 Finished compiler/parsing                                        54s   2GB
Sep 28 08:52:33 Starting characteristic
Sep 28 08:57:39 Finished characteristic                                        5m05s   1GB
Sep 28 08:57:39 Starting translator/monadic
Sep 28 08:59:07 Finished translator/monadic                                    1m27s   1GB
Sep 28 08:59:07 Starting basis
Sep 28 09:17:45 Finished basis                                                18m38s   3GB
Sep 28 09:17:46 Starting compiler/inference
Sep 28 09:19:37 Finished compiler/inference                                    1m51s   1GB
Sep 28 09:19:37 Starting compiler/backend/reg_alloc
Sep 28 09:20:35 Finished compiler/backend/reg_alloc                              57s   1GB
Sep 28 09:20:35 Starting compiler/backend/gc
Sep 28 09:29:22 Finished compiler/backend/gc                                   8m46s   2GB
Sep 28 09:29:22 Starting compiler/backend
Sep 28 09:29:24 Finished compiler/backend                                         2s  22MB
Sep 28 09:29:24 Starting compiler/encoders/asm
Sep 28 09:29:25 Finished compiler/encoders/asm                                    1s  27MB
Sep 28 09:29:26 Starting compiler/encoders/x64
Sep 28 09:30:24 Finished compiler/encoders/x64                                   58s 752MB
Sep 28 09:30:24 Starting compiler/encoders/arm7
Sep 28 09:31:59 Finished compiler/encoders/arm7                                1m35s   1GB
Sep 28 09:31:59 Starting compiler/encoders/arm8
Sep 28 09:32:30 Finished compiler/encoders/arm8                                  31s 915MB
Sep 28 09:32:30 Starting compiler/encoders/mips
Sep 28 09:33:35 Finished compiler/encoders/mips                                1m04s   1GB
Sep 28 09:33:35 Starting compiler/encoders/riscv
Sep 28 09:34:52 Finished compiler/encoders/riscv                               1m17s   1GB
Sep 28 09:34:52 Starting compiler/encoders/ag32
Sep 28 09:35:08 Finished compiler/encoders/ag32                                  16s 791MB
Sep 28 09:35:08 Starting compiler/backend/x64
Sep 28 09:35:26 Finished compiler/backend/x64                                    17s 951MB
Sep 28 09:35:26 Starting compiler/backend/arm7
Sep 28 09:35:45 Finished compiler/backend/arm7                                   18s   1GB
Sep 28 09:35:45 Starting compiler/backend/arm8
Sep 28 09:36:03 Finished compiler/backend/arm8                                   17s   1GB
Sep 28 09:36:03 Starting compiler/backend/mips
Sep 28 09:36:21 Finished compiler/backend/mips                                   18s   1GB
Sep 28 09:36:21 Starting compiler/backend/riscv
Sep 28 09:36:40 Finished compiler/backend/riscv                                  18s   1GB
Sep 28 09:36:40 Starting compiler/backend/ag32
Sep 28 09:37:45 Finished compiler/backend/ag32                                 1m04s 971MB
Sep 28 09:37:45 Starting compiler/parsing/proofs
Sep 28 09:43:14 Finished compiler/parsing/proofs                               5m29s 835MB
Sep 28 09:43:14 Starting compiler/inference/proofs
Sep 28 09:45:52 Finished compiler/inference/proofs                             2m37s   1GB
Sep 28 09:45:52 Starting compiler/backend/semantics
Sep 28 09:51:26 Finished compiler/backend/semantics                            5m33s   2GB
Sep 28 09:51:26 Starting compiler/backend/reg_alloc/proofs
Sep 28 09:54:32 Finished compiler/backend/reg_alloc/proofs                     3m05s 833MB
Sep 28 09:54:32 Starting compiler/backend/proofs
Sep 28 10:30:51 Finished compiler/backend/proofs                              36m19s   4GB
Sep 28 10:30:51 Starting compiler/encoders/x64/proofs
Sep 28 10:40:23 Finished compiler/encoders/x64/proofs                          9m31s   4GB
Sep 28 10:40:23 Starting compiler/encoders/arm7/proofs
Sep 28 10:53:00 Finished compiler/encoders/arm7/proofs                        12m37s   3GB
Sep 28 10:53:00 Starting compiler/encoders/arm8/proofs
Sep 28 10:59:18 Finished compiler/encoders/arm8/proofs                         6m17s   1GB
Sep 28 10:59:18 Starting compiler/encoders/mips/proofs
Sep 28 11:08:44 Finished compiler/encoders/mips/proofs                         9m25s   1GB
Sep 28 11:08:44 Starting compiler/encoders/riscv/proofs
Sep 28 11:16:38 Finished compiler/encoders/riscv/proofs                        7m54s   1GB
Sep 28 11:16:38 Starting compiler/encoders/ag32/proofs
Sep 28 11:19:00 Finished compiler/encoders/ag32/proofs                         2m21s 683MB
Sep 28 11:19:00 Starting compiler/backend/x64/proofs
Sep 28 11:19:19 Finished compiler/backend/x64/proofs                             18s   1GB
Sep 28 11:19:19 Starting compiler/backend/arm7/proofs
Sep 28 11:19:39 Finished compiler/backend/arm7/proofs                            19s   1GB
Sep 28 11:19:39 Starting compiler/backend/arm8/proofs
Sep 28 11:19:57 Finished compiler/backend/arm8/proofs                            18s   1GB
Sep 28 11:19:57 Starting compiler/backend/mips/proofs
Sep 28 11:20:16 Finished compiler/backend/mips/proofs                            18s   1GB
Sep 28 11:20:16 Starting compiler/backend/riscv/proofs
Sep 28 11:20:35 Finished compiler/backend/riscv/proofs                           18s   1GB
Sep 28 11:20:35 Starting compiler/backend/ag32/proofs
Sep 28 11:28:47 Finished compiler/backend/ag32/proofs                          8m11s   2GB
Sep 28 11:28:47 Starting compiler/proofs
Sep 28 11:30:30 Finished compiler/proofs                                       1m42s   3GB
Sep 28 11:30:30 Starting candle/set-theory
Sep 28 11:30:56 Finished candle/set-theory                                       25s 671MB
Sep 28 11:30:56 Starting candle/syntax-lib
Sep 28 11:31:06 Finished candle/syntax-lib                                       10s 468MB
Sep 28 11:31:06 Starting candle/standard/syntax
Sep 28 11:32:45 Finished candle/standard/syntax                                1m38s 895MB
Sep 28 11:32:45 Starting candle/standard/semantics
Sep 28 11:34:18 Finished candle/standard/semantics                             1m32s   1GB
Sep 28 11:34:18 Starting candle/standard/monadic
Sep 28 11:35:49 Finished candle/standard/monadic                               1m30s   1GB
Sep 28 11:35:49 Starting candle/standard/ml_kernel
Sep 28 11:39:25 Finished candle/standard/ml_kernel                             3m35s   5GB
Sep 28 11:39:25 Starting candle/standard/opentheory
Sep 28 11:47:46 Finished candle/standard/opentheory                            8m21s   4GB
Sep 28 11:47:46 Starting candle/standard/opentheory/compilation
Sep 28 12:15:29 Finished candle/standard/opentheory/compilation               27m42s  16GB
Sep 28 12:15:29 Starting candle/standard/opentheory/compilation/proofs
Sep 28 12:16:17 Finished candle/standard/opentheory/compilation/proofs           48s   2GB
Sep 28 12:16:17 Starting characteristic/examples
Sep 28 12:17:39 Finished characteristic/examples                               1m21s   2GB
Sep 28 12:17:39 Starting tutorial/solutions
Sep 28 12:30:15 Finished tutorial/solutions                                   12m36s   7GB
Sep 28 12:30:15 Starting translator/monadic/examples
Sep 28 12:32:58 Finished translator/monadic/examples                           2m42s   2GB
Sep 28 12:32:58 Starting examples
Sep 28 12:36:00 FAILED: examples
]0;Holmake: ~/cakeml/regression/HOL-1fbe26f2ca95a6681d6e2bcc7d28a2eae130fe3a/examples/formal-languages/regular]0;Holmake: ~/cakeml/regression/HOL-1fbe26f2ca95a6681d6e2bcc7d28a2eae130fe3a/examples/formal-languages]0;Holmake: ~/cakeml/regression/HOL-1fbe26f2ca95a6681d6e2bcc7d28a2eae130fe3a/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/cakeml/regression/HOL-1fbe26f2ca95a6681d6e2bcc7d28a2eae130fe3a/examples/formal-languages/regular]0;Holmake: ~/cakeml/regression/HOL-1fbe26f2ca95a6681d6e2bcc7d28a2eae130fe3a/examples/formal-languages/context-free]0;Holmake: ~/cakeml/regression/HOL-1fbe26f2ca95a6681d6e2bcc7d28a2eae130fe3a/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/cakeml/regression/HOL-1fbe26f2ca95a6681d6e2bcc7d28a2eae130fe3a/examples/formal-languages/regular]0;Holmake: ~/cakeml/regression/HOL-1fbe26f2ca95a6681d6e2bcc7d28a2eae130fe3a/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: .]0;Holmake: ~/cakeml/regression/cakeml-1043/basis]0;Holmake: ~/cakeml/regression/cakeml-1043/basis/pure]0;Holmake: ~/cakeml/regression/cakeml-1043/misc]0;Holmake: ~/cakeml/regression/HOL-1fbe26f2ca95a6681d6e2bcc7d28a2eae130fe3a/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/cakeml/regression/HOL-1fbe26f2ca95a6681d6e2bcc7d28a2eae130fe3a/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/cakeml/regression/cakeml-1043/misc]0;Holmake: ~/cakeml/regression/HOL-1fbe26f2ca95a6681d6e2bcc7d28a2eae130fe3a/examples/machine-code/hoare-triple]0;Holmake: ~/cakeml/regression/HOL-1fbe26f2ca95a6681d6e2bcc7d28a2eae130fe3a/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/cakeml/regression/cakeml-1043/misc]0;Holmake: ~/cakeml/regression/cakeml-1043/developers]0;Holmake: ~/cakeml/regression/cakeml-1043/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/cakeml/regression/cakeml-1043/misc]0;Holmake: ~/cakeml/regression/cakeml-1043/misc/lem_lib_stub]0;Holmake: ~/cakeml/regression/cakeml-1043/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/cakeml/regression/cakeml-1043/misc]0;Holmake: ~/cakeml/regression/cakeml-1043/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/cakeml/regression/cakeml-1043/basis/pure]0;Holmake: ~/cakeml/regression/cakeml-1043/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ~/cakeml/regression/cakeml-1043/basis]0;Holmake: ~/cakeml/regression/cakeml-1043/characteristic]0;Holmake: ~/cakeml/regression/cakeml-1043/compiler/parsing]0;Holmake: ~/cakeml/regression/cakeml-1043/semantics]0;Holmake: ~/cakeml/regression/cakeml-1043/semantics/ffi]0;Holmake: ~/cakeml/regression/cakeml-1043/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/cakeml/regression/cakeml-1043/semantics]0;Holmake: ~/cakeml/regression/cakeml-1043/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/cakeml/regression/cakeml-1043/compiler/parsing]0;Holmake: ~/cakeml/regression/cakeml-1043/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/cakeml/regression/cakeml-1043/characteristic]0;Holmake: ~/cakeml/regression/cakeml-1043/semantics/proofs]0;Holmake: ~/cakeml/regression/cakeml-1043/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ~/cakeml/regression/cakeml-1043/characteristic]0;Holmake: ~/cakeml/regression/cakeml-1043/translator]0;Holmake: ~/cakeml/regression/cakeml-1043/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/cakeml/regression/cakeml-1043/characteristic]0;Holmake: ~/cakeml/regression/cakeml-1043/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ~/cakeml/regression/cakeml-1043/basis]0;Holmake: ~/cakeml/regression/cakeml-1043/translator/monadic]0;Holmake: ~/cakeml/regression/cakeml-1043/translator/monadic/monad_base]0;Holmake: ~/cakeml/regression/cakeml-1043/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ~/cakeml/regression/cakeml-1043/translator/monadic]0;Holmake: ~/cakeml/regression/cakeml-1043/translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ~/cakeml/regression/cakeml-1043/basis]0;Holmake: ~/cakeml/regression/cakeml-1043/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                                       real:   12s  user:   11s     OK
Starting work on diffTheory
diffTheory                                      real:   42s  user:   41s     OK
Starting work on diffProgTheory
catProgTheory                                   real:   78s  user:   75s     OK
Starting work on doubleProgTheory
quicksortProgTheory                             real:  107s  user:  105s     OK
Starting work on array_searchProgTheory
diffProgTheory                                  real:   84s  user:   82s     OK
Starting work on echoProgTheory
divTheory                                       real:  145s  user:  143s     OK
Starting work on filterProgTheory
filterProgTheory                                real:   33s  user:   32sFAIL<1>
 <<HOL message: mk_functional: 
   pattern completion has added 1 clause to the original specification.>>
 <<HOL message: Created theory "filterProg">>
 error in quse /home/cur/sao/cakeml/regression/cakeml-1043/examples/filterProgScript.sml : Fail "Static Errors"
 error in load filterProgScript : Fail "Static Errors"
 Loading translation: MapProg ... done.
 /home/cur/sao/cakeml/regression/cakeml-1043/examples/filterProgScript.sml:22: error: Value or constructor (gen_dfa) has not been declared in structure regexpLib
 Found near
   regexpLib.gen_dfa regexpLib.HOL (Regexp_Type.fromString the_regexp)
 Uncaught exception: Fail "Static Errors"
doubleProgTheory                                                        M-KILLED
array_searchProgTheory                                                  M-KILLED
echoProgTheory                                                          M-KILLED