Job 2555

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:201b9451bbb6cc11025a8c71b859f6249529084a
  Change addUDEdge to take set of nodes as edge argument [Aug 14 10:39:41]
Machine:lammmington

Aug 15 03:45:28 Claimed job
Aug 15 03:45:33 Building HOL
Aug 15 04:00:02 Starting developers
Aug 15 04:00:06 Finished developers                                               2s 230MB
Aug 15 04:00:07 Starting developers/bin
Aug 15 04:00:17 Finished developers/bin                                           9s   1GB
Aug 15 04:00:17 Starting compiler/proofs
Aug 15 05:45:52 Finished compiler/proofs                                    1h45m33s  35GB
Aug 15 05:45:53 Starting compiler/bootstrap/translation
Aug 15 14:20:11 Finished compiler/bootstrap/translation                     8h34m16s  58GB
Aug 15 14:20:12 Starting semantics/ffi
Aug 15 14:20:21 Finished semantics/ffi                                            8s 752MB
Aug 15 14:20:22 Starting semantics
Aug 15 14:20:23 Finished semantics                                                0s  64MB
Aug 15 14:20:24 Starting semantics/proofs
Aug 15 14:20:47 Finished semantics/proofs                                        22s 807MB
Aug 15 14:20:48 Starting semantics/alt_semantics
Aug 15 14:21:14 Finished semantics/alt_semantics                                 24s 705MB
Aug 15 14:21:14 Starting semantics/alt_semantics/proofs
Aug 15 14:31:24 Finished semantics/alt_semantics/proofs                       10m08s   3GB
Aug 15 14:31:25 Starting basis/pure
Aug 15 14:31:26 Finished basis/pure                                               0s  70MB
Aug 15 14:31:27 Starting translator
Aug 15 14:33:01 Finished translator                                            1m33s   5GB
Aug 15 14:33:02 Starting compiler/parsing
Aug 15 14:33:03 Finished compiler/parsing                                         0s  73MB
Aug 15 14:33:04 Starting characteristic
Aug 15 14:33:06 Finished characteristic                                           0s  90MB
Aug 15 14:33:07 Starting translator/monadic
Aug 15 14:33:08 Finished translator/monadic                                       0s  94MB
Aug 15 14:33:09 Starting basis
Aug 15 14:36:30 Finished basis                                                 3m19s   7GB
Aug 15 14:36:30 Starting compiler/inference
Aug 15 14:36:32 Finished compiler/inference                                       0s  94MB
Aug 15 14:36:33 Starting compiler/backend/reg_alloc
Aug 15 14:36:34 Finished compiler/backend/reg_alloc                               0s  67MB
Aug 15 14:36:35 Starting compiler/backend/gc
Aug 15 14:36:37 Finished compiler/backend/gc                                      0s 142MB
Aug 15 14:36:38 Starting compiler/backend
Aug 15 14:36:43 Finished compiler/backend                                         4s 352MB
Aug 15 14:36:44 Starting compiler/encoders/asm
Aug 15 14:36:45 Finished compiler/encoders/asm                                    0s  91MB
Aug 15 14:36:46 Starting compiler/encoders/x64
Aug 15 14:36:47 Finished compiler/encoders/x64                                    0s 102MB
Aug 15 14:36:48 Starting compiler/encoders/arm7
Aug 15 14:36:50 Finished compiler/encoders/arm7                                   0s 103MB
Aug 15 14:36:51 Starting compiler/encoders/arm8
Aug 15 14:36:52 Finished compiler/encoders/arm8                                   0s 102MB
Aug 15 14:36:53 Starting compiler/encoders/arm8_asl
Aug 15 17:00:11 Finished compiler/encoders/arm8_asl                         2h23m16s  48GB
Aug 15 17:00:12 Starting compiler/encoders/mips
Aug 15 17:00:13 Finished compiler/encoders/mips                                   0s 103MB
Aug 15 17:00:15 Starting compiler/encoders/riscv
Aug 15 17:00:17 Finished compiler/encoders/riscv                                  0s 103MB
Aug 15 17:00:18 Starting compiler/encoders/ag32
Aug 15 17:00:19 Finished compiler/encoders/ag32                                   0s  91MB
Aug 15 17:00:20 Starting compiler/backend/x64
Aug 15 17:00:22 Finished compiler/backend/x64                                     0s 146MB
Aug 15 17:00:23 Starting compiler/backend/arm7
Aug 15 17:00:25 Finished compiler/backend/arm7                                    0s 141MB
Aug 15 17:00:26 Starting compiler/backend/arm8
Aug 15 17:00:28 Finished compiler/backend/arm8                                    0s 131MB
Aug 15 17:00:28 Starting compiler/backend/mips
Aug 15 17:00:30 Finished compiler/backend/mips                                    0s 130MB
Aug 15 17:00:31 Starting compiler/backend/riscv
Aug 15 17:00:33 Finished compiler/backend/riscv                                   0s 132MB
Aug 15 17:00:34 Starting compiler/backend/ag32
Aug 15 17:01:55 Finished compiler/backend/ag32                                 1m19s   3GB
Aug 15 17:01:55 Starting compiler/parsing/proofs
Aug 15 17:01:57 Finished compiler/parsing/proofs                                  0s  74MB
Aug 15 17:01:58 Starting compiler/inference/proofs
Aug 15 17:01:59 Finished compiler/inference/proofs                                0s  92MB
Aug 15 17:02:00 Starting compiler/backend/semantics
Aug 15 17:05:08 Finished compiler/backend/semantics                            3m06s   3GB
Aug 15 17:05:09 Starting compiler/backend/reg_alloc/proofs
Aug 15 17:05:10 Finished compiler/backend/reg_alloc/proofs                        0s  99MB
Aug 15 17:05:11 Starting compiler/backend/proofs
Aug 15 17:06:07 Finished compiler/backend/proofs                                 55s   5GB
Aug 15 17:06:08 Starting compiler/backend/serialiser
Aug 15 17:06:10 Finished compiler/backend/serialiser                              0s 141MB
Aug 15 17:06:11 Starting compiler/encoders/x64/proofs
Aug 15 17:15:26 Finished compiler/encoders/x64/proofs                          9m14s   5GB
Aug 15 17:15:27 Starting compiler/encoders/arm7/proofs
Aug 15 17:28:52 Finished compiler/encoders/arm7/proofs                        13m24s  13GB
Aug 15 17:28:53 Starting compiler/encoders/arm8/proofs
Aug 15 17:35:22 Finished compiler/encoders/arm8/proofs                         6m28s   4GB
Aug 15 17:35:23 Starting compiler/encoders/arm8_asl/proofs
Aug 15 18:22:54 Finished compiler/encoders/arm8_asl/proofs                    47m29s  11GB
Aug 15 18:22:55 Starting compiler/encoders/mips/proofs
Aug 15 18:32:48 Finished compiler/encoders/mips/proofs                         9m51s   9GB
Aug 15 18:32:48 Starting compiler/encoders/riscv/proofs
Aug 15 18:40:55 Finished compiler/encoders/riscv/proofs                        8m05s   4GB
Aug 15 18:40:56 Starting compiler/encoders/ag32/proofs
Aug 15 18:43:23 Finished compiler/encoders/ag32/proofs                         2m26s   4GB
Aug 15 18:43:24 Starting compiler/backend/x64/proofs
Aug 15 18:44:09 Finished compiler/backend/x64/proofs                             44s   3GB
Aug 15 18:44:10 Starting compiler/backend/arm7/proofs
Aug 15 18:44:56 Finished compiler/backend/arm7/proofs                            45s   2GB
Aug 15 18:44:57 Starting compiler/backend/arm8/proofs
Aug 15 18:45:42 Finished compiler/backend/arm8/proofs                            43s   3GB
Aug 15 18:45:43 Starting compiler/backend/arm8_asl
Aug 15 18:46:14 Finished compiler/backend/arm8_asl                               30s   2GB
Aug 15 18:46:15 Starting compiler/backend/mips/proofs
Aug 15 18:47:01 Finished compiler/backend/mips/proofs                            45s   3GB
Aug 15 18:47:02 Starting compiler/backend/riscv/proofs
Aug 15 18:47:54 Finished compiler/backend/riscv/proofs                           50s   3GB
Aug 15 18:47:55 Starting compiler/backend/ag32/proofs
Aug 15 19:01:54 Finished compiler/backend/ag32/proofs                         13m58s   6GB
Aug 15 19:01:55 Starting compiler/backend/cv_compute
Aug 15 19:03:37 Finished compiler/backend/cv_compute                           1m41s   3GB
Aug 15 19:03:38 Starting cv_translator
Aug 15 19:22:53 Finished cv_translator                                        19m13s  10GB
Aug 15 19:22:54 Starting candle/set-theory
Aug 15 19:23:43 Finished candle/set-theory                                       48s   1GB
Aug 15 19:23:44 Starting candle/syntax-lib
Aug 15 19:23:46 Finished candle/syntax-lib                                        0s  73MB
Aug 15 19:23:46 Starting candle/standard/syntax
Aug 15 19:24:05 Finished candle/standard/syntax                                  17s   1GB
Aug 15 19:24:07 Starting candle/standard/semantics
Aug 15 19:26:46 Finished candle/standard/semantics                             2m38s   2GB
Aug 15 19:26:46 Starting candle/standard/monadic
Aug 15 19:26:48 Finished candle/standard/monadic                                  0s 108MB
Aug 15 19:26:49 Starting candle/standard/ml_kernel
Aug 15 19:28:51 Finished candle/standard/ml_kernel                             2m01s   5GB
Aug 15 19:28:52 Starting candle/overloading/syntax
Aug 15 19:32:33 Finished candle/overloading/syntax                             3m39s   3GB
Aug 15 19:32:34 Starting candle/overloading/semantics
Aug 15 19:44:12 Finished candle/overloading/semantics                         11m37s   5GB
Aug 15 19:44:13 Starting candle/overloading/monadic
Aug 15 19:46:49 Finished candle/overloading/monadic                            2m35s   2GB
Aug 15 19:46:50 Starting candle/overloading/ml_kernel
Aug 15 19:54:38 Finished candle/overloading/ml_kernel                          7m47s   7GB
Aug 15 19:54:39 Starting candle/overloading/ml_checker
Aug 15 19:57:17 Finished candle/overloading/ml_checker                         2m36s   7GB
Aug 15 19:57:17 Starting candle/prover
Aug 15 20:07:37 Finished candle/prover                                        10m18s   5GB
Aug 15 20:07:38 Starting pancake
Aug 15 20:08:02 Finished pancake                                                 23s 844MB
Aug 15 20:08:03 Starting pancake/ffi
Aug 15 20:08:04 Finished pancake/ffi                                              0s  23MB
Aug 15 20:08:05 Starting pancake/semantics
Aug 15 20:10:09 Finished pancake/semantics                                     2m03s   2GB
Aug 15 20:10:10 Starting pancake/parser
Aug 15 20:10:31 Finished pancake/parser                                          19s 792MB
Aug 15 20:10:32 Starting pancake/proofs
Aug 15 20:25:30 Finished pancake/proofs                                       14m56s   7GB
Aug 15 20:25:31 Starting characteristic/examples
Aug 15 20:26:57 Finished characteristic/examples                               1m25s   4GB
Aug 15 20:26:58 Starting tutorial/solutions
Aug 15 20:29:45 Finished tutorial/solutions                                    2m45s   5GB
Aug 15 20:29:46 Starting translator/monadic/examples
Aug 15 20:32:57 Finished translator/monadic/examples                           3m10s   4GB
Aug 15 20:32:58 Starting examples
Aug 15 20:45:26 Finished examples                                             12m27s   5GB
Aug 15 20:45:27 Starting examples/compilation/x64
Aug 15 20:55:01 Finished examples/compilation/x64                              9m33s   6GB
Aug 15 20:55:02 Starting examples/compilation/x64/proofs
Aug 15 20:59:51 Finished examples/compilation/x64/proofs                       4m48s   8GB
Aug 15 20:59:51 Starting examples/compilation/ag32
Aug 15 21:02:35 Finished examples/compilation/ag32                             2m42s   5GB
Aug 15 21:02:36 Starting examples/compilation/ag32/proofs
Aug 15 21:04:33 Finished examples/compilation/ag32/proofs                      1m56s   9GB
Aug 15 21:04:34 Starting examples/compilation/to_word
Aug 15 21:08:35 Finished examples/compilation/to_word                          4m00s  13GB
Aug 15 21:08:35 Starting examples/lpr_checker
Aug 15 21:08:58 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                                                       (10s)     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/regression2/cakeml-2555/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/regression2/cakeml-2555/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"}