Job 2558

CakeML:19be9391bae6a7181cb293a6f49549940368e8c0
  Get md5 to build with heap [Aug 14 10:16:33]
#1043 (heaps)
Merging into:a61f2812e286bddf33d858448ec9dd5d671bbfcb
  Merge pull request #1025 from talsewell/word_simp_separated_if [Aug 12 08:13:37]
HOL:a18a10ab99c90f2d4e47536b411eeee5bec72004
  some FUNPOW Tau and spin lemmas for itreeTau [Aug 16 00:45:50]
Machine:pavlova

Aug 20 11:24:29 Claimed job
Aug 20 11:24:39 Building HOL
Aug 20 11:38:57 Starting developers
Aug 20 11:39:01 Finished developers                                               2s 205MB
Aug 20 11:39:02 Starting developers/bin
Aug 20 11:39:13 Finished developers/bin                                          10s   1GB
Aug 20 11:39:14 Starting compiler/proofs
Aug 20 13:24:19 Finished compiler/proofs                                    1h45m03s  41GB
Aug 20 13:24:20 Starting compiler/bootstrap/translation
Aug 20 22:11:01 Finished compiler/bootstrap/translation                     8h46m39s  84GB
Aug 20 22:11:02 Starting semantics/ffi
Aug 20 22:11:11 Finished semantics/ffi                                            7s 624MB
Aug 20 22:11:11 Starting semantics
Aug 20 22:11:13 Finished semantics                                                0s  64MB
Aug 20 22:11:14 Starting semantics/proofs
Aug 20 22:11:37 Finished semantics/proofs                                        22s 823MB
Aug 20 22:11:38 Starting semantics/alt_semantics
Aug 20 22:12:03 Finished semantics/alt_semantics                                 24s 916MB
Aug 20 22:12:03 Starting semantics/alt_semantics/proofs
Aug 20 22:22:18 Finished semantics/alt_semantics/proofs                       10m13s   3GB
Aug 20 22:22:18 Starting basis/pure
Aug 20 22:22:20 Finished basis/pure                                               0s  71MB
Aug 20 22:22:21 Starting translator
Aug 20 22:23:55 Finished translator                                            1m33s   4GB
Aug 20 22:23:56 Starting compiler/parsing
Aug 20 22:23:57 Finished compiler/parsing                                         0s  73MB
Aug 20 22:23:58 Starting characteristic
Aug 20 22:24:00 Finished characteristic                                           0s  90MB
Aug 20 22:24:01 Starting translator/monadic
Aug 20 22:24:02 Finished translator/monadic                                       0s 102MB
Aug 20 22:24:03 Starting basis
Aug 20 22:27:22 Finished basis                                                 3m17s   5GB
Aug 20 22:27:23 Starting compiler/inference
Aug 20 22:27:24 Finished compiler/inference                                       0s  94MB
Aug 20 22:27:25 Starting compiler/backend/reg_alloc
Aug 20 22:27:26 Finished compiler/backend/reg_alloc                               0s  67MB
Aug 20 22:27:27 Starting compiler/backend/gc
Aug 20 22:27:29 Finished compiler/backend/gc                                      0s 142MB
Aug 20 22:27:30 Starting compiler/backend
Aug 20 22:27:35 Finished compiler/backend                                         4s 362MB
Aug 20 22:27:36 Starting compiler/encoders/asm
Aug 20 22:27:37 Finished compiler/encoders/asm                                    0s  91MB
Aug 20 22:27:38 Starting compiler/encoders/x64
Aug 20 22:27:40 Finished compiler/encoders/x64                                    0s 104MB
Aug 20 22:27:40 Starting compiler/encoders/arm7
Aug 20 22:27:42 Finished compiler/encoders/arm7                                   0s 103MB
Aug 20 22:27:43 Starting compiler/encoders/arm8
Aug 20 22:27:44 Finished compiler/encoders/arm8                                   0s 103MB
Aug 20 22:27:45 Starting compiler/encoders/arm8_asl
Aug 21 00:41:15 Finished compiler/encoders/arm8_asl                         2h13m27s  40GB
Aug 21 00:41:16 Starting compiler/encoders/mips
Aug 21 00:41:17 Finished compiler/encoders/mips                                   0s 104MB
Aug 21 00:41:18 Starting compiler/encoders/riscv
Aug 21 00:41:19 Finished compiler/encoders/riscv                                  0s 100MB
Aug 21 00:41:20 Starting compiler/encoders/ag32
Aug 21 00:41:22 Finished compiler/encoders/ag32                                   0s  92MB
Aug 21 00:41:23 Starting compiler/backend/x64
Aug 21 00:41:25 Finished compiler/backend/x64                                     0s 146MB
Aug 21 00:41:25 Starting compiler/backend/arm7
Aug 21 00:41:27 Finished compiler/backend/arm7                                    0s 139MB
Aug 21 00:41:28 Starting compiler/backend/arm8
Aug 21 00:41:30 Finished compiler/backend/arm8                                    0s 134MB
Aug 21 00:41:31 Starting compiler/backend/mips
Aug 21 00:41:33 Finished compiler/backend/mips                                    0s 130MB
Aug 21 00:41:33 Starting compiler/backend/riscv
Aug 21 00:41:35 Finished compiler/backend/riscv                                   0s 130MB
Aug 21 00:41:36 Starting compiler/backend/ag32
Aug 21 00:42:57 Finished compiler/backend/ag32                                 1m19s   2GB
Aug 21 00:42:58 Starting compiler/parsing/proofs
Aug 21 00:42:59 Finished compiler/parsing/proofs                                  0s  76MB
Aug 21 00:43:00 Starting compiler/inference/proofs
Aug 21 00:43:01 Finished compiler/inference/proofs                                0s  92MB
Aug 21 00:43:02 Starting compiler/backend/semantics
Aug 21 00:46:12 Finished compiler/backend/semantics                            3m08s   2GB
Aug 21 00:46:13 Starting compiler/backend/reg_alloc/proofs
Aug 21 00:46:14 Finished compiler/backend/reg_alloc/proofs                        0s  99MB
Aug 21 00:46:15 Starting compiler/backend/proofs
Aug 21 00:47:10 Finished compiler/backend/proofs                                 53s   3GB
Aug 21 00:47:11 Starting compiler/backend/serialiser
Aug 21 00:47:13 Finished compiler/backend/serialiser                              0s 140MB
Aug 21 00:47:14 Starting compiler/encoders/x64/proofs
Aug 21 00:56:34 Finished compiler/encoders/x64/proofs                          9m19s   5GB
Aug 21 00:56:35 Starting compiler/encoders/arm7/proofs
Aug 21 01:10:37 Finished compiler/encoders/arm7/proofs                        14m00s  11GB
Aug 21 01:10:37 Starting compiler/encoders/arm8/proofs
Aug 21 01:17:27 Finished compiler/encoders/arm8/proofs                         6m48s   4GB
Aug 21 01:17:28 Starting compiler/encoders/arm8_asl/proofs
Aug 21 02:05:17 Finished compiler/encoders/arm8_asl/proofs                    47m48s   5GB
Aug 21 02:05:18 Starting compiler/encoders/mips/proofs
Aug 21 02:15:32 Finished compiler/encoders/mips/proofs                        10m13s   9GB
Aug 21 02:15:33 Starting compiler/encoders/riscv/proofs
Aug 21 02:24:04 Finished compiler/encoders/riscv/proofs                        8m29s   4GB
Aug 21 02:24:05 Starting compiler/encoders/ag32/proofs
Aug 21 02:26:34 Finished compiler/encoders/ag32/proofs                         2m28s   3GB
Aug 21 02:26:35 Starting compiler/backend/x64/proofs
Aug 21 02:27:22 Finished compiler/backend/x64/proofs                             46s   2GB
Aug 21 02:27:23 Starting compiler/backend/arm7/proofs
Aug 21 02:28:08 Finished compiler/backend/arm7/proofs                            44s   2GB
Aug 21 02:28:09 Starting compiler/backend/arm8/proofs
Aug 21 02:28:51 Finished compiler/backend/arm8/proofs                            41s   3GB
Aug 21 02:28:53 Starting compiler/backend/arm8_asl
Aug 21 02:29:23 Finished compiler/backend/arm8_asl                               29s   2GB
Aug 21 02:29:24 Starting compiler/backend/mips/proofs
Aug 21 02:30:11 Finished compiler/backend/mips/proofs                            45s   3GB
Aug 21 02:30:12 Starting compiler/backend/riscv/proofs
Aug 21 02:31:05 Finished compiler/backend/riscv/proofs                           52s   4GB
Aug 21 02:31:06 Starting compiler/backend/ag32/proofs
Aug 21 02:45:09 Finished compiler/backend/ag32/proofs                         14m01s   6GB
Aug 21 02:45:10 Starting compiler/backend/cv_compute
Aug 21 02:46:55 Finished compiler/backend/cv_compute                           1m44s   3GB
Aug 21 02:46:56 Starting cv_translator
Aug 21 03:06:21 Finished cv_translator                                        19m24s  10GB
Aug 21 03:06:22 Starting candle/set-theory
Aug 21 03:07:13 Finished candle/set-theory                                       49s   1GB
Aug 21 03:07:14 Starting candle/syntax-lib
Aug 21 03:07:15 Finished candle/syntax-lib                                        0s  74MB
Aug 21 03:07:16 Starting candle/standard/syntax
Aug 21 03:07:35 Finished candle/standard/syntax                                  18s   1GB
Aug 21 03:07:36 Starting candle/standard/semantics
Aug 21 03:10:15 Finished candle/standard/semantics                             2m38s   3GB
Aug 21 03:10:16 Starting candle/standard/monadic
Aug 21 03:10:17 Finished candle/standard/monadic                                  0s  97MB
Aug 21 03:10:18 Starting candle/standard/ml_kernel
Aug 21 03:12:17 Finished candle/standard/ml_kernel                             1m58s   5GB
Aug 21 03:12:18 Starting candle/overloading/syntax
Aug 21 03:15:55 Finished candle/overloading/syntax                             3m35s   3GB
Aug 21 03:15:56 Starting candle/overloading/semantics
Aug 21 03:27:37 Finished candle/overloading/semantics                         11m39s   6GB
Aug 21 03:27:38 Starting candle/overloading/monadic
Aug 21 03:30:12 Finished candle/overloading/monadic                            2m33s   2GB
Aug 21 03:30:13 Starting candle/overloading/ml_kernel
Aug 21 03:38:04 Finished candle/overloading/ml_kernel                          7m50s   6GB
Aug 21 03:38:05 Starting candle/overloading/ml_checker
Aug 21 03:40:42 Finished candle/overloading/ml_checker                         2m35s   6GB
Aug 21 03:40:42 Starting candle/prover
Aug 21 03:50:58 Finished candle/prover                                        10m13s   5GB
Aug 21 03:50:59 Starting pancake
Aug 21 03:51:24 Finished pancake                                                 24s   1GB
Aug 21 03:51:25 Starting pancake/ffi
Aug 21 03:51:26 Finished pancake/ffi                                              0s  23MB
Aug 21 03:51:27 Starting pancake/semantics
Aug 21 03:53:33 Finished pancake/semantics                                     2m05s   2GB
Aug 21 03:53:34 Starting pancake/parser
Aug 21 03:53:55 Finished pancake/parser                                          19s 802MB
Aug 21 03:53:56 Starting pancake/proofs
Aug 21 04:09:02 Finished pancake/proofs                                       15m05s   7GB
Aug 21 04:09:03 Starting characteristic/examples
Aug 21 04:10:29 Finished characteristic/examples                               1m25s   5GB
Aug 21 04:10:30 Starting tutorial/solutions
Aug 21 04:13:16 Finished tutorial/solutions                                    2m44s   5GB
Aug 21 04:13:17 Starting translator/monadic/examples
Aug 21 04:16:26 Finished translator/monadic/examples                           3m08s   4GB
Aug 21 04:16:27 Starting examples
Aug 21 04:28:47 Finished examples                                             12m18s   5GB
Aug 21 04:28:48 Starting examples/compilation/x64
Aug 21 04:38:15 Finished examples/compilation/x64                              9m26s   8GB
Aug 21 04:38:16 Starting examples/compilation/x64/proofs
Aug 21 04:42:57 Finished examples/compilation/x64/proofs                       4m40s   9GB
Aug 21 04:42:58 Starting examples/compilation/ag32
Aug 21 04:45:46 Finished examples/compilation/ag32                             2m47s   5GB
Aug 21 04:45:47 Starting examples/compilation/ag32/proofs
Aug 21 04:47:30 Finished examples/compilation/ag32/proofs                      1m42s  10GB
Aug 21 04:47:31 Starting examples/compilation/to_word
Aug 21 04:51:38 Finished examples/compilation/to_word                          4m05s  11GB
Aug 21 04:51:39 Starting examples/lpr_checker
Aug 21 04:52:02 FAILED: examples/lpr_checker
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/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
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
Scanned 29 directories
Starting work on README.md
Starting work on satSemTheory
README.md                                                           (0s)     OK
satSemTheory                                                       (11s)     OK
Starting work on lprTheory
lprTheory                                                           (7s)FAIL<1>
 Saved definition ____ "is_AT_def"
 Saved definition ____ "check_overlap_def"
 Saved definition ____ "flip_def"
 Saved definition ____ "overlap_assignment_def"
 Saved definition ____ "check_RAT_def"
 Saved definition ____ "check_PR_def"
 Saved definition ____ "is_PR_def"
 error in quse /scratch/cakeml/regression/cakeml-2558/examples/lpr_checker/lprScript.sml : HOL_ERR {message = "on line 180, characters 23-24:\n\nType inference failure: unable to infer a type for the application of\n\nis_PR (fml :int list sptree$num_map) (p :int) (C :int list)\n  (w :int list option)\n\non line 180, characters 7-21\n\nwhich has type\n\n:(int list sptree$num_map, int list) map list ->\n(num # (int list sptree$num_map, int list) map list) list -> bool\n\nto\n\n(i0 :num list)\n\non line 180, characters 23-24\n\nunification failure message: Attempt to unify different type operators: mlmap$map and num$num\n", origin_function = "type-analysis", origin_structure = "Preterm"}
 error in load /scratch/cakeml/regression/cakeml-2558/examples/lpr_checker/lprScript : HOL_ERR {message = "on line 180, characters 23-24:\n\nType inference failure: unable to infer a type for the application of\n\nis_PR (fml :int list sptree$num_map) (p :int) (C :int list)\n  (w :int list option)\n\non line 180, characters 7-21\n\nwhich has type\n\n:(int list sptree$num_map, int list) map list ->\n(num # (int list sptree$num_map, int list) map list) list -> bool\n\nto\n\n(i0 :num list)\n\non line 180, characters 23-24\n\nunification failure message: Attempt to unify different type operators: mlmap$map and num$num\n", origin_function = "type-analysis", origin_structure = "Preterm"}
 Uncaught exception: HOL_ERR {message = "on line 180, characters 23-24:\n\nType inference failure: unable to infer a type for the application of\n\nis_PR (fml :int list sptree$num_map) (p :int) (C :int list)\n  (w :int list option)\n\non line 180, characters 7-21\n\nwhich has type\n\n:(int list sptree$num_map, int list) map list ->\n(num # (int list sptree$num_map, int list) map list) list -> bool\n\nto\n\n(i0 :num list)\n\non line 180, characters 23-24\n\nunification failure message: Attempt to unify different type operators: mlmap$map and num$num\n", origin_function = "type-analysis", origin_structure = "Preterm"}