Job 1032

CakeML:4833035eb6a9c7ec4b99dd50da57d837469725ad
  adapt to changes in regexpLib [Sep 09 08:40:53]
#689 (regexp_repair)
Merging into:f8746ce03b63e2867d62acf3ea403ea5414963c7
  Merge pull request #688 from CakeML/issue683 [Sep 08 06:17:31]
HOL:4dba4f20d2f9dce4c8a659aeb7ebbe040a90fda6
  upgraded regexp compiler to use binary-map set to represent worklist; [Sep 04 04:16:57]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Sep 09 10:49:33 Claimed job
Sep 09 10:49:38 Reusing HOL
Sep 09 10:49:47 Starting developers
Sep 09 10:49:49 Finished developers                                               1s 123MB
Sep 09 10:49:49 Starting developers/bin
Sep 09 10:49:53 Finished developers/bin                                           3s 238MB
Sep 09 10:49:54 Starting semantics/ffi
Sep 09 10:50:03 Finished semantics/ffi                                            8s 215MB
Sep 09 10:50:03 Starting semantics
Sep 09 10:51:19 Finished semantics                                             1m16s   1GB
Sep 09 10:51:20 Starting semantics/proofs
Sep 09 10:54:17 Finished semantics/proofs                                      2m57s   1GB
Sep 09 10:54:17 Starting semantics/alt_semantics
Sep 09 10:54:24 Finished semantics/alt_semantics                                  5s 246MB
Sep 09 10:54:24 Starting semantics/alt_semantics/proofs
Sep 09 10:56:12 Finished semantics/alt_semantics/proofs                        1m47s 787MB
Sep 09 10:56:12 Starting basis/pure
Sep 09 10:56:56 Finished basis/pure                                              44s 659MB
Sep 09 10:56:57 Starting translator
Sep 09 10:58:41 Finished translator                                            1m43s   1GB
Sep 09 10:58:41 Starting compiler/parsing
Sep 09 10:59:39 Finished compiler/parsing                                        57s   1GB
Sep 09 10:59:39 Starting characteristic
Sep 09 11:04:46 Finished characteristic                                        5m06s   2GB
Sep 09 11:04:46 Starting translator/monadic
Sep 09 11:06:10 Finished translator/monadic                                    1m24s   1GB
Sep 09 11:06:11 Starting basis
Sep 09 11:25:27 Finished basis                                                19m16s   2GB
Sep 09 11:25:27 Starting compiler/inference
Sep 09 11:27:01 Finished compiler/inference                                    1m33s   2GB
Sep 09 11:27:01 Starting compiler/backend/reg_alloc
Sep 09 11:27:58 Finished compiler/backend/reg_alloc                              56s   1GB
Sep 09 11:27:59 Starting compiler/backend/gc
Sep 09 11:35:59 Finished compiler/backend/gc                                   7m59s   1GB
Sep 09 11:35:59 Starting compiler/backend
Sep 09 11:36:00 Finished compiler/backend                                         0s  45MB
Sep 09 11:36:00 Starting compiler/encoders/asm
Sep 09 11:36:01 Finished compiler/encoders/asm                                    0s  35MB
Sep 09 11:36:01 Starting compiler/encoders/x64
Sep 09 11:36:24 Finished compiler/encoders/x64                                   22s 664MB
Sep 09 11:36:24 Starting compiler/encoders/arm7
Sep 09 11:37:09 Finished compiler/encoders/arm7                                  44s 747MB
Sep 09 11:37:09 Starting compiler/encoders/arm8
Sep 09 11:37:21 Finished compiler/encoders/arm8                                  11s 533MB
Sep 09 11:37:21 Starting compiler/encoders/mips
Sep 09 11:37:36 Finished compiler/encoders/mips                                  14s 801MB
Sep 09 11:37:37 Starting compiler/encoders/riscv
Sep 09 11:37:50 Finished compiler/encoders/riscv                                 12s 810MB
Sep 09 11:37:50 Starting compiler/encoders/ag32
Sep 09 11:38:05 Finished compiler/encoders/ag32                                  14s 758MB
Sep 09 11:38:05 Starting compiler/backend/x64
Sep 09 11:38:21 Finished compiler/backend/x64                                    15s   1GB
Sep 09 11:38:21 Starting compiler/backend/arm7
Sep 09 11:38:39 Finished compiler/backend/arm7                                   17s   1GB
Sep 09 11:38:40 Starting compiler/backend/arm8
Sep 09 11:38:56 Finished compiler/backend/arm8                                   15s 918MB
Sep 09 11:38:56 Starting compiler/backend/mips
Sep 09 11:39:13 Finished compiler/backend/mips                                   16s   1GB
Sep 09 11:39:13 Starting compiler/backend/riscv
Sep 09 11:39:30 Finished compiler/backend/riscv                                  16s   1GB
Sep 09 11:39:30 Starting compiler/backend/ag32
Sep 09 11:40:36 Finished compiler/backend/ag32                                 1m05s   1GB
Sep 09 11:40:36 Starting compiler/parsing/proofs
Sep 09 11:46:02 Finished compiler/parsing/proofs                               5m26s 815MB
Sep 09 11:46:03 Starting compiler/inference/proofs
Sep 09 11:48:41 Finished compiler/inference/proofs                             2m37s   1GB
Sep 09 11:48:41 Starting compiler/backend/semantics
Sep 09 11:54:31 Finished compiler/backend/semantics                            5m49s   2GB
Sep 09 11:54:31 Starting compiler/backend/reg_alloc/proofs
Sep 09 11:57:43 Finished compiler/backend/reg_alloc/proofs                     3m11s 775MB
Sep 09 11:57:44 Starting compiler/backend/proofs
Sep 09 12:37:37 Finished compiler/backend/proofs                              39m53s   4GB
Sep 09 12:37:38 Starting compiler/encoders/x64/proofs
Sep 09 12:46:42 Finished compiler/encoders/x64/proofs                          9m04s   4GB
Sep 09 12:46:42 Starting compiler/encoders/arm7/proofs
Sep 09 12:58:58 Finished compiler/encoders/arm7/proofs                        12m15s   3GB
Sep 09 12:58:58 Starting compiler/encoders/arm8/proofs
Sep 09 13:05:27 Finished compiler/encoders/arm8/proofs                         6m28s   1GB
Sep 09 13:05:27 Starting compiler/encoders/mips/proofs
Sep 09 13:14:48 Finished compiler/encoders/mips/proofs                         9m21s   2GB
Sep 09 13:14:49 Starting compiler/encoders/riscv/proofs
Sep 09 13:22:59 Finished compiler/encoders/riscv/proofs                        8m10s   1GB
Sep 09 13:23:00 Starting compiler/encoders/ag32/proofs
Sep 09 13:25:26 Finished compiler/encoders/ag32/proofs                         2m26s 835MB
Sep 09 13:25:26 Starting compiler/backend/x64/proofs
Sep 09 13:25:43 Finished compiler/backend/x64/proofs                             16s   1GB
Sep 09 13:25:43 Starting compiler/backend/arm7/proofs
Sep 09 13:26:00 Finished compiler/backend/arm7/proofs                            16s 877MB
Sep 09 13:26:00 Starting compiler/backend/arm8/proofs
Sep 09 13:26:16 Finished compiler/backend/arm8/proofs                            15s   1GB
Sep 09 13:26:16 Starting compiler/backend/mips/proofs
Sep 09 13:26:34 Finished compiler/backend/mips/proofs                            17s   1GB
Sep 09 13:26:34 Starting compiler/backend/riscv/proofs
Sep 09 13:26:51 Finished compiler/backend/riscv/proofs                           16s   1GB
Sep 09 13:26:51 Starting compiler/backend/ag32/proofs
Sep 09 13:35:32 Finished compiler/backend/ag32/proofs                          8m41s   2GB
Sep 09 13:35:33 Starting compiler/proofs
Sep 09 13:36:51 Finished compiler/proofs                                       1m17s   3GB
Sep 09 13:36:51 Starting candle/set-theory
Sep 09 13:37:16 Finished candle/set-theory                                       24s 673MB
Sep 09 13:37:16 Starting candle/syntax-lib
Sep 09 13:37:25 Finished candle/syntax-lib                                        8s 642MB
Sep 09 13:37:26 Starting candle/standard/syntax
Sep 09 13:39:05 Finished candle/standard/syntax                                1m39s   1GB
Sep 09 13:39:06 Starting candle/standard/semantics
Sep 09 13:40:39 Finished candle/standard/semantics                             1m33s   1GB
Sep 09 13:40:39 Starting candle/standard/monadic
Sep 09 13:42:11 Finished candle/standard/monadic                               1m31s   1GB
Sep 09 13:42:12 Starting candle/standard/ml_kernel
Sep 09 13:45:59 Finished candle/standard/ml_kernel                             3m47s   6GB
Sep 09 13:45:59 Starting candle/standard/opentheory
Sep 09 13:54:36 Finished candle/standard/opentheory                            8m36s   3GB
Sep 09 13:54:36 Starting candle/standard/opentheory/compilation
Sep 09 14:24:49 Finished candle/standard/opentheory/compilation               30m12s  17GB
Sep 09 14:24:50 Starting candle/standard/opentheory/compilation/proofs
Sep 09 14:25:33 Finished candle/standard/opentheory/compilation/proofs           42s   2GB
Sep 09 14:25:33 Starting characteristic/examples
Sep 09 14:26:58 Finished characteristic/examples                               1m24s   2GB
Sep 09 14:26:58 Starting tutorial/solutions
Sep 09 14:39:44 Finished tutorial/solutions                                   12m45s   6GB
Sep 09 14:39:44 Starting translator/monadic/examples
Sep 09 14:42:34 Finished translator/monadic/examples                           2m49s   2GB
Sep 09 14:42:34 Starting examples
Sep 09 14:46:17 FAILED: examples
]0;Holmake: ~/regression/HOL-4dba4f20d2f9dce4c8a659aeb7ebbe040a90fda6/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-4dba4f20d2f9dce4c8a659aeb7ebbe040a90fda6/examples/formal-languages]0;Holmake: ~/regression/HOL-4dba4f20d2f9dce4c8a659aeb7ebbe040a90fda6/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression/HOL-4dba4f20d2f9dce4c8a659aeb7ebbe040a90fda6/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-4dba4f20d2f9dce4c8a659aeb7ebbe040a90fda6/examples/formal-languages/context-free]0;Holmake: ~/regression/HOL-4dba4f20d2f9dce4c8a659aeb7ebbe040a90fda6/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression/HOL-4dba4f20d2f9dce4c8a659aeb7ebbe040a90fda6/examples/formal-languages/regular]0;Holmake: ~/regression/HOL-4dba4f20d2f9dce4c8a659aeb7ebbe040a90fda6/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: .]0;Holmake: ~/regression/cakeml-1032/basis]0;Holmake: ~/regression/cakeml-1032/basis/pure]0;Holmake: ~/regression/cakeml-1032/misc]0;Holmake: ~/regression/HOL-4dba4f20d2f9dce4c8a659aeb7ebbe040a90fda6/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression/HOL-4dba4f20d2f9dce4c8a659aeb7ebbe040a90fda6/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ~/regression/cakeml-1032/misc]0;Holmake: ~/regression/HOL-4dba4f20d2f9dce4c8a659aeb7ebbe040a90fda6/examples/machine-code/hoare-triple]0;Holmake: ~/regression/HOL-4dba4f20d2f9dce4c8a659aeb7ebbe040a90fda6/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ~/regression/cakeml-1032/misc]0;Holmake: ~/regression/cakeml-1032/developers]0;Holmake: ~/regression/cakeml-1032/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-1032/misc]0;Holmake: ~/regression/cakeml-1032/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-1032/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-1032/misc]0;Holmake: ~/regression/cakeml-1032/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression/cakeml-1032/basis/pure]0;Holmake: ~/regression/cakeml-1032/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ~/regression/cakeml-1032/basis]0;Holmake: ~/regression/cakeml-1032/characteristic]0;Holmake: ~/regression/cakeml-1032/compiler/parsing]0;Holmake: ~/regression/cakeml-1032/semantics]0;Holmake: ~/regression/cakeml-1032/semantics/ffi]0;Holmake: ~/regression/cakeml-1032/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-1032/semantics]0;Holmake: ~/regression/cakeml-1032/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression/cakeml-1032/compiler/parsing]0;Holmake: ~/regression/cakeml-1032/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/regression/cakeml-1032/characteristic]0;Holmake: ~/regression/cakeml-1032/semantics/proofs]0;Holmake: ~/regression/cakeml-1032/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ~/regression/cakeml-1032/characteristic]0;Holmake: ~/regression/cakeml-1032/translator]0;Holmake: ~/regression/cakeml-1032/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/regression/cakeml-1032/characteristic]0;Holmake: ~/regression/cakeml-1032/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ~/regression/cakeml-1032/basis]0;Holmake: ~/regression/cakeml-1032/translator/monadic]0;Holmake: ~/regression/cakeml-1032/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-1032/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ~/regression/cakeml-1032/translator/monadic]0;Holmake: ~/regression/cakeml-1032/translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ~/regression/cakeml-1032/basis]0;Holmake: ~/regression/cakeml-1032/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
diffProgTheory                                                                                             OK
Starting work on echoProgTheory
divTheory                                                                                                  OK
Starting work on filterProgTheory
doubleProgTheory                                                                                           OK
Starting work on grepProgTheory
filterProgTheory                                                                                  FAILED! <1>
 WARNING: matcher has a precondition.
 
 Saved theorem _____ "matcher_v_thm"
 /home/myreen/regression/cakeml-1032/examples/filterProgScript.sml:179: error: Value or constructor (compile_regexp_good_vec) has not been declared in structure regexp_compilerTheory
 Found near
   SIMP_RULE std_ss [dom_Brz_alt_equal]
   regexp_compilerTheory.compile_regexp_good_vec
 error in quse /home/myreen/regression/cakeml-1032/examples/filterProgScript.sml : Fail "Static Errors"
 error in load filterProgScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"
array_searchProgTheory                                                                               M-KILLED
echoProgTheory                                                                                       M-KILLED
grepProgTheory                                                                                       M-KILLED