CakeML Regression Test

Job 1030

CakeML:a8e2240b45c8f858615a65f130198101bb07e6b6
  Remove a bug from ml_translatorLib.clean_v_thms [Sep 07 19:55:11]
#688 (issue683)
Merging into: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 07 19:56:13 Claimed job
Sep 07 19:56:16 Reusing HOL
Sep 07 19:56:21 Starting developers
Sep 07 19:56:23 Finished developers                                               2s  86MB
Sep 07 19:56:23 Starting developers/bin
Sep 07 19:57:47 Finished developers/bin                                        1m23s 164MB
Sep 07 19:57:47 Starting semantics/ffi
Sep 07 19:57:56 Finished semantics/ffi                                            8s 224MB
Sep 07 19:57:56 Starting semantics
Sep 07 19:59:19 Finished semantics                                             1m22s   1GB
Sep 07 19:59:19 Starting semantics/proofs
Sep 07 20:02:24 Finished semantics/proofs                                      3m04s 984MB
Sep 07 20:02:24 Starting semantics/alt_semantics
Sep 07 20:02:31 Finished semantics/alt_semantics                                  6s 319MB
Sep 07 20:02:31 Starting semantics/alt_semantics/proofs
Sep 07 20:04:22 Finished semantics/alt_semantics/proofs                        1m50s   1GB
Sep 07 20:04:22 Starting basis/pure
Sep 07 20:05:09 Finished basis/pure                                              46s 688MB
Sep 07 20:05:09 Starting translator
Sep 07 20:07:00 Finished translator                                            1m50s   1GB
Sep 07 20:07:00 Starting compiler/parsing
Sep 07 20:08:04 Finished compiler/parsing                                      1m03s   3GB
Sep 07 20:08:05 Starting characteristic
Sep 07 20:13:27 Finished characteristic                                        5m22s   1GB
Sep 07 20:13:28 Starting translator/monadic
Sep 07 20:14:58 Finished translator/monadic                                    1m29s   1GB
Sep 07 20:14:58 Starting basis
Sep 07 20:35:38 Finished basis                                                20m39s   2GB
Sep 07 20:35:38 Starting compiler/inference
Sep 07 20:37:16 Finished compiler/inference                                    1m37s   1GB
Sep 07 20:37:16 Starting compiler/backend/reg_alloc
Sep 07 20:38:18 Finished compiler/backend/reg_alloc                            1m00s   1GB
Sep 07 20:38:18 Starting compiler/backend/gc
Sep 07 20:47:05 Finished compiler/backend/gc                                   8m47s   2GB
Sep 07 20:47:06 Starting compiler/backend
Sep 07 20:47:07 Finished compiler/backend                                         0s  45MB
Sep 07 20:47:07 Starting compiler/encoders/asm
Sep 07 20:47:07 Finished compiler/encoders/asm                                    0s  35MB
Sep 07 20:47:08 Starting compiler/encoders/x64
Sep 07 20:47:32 Finished compiler/encoders/x64                                   23s 757MB
Sep 07 20:47:32 Starting compiler/encoders/arm7
Sep 07 20:48:18 Finished compiler/encoders/arm7                                  45s 721MB
Sep 07 20:48:19 Starting compiler/encoders/arm8
Sep 07 20:48:31 Finished compiler/encoders/arm8                                  12s 526MB
Sep 07 20:48:31 Starting compiler/encoders/mips
Sep 07 20:48:47 Finished compiler/encoders/mips                                  15s 766MB
Sep 07 20:48:47 Starting compiler/encoders/riscv
Sep 07 20:49:01 Finished compiler/encoders/riscv                                 13s   1GB
Sep 07 20:49:02 Starting compiler/encoders/ag32
Sep 07 20:49:17 Finished compiler/encoders/ag32                                  15s 793MB
Sep 07 20:49:18 Starting compiler/backend/x64
Sep 07 20:49:34 Finished compiler/backend/x64                                    15s 871MB
Sep 07 20:49:34 Starting compiler/backend/arm7
Sep 07 20:49:53 Finished compiler/backend/arm7                                   18s   1GB
Sep 07 20:49:53 Starting compiler/backend/arm8
Sep 07 20:50:10 Finished compiler/backend/arm8                                   16s   1GB
Sep 07 20:50:10 Starting compiler/backend/mips
Sep 07 20:50:27 Finished compiler/backend/mips                                   16s   1GB
Sep 07 20:50:28 Starting compiler/backend/riscv
Sep 07 20:50:44 Finished compiler/backend/riscv                                  15s 887MB
Sep 07 20:50:44 Starting compiler/backend/ag32
Sep 07 20:51:53 Finished compiler/backend/ag32                                 1m08s   1GB
Sep 07 20:51:53 Starting compiler/parsing/proofs
Sep 07 20:57:30 Finished compiler/parsing/proofs                               5m36s 873MB
Sep 07 20:57:30 Starting compiler/inference/proofs
Sep 07 21:00:18 Finished compiler/inference/proofs                             2m47s   1GB
Sep 07 21:00:19 Starting compiler/backend/semantics
Sep 07 21:07:09 Finished compiler/backend/semantics                            6m50s   2GB
Sep 07 21:07:09 Starting compiler/backend/reg_alloc/proofs
Sep 07 21:10:34 Finished compiler/backend/reg_alloc/proofs                     3m23s 769MB
Sep 07 21:10:34 Starting compiler/backend/proofs
Sep 07 21:57:48 Finished compiler/backend/proofs                              47m13s   4GB
Sep 07 21:57:48 Starting compiler/encoders/x64/proofs
Sep 07 22:07:59 Finished compiler/encoders/x64/proofs                         10m10s   6GB
Sep 07 22:07:59 Starting compiler/encoders/arm7/proofs
Sep 07 22:21:35 Finished compiler/encoders/arm7/proofs                        13m35s   3GB
Sep 07 22:21:35 Starting compiler/encoders/arm8/proofs
Sep 07 22:28:54 Finished compiler/encoders/arm8/proofs                         7m19s   1GB
Sep 07 22:28:55 Starting compiler/encoders/mips/proofs
Sep 07 22:39:44 Finished compiler/encoders/mips/proofs                        10m49s   2GB
Sep 07 22:39:45 Starting compiler/encoders/riscv/proofs
Sep 07 22:48:43 Finished compiler/encoders/riscv/proofs                        8m57s 658MB
Sep 07 22:48:43 Starting compiler/encoders/ag32/proofs
Sep 07 22:51:11 Finished compiler/encoders/ag32/proofs                         2m27s 886MB
Sep 07 22:51:11 Starting compiler/backend/x64/proofs
Sep 07 22:51:28 Finished compiler/backend/x64/proofs                             16s 987MB
Sep 07 22:51:28 Starting compiler/backend/arm7/proofs
Sep 07 22:51:47 Finished compiler/backend/arm7/proofs                            17s   1GB
Sep 07 22:51:47 Starting compiler/backend/arm8/proofs
Sep 07 22:52:04 Finished compiler/backend/arm8/proofs                            15s   1GB
Sep 07 22:52:04 Starting compiler/backend/mips/proofs
Sep 07 22:52:21 Finished compiler/backend/mips/proofs                            16s   1GB
Sep 07 22:52:21 Starting compiler/backend/riscv/proofs
Sep 07 22:52:38 Finished compiler/backend/riscv/proofs                           16s   1GB
Sep 07 22:52:38 Starting compiler/backend/ag32/proofs
Sep 07 23:01:39 Finished compiler/backend/ag32/proofs                          8m59s   2GB
Sep 07 23:01:39 Starting compiler/proofs
Sep 07 23:03:09 Finished compiler/proofs                                       1m30s   3GB
Sep 07 23:03:10 Starting candle/set-theory
Sep 07 23:03:35 Finished candle/set-theory                                       24s 790MB
Sep 07 23:03:35 Starting candle/syntax-lib
Sep 07 23:03:45 Finished candle/syntax-lib                                        9s 611MB
Sep 07 23:03:45 Starting candle/standard/syntax
Sep 07 23:05:26 Finished candle/standard/syntax                                1m39s 966MB
Sep 07 23:05:26 Starting candle/standard/semantics
Sep 07 23:06:59 Finished candle/standard/semantics                             1m32s   1GB
Sep 07 23:06:59 Starting candle/standard/monadic
Sep 07 23:08:30 Finished candle/standard/monadic                               1m30s   1GB
Sep 07 23:08:30 Starting candle/standard/ml_kernel
Sep 07 23:12:17 Finished candle/standard/ml_kernel                             3m46s   3GB
Sep 07 23:12:17 Starting candle/standard/opentheory
Sep 07 23:20:44 Finished candle/standard/opentheory                            8m26s   3GB
Sep 07 23:20:45 Starting candle/standard/opentheory/compilation
Sep 07 23:50:32 Finished candle/standard/opentheory/compilation               29m47s  17GB
Sep 07 23:50:33 Starting candle/standard/opentheory/compilation/proofs
Sep 07 23:51:16 Finished candle/standard/opentheory/compilation/proofs           42s   3GB
Sep 07 23:51:17 Starting characteristic/examples
Sep 07 23:52:41 Finished characteristic/examples                               1m24s   2GB
Sep 07 23:52:42 Starting tutorial/solutions
Sep 08 00:05:44 Finished tutorial/solutions                                   13m02s   7GB
Sep 08 00:05:45 Starting translator/monadic/examples
Sep 08 00:08:33 Finished translator/monadic/examples                           2m48s   2GB
Sep 08 00:08:34 Starting examples
Sep 08 00:12:02 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-1030/basis]0;Holmake: ~/regression/cakeml-1030/basis/pure]0;Holmake: ~/regression/cakeml-1030/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-1030/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-1030/misc]0;Holmake: ~/regression/cakeml-1030/developers]0;Holmake: ~/regression/cakeml-1030/developers[1mWorking in $(CAKEMLDIR)/developers[0m
]0;Holmake: ~/regression/cakeml-1030/misc]0;Holmake: ~/regression/cakeml-1030/misc/lem_lib_stub]0;Holmake: ~/regression/cakeml-1030/misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ~/regression/cakeml-1030/misc]0;Holmake: ~/regression/cakeml-1030/misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ~/regression/cakeml-1030/basis/pure]0;Holmake: ~/regression/cakeml-1030/basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ~/regression/cakeml-1030/basis]0;Holmake: ~/regression/cakeml-1030/characteristic]0;Holmake: ~/regression/cakeml-1030/compiler/parsing]0;Holmake: ~/regression/cakeml-1030/semantics]0;Holmake: ~/regression/cakeml-1030/semantics/ffi]0;Holmake: ~/regression/cakeml-1030/semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ~/regression/cakeml-1030/semantics]0;Holmake: ~/regression/cakeml-1030/semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ~/regression/cakeml-1030/compiler/parsing]0;Holmake: ~/regression/cakeml-1030/compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ~/regression/cakeml-1030/characteristic]0;Holmake: ~/regression/cakeml-1030/semantics/proofs]0;Holmake: ~/regression/cakeml-1030/semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ~/regression/cakeml-1030/characteristic]0;Holmake: ~/regression/cakeml-1030/translator]0;Holmake: ~/regression/cakeml-1030/translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ~/regression/cakeml-1030/characteristic]0;Holmake: ~/regression/cakeml-1030/characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ~/regression/cakeml-1030/basis]0;Holmake: ~/regression/cakeml-1030/translator/monadic]0;Holmake: ~/regression/cakeml-1030/translator/monadic/monad_base]0;Holmake: ~/regression/cakeml-1030/translator/monadic/monad_base[1mWorking in $(CAKEMLDIR)/translator/monadic/monad_base[0m
]0;Holmake: ~/regression/cakeml-1030/translator/monadic]0;Holmake: ~/regression/cakeml-1030/translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ~/regression/cakeml-1030/basis]0;Holmake: ~/regression/cakeml-1030/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-1030/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