Job 2799

CakeML:4dc27826a8f14f45cf83be4923cc034b644c12c8
  Fix breakage [Apr 07 13:04:54]
#1152 (lexer-fix)
Merging into:e7e9834e1b1dfda72d0c264ed85dc7a674f82796
  Merge pull request #1151 from CakeML/pb_opt [Apr 06 20:39:02]
HOL:aa266667af464b9d3a22e8be1415d8f3af014c82
  Implement EQ_MP_TAC, which reverses primitive rule EQ_MP [Apr 01 04:57:21]
Machine:pavlova

Apr 07 15:56:37 Claimed job
Apr 07 15:56:44 Reusing HOL
Apr 07 15:56:54 Starting developers
Apr 07 15:56:58 Finished developers                                               2s 144MB
Apr 07 15:56:59 Starting developers/bin
Apr 07 15:57:05 Finished developers/bin                                           5s 746MB
Apr 07 15:57:06 Starting misc
Apr 07 15:57:49 Finished misc                                                    41s   1GB
Apr 07 15:57:50 Starting compiler/proofs
Apr 07 17:42:35 Finished compiler/proofs                                    1h44m44s  30GB
Apr 07 17:42:36 Starting compiler/bootstrap/translation
Apr 07 23:33:34 Finished compiler/bootstrap/translation                     5h50m55s 102GB
Apr 07 23:33:35 Starting semantics/ffi
Apr 07 23:33:45 Finished semantics/ffi                                            9s 598MB
Apr 07 23:33:46 Starting semantics
Apr 07 23:33:47 Finished semantics                                                0s  52MB
Apr 07 23:33:48 Starting semantics/proofs
Apr 07 23:34:11 Finished semantics/proofs                                        22s 708MB
Apr 07 23:34:12 Starting semantics/alt_semantics
Apr 07 23:34:33 Finished semantics/alt_semantics                                 19s 896MB
Apr 07 23:34:34 Starting semantics/alt_semantics/proofs
Apr 07 23:44:46 Finished semantics/alt_semantics/proofs                       10m11s   2GB
Apr 07 23:44:47 Starting basis/pure
Apr 07 23:44:49 Finished basis/pure                                               0s  99MB
Apr 07 23:44:50 Starting translator
Apr 07 23:46:26 Finished translator                                            1m35s   2GB
Apr 07 23:46:27 Starting compiler/parsing
Apr 07 23:46:29 Finished compiler/parsing                                         0s  62MB
Apr 07 23:46:29 Starting characteristic
Apr 07 23:46:32 Finished characteristic                                           1s 120MB
Apr 07 23:46:32 Starting translator/monadic
Apr 07 23:46:34 Finished translator/monadic                                       1s 118MB
Apr 07 23:46:35 Starting translator/monadic/monad_base
Apr 07 23:46:37 Finished translator/monadic/monad_base                            0s  55MB
Apr 07 23:46:38 Starting basis
Apr 07 23:48:57 Finished basis                                                 2m17s   3GB
Apr 07 23:48:58 Starting compiler
Apr 07 23:49:00 Finished compiler                                                 1s 211MB
Apr 07 23:49:01 Starting compiler/inference
Apr 07 23:49:03 Finished compiler/inference                                       1s 119MB
Apr 07 23:49:04 Starting compiler/backend/reg_alloc
Apr 07 23:49:06 Finished compiler/backend/reg_alloc                               0s  58MB
Apr 07 23:49:06 Starting compiler/backend/gc
Apr 07 23:49:09 Finished compiler/backend/gc                                      1s 144MB
Apr 07 23:49:10 Starting compiler/backend
Apr 07 23:49:15 Finished compiler/backend                                         4s 259MB
Apr 07 23:49:15 Starting compiler/encoders/asm
Apr 07 23:49:17 Finished compiler/encoders/asm                                    0s  86MB
Apr 07 23:49:18 Starting compiler/encoders/x64
Apr 07 23:49:20 Finished compiler/encoders/x64                                    0s  89MB
Apr 07 23:49:21 Starting compiler/encoders/arm7
Apr 07 23:49:22 Finished compiler/encoders/arm7                                   0s  92MB
Apr 07 23:49:23 Starting compiler/encoders/arm8
Apr 07 23:49:25 Finished compiler/encoders/arm8                                   0s  88MB
Apr 07 23:49:26 Starting compiler/encoders/arm8_asl
Apr 07 23:50:23 Finished compiler/encoders/arm8_asl                              55s  20GB
Apr 07 23:50:24 Starting compiler/encoders/mips
Apr 07 23:50:26 Finished compiler/encoders/mips                                   0s  89MB
Apr 07 23:50:26 Starting compiler/encoders/riscv
Apr 07 23:50:28 Finished compiler/encoders/riscv                                  0s  88MB
Apr 07 23:50:29 Starting compiler/encoders/ag32
Apr 07 23:50:31 Finished compiler/encoders/ag32                                   0s  82MB
Apr 07 23:50:32 Starting compiler/encoders/tests
Apr 07 23:50:34 Finished compiler/encoders/tests                                  0s 109MB
Apr 07 23:50:34 Starting compiler/encoders/monadic_enc
Apr 07 23:50:37 Finished compiler/encoders/monadic_enc                            1s 141MB
Apr 07 23:50:38 Starting compiler/backend/x64
Apr 07 23:50:40 Finished compiler/backend/x64                                     1s 143MB
Apr 07 23:50:41 Starting compiler/backend/arm7
Apr 07 23:50:43 Finished compiler/backend/arm7                                    1s 143MB
Apr 07 23:50:44 Starting compiler/backend/arm8
Apr 07 23:50:46 Finished compiler/backend/arm8                                    1s 143MB
Apr 07 23:50:47 Starting compiler/backend/mips
Apr 07 23:50:49 Finished compiler/backend/mips                                    1s 142MB
Apr 07 23:50:50 Starting compiler/backend/riscv
Apr 07 23:50:52 Finished compiler/backend/riscv                                   1s 143MB
Apr 07 23:50:53 Starting compiler/backend/ag32
Apr 07 23:52:00 Finished compiler/backend/ag32                                 1m06s   3GB
Apr 07 23:52:01 Starting compiler/backend/pattern_matching
Apr 07 23:52:03 Finished compiler/backend/pattern_matching                        0s  52MB
Apr 07 23:52:04 Starting compiler/parsing/ocaml
Apr 07 23:53:45 Finished compiler/parsing/ocaml                                1m40s   1GB
Apr 07 23:53:46 Starting compiler/printing
Apr 07 23:53:48 Finished compiler/printing                                        1s 112MB
Apr 07 23:53:49 Starting compiler/parsing/proofs
Apr 07 23:53:51 Finished compiler/parsing/proofs                                  0s  62MB
Apr 07 23:53:51 Starting compiler/inference/proofs
Apr 07 23:53:53 Finished compiler/inference/proofs                                1s 113MB
Apr 07 23:53:54 Starting compiler/backend/semantics
Apr 07 23:57:03 Finished compiler/backend/semantics                            3m07s   3GB
Apr 07 23:57:04 Starting compiler/backend/reg_alloc/proofs
Apr 07 23:57:06 Finished compiler/backend/reg_alloc/proofs                        1s 119MB
Apr 07 23:57:07 Starting compiler/backend/proofs
Apr 07 23:57:56 Finished compiler/backend/proofs                                 47s   3GB
Apr 07 23:57:57 Starting compiler/backend/serialiser
Apr 07 23:57:59 Finished compiler/backend/serialiser                              1s 145MB
Apr 07 23:58:00 Starting compiler/encoders/x64/proofs
Apr 08 00:08:08 Finished compiler/encoders/x64/proofs                         10m07s   4GB
Apr 08 00:08:09 Starting compiler/encoders/arm7/proofs
Apr 08 00:21:21 Finished compiler/encoders/arm7/proofs                        13m10s  10GB
Apr 08 00:21:22 Starting compiler/encoders/arm8/proofs
Apr 08 00:28:19 Finished compiler/encoders/arm8/proofs                         6m56s   4GB
Apr 08 00:28:20 Starting compiler/encoders/arm8_asl/proofs
Apr 08 00:43:44 Finished compiler/encoders/arm8_asl/proofs                    15m22s   3GB
Apr 08 00:43:45 Starting compiler/encoders/mips/proofs
Apr 08 00:53:58 Finished compiler/encoders/mips/proofs                        10m12s   8GB
Apr 08 00:54:00 Starting compiler/encoders/riscv/proofs
Apr 08 01:02:15 Finished compiler/encoders/riscv/proofs                        8m14s   3GB
Apr 08 01:02:16 Starting compiler/encoders/ag32/proofs
Apr 08 01:05:06 Finished compiler/encoders/ag32/proofs                         2m49s   1GB
Apr 08 01:05:07 Starting compiler/backend/x64/proofs
Apr 08 01:05:39 Finished compiler/backend/x64/proofs                             31s   2GB
Apr 08 01:05:40 Starting compiler/backend/arm7/proofs
Apr 08 01:06:14 Finished compiler/backend/arm7/proofs                            32s   2GB
Apr 08 01:06:15 Starting compiler/backend/arm8/proofs
Apr 08 01:06:45 Finished compiler/backend/arm8/proofs                            29s   2GB
Apr 08 01:06:46 Starting compiler/backend/arm8_asl
Apr 08 01:07:07 Finished compiler/backend/arm8_asl                               20s   1GB
Apr 08 01:07:08 Starting compiler/backend/mips/proofs
Apr 08 01:07:39 Finished compiler/backend/mips/proofs                            29s   2GB
Apr 08 01:07:39 Starting compiler/backend/riscv/proofs
Apr 08 01:08:11 Finished compiler/backend/riscv/proofs                           31s   2GB
Apr 08 01:08:12 Starting compiler/backend/ag32/proofs
Apr 08 01:21:49 Finished compiler/backend/ag32/proofs                         13m35s   5GB
Apr 08 01:21:50 Starting compiler/backend/cv_compute
Apr 08 01:22:59 Finished compiler/backend/cv_compute                           1m09s   2GB
Apr 08 01:23:00 Starting cv_translator
Apr 08 01:43:51 Finished cv_translator                                        20m48s   7GB
Apr 08 01:43:52 Starting candle
Apr 08 01:43:53 Finished candle                                                   0s  12MB
Apr 08 01:43:54 Starting candle/set-theory
Apr 08 01:44:29 Finished candle/set-theory                                       33s   1GB
Apr 08 01:44:30 Starting candle/syntax-lib
Apr 08 01:44:31 Finished candle/syntax-lib                                        0s  96MB
Apr 08 01:44:32 Starting candle/standard
Apr 08 01:44:33 Finished candle/standard                                          0s  11MB
Apr 08 01:44:34 Starting candle/standard/syntax
Apr 08 01:44:47 Finished candle/standard/syntax                                  11s 794MB
Apr 08 01:44:48 Starting candle/standard/semantics
Apr 08 01:46:49 Finished candle/standard/semantics                             2m00s   2GB
Apr 08 01:46:50 Starting candle/standard/monadic
Apr 08 01:46:52 Finished candle/standard/monadic                                  1s 126MB
Apr 08 01:46:53 Starting candle/standard/ml_kernel
Apr 08 01:48:43 Finished candle/standard/ml_kernel                             1m48s   4GB
Apr 08 01:48:44 Starting candle/standard/ml_kernel/lisp
Apr 08 01:48:45 Finished candle/standard/ml_kernel/lisp                           0s  51MB
Apr 08 01:48:46 Starting candle/overloading
Apr 08 01:48:47 Finished candle/overloading                                       0s  11MB
Apr 08 01:48:48 Starting candle/overloading/syntax
Apr 08 01:51:52 Finished candle/overloading/syntax                             3m03s   2GB
Apr 08 01:51:53 Starting candle/overloading/semantics
Apr 08 02:02:53 Finished candle/overloading/semantics                         10m59s   6GB
Apr 08 02:02:54 Starting candle/overloading/monadic
Apr 08 02:05:13 Finished candle/overloading/monadic                            2m18s   2GB
Apr 08 02:05:14 Starting candle/overloading/ml_kernel
Apr 08 02:12:26 Finished candle/overloading/ml_kernel                          7m11s   5GB
Apr 08 02:12:27 Starting candle/overloading/ml_checker
Apr 08 02:14:39 Finished candle/overloading/ml_checker                         2m10s   6GB
Apr 08 02:14:39 Starting candle/prover
Apr 08 02:24:19 Finished candle/prover                                         9m38s   5GB
Apr 08 02:24:20 Starting candle/prover/compute
Apr 08 02:24:22 Finished candle/prover/compute                                    1s 145MB
Apr 08 02:24:23 Starting pancake
Apr 08 02:24:46 Finished pancake                                                 21s 833MB
Apr 08 02:24:47 Starting pancake/semantics
Apr 08 02:26:54 Finished pancake/semantics                                     2m06s   1GB
Apr 08 02:26:55 Starting pancake/parser
Apr 08 02:27:19 Finished pancake/parser                                          22s 485MB
Apr 08 02:27:20 Starting pancake/static_checker
Apr 08 02:27:56 Finished pancake/static_checker                                  35s   1GB
Apr 08 02:27:57 Starting pancake/proofs
Apr 08 02:43:47 Finished pancake/proofs                                       15m48s   7GB
Apr 08 02:43:48 Starting pancake/ta_progs
Apr 08 02:43:49 Finished pancake/ta_progs                                         0s  12MB
Apr 08 02:43:50 Starting compiler/dafny
Apr 08 02:46:48 Finished compiler/dafny                                        2m56s  11GB
Apr 08 02:46:49 Starting compiler/dafny/translation
Apr 08 03:06:06 Finished compiler/dafny/translation                           19m16s  19GB
Apr 08 03:06:07 Starting compiler/dafny/compilation
Apr 08 03:09:06 Finished compiler/dafny/compilation                            2m57s  11GB
Apr 08 03:09:07 Starting compiler/dafny/semantics
Apr 08 03:09:43 Finished compiler/dafny/semantics                                34s   1GB
Apr 08 03:09:43 Starting characteristic/examples
Apr 08 03:11:07 Finished characteristic/examples                               1m22s   4GB
Apr 08 03:11:08 Starting tutorial/solutions
Apr 08 03:13:31 Finished tutorial/solutions                                    2m22s   3GB
Apr 08 03:13:32 Starting translator/monadic/examples
Apr 08 03:16:26 Finished translator/monadic/examples                           2m52s   3GB
Apr 08 03:16:27 Starting examples
Apr 08 03:22:23 Finished examples                                              5m54s   4GB
Apr 08 03:22:23 Starting examples/compilation
Apr 08 03:22:24 Finished examples/compilation                                     0s  11MB
Apr 08 03:22:25 Starting examples/compilation/x64
Apr 08 03:29:20 Finished examples/compilation/x64                              6m53s   4GB
Apr 08 03:29:21 Starting examples/compilation/x64/proofs
Apr 08 03:31:45 Finished examples/compilation/x64/proofs                       2m23s   4GB
Apr 08 03:31:46 Starting examples/compilation/ag32
Apr 08 03:33:42 Finished examples/compilation/ag32                             1m54s   3GB
Apr 08 03:33:43 Starting examples/compilation/ag32/proofs
Apr 08 03:34:45 Finished examples/compilation/ag32/proofs                      1m01s   5GB
Apr 08 03:34:45 Starting examples/lpr_checker
Apr 08 03:35:15 Finished examples/lpr_checker                                    29s   1GB
Apr 08 03:35:16 Starting examples/lpr_checker/array
Apr 08 04:01:23 Finished examples/lpr_checker/array                           26m04s  29GB
Apr 08 04:01:23 Starting examples/lpr_checker/array/compilation
Apr 08 04:03:44 Finished examples/lpr_checker/array/compilation                2m19s   7GB
Apr 08 04:03:45 Starting examples/lpr_checker/array/compilation/proofs
Apr 08 04:04:57 Finished examples/lpr_checker/array/compilation/proofs         1m11s   6GB
Apr 08 04:04:58 Starting examples/lpr_checker/array/compilation/proofsARM8
Apr 08 04:06:04 Finished examples/lpr_checker/array/compilation/proofsARM8     1m04s   6GB
Apr 08 04:06:05 Starting .
Apr 08 04:06:09 Finished .                                                        2s 305MB
Apr 08 04:06:10 Starting examples/xlrup_checker
Apr 08 04:06:44 Finished examples/xlrup_checker                                  33s   1GB
Apr 08 04:06:45 Starting examples/xlrup_checker/array
Apr 08 04:19:32 Finished examples/xlrup_checker/array                         12m45s   7GB
Apr 08 04:19:33 Starting examples/xlrup_checker/array/compilation
Apr 08 04:20:34 Finished examples/xlrup_checker/array/compilation              1m00s   4GB
Apr 08 04:20:35 Starting examples/xlrup_checker/array/compilation/proofs
Apr 08 04:21:37 Finished examples/xlrup_checker/array/compilation/proofs       1m01s   4GB
Apr 08 04:21:38 Starting examples/pseudo_bool
Apr 08 04:23:09 Finished examples/pseudo_bool                                  1m29s   2GB
Apr 08 04:23:10 Starting examples/pseudo_bool/cnf_encoding
Apr 08 04:23:39 Finished examples/pseudo_bool/cnf_encoding                       28s   1GB
Apr 08 04:23:40 Starting examples/pseudo_bool/graph_encoding
Apr 08 04:24:23 Finished examples/pseudo_bool/graph_encoding                     41s   1GB
Apr 08 04:24:24 Starting examples/pseudo_bool/array
Apr 08 05:32:26 Finished examples/pseudo_bool/array                         1h08m00s  42GB
Apr 08 05:32:27 Starting examples/pseudo_bool/array/compilation
Apr 08 05:42:13 Finished examples/pseudo_bool/array/compilation                9m44s  20GB
Apr 08 05:42:14 Starting examples/pseudo_bool/array/compilation/proofs
Apr 08 05:44:50 Finished examples/pseudo_bool/array/compilation/proofs         2m35s   6GB
Apr 08 05:44:51 Starting examples/pseudo_bool/array/compilation/proofsARM8
Apr 08 05:46:04 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m12s   6GB
Apr 08 05:46:05 Starting examples/opentheory
Apr 08 05:54:32 Finished examples/opentheory                                   8m25s   5GB
Apr 08 05:54:33 Starting examples/opentheory/compilation
Apr 08 05:56:04 Finished examples/opentheory/compilation                       1m30s   6GB
Apr 08 05:56:05 Starting examples/opentheory/compilation/proofs
Apr 08 05:57:05 Finished examples/opentheory/compilation/proofs                  59s   4GB
Apr 08 05:57:06 Starting examples/opentheory/compilation/ag32
Apr 08 05:58:46 Finished examples/opentheory/compilation/ag32                  1m39s   7GB
Apr 08 05:58:47 Starting examples/opentheory/compilation/ag32/proofs
Apr 08 06:00:26 Finished examples/opentheory/compilation/ag32/proofs           1m37s   7GB
Apr 08 06:00:28 Starting examples/sat_encodings
Apr 08 06:01:28 Finished examples/sat_encodings                                  59s 907MB
Apr 08 06:01:29 Starting examples/sat_encodings/demo
Apr 08 06:01:30 Finished examples/sat_encodings/demo                              0s  11MB
Apr 08 06:01:31 Starting examples/sat_encodings/case_studies
Apr 08 06:03:14 Finished examples/sat_encodings/case_studies                   1m42s   1GB
Apr 08 06:03:15 Starting examples/sat_encodings/translation
Apr 08 06:06:51 Finished examples/sat_encodings/translation                    3m35s   3GB
Apr 08 06:06:52 Starting examples/sat_encodings/translation/compilation
Apr 08 06:08:47 Finished examples/sat_encodings/translation/compilation        1m53s   4GB
Apr 08 06:08:48 Starting examples/deflate
Apr 08 06:09:16 Finished examples/deflate                                        26s 664MB
Apr 08 06:09:17 Starting examples/deflate/translation
Apr 08 06:10:22 Finished examples/deflate/translation                          1m04s   4GB
Apr 08 06:10:23 Starting examples/deflate/translation/compilation
Apr 08 06:11:14 Finished examples/deflate/translation/compilation                49s   4GB
Apr 08 06:11:15 Starting examples/vipr
Apr 08 06:14:44 Finished examples/vipr                                         3m27s   4GB
Apr 08 06:14:45 Starting examples/vipr/compilation
Apr 08 06:15:42 Finished examples/vipr/compilation                               56s   4GB
Apr 08 06:15:43 Starting translator/okasaki-examples
Apr 08 06:19:50 Finished translator/okasaki-examples                           4m05s   2GB
Apr 08 06:19:51 Starting translator/other-examples
Apr 08 06:20:40 Finished translator/other-examples                               48s   2GB
Apr 08 06:20:41 Starting translator/other-examples/auxiliary
Apr 08 06:20:42 Finished translator/other-examples/auxiliary                      0s  13MB
Apr 08 06:20:43 Starting compiler/parsing/tests
Apr 08 06:20:56 FAILED: compiler/parsing/tests
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)/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)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/parsing
Scanned 20 directories
Starting work on README.md
Starting work on cmlTestsTheory
Starting work on lexerTestsTheory
README.md                                                           (0s)     OK
lexerTestsTheory                                                    (9s)FAIL<1>
 <<HOL message: Created theory "lexerTests">>
 
 Type inference failure: unable to infer a type for the application of
 
 LongidT :path -> string -> token
 
 on line 31, characters 40-46
 
 to
 
 "a_1'"
 
 on frag 0 row 0, between cols 9 and 14
 
 which has type
 
 :string
 
 unification failure message: Attempt to unify different type operators: tokens$path and list$list
 error in quse /scratch/cakeml/regression/cakeml-2799/compiler/parsing/tests/lexerTestsScript.sml : HOL_ERR {message = "\nType inference failure: unable to infer a type for the application of\n\nLongidT :path -> string -> token\n\non line 31, characters 40-46\n\nto\n\n\"a_1'\"\n\non frag 0 row 0, between cols 9 and 14\n\nwhich has type\n\n:string\n\nunification failure message: Attempt to unify different type operators: tokens$path and list$list\n", origin_function = "type-analysis", origin_structure = "Preterm", source_location = Loc (LocP (0, 0, 9), LocP (0, 0, 14))}
 error in load /scratch/cakeml/regression/cakeml-2799/compiler/parsing/tests/lexerTestsScript : HOL_ERR {message = "\nType inference failure: unable to infer a type for the application of\n\nLongidT :path -> string -> token\n\non line 31, characters 40-46\n\nto\n\n\"a_1'\"\n\non frag 0 row 0, between cols 9 and 14\n\nwhich has type\n\n:string\n\nunification failure message: Attempt to unify different type operators: tokens$path and list$list\n", origin_function = "type-analysis", origin_structure = "Preterm", source_location = Loc (LocP (0, 0, 9), LocP (0, 0, 14))}
 Uncaught exception at /scratch/cakeml/regression/HOL-aa266667af464b9d3a22e8be1415d8f3af014c82/src/parse/TermParse.sml:256: HOL_ERR {message = "\nType inference failure: unable to infer a type for the application of\n\nLongidT :path -> string -> token\n\non line 31, characters 40-46\n\nto\n\n\"a_1'\"\n\non frag 0 row 0, between cols 9 and 14\n\nwhich has type\n\n:string\n\nunification failure message: Attempt to unify different type operators: tokens$path and list$list\n", origin_function = "type-analysis", origin_structure = "Preterm", source_location = Loc (LocP (0, 0, 9), LocP (0, 0, 14))}
cmlTestsTheory                                                      (9s)MKILLED