Overview

Job 1043

CakeML:880f818f08f12d69b750c9a9b81af72b37d64d92
  adjust to changes in regexpLib
#691 (regexp_delta)
Merging into:30193e4df86fc6ee1df59c8baf4b125c84ba01d4
  Merge pull request #690 from CakeML/close-files
HOL:1fbe26f2ca95a6681d6e2bcc7d28a2eae130fe3a
  Merge commit '51d49' into develop
Machine:stove 4.15.0-55-generic x86_64 GNU/Linux

 Claimed job
 Building HOL
 Starting developers
 Finished developers                                               3s 113MB
 Starting developers/bin
 Finished developers/bin                                           5s 963MB
 Starting semantics/ffi
 Finished semantics/ffi                                           37s 385MB
 Starting semantics
 Finished semantics                                             1m31s   1GB
 Starting semantics/proofs
 Finished semantics/proofs                                      2m51s   1GB
 Starting semantics/alt_semantics
 Finished semantics/alt_semantics                                  7s 327MB
 Starting semantics/alt_semantics/proofs
 Finished semantics/alt_semantics/proofs                        1m45s 777MB
 Starting basis/pure
 Finished basis/pure                                            3m39s 715MB
 Starting translator
 Finished translator                                            1m43s   1GB
 Starting compiler/parsing
 Finished compiler/parsing                                        54s   2GB
 Starting characteristic
 Finished characteristic                                        5m05s   1GB
 Starting translator/monadic
 Finished translator/monadic                                    1m27s   1GB
 Starting basis
 Finished basis                                                18m38s   3GB
 Starting compiler/inference
 Finished compiler/inference                                    1m51s   1GB
 Starting compiler/backend/reg_alloc
 Finished compiler/backend/reg_alloc                              57s   1GB
 Starting compiler/backend/gc
 Finished compiler/backend/gc                                   8m46s   2GB
 Starting compiler/backend
 Finished compiler/backend                                         2s  22MB
 Starting compiler/encoders/asm
 Finished compiler/encoders/asm                                    1s  27MB
 Starting compiler/encoders/x64
 Finished compiler/encoders/x64                                   58s 752MB
 Starting compiler/encoders/arm7
 Finished compiler/encoders/arm7                                1m35s   1GB
 Starting compiler/encoders/arm8
 Finished compiler/encoders/arm8                                  31s 915MB
 Starting compiler/encoders/mips
 Finished compiler/encoders/mips                                1m04s   1GB
 Starting compiler/encoders/riscv
 Finished compiler/encoders/riscv                               1m17s   1GB
 Starting compiler/encoders/ag32
 Finished compiler/encoders/ag32                                  16s 791MB
 Starting compiler/backend/x64
 Finished compiler/backend/x64                                    17s 951MB
 Starting compiler/backend/arm7
 Finished compiler/backend/arm7                                   18s   1GB
 Starting compiler/backend/arm8
 Finished compiler/backend/arm8                                   17s   1GB
 Starting compiler/backend/mips
 Finished compiler/backend/mips                                   18s   1GB
 Starting compiler/backend/riscv
 Finished compiler/backend/riscv                                  18s   1GB
 Starting compiler/backend/ag32
 Finished compiler/backend/ag32                                 1m04s 971MB
 Starting compiler/parsing/proofs
 Finished compiler/parsing/proofs                               5m29s 835MB
 Starting compiler/inference/proofs
 Finished compiler/inference/proofs                             2m37s   1GB
 Starting compiler/backend/semantics
 Finished compiler/backend/semantics                            5m33s   2GB
 Starting compiler/backend/reg_alloc/proofs
 Finished compiler/backend/reg_alloc/proofs                     3m05s 833MB
 Starting compiler/backend/proofs
 Finished compiler/backend/proofs                              36m19s   4GB
 Starting compiler/encoders/x64/proofs
 Finished compiler/encoders/x64/proofs                          9m31s   4GB
 Starting compiler/encoders/arm7/proofs
 Finished compiler/encoders/arm7/proofs                        12m37s   3GB
 Starting compiler/encoders/arm8/proofs
 Finished compiler/encoders/arm8/proofs                         6m17s   1GB
 Starting compiler/encoders/mips/proofs
 Finished compiler/encoders/mips/proofs                         9m25s   1GB
 Starting compiler/encoders/riscv/proofs
 Finished compiler/encoders/riscv/proofs                        7m54s   1GB
 Starting compiler/encoders/ag32/proofs
 Finished compiler/encoders/ag32/proofs                         2m21s 683MB
 Starting compiler/backend/x64/proofs
 Finished compiler/backend/x64/proofs                             18s   1GB
 Starting compiler/backend/arm7/proofs
 Finished compiler/backend/arm7/proofs                            19s   1GB
 Starting compiler/backend/arm8/proofs
 Finished compiler/backend/arm8/proofs                            18s   1GB
 Starting compiler/backend/mips/proofs
 Finished compiler/backend/mips/proofs                            18s   1GB
 Starting compiler/backend/riscv/proofs
 Finished compiler/backend/riscv/proofs                           18s   1GB
 Starting compiler/backend/ag32/proofs
 Finished compiler/backend/ag32/proofs                          8m11s   2GB
 Starting compiler/proofs
 Finished compiler/proofs                                       1m42s   3GB
 Starting candle/set-theory
 Finished candle/set-theory                                       25s 671MB
 Starting candle/syntax-lib
 Finished candle/syntax-lib                                       10s 468MB
 Starting candle/standard/syntax
 Finished candle/standard/syntax                                1m38s 895MB
 Starting candle/standard/semantics
 Finished candle/standard/semantics                             1m32s   1GB
 Starting candle/standard/monadic
 Finished candle/standard/monadic                               1m30s   1GB
 Starting candle/standard/ml_kernel
 Finished candle/standard/ml_kernel                             3m35s   5GB
 Starting candle/standard/opentheory
 Finished candle/standard/opentheory                            8m21s   4GB
 Starting candle/standard/opentheory/compilation
 Finished candle/standard/opentheory/compilation               27m42s  16GB
 Starting candle/standard/opentheory/compilation/proofs
 Finished candle/standard/opentheory/compilation/proofs           48s   2GB
 Starting characteristic/examples
 Finished characteristic/examples                               1m21s   2GB
 Starting tutorial/solutions
 Finished tutorial/solutions                                   12m36s   7GB
 Starting translator/monadic/examples
 Finished translator/monadic/examples                           2m42s   2GB
 Starting examples
 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