CakeML Regression Test

Job 1028

CakeML:67adb612363d45c5e20127cef6b64a9d3ad43081
  Make some disruptive overloads local [Sep 06 05:34:04]
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 06 05:34:19 Claimed job
Sep 06 05:34:27 Reusing HOL
Sep 06 05:34:32 Starting developers
Sep 06 05:34:34 Finished developers                                               2s 114MB
Sep 06 05:34:34 Starting developers/bin
Sep 06 05:35:59 Finished developers/bin                                        1m24s 165MB
Sep 06 05:36:00 Starting semantics/ffi
Sep 06 05:36:11 Finished semantics/ffi                                           11s 217MB
Sep 06 05:36:12 Starting semantics
Sep 06 05:38:03 Finished semantics                                             1m51s   1GB
Sep 06 05:38:04 Starting semantics/proofs
Sep 06 05:41:17 Finished semantics/proofs                                      3m12s   1GB
Sep 06 05:41:17 Starting semantics/alt_semantics
Sep 06 05:41:23 Finished semantics/alt_semantics                                  5s 267MB
Sep 06 05:41:23 Starting semantics/alt_semantics/proofs
Sep 06 05:43:10 Finished semantics/alt_semantics/proofs                        1m46s   1GB
Sep 06 05:43:10 Starting basis/pure
Sep 06 05:43:55 Finished basis/pure                                              44s 660MB
Sep 06 05:43:55 Starting translator
Sep 06 05:45:40 Finished translator                                            1m43s   1GB
Sep 06 05:45:40 Starting compiler/parsing
Sep 06 05:46:36 Finished compiler/parsing                                        55s   1GB
Sep 06 05:46:37 Starting characteristic
Sep 06 05:51:44 Finished characteristic                                        5m06s   1GB
Sep 06 05:51:44 Starting translator/monadic
Sep 06 05:53:09 Finished translator/monadic                                    1m25s   1GB
Sep 06 05:53:09 Starting basis
Sep 06 06:12:10 Finished basis                                                19m00s   2GB
Sep 06 06:12:10 Starting compiler/inference
Sep 06 06:13:46 Finished compiler/inference                                    1m35s   1GB
Sep 06 06:13:46 Starting compiler/backend/reg_alloc
Sep 06 06:14:44 Finished compiler/backend/reg_alloc                              57s   1GB
Sep 06 06:14:45 Starting compiler/backend/gc
Sep 06 06:22:40 Finished compiler/backend/gc                                   7m54s   1GB
Sep 06 06:22:40 Starting compiler/backend
Sep 06 06:22:42 Finished compiler/backend                                         0s  45MB
Sep 06 06:22:42 Starting compiler/encoders/asm
Sep 06 06:22:43 Finished compiler/encoders/asm                                    0s  35MB
Sep 06 06:22:43 Starting compiler/encoders/x64
Sep 06 06:23:06 Finished compiler/encoders/x64                                   22s 703MB
Sep 06 06:23:07 Starting compiler/encoders/arm7
Sep 06 06:23:51 Finished compiler/encoders/arm7                                  44s 745MB
Sep 06 06:23:52 Starting compiler/encoders/arm8
Sep 06 06:24:03 Finished compiler/encoders/arm8                                  11s 884MB
Sep 06 06:24:04 Starting compiler/encoders/mips
Sep 06 06:24:19 Finished compiler/encoders/mips                                  14s 766MB
Sep 06 06:24:19 Starting compiler/encoders/riscv
Sep 06 06:24:33 Finished compiler/encoders/riscv                                 12s 807MB
Sep 06 06:24:33 Starting compiler/encoders/ag32
Sep 06 06:24:48 Finished compiler/encoders/ag32                                  14s 745MB
Sep 06 06:24:49 Starting compiler/backend/x64
Sep 06 06:25:05 Finished compiler/backend/x64                                    15s   1GB
Sep 06 06:25:05 Starting compiler/backend/arm7
Sep 06 06:25:23 Finished compiler/backend/arm7                                   17s   1GB
Sep 06 06:25:24 Starting compiler/backend/arm8
Sep 06 06:25:40 Finished compiler/backend/arm8                                   15s   1GB
Sep 06 06:25:40 Starting compiler/backend/mips
Sep 06 06:25:57 Finished compiler/backend/mips                                   16s   1GB
Sep 06 06:25:57 Starting compiler/backend/riscv
Sep 06 06:26:14 Finished compiler/backend/riscv                                  16s   1GB
Sep 06 06:26:15 Starting compiler/backend/ag32
Sep 06 06:27:20 Finished compiler/backend/ag32                                 1m05s   1GB
Sep 06 06:27:21 Starting compiler/parsing/proofs
Sep 06 06:32:50 Finished compiler/parsing/proofs                               5m28s 934MB
Sep 06 06:32:50 Starting compiler/inference/proofs
Sep 06 06:35:28 Finished compiler/inference/proofs                             2m37s 817MB
Sep 06 06:35:28 Starting compiler/backend/semantics
Sep 06 06:41:18 Finished compiler/backend/semantics                            5m49s   1GB
Sep 06 06:41:19 Starting compiler/backend/reg_alloc/proofs
Sep 06 06:44:30 Finished compiler/backend/reg_alloc/proofs                     3m10s 849MB
Sep 06 06:44:30 Starting compiler/backend/proofs
Sep 06 07:23:54 Finished compiler/backend/proofs                              39m23s   3GB
Sep 06 07:23:55 Starting compiler/encoders/x64/proofs
Sep 06 07:32:58 Finished compiler/encoders/x64/proofs                          9m02s   4GB
Sep 06 07:32:58 Starting compiler/encoders/arm7/proofs
Sep 06 07:45:11 Finished compiler/encoders/arm7/proofs                        12m13s   2GB
Sep 06 07:45:12 Starting compiler/encoders/arm8/proofs
Sep 06 07:51:38 Finished compiler/encoders/arm8/proofs                         6m25s   1GB
Sep 06 07:51:38 Starting compiler/encoders/mips/proofs
Sep 06 08:01:05 Finished compiler/encoders/mips/proofs                         9m26s   2GB
Sep 06 08:01:05 Starting compiler/encoders/riscv/proofs
Sep 06 08:09:24 Finished compiler/encoders/riscv/proofs                        8m18s   1GB
Sep 06 08:09:24 Starting compiler/encoders/ag32/proofs
Sep 06 08:11:52 Finished compiler/encoders/ag32/proofs                         2m27s 888MB
Sep 06 08:11:52 Starting compiler/backend/x64/proofs
Sep 06 08:12:09 Finished compiler/backend/x64/proofs                             16s   1GB
Sep 06 08:12:10 Starting compiler/backend/arm7/proofs
Sep 06 08:12:27 Finished compiler/backend/arm7/proofs                            17s   1GB
Sep 06 08:12:28 Starting compiler/backend/arm8/proofs
Sep 06 08:12:44 Finished compiler/backend/arm8/proofs                            15s   1GB
Sep 06 08:12:44 Starting compiler/backend/mips/proofs
Sep 06 08:13:01 Finished compiler/backend/mips/proofs                            16s   1GB
Sep 06 08:13:01 Starting compiler/backend/riscv/proofs
Sep 06 08:13:19 Finished compiler/backend/riscv/proofs                           17s   1GB
Sep 06 08:13:19 Starting compiler/backend/ag32/proofs
Sep 06 08:22:13 Finished compiler/backend/ag32/proofs                          8m53s   2GB
Sep 06 08:22:14 Starting compiler/proofs
Sep 06 08:23:29 Finished compiler/proofs                                       1m14s   3GB
Sep 06 08:23:29 Starting candle/set-theory
Sep 06 08:23:55 Finished candle/set-theory                                       25s 765MB
Sep 06 08:23:55 Starting candle/syntax-lib
Sep 06 08:24:04 Finished candle/syntax-lib                                        8s 600MB
Sep 06 08:24:05 Starting candle/standard/syntax
Sep 06 08:25:44 Finished candle/standard/syntax                                1m39s   1GB
Sep 06 08:25:45 Starting candle/standard/semantics
Sep 06 08:27:18 Finished candle/standard/semantics                             1m32s   1GB
Sep 06 08:27:18 Starting candle/standard/monadic
Sep 06 08:28:50 Finished candle/standard/monadic                               1m31s   1GB
Sep 06 08:28:50 Starting candle/standard/ml_kernel
Sep 06 08:32:36 Finished candle/standard/ml_kernel                             3m45s   3GB
Sep 06 08:32:37 Starting candle/standard/opentheory
Sep 06 08:41:13 Finished candle/standard/opentheory                            8m35s   3GB
Sep 06 08:41:13 Starting candle/standard/opentheory/compilation
Sep 06 09:10:31 Finished candle/standard/opentheory/compilation               29m17s  12GB
Sep 06 09:10:31 Starting candle/standard/opentheory/compilation/proofs
Sep 06 09:11:09 Finished candle/standard/opentheory/compilation/proofs           37s   2GB
Sep 06 09:11:10 Starting characteristic/examples
Sep 06 09:12:37 Finished characteristic/examples                               1m26s   2GB
Sep 06 09:12:37 Starting tutorial/solutions
Sep 06 09:25:34 Finished tutorial/solutions                                   12m56s   6GB
Sep 06 09:25:34 Starting translator/monadic/examples
Sep 06 09:28:20 Finished translator/monadic/examples                           2m45s   3GB
Sep 06 09:28:21 Starting examples
Sep 06 09:31:53 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-1028/basis]0;Holmake: ~/regression/cakeml-1028/basis/pure]0;Holmake: ~/regression/cakeml-1028/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-1028/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-1028/misc]0;Holmake: ~/regression/cakeml-1028/developers]0;Holmake: ~/regression/cakeml-1028/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-1028/misc]0;Holmake: ~/regression/cakeml-1028/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-1028/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-1028/misc]0;Holmake: ~/regression/cakeml-1028/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression/cakeml-1028/basis/pure]0;Holmake: ~/regression/cakeml-1028/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ~/regression/cakeml-1028/basis]0;Holmake: ~/regression/cakeml-1028/characteristic]0;Holmake: ~/regression/cakeml-1028/compiler/parsing]0;Holmake: ~/regression/cakeml-1028/semantics]0;Holmake: ~/regression/cakeml-1028/semantics/ffi]0;Holmake: ~/regression/cakeml-1028/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-1028/semantics]0;Holmake: ~/regression/cakeml-1028/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression/cakeml-1028/compiler/parsing]0;Holmake: ~/regression/cakeml-1028/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/regression/cakeml-1028/characteristic]0;Holmake: ~/regression/cakeml-1028/semantics/proofs]0;Holmake: ~/regression/cakeml-1028/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ~/regression/cakeml-1028/characteristic]0;Holmake: ~/regression/cakeml-1028/translator]0;Holmake: ~/regression/cakeml-1028/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/regression/cakeml-1028/characteristic]0;Holmake: ~/regression/cakeml-1028/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ~/regression/cakeml-1028/basis]0;Holmake: ~/regression/cakeml-1028/translator/monadic]0;Holmake: ~/regression/cakeml-1028/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-1028/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ~/regression/cakeml-1028/translator/monadic]0;Holmake: ~/regression/cakeml-1028/translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ~/regression/cakeml-1028/basis]0;Holmake: ~/regression/cakeml-1028/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>
 on line 40, characters 42-63
 
 which has type
 
 :regexp list
 
 unification failure message: Attempt to unify different type operators: balanced_map$balanced_map and list$list
 error in quse /home/myreen/regression/cakeml-1028/examples/filterProgScript.sml : HOL_ERR {message = "on line 40, characters 42-63:\n\nType inference failure: unable to infer a type for the application of\n\ndom_Brz_alt (empty :regexp oset )\n\non line 40, characters 24-63\n\nwhich has type\n\n:regexp oset -> bool\n\nto\n\n[normalize\n   (Cat\n      (Chset\n         (Charset (0w :word64) (4503599627370496w :word64) (0w :word64)\n            (0w :word64)))\n      (Cat\n         (Chset\n            (Charset (0w :word64) (1099511627776w :word64) (0w :word64)\n               (0w :word64)))\n         (Cat\n            (Chset\n               (Charset (0w :word64) (1125899906842624w :word64) (0w :word64)\n                  (0w :word64)))\n            (Cat\n               (Chset\n                  (Charset (0w :word64) (140737488355328w :word64)\n                     (0w :word64) (0w :word64)))\n               (Cat\n                  (Chset\n                     (Charset (0w :word64) (9007199254740992w :word64)\n                        (0w :word64) (0w :word64)))\n                  (Cat\n                     (Chset\n                        (Charset (0w :...) (549755813888w :word64)\n                           (0w :word64) (0w :word64)))\n                     (Cat\n                        (Chset\n                           (... ... (1099511627776w :...) (0w :word64)\n                              (0w :word64)))\n                        (Chset\n                           (Charset (1w :...) (0w :word64) (0w :word64)\n                              (0w :word64))))))))))]\n\non line 40, characters 42-63\n\nwhich has type\n\n:regexp list\n\nunification failure message: Attempt to unify different type operators: balanced_map$balanced_map and list$list\n", origin_function = "type-analysis", origin_structure = "Preterm"}
 error in load filterProgScript : HOL_ERR {message = "on line 40, characters 42-63:\n\nType inference failure: unable to infer a type for the application of\n\ndom_Brz_alt (empty :regexp oset )\n\non line 40, characters 24-63\n\nwhich has type\n\n:regexp oset -> bool\n\nto\n\n[normalize\n   (Cat\n      (Chset\n         (Charset (0w :word64) (4503599627370496w :word64) (0w :word64)\n            (0w :word64)))\n      (Cat\n         (Chset\n            (Charset (0w :word64) (1099511627776w :word64) (0w :word64)\n               (0w :word64)))\n         (Cat\n            (Chset\n               (Charset (0w :word64) (1125899906842624w :word64) (0w :word64)\n                  (0w :word64)))\n            (Cat\n               (Chset\n                  (Charset (0w :word64) (140737488355328w :word64)\n                     (0w :word64) (0w :word64)))\n               (Cat\n                  (Chset\n                     (Charset (0w :word64) (9007199254740992w :word64)\n                        (0w :word64) (0w :word64)))\n                  (Cat\n                     (Chset\n                        (Charset (0w :...) (549755813888w :word64)\n                           (0w :word64) (0w :word64)))\n                     (Cat\n                        (Chset\n                           (... ... (1099511627776w :...) (0w :word64)\n                              (0w :word64)))\n                        (Chset\n                           (Charset (1w :...) (0w :word64) (0w :word64)\n                              (0w :word64))))))))))]\n\non line 40, characters 42-63\n\nwhich has type\n\n:regexp list\n\nunification failure message: Attempt to unify different type operators: balanced_map$balanced_map and list$list\n", origin_function = "type-analysis", origin_structure = "Preterm"}
 Uncaught exception: HOL_ERR {message = "on line 40, characters 42-63:\n\nType inference failure: unable to infer a type for the application of\n\ndom_Brz_alt (empty :regexp oset )\n\non line 40, characters 24-63\n\nwhich has type\n\n:regexp oset -> bool\n\nto\n\n[normalize\n   (Cat\n      (Chset\n         (Charset (0w :word64) (4503599627370496w :word64) (0w :word64)\n            (0w :word64)))\n      (Cat\n         (Chset\n            (Charset (0w :word64) (1099511627776w :word64) (0w :word64)\n               (0w :word64)))\n         (Cat\n            (Chset\n               (Charset (0w :word64) (1125899906842624w :word64) (0w :word64)\n                  (0w :word64)))\n            (Cat\n               (Chset\n                  (Charset (0w :word64) (140737488355328w :word64)\n                     (0w :word64) (0w :word64)))\n               (Cat\n                  (Chset\n                     (Charset (0w :word64) (9007199254740992w :word64)\n                        (0w :word64) (0w :word64)))\n                  (Cat\n                     (Chset\n                        (Charset (0w :...) (549755813888w :word64)\n                           (0w :word64) (0w :word64)))\n                     (Cat\n                        (Chset\n                           (... ... (1099511627776w :...) (0w :word64)\n                              (0w :word64)))\n                        (Chset\n                           (Charset (1w :...) (0w :word64) (0w :word64)\n                              (0w :word64))))))))))]\n\non line 40, characters 42-63\n\nwhich has type\n\n:regexp list\n\nunification failure message: Attempt to unify different type operators: balanced_map$balanced_map and list$list\n", origin_function = "type-analysis", origin_structure = "Preterm"}
array_searchProgTheory                                                                               M-KILLED
echoProgTheory                                                                                       M-KILLED
grepProgTheory                                                                                       M-KILLED