CakeML Regression Test

Job 2552

CakeML:335f8f4ebf9eb0253a6d6eb9639ecc19a08d8466
  Avoid using a heap in "other-examples" [Aug 13 09:50:41]
#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:pavlova

Aug 13 09:54:57 Claimed job
Aug 13 09:55:06 Reusing HOL
Aug 13 09:55:17 Starting developers
Aug 13 09:55:20 Finished developers                                               2s 213MB
Aug 13 09:55:21 Starting developers/bin
Aug 13 09:55:31 Finished developers/bin                                           9s   1GB
Aug 13 09:55:32 Starting compiler/proofs
Aug 13 11:36:33 Finished compiler/proofs                                    1h40m59s  29GB
Aug 13 11:36:34 Starting compiler/bootstrap/translation
Aug 13 20:18:10 Finished compiler/bootstrap/translation                     8h41m35s  91GB
Aug 13 20:18:11 Starting semantics/ffi
Aug 13 20:18:20 Finished semantics/ffi                                            8s 753MB
Aug 13 20:18:21 Starting semantics
Aug 13 20:18:22 Finished semantics                                                0s  64MB
Aug 13 20:18:23 Starting semantics/proofs
Aug 13 20:18:46 Finished semantics/proofs                                        22s 806MB
Aug 13 20:18:47 Starting semantics/alt_semantics
Aug 13 20:19:12 Finished semantics/alt_semantics                                 24s 705MB
Aug 13 20:19:13 Starting semantics/alt_semantics/proofs
Aug 13 20:29:17 Finished semantics/alt_semantics/proofs                       10m03s   3GB
Aug 13 20:29:18 Starting basis/pure
Aug 13 20:29:19 Finished basis/pure                                               0s  70MB
Aug 13 20:29:20 Starting translator
Aug 13 20:30:55 Finished translator                                            1m33s   4GB
Aug 13 20:30:56 Starting compiler/parsing
Aug 13 20:30:57 Finished compiler/parsing                                         0s  68MB
Aug 13 20:30:58 Starting characteristic
Aug 13 20:31:00 Finished characteristic                                           0s  97MB
Aug 13 20:31:01 Starting translator/monadic
Aug 13 20:31:02 Finished translator/monadic                                       0s 101MB
Aug 13 20:31:03 Starting basis
Aug 13 20:34:14 Finished basis                                                 3m10s   4GB
Aug 13 20:34:15 Starting compiler/inference
Aug 13 20:34:17 Finished compiler/inference                                       0s  94MB
Aug 13 20:34:18 Starting compiler/backend/reg_alloc
Aug 13 20:34:19 Finished compiler/backend/reg_alloc                               0s  67MB
Aug 13 20:34:20 Starting compiler/backend/gc
Aug 13 20:34:22 Finished compiler/backend/gc                                      0s 147MB
Aug 13 20:34:22 Starting compiler/backend
Aug 13 20:34:27 Finished compiler/backend                                         3s 336MB
Aug 13 20:34:28 Starting compiler/encoders/asm
Aug 13 20:34:30 Finished compiler/encoders/asm                                    0s  90MB
Aug 13 20:34:31 Starting compiler/encoders/x64
Aug 13 20:34:32 Finished compiler/encoders/x64                                    0s 103MB
Aug 13 20:34:33 Starting compiler/encoders/arm7
Aug 13 20:34:34 Finished compiler/encoders/arm7                                   0s 102MB
Aug 13 20:34:35 Starting compiler/encoders/arm8
Aug 13 20:34:37 Finished compiler/encoders/arm8                                   0s 103MB
Aug 13 20:34:38 Starting compiler/encoders/arm8_asl
Aug 13 20:36:48 Finished compiler/encoders/arm8_asl                            2m09s   1GB
Aug 13 20:36:49 Starting compiler/encoders/mips
Aug 13 20:36:50 Finished compiler/encoders/mips                                   0s 103MB
Aug 13 20:36:51 Starting compiler/encoders/riscv
Aug 13 20:36:53 Finished compiler/encoders/riscv                                  0s 103MB
Aug 13 20:36:54 Starting compiler/encoders/ag32
Aug 13 20:36:55 Finished compiler/encoders/ag32                                   0s  92MB
Aug 13 20:36:56 Starting compiler/backend/x64
Aug 13 20:36:58 Finished compiler/backend/x64                                     0s 137MB
Aug 13 20:36:59 Starting compiler/backend/arm7
Aug 13 20:37:00 Finished compiler/backend/arm7                                    0s 137MB
Aug 13 20:37:01 Starting compiler/backend/arm8
Aug 13 20:37:03 Finished compiler/backend/arm8                                    0s 137MB
Aug 13 20:37:04 Starting compiler/backend/mips
Aug 13 20:37:06 Finished compiler/backend/mips                                    0s 137MB
Aug 13 20:37:07 Starting compiler/backend/riscv
Aug 13 20:37:08 Finished compiler/backend/riscv                                   0s 137MB
Aug 13 20:37:09 Starting compiler/backend/ag32
Aug 13 20:38:30 Finished compiler/backend/ag32                                 1m19s   2GB
Aug 13 20:38:31 Starting compiler/parsing/proofs
Aug 13 20:38:32 Finished compiler/parsing/proofs                                  0s  76MB
Aug 13 20:38:33 Starting compiler/inference/proofs
Aug 13 20:38:35 Finished compiler/inference/proofs                                0s  91MB
Aug 13 20:38:36 Starting compiler/backend/semantics
Aug 13 20:41:44 Finished compiler/backend/semantics                            3m07s   2GB
Aug 13 20:41:45 Starting compiler/backend/reg_alloc/proofs
Aug 13 20:41:46 Finished compiler/backend/reg_alloc/proofs                        0s 100MB
Aug 13 20:41:47 Starting compiler/backend/proofs
Aug 13 20:42:41 Finished compiler/backend/proofs                                 52s   3GB
Aug 13 20:42:42 Starting compiler/backend/serialiser
Aug 13 20:42:44 Finished compiler/backend/serialiser                              0s 140MB
Aug 13 20:42:45 Starting compiler/encoders/x64/proofs
Aug 13 20:52:14 Finished compiler/encoders/x64/proofs                          9m28s   5GB
Aug 13 20:52:15 Starting compiler/encoders/arm7/proofs
Aug 13 21:04:59 Finished compiler/encoders/arm7/proofs                        12m42s   7GB
Aug 13 21:05:00 Starting compiler/encoders/arm8/proofs
Aug 13 21:11:45 Finished compiler/encoders/arm8/proofs                         6m44s   5GB
Aug 13 21:11:46 Starting compiler/encoders/arm8_asl/proofs
Aug 13 21:25:52 Finished compiler/encoders/arm8_asl/proofs                    14m04s   4GB
Aug 13 21:25:53 Starting compiler/encoders/mips/proofs
Aug 13 21:35:59 Finished compiler/encoders/mips/proofs                        10m05s   8GB
Aug 13 21:36:00 Starting compiler/encoders/riscv/proofs
Aug 13 21:44:14 Finished compiler/encoders/riscv/proofs                        8m13s   4GB
Aug 13 21:44:15 Starting compiler/encoders/ag32/proofs
Aug 13 21:46:40 Finished compiler/encoders/ag32/proofs                         2m24s   2GB
Aug 13 21:46:41 Starting compiler/backend/x64/proofs
Aug 13 21:47:26 Finished compiler/backend/x64/proofs                             44s   3GB
Aug 13 21:47:27 Starting compiler/backend/arm7/proofs
Aug 13 21:48:11 Finished compiler/backend/arm7/proofs                            43s   2GB
Aug 13 21:48:12 Starting compiler/backend/arm8/proofs
Aug 13 21:48:55 Finished compiler/backend/arm8/proofs                            41s   3GB
Aug 13 21:48:56 Starting compiler/backend/arm8_asl
Aug 13 21:49:24 Finished compiler/backend/arm8_asl                               27s   2GB
Aug 13 21:49:25 Starting compiler/backend/mips/proofs
Aug 13 21:50:12 Finished compiler/backend/mips/proofs                            46s   3GB
Aug 13 21:50:13 Starting compiler/backend/riscv/proofs
Aug 13 21:51:06 Finished compiler/backend/riscv/proofs                           52s   3GB
Aug 13 21:51:07 Starting compiler/backend/ag32/proofs
Aug 13 22:05:08 Finished compiler/backend/ag32/proofs                         13m59s   6GB
Aug 13 22:05:09 Starting compiler/backend/cv_compute
Aug 13 22:06:53 Finished compiler/backend/cv_compute                           1m43s   4GB
Aug 13 22:06:54 Starting cv_translator
Aug 13 22:26:11 Finished cv_translator                                        19m16s  10GB
Aug 13 22:26:12 Starting candle/set-theory
Aug 13 22:27:02 Finished candle/set-theory                                       49s   1GB
Aug 13 22:27:03 Starting candle/syntax-lib
Aug 13 22:27:04 Finished candle/syntax-lib                                        0s  73MB
Aug 13 22:27:05 Starting candle/standard/syntax
Aug 13 22:27:24 Finished candle/standard/syntax                                  18s   1GB
Aug 13 22:27:25 Starting candle/standard/semantics
Aug 13 22:30:07 Finished candle/standard/semantics                             2m40s   3GB
Aug 13 22:30:08 Starting candle/standard/monadic
Aug 13 22:30:10 Finished candle/standard/monadic                                  0s 108MB
Aug 13 22:30:10 Starting candle/standard/ml_kernel
Aug 13 22:32:16 Finished candle/standard/ml_kernel                             2m04s   4GB
Aug 13 22:32:17 Starting candle/overloading/syntax
Aug 13 22:35:45 Finished candle/overloading/syntax                             3m27s   2GB
Aug 13 22:35:46 Starting candle/overloading/semantics
Aug 13 22:47:21 Finished candle/overloading/semantics                         11m34s   8GB
Aug 13 22:47:22 Starting candle/overloading/monadic
Aug 13 22:49:56 Finished candle/overloading/monadic                            2m33s   3GB
Aug 13 22:49:57 Starting candle/overloading/ml_kernel
Aug 13 22:57:46 Finished candle/overloading/ml_kernel                          7m47s   6GB
Aug 13 22:57:47 Starting candle/overloading/ml_checker
Aug 13 23:00:23 Finished candle/overloading/ml_checker                         2m35s   7GB
Aug 13 23:00:24 Starting candle/prover
Aug 13 23:10:39 Finished candle/prover                                        10m14s   5GB
Aug 13 23:10:40 Starting pancake
Aug 13 23:11:06 Finished pancake                                                 24s 987MB
Aug 13 23:11:07 Starting pancake/ffi
Aug 13 23:11:08 Finished pancake/ffi                                              0s  23MB
Aug 13 23:11:09 Starting pancake/semantics
Aug 13 23:13:13 Finished pancake/semantics                                     2m03s   2GB
Aug 13 23:13:14 Starting pancake/parser
Aug 13 23:13:35 Finished pancake/parser                                          19s 804MB
Aug 13 23:13:35 Starting pancake/proofs
Aug 13 23:28:34 Finished pancake/proofs                                       14m58s   7GB
Aug 13 23:28:35 Starting characteristic/examples
Aug 13 23:30:02 Finished characteristic/examples                               1m25s   4GB
Aug 13 23:30:03 Starting tutorial/solutions
Aug 13 23:32:45 Finished tutorial/solutions                                    2m40s   5GB
Aug 13 23:32:45 Starting translator/monadic/examples
Aug 13 23:35:52 Finished translator/monadic/examples                           3m05s   4GB
Aug 13 23:35:53 Starting examples
Aug 13 23:39:44 FAILED: examples
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)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(HOLDIR)/src/ring/src
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/src/rational
Scanning $(HOLDIR)/src/num/theories/cv_compute/automation
Scanning $(HOLDIR)/examples/bootstrap
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)/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 34 directories
Starting work on README.md
Starting work on quicksortProgTheory
Starting work on catProgTheory
Starting work on lcsTheory
README.md                                                           (0s)     OK
Starting work on divTheory
lcsTheory                                                          (13s)     OK
Starting work on diffTheory
catProgTheory                                                      (50s)     OK
Starting work on doubleArgProgTheory
diffTheory                                                         (41s)     OK
Starting work on diffProgTheory
quicksortProgTheory                                                (58s)     OK
Starting work on array_searchProgTheory
divTheory                                                          (75s)     OK
Starting work on echoProgTheory
doubleArgProgTheory                                                (47s)     OK
Starting work on filterProgTheory
echoProgTheory                                                     (35s)     OK
Starting work on grepProgTheory
diffProgTheory                                                     (56s)     OK
Starting work on helloErrProgTheory
array_searchProgTheory                                             (63s)     OK
Starting work on helloProgTheory
helloErrProgTheory                                                 (39s)     OK
Starting work on insertSortProgTheory
helloProgTheory                                                    (32s)     OK
Starting work on iocatProgTheory
iocatProgTheory                                                    (40s)     OK
Starting work on lispProgTheory
insertSortProgTheory                                               (49s)     OK
Starting work on md5Theory
md5Theory                                                           (9s)FAIL<1>
 Saved definition ____ "transform_def"
 Saved theorem _______ "genlist_rev_compute"
 Saved definition ____ "genlist_rev_def"
 Saved definition ____ "extract_def"
 Saved definition ____ "loop_def"
 Saved induction _____ "loop_ind"
 Saved definition ____ "take_rev_def"
 error in quse /scratch/cakeml/regression/cakeml-2552/examples/md5Script.sml : HOL_ERR {message = "between line 453, character 2 and line 472, character 81:\nat Defn.parse_quote:\nat Preterm.type-analysis:\non line 457, characters 15-19:\n\nType inference failure: unable to infer a type for the application of\n\n\206\187(rcd :md5state). rcd.mlen\n\non line 457, characters 21-24\n\nwhich has type\n\n:md5state -> w64\n\nto\n\n(state :type_env ->\n        (num -> bool) ->\n        \206\177 semanticPrimitives$state -> v sem_env -> \206\177 semantics$state) :type_env ->\n(num -> bool) -> \206\177 semanticPrimitives$state -> v sem_env -> \206\177 semantics$state\n\non line 457, characters 15-19\n\nunification failure message: Attempt to unify different type operators: md5$md5state and min$fun\n", origin_function = "Hol_defn", origin_structure = "Defn"}
 error in load /scratch/cakeml/regression/cakeml-2552/examples/md5Script : HOL_ERR {message = "between line 453, character 2 and line 472, character 81:\nat Defn.parse_quote:\nat Preterm.type-analysis:\non line 457, characters 15-19:\n\nType inference failure: unable to infer a type for the application of\n\n\206\187(rcd :md5state). rcd.mlen\n\non line 457, characters 21-24\n\nwhich has type\n\n:md5state -> w64\n\nto\n\n(state :type_env ->\n        (num -> bool) ->\n        \206\177 semanticPrimitives$state -> v sem_env -> \206\177 semantics$state) :type_env ->\n(num -> bool) -> \206\177 semanticPrimitives$state -> v sem_env -> \206\177 semantics$state\n\non line 457, characters 15-19\n\nunification failure message: Attempt to unify different type operators: md5$md5state and min$fun\n", origin_function = "Hol_defn", origin_structure = "Defn"}
 Uncaught exception: HOL_ERR {message = "between line 453, character 2 and line 472, character 81:\nat Defn.parse_quote:\nat Preterm.type-analysis:\non line 457, characters 15-19:\n\nType inference failure: unable to infer a type for the application of\n\n\206\187(rcd :md5state). rcd.mlen\n\non line 457, characters 21-24\n\nwhich has type\n\n:md5state -> w64\n\nto\n\n(state :type_env ->\n        (num -> bool) ->\n        \206\177 semanticPrimitives$state -> v sem_env -> \206\177 semantics$state) :type_env ->\n(num -> bool) -> \206\177 semanticPrimitives$state -> v sem_env -> \206\177 semantics$state\n\non line 457, characters 15-19\n\nunification failure message: Attempt to unify different type operators: md5$md5state and min$fun\n", origin_function = "Hol_defn", origin_structure = "Defn"}
filterProgTheory                                                  (119s)MKILLED
grepProgTheory                                                    (105s)MKILLED
lispProgTheory                                                     (18s)MKILLED