Job 2616

CakeML:40152b7e468b31ddee1c40ce07ee9c75cee53338
  Update to account for changed Dafny IR [Sep 22 10:21:07]
#1058 (dafny-ir-update)
Merging into:49f0d44be26ff907ef52240f3818a4c3caa10598
  Merge pull request #1055 from CakeML/pan_news [Sep 18 13:05:16]
HOL:72a01e7935ee7175f22527332d54ac58085668ed
  Add more primitive proof rules [Sep 23 23:08:36]
Machine:pavlova

Sep 25 19:07:20 Claimed job
Sep 25 19:07:29 Building HOL
Sep 25 19:22:40 Starting developers
Sep 25 19:22:44 Finished developers                                               2s 131MB
Sep 25 19:22:45 Starting developers/bin
Sep 25 19:23:05 Finished developers/bin                                          19s   1GB
Sep 25 19:23:06 Starting compiler/proofs
Sep 25 21:12:17 Finished compiler/proofs                                    1h49m09s  31GB
Sep 25 21:12:18 Starting compiler/bootstrap/translation
Sep 26 06:15:33 Finished compiler/bootstrap/translation                     9h03m13s  58GB
Sep 26 06:15:34 Starting semantics/ffi
Sep 26 06:15:43 Finished semantics/ffi                                            8s 735MB
Sep 26 06:15:44 Starting semantics
Sep 26 06:15:46 Finished semantics                                                0s  64MB
Sep 26 06:15:47 Starting semantics/proofs
Sep 26 06:16:10 Finished semantics/proofs                                        22s 779MB
Sep 26 06:16:11 Starting semantics/alt_semantics
Sep 26 06:16:38 Finished semantics/alt_semantics                                 26s 928MB
Sep 26 06:16:39 Starting semantics/alt_semantics/proofs
Sep 26 06:26:58 Finished semantics/alt_semantics/proofs                       10m17s   2GB
Sep 26 06:26:58 Starting basis/pure
Sep 26 06:27:00 Finished basis/pure                                               0s  70MB
Sep 26 06:27:01 Starting translator
Sep 26 06:28:40 Finished translator                                            1m38s   5GB
Sep 26 06:28:41 Starting compiler/parsing
Sep 26 06:28:42 Finished compiler/parsing                                         0s  71MB
Sep 26 06:28:43 Starting characteristic
Sep 26 06:28:45 Finished characteristic                                           0s  91MB
Sep 26 06:28:46 Starting translator/monadic
Sep 26 06:28:47 Finished translator/monadic                                       0s  99MB
Sep 26 06:28:48 Starting basis
Sep 26 06:31:22 Finished basis                                                 2m32s   5GB
Sep 26 06:31:23 Starting compiler/inference
Sep 26 06:31:24 Finished compiler/inference                                       0s  99MB
Sep 26 06:31:25 Starting compiler/backend/reg_alloc
Sep 26 06:31:27 Finished compiler/backend/reg_alloc                               0s  68MB
Sep 26 06:31:28 Starting compiler/backend/gc
Sep 26 06:31:30 Finished compiler/backend/gc                                      1s 141MB
Sep 26 06:31:31 Starting compiler/backend
Sep 26 06:31:36 Finished compiler/backend                                         4s 318MB
Sep 26 06:31:37 Starting compiler/encoders/asm
Sep 26 06:31:38 Finished compiler/encoders/asm                                    0s  93MB
Sep 26 06:31:39 Starting compiler/encoders/x64
Sep 26 06:31:41 Finished compiler/encoders/x64                                    0s 103MB
Sep 26 06:31:42 Starting compiler/encoders/arm7
Sep 26 06:31:44 Finished compiler/encoders/arm7                                   0s  98MB
Sep 26 06:31:45 Starting compiler/encoders/arm8
Sep 26 06:31:46 Finished compiler/encoders/arm8                                   0s  96MB
Sep 26 06:31:47 Starting compiler/encoders/arm8_asl
Sep 26 08:49:25 Finished compiler/encoders/arm8_asl                         2h17m36s  40GB
Sep 26 08:49:26 Starting compiler/encoders/mips
Sep 26 08:49:27 Finished compiler/encoders/mips                                   0s  99MB
Sep 26 08:49:28 Starting compiler/encoders/riscv
Sep 26 08:49:30 Finished compiler/encoders/riscv                                  0s  99MB
Sep 26 08:49:31 Starting compiler/encoders/ag32
Sep 26 08:49:32 Finished compiler/encoders/ag32                                   0s  98MB
Sep 26 08:49:33 Starting compiler/backend/x64
Sep 26 08:49:35 Finished compiler/backend/x64                                     1s 131MB
Sep 26 08:49:36 Starting compiler/backend/arm7
Sep 26 08:49:38 Finished compiler/backend/arm7                                    1s 139MB
Sep 26 08:49:39 Starting compiler/backend/arm8
Sep 26 08:49:41 Finished compiler/backend/arm8                                    1s 139MB
Sep 26 08:49:42 Starting compiler/backend/mips
Sep 26 08:49:44 Finished compiler/backend/mips                                    1s 139MB
Sep 26 08:49:45 Starting compiler/backend/riscv
Sep 26 08:49:47 Finished compiler/backend/riscv                                   1s 139MB
Sep 26 08:49:48 Starting compiler/backend/ag32
Sep 26 08:51:14 Finished compiler/backend/ag32                                 1m24s   3GB
Sep 26 08:51:15 Starting compiler/parsing/proofs
Sep 26 08:51:16 Finished compiler/parsing/proofs                                  0s  72MB
Sep 26 08:51:17 Starting compiler/inference/proofs
Sep 26 08:51:19 Finished compiler/inference/proofs                                0s  92MB
Sep 26 08:51:20 Starting compiler/backend/semantics
Sep 26 08:54:31 Finished compiler/backend/semantics                            3m10s   4GB
Sep 26 08:54:32 Starting compiler/backend/reg_alloc/proofs
Sep 26 08:54:33 Finished compiler/backend/reg_alloc/proofs                        0s  96MB
Sep 26 08:54:34 Starting compiler/backend/proofs
Sep 26 08:55:34 Finished compiler/backend/proofs                                 59s   5GB
Sep 26 08:55:35 Starting compiler/backend/serialiser
Sep 26 08:55:37 Finished compiler/backend/serialiser                              1s 149MB
Sep 26 08:55:38 Starting compiler/encoders/x64/proofs
Sep 26 09:05:50 Finished compiler/encoders/x64/proofs                         10m10s   5GB
Sep 26 09:05:51 Starting compiler/encoders/arm7/proofs
Sep 26 09:18:53 Finished compiler/encoders/arm7/proofs                        13m01s   7GB
Sep 26 09:18:54 Starting compiler/encoders/arm8/proofs
Sep 26 09:25:45 Finished compiler/encoders/arm8/proofs                         6m49s   6GB
Sep 26 09:25:46 Starting compiler/encoders/arm8_asl/proofs
Sep 26 10:16:45 Finished compiler/encoders/arm8_asl/proofs                    50m58s  12GB
Sep 26 10:16:46 Starting compiler/encoders/mips/proofs
Sep 26 10:27:06 Finished compiler/encoders/mips/proofs                        10m19s  10GB
Sep 26 10:27:07 Starting compiler/encoders/riscv/proofs
Sep 26 10:35:35 Finished compiler/encoders/riscv/proofs                        8m27s   4GB
Sep 26 10:35:36 Starting compiler/encoders/ag32/proofs
Sep 26 10:38:31 Finished compiler/encoders/ag32/proofs                         2m54s   2GB
Sep 26 10:38:32 Starting compiler/backend/x64/proofs
Sep 26 10:39:19 Finished compiler/backend/x64/proofs                             46s   3GB
Sep 26 10:39:20 Starting compiler/backend/arm7/proofs
Sep 26 10:40:10 Finished compiler/backend/arm7/proofs                            48s   3GB
Sep 26 10:40:10 Starting compiler/backend/arm8/proofs
Sep 26 10:40:58 Finished compiler/backend/arm8/proofs                            46s   3GB
Sep 26 10:40:59 Starting compiler/backend/arm8_asl
Sep 26 10:41:33 Finished compiler/backend/arm8_asl                               32s   2GB
Sep 26 10:41:33 Starting compiler/backend/mips/proofs
Sep 26 10:42:24 Finished compiler/backend/mips/proofs                            49s   3GB
Sep 26 10:42:25 Starting compiler/backend/riscv/proofs
Sep 26 10:43:22 Finished compiler/backend/riscv/proofs                           56s   3GB
Sep 26 10:43:23 Starting compiler/backend/ag32/proofs
Sep 26 10:57:55 Finished compiler/backend/ag32/proofs                         14m30s   6GB
Sep 26 10:57:56 Starting compiler/backend/cv_compute
Sep 26 10:59:47 Finished compiler/backend/cv_compute                           1m50s   3GB
Sep 26 10:59:48 Starting cv_translator
Sep 26 11:19:43 Finished cv_translator                                        19m54s  10GB
Sep 26 11:19:44 Starting candle/set-theory
Sep 26 11:20:39 Finished candle/set-theory                                       54s   1GB
Sep 26 11:20:40 Starting candle/syntax-lib
Sep 26 11:20:42 Finished candle/syntax-lib                                        0s  73MB
Sep 26 11:20:42 Starting candle/standard/syntax
Sep 26 11:21:02 Finished candle/standard/syntax                                  18s   1GB
Sep 26 11:21:03 Starting candle/standard/semantics
Sep 26 11:23:56 Finished candle/standard/semantics                             2m52s   3GB
Sep 26 11:23:57 Starting candle/standard/monadic
Sep 26 11:23:59 Finished candle/standard/monadic                                  0s 102MB
Sep 26 11:24:00 Starting candle/standard/ml_kernel
Sep 26 11:26:12 Finished candle/standard/ml_kernel                             2m11s   4GB
Sep 26 11:26:13 Starting candle/overloading/syntax
Sep 26 11:29:54 Finished candle/overloading/syntax                             3m39s   2GB
Sep 26 11:29:55 Starting candle/overloading/semantics
Sep 26 11:41:51 Finished candle/overloading/semantics                         11m55s  12GB
Sep 26 11:41:52 Starting candle/overloading/monadic
Sep 26 11:44:32 Finished candle/overloading/monadic                            2m39s   3GB
Sep 26 11:44:33 Starting candle/overloading/ml_kernel
Sep 26 11:52:40 Finished candle/overloading/ml_kernel                          8m06s   7GB
Sep 26 11:52:41 Starting candle/overloading/ml_checker
Sep 26 11:55:27 Finished candle/overloading/ml_checker                         2m44s   7GB
Sep 26 11:55:28 Starting candle/prover
Sep 26 12:06:06 Finished candle/prover                                        10m37s   5GB
Sep 26 12:06:06 Starting pancake
Sep 26 12:06:34 Finished pancake                                                 27s 994MB
Sep 26 12:06:35 Starting pancake/ffi
Sep 26 12:06:36 Finished pancake/ffi                                              0s  22MB
Sep 26 12:06:37 Starting pancake/semantics
Sep 26 12:08:50 Finished pancake/semantics                                     2m12s   2GB
Sep 26 12:08:51 Starting pancake/parser
Sep 26 12:09:15 Finished pancake/parser                                          22s 805MB
Sep 26 12:09:16 Starting pancake/proofs
Sep 26 12:25:21 Finished pancake/proofs                                       16m04s   7GB
Sep 26 12:25:22 Starting compiler/dafny
Sep 26 12:28:05 Finished compiler/dafny                                        2m42s  11GB
Sep 26 12:28:06 Starting compiler/dafny/translation
Sep 26 12:56:54 Finished compiler/dafny/translation                           28m46s  20GB
Sep 26 12:56:55 Starting compiler/dafny/compilation
Sep 26 13:00:39 Finished compiler/dafny/compilation                            3m43s  15GB
Sep 26 13:00:40 Starting compiler/dafny/semantics
Sep 26 13:00:56 FAILED: compiler/dafny/semantics
Scanning $(HOLDIR)/src/bag
Scanning $(HOLDIR)/src/sort
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/basis
Scanning $(CAKEMLDIR)/compiler/dafny
Scanned 30 directories
Starting work on README.md
Starting work on dafny_semanticPrimitivesTheory
README.md                                                           (0s)     OK
dafny_semanticPrimitivesTheory                                      (7s)     OK
Starting work on dafny_evaluateTheory
dafny_evaluateTheory                                                (4s)FAIL<1>
 <<HOL message: Created theory "dafny_evaluate">>
 error in quse /scratch/cakeml/regression/cakeml-2616/compiler/dafny/semantics/dafny_evaluateScript.sml : HOL_ERR {message = "on line 18, characters 2-51:\nat Pmatch.mk_case0:\ncould not get case constructors for type :varName list option -> method", origin_function = "Hol_defn", origin_structure = "Defn"}
 error in load /scratch/cakeml/regression/cakeml-2616/compiler/dafny/semantics/dafny_evaluateScript : HOL_ERR {message = "on line 18, characters 2-51:\nat Pmatch.mk_case0:\ncould not get case constructors for type :varName list option -> method", origin_function = "Hol_defn", origin_structure = "Defn"}
 Uncaught exception at /scratch/cakeml/regression/HOL-72a01e7935ee7175f22527332d54ac58085668ed/src/num/termination/TotalDefn.sml:30: HOL_ERR {message = "on line 18, characters 2-51:\nat Pmatch.mk_case0:\ncould not get case constructors for type :varName list option -> method", origin_function = "Hol_defn", origin_structure = "Defn"}