Job 2553

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:37990a0757640901f13b89fb0114ac3aa2d5e064
  Fix issues simplifying and evaluating {NUM,INT}_{FLOOR,CEILING} [Aug 06 07:52:03]
Machine:lammmington

Aug 14 10:19:20 Claimed job
Aug 14 10:19:25 Reusing HOL
Aug 14 10:19:36 Starting developers
Aug 14 10:19:40 Finished developers                                               2s 210MB
Aug 14 10:19:41 Starting developers/bin
Aug 14 10:19:50 Finished developers/bin                                           9s   1GB
Aug 14 10:19:51 Starting compiler/proofs
Aug 14 12:00:50 Finished compiler/proofs                                    1h40m57s  36GB
Aug 14 12:00:51 Starting compiler/bootstrap/translation
Aug 14 20:52:19 Finished compiler/bootstrap/translation                     8h51m27s  81GB
Aug 14 20:52:20 Starting semantics/ffi
Aug 14 20:52:29 Finished semantics/ffi                                            8s 752MB
Aug 14 20:52:30 Starting semantics
Aug 14 20:52:31 Finished semantics                                                0s  64MB
Aug 14 20:52:32 Starting semantics/proofs
Aug 14 20:52:55 Finished semantics/proofs                                        21s 814MB
Aug 14 20:52:56 Starting semantics/alt_semantics
Aug 14 20:53:21 Finished semantics/alt_semantics                                 24s 706MB
Aug 14 20:53:22 Starting semantics/alt_semantics/proofs
Aug 14 21:03:38 Finished semantics/alt_semantics/proofs                       10m14s   2GB
Aug 14 21:03:38 Starting basis/pure
Aug 14 21:03:40 Finished basis/pure                                               0s  70MB
Aug 14 21:03:41 Starting translator
Aug 14 21:05:14 Finished translator                                            1m32s   4GB
Aug 14 21:05:15 Starting compiler/parsing
Aug 14 21:05:17 Finished compiler/parsing                                         0s  73MB
Aug 14 21:05:17 Starting characteristic
Aug 14 21:05:19 Finished characteristic                                           0s  89MB
Aug 14 21:05:20 Starting translator/monadic
Aug 14 21:05:21 Finished translator/monadic                                       0s 101MB
Aug 14 21:05:22 Starting basis
Aug 14 21:08:40 Finished basis                                                 3m16s   6GB
Aug 14 21:08:41 Starting compiler/inference
Aug 14 21:08:42 Finished compiler/inference                                       0s  94MB
Aug 14 21:08:43 Starting compiler/backend/reg_alloc
Aug 14 21:08:45 Finished compiler/backend/reg_alloc                               0s  67MB
Aug 14 21:08:45 Starting compiler/backend/gc
Aug 14 21:08:47 Finished compiler/backend/gc                                      0s 138MB
Aug 14 21:08:48 Starting compiler/backend
Aug 14 21:08:53 Finished compiler/backend                                         4s 346MB
Aug 14 21:08:54 Starting compiler/encoders/asm
Aug 14 21:08:56 Finished compiler/encoders/asm                                    0s  90MB
Aug 14 21:08:57 Starting compiler/encoders/x64
Aug 14 21:08:58 Finished compiler/encoders/x64                                    0s  95MB
Aug 14 21:08:59 Starting compiler/encoders/arm7
Aug 14 21:09:01 Finished compiler/encoders/arm7                                   0s 102MB
Aug 14 21:09:02 Starting compiler/encoders/arm8
Aug 14 21:09:03 Finished compiler/encoders/arm8                                   0s 102MB
Aug 14 21:09:04 Starting compiler/encoders/arm8_asl
Aug 14 21:11:14 Finished compiler/encoders/arm8_asl                            2m09s   1GB
Aug 14 21:11:15 Starting compiler/encoders/mips
Aug 14 21:11:17 Finished compiler/encoders/mips                                   0s 104MB
Aug 14 21:11:18 Starting compiler/encoders/riscv
Aug 14 21:11:19 Finished compiler/encoders/riscv                                  0s 103MB
Aug 14 21:11:20 Starting compiler/encoders/ag32
Aug 14 21:11:22 Finished compiler/encoders/ag32                                   0s 102MB
Aug 14 21:11:22 Starting compiler/backend/x64
Aug 14 21:11:24 Finished compiler/backend/x64                                     0s 145MB
Aug 14 21:11:25 Starting compiler/backend/arm7
Aug 14 21:11:27 Finished compiler/backend/arm7                                    0s 145MB
Aug 14 21:11:28 Starting compiler/backend/arm8
Aug 14 21:11:30 Finished compiler/backend/arm8                                    0s 144MB
Aug 14 21:11:31 Starting compiler/backend/mips
Aug 14 21:11:32 Finished compiler/backend/mips                                    0s 139MB
Aug 14 21:11:33 Starting compiler/backend/riscv
Aug 14 21:11:35 Finished compiler/backend/riscv                                   0s 137MB
Aug 14 21:11:36 Starting compiler/backend/ag32
Aug 14 21:12:57 Finished compiler/backend/ag32                                 1m19s   3GB
Aug 14 21:12:58 Starting compiler/parsing/proofs
Aug 14 21:12:59 Finished compiler/parsing/proofs                                  0s  74MB
Aug 14 21:13:00 Starting compiler/inference/proofs
Aug 14 21:13:02 Finished compiler/inference/proofs                                0s  91MB
Aug 14 21:13:02 Starting compiler/backend/semantics
Aug 14 21:16:19 Finished compiler/backend/semantics                            3m15s   3GB
Aug 14 21:16:19 Starting compiler/backend/reg_alloc/proofs
Aug 14 21:16:21 Finished compiler/backend/reg_alloc/proofs                        0s  98MB
Aug 14 21:16:22 Starting compiler/backend/proofs
Aug 14 21:17:15 Finished compiler/backend/proofs                                 52s   2GB
Aug 14 21:17:16 Starting compiler/backend/serialiser
Aug 14 21:17:18 Finished compiler/backend/serialiser                              0s 141MB
Aug 14 21:17:19 Starting compiler/encoders/x64/proofs
Aug 14 21:26:54 Finished compiler/encoders/x64/proofs                          9m34s   5GB
Aug 14 21:26:55 Starting compiler/encoders/arm7/proofs
Aug 14 21:39:42 Finished compiler/encoders/arm7/proofs                        12m46s  10GB
Aug 14 21:39:43 Starting compiler/encoders/arm8/proofs
Aug 14 21:46:02 Finished compiler/encoders/arm8/proofs                         6m17s   4GB
Aug 14 21:46:03 Starting compiler/encoders/arm8_asl/proofs
Aug 14 21:59:56 Finished compiler/encoders/arm8_asl/proofs                    13m51s   4GB
Aug 14 21:59:56 Starting compiler/encoders/mips/proofs
Aug 14 22:10:06 Finished compiler/encoders/mips/proofs                        10m09s   7GB
Aug 14 22:10:07 Starting compiler/encoders/riscv/proofs
Aug 14 22:18:17 Finished compiler/encoders/riscv/proofs                        8m09s   3GB
Aug 14 22:18:18 Starting compiler/encoders/ag32/proofs
Aug 14 22:20:41 Finished compiler/encoders/ag32/proofs                         2m21s   2GB
Aug 14 22:20:42 Starting compiler/backend/x64/proofs
Aug 14 22:21:25 Finished compiler/backend/x64/proofs                             42s   2GB
Aug 14 22:21:26 Starting compiler/backend/arm7/proofs
Aug 14 22:22:11 Finished compiler/backend/arm7/proofs                            44s   2GB
Aug 14 22:22:12 Starting compiler/backend/arm8/proofs
Aug 14 22:22:57 Finished compiler/backend/arm8/proofs                            43s   3GB
Aug 14 22:22:58 Starting compiler/backend/arm8_asl
Aug 14 22:23:28 Finished compiler/backend/arm8_asl                               29s   2GB
Aug 14 22:23:28 Starting compiler/backend/mips/proofs
Aug 14 22:24:16 Finished compiler/backend/mips/proofs                            46s   3GB
Aug 14 22:24:17 Starting compiler/backend/riscv/proofs
Aug 14 22:25:07 Finished compiler/backend/riscv/proofs                           49s   3GB
Aug 14 22:25:08 Starting compiler/backend/ag32/proofs
Aug 14 22:39:15 Finished compiler/backend/ag32/proofs                         14m05s   6GB
Aug 14 22:39:16 Starting compiler/backend/cv_compute
Aug 14 22:40:59 Finished compiler/backend/cv_compute                           1m42s   2GB
Aug 14 22:41:00 Starting cv_translator
Aug 14 23:00:27 Finished cv_translator                                        19m26s   9GB
Aug 14 23:00:28 Starting candle/set-theory
Aug 14 23:01:17 Finished candle/set-theory                                       47s   1GB
Aug 14 23:01:18 Starting candle/syntax-lib
Aug 14 23:01:19 Finished candle/syntax-lib                                        0s  73MB
Aug 14 23:01:20 Starting candle/standard/syntax
Aug 14 23:01:39 Finished candle/standard/syntax                                  17s   1GB
Aug 14 23:01:39 Starting candle/standard/semantics
Aug 14 23:04:20 Finished candle/standard/semantics                             2m39s   2GB
Aug 14 23:04:21 Starting candle/standard/monadic
Aug 14 23:04:22 Finished candle/standard/monadic                                  0s 106MB
Aug 14 23:04:23 Starting candle/standard/ml_kernel
Aug 14 23:06:23 Finished candle/standard/ml_kernel                             1m58s   5GB
Aug 14 23:06:24 Starting candle/overloading/syntax
Aug 14 23:09:57 Finished candle/overloading/syntax                             3m32s   3GB
Aug 14 23:09:58 Starting candle/overloading/semantics
Aug 14 23:21:19 Finished candle/overloading/semantics                         11m20s   5GB
Aug 14 23:21:20 Starting candle/overloading/monadic
Aug 14 23:24:04 Finished candle/overloading/monadic                            2m42s   3GB
Aug 14 23:24:05 Starting candle/overloading/ml_kernel
Aug 14 23:31:46 Finished candle/overloading/ml_kernel                          7m40s   6GB
Aug 14 23:31:47 Starting candle/overloading/ml_checker
Aug 14 23:34:26 Finished candle/overloading/ml_checker                         2m38s   7GB
Aug 14 23:34:27 Starting candle/prover
Aug 14 23:44:43 Finished candle/prover                                        10m14s   5GB
Aug 14 23:44:44 Starting pancake
Aug 14 23:45:10 Finished pancake                                                 25s 963MB
Aug 14 23:45:11 Starting pancake/ffi
Aug 14 23:45:12 Finished pancake/ffi                                              0s  24MB
Aug 14 23:45:13 Starting pancake/semantics
Aug 14 23:47:17 Finished pancake/semantics                                     2m04s   2GB
Aug 14 23:47:18 Starting pancake/parser
Aug 14 23:47:39 Finished pancake/parser                                          19s 790MB
Aug 14 23:47:40 Starting pancake/proofs
Aug 15 00:02:42 Finished pancake/proofs                                       15m01s   7GB
Aug 15 00:02:43 Starting characteristic/examples
Aug 15 00:04:11 Finished characteristic/examples                               1m26s   4GB
Aug 15 00:04:11 Starting tutorial/solutions
Aug 15 00:06:52 Finished tutorial/solutions                                    2m40s   4GB
Aug 15 00:06:53 Starting translator/monadic/examples
Aug 15 00:09:58 Finished translator/monadic/examples                           3m03s   4GB
Aug 15 00:09:59 Starting examples
Aug 15 00:22:05 Finished examples                                             12m04s   4GB
Aug 15 00:22:06 Starting examples/compilation/x64
Aug 15 00:31:41 Finished examples/compilation/x64                              9m34s   8GB
Aug 15 00:31:42 Starting examples/compilation/x64/proofs
Aug 15 00:36:17 Finished examples/compilation/x64/proofs                       4m33s   8GB
Aug 15 00:36:18 Starting examples/compilation/ag32
Aug 15 00:39:01 Finished examples/compilation/ag32                             2m42s   5GB
Aug 15 00:39:02 Starting examples/compilation/ag32/proofs
Aug 15 00:40:50 Finished examples/compilation/ag32/proofs                      1m46s   9GB
Aug 15 00:40:51 Starting examples/compilation/to_word
Aug 15 00:44:51 Finished examples/compilation/to_word                          3m59s  11GB
Aug 15 00:44:52 Starting examples/lpr_checker
Aug 15 00:45:14 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/regression2/cakeml-2553/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-2553/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"}