Job 2587

CakeML:4f8e5714e6b515e367c495059f846916112b12e1
  Fix translator typo [Aug 27 23:41:30]
#1049 (halogentlepersuasion:pan_loadprec)
Merging into:f3c340890fdf92edb95a576acaa607627bc28007
  Merge pull request #1047 from CakeML/alpha-renaming [Aug 27 07:26:20]
HOL:5fc7a6047d48839800489adfb2c2eac7f3ffd5fc
  Add missing export [Aug 21 10:25:23]
Machine:pavlova

Aug 28 00:43:55 Claimed job
Aug 28 00:44:04 Reusing HOL
Aug 28 00:44:15 Starting developers
Aug 28 00:44:19 Finished developers                                               2s 218MB
Aug 28 00:44:19 Starting developers/bin
Aug 28 00:44:30 Finished developers/bin                                           9s   1GB
Aug 28 00:44:31 Starting compiler/proofs
Aug 28 02:26:55 Finished compiler/proofs                                    1h42m23s  23GB
Aug 28 02:26:56 Starting compiler/bootstrap/translation
Aug 28 11:16:49 Finished compiler/bootstrap/translation                     8h49m52s  84GB
Aug 28 11:16:50 Starting semantics/ffi
Aug 28 11:16:59 Finished semantics/ffi                                            7s 830MB
Aug 28 11:17:00 Starting semantics
Aug 28 11:17:01 Finished semantics                                                0s  64MB
Aug 28 11:17:02 Starting semantics/proofs
Aug 28 11:17:25 Finished semantics/proofs                                        22s 796MB
Aug 28 11:17:26 Starting semantics/alt_semantics
Aug 28 11:17:51 Finished semantics/alt_semantics                                 24s 707MB
Aug 28 11:17:52 Starting semantics/alt_semantics/proofs
Aug 28 11:28:12 Finished semantics/alt_semantics/proofs                       10m19s   3GB
Aug 28 11:28:13 Starting basis/pure
Aug 28 11:28:14 Finished basis/pure                                               0s  71MB
Aug 28 11:28:15 Starting translator
Aug 28 11:29:52 Finished translator                                            1m35s   4GB
Aug 28 11:29:53 Starting compiler/parsing
Aug 28 11:29:54 Finished compiler/parsing                                         0s  73MB
Aug 28 11:29:55 Starting characteristic
Aug 28 11:29:57 Finished characteristic                                           0s  90MB
Aug 28 11:29:58 Starting translator/monadic
Aug 28 11:29:59 Finished translator/monadic                                       0s  98MB
Aug 28 11:30:00 Starting basis
Aug 28 11:32:21 Finished basis                                                 2m20s   4GB
Aug 28 11:32:22 Starting compiler/inference
Aug 28 11:32:24 Finished compiler/inference                                       0s  94MB
Aug 28 11:32:24 Starting compiler/backend/reg_alloc
Aug 28 11:32:26 Finished compiler/backend/reg_alloc                               0s  67MB
Aug 28 11:32:27 Starting compiler/backend/gc
Aug 28 11:32:28 Finished compiler/backend/gc                                      0s 147MB
Aug 28 11:32:29 Starting compiler/backend
Aug 28 11:32:34 Finished compiler/backend                                         4s 356MB
Aug 28 11:32:35 Starting compiler/encoders/asm
Aug 28 11:32:37 Finished compiler/encoders/asm                                    0s  91MB
Aug 28 11:32:38 Starting compiler/encoders/x64
Aug 28 11:32:39 Finished compiler/encoders/x64                                    0s 103MB
Aug 28 11:32:40 Starting compiler/encoders/arm7
Aug 28 11:32:41 Finished compiler/encoders/arm7                                   0s 102MB
Aug 28 11:32:42 Starting compiler/encoders/arm8
Aug 28 11:32:44 Finished compiler/encoders/arm8                                   0s 104MB
Aug 28 11:32:45 Starting compiler/encoders/arm8_asl
Aug 28 11:34:55 Finished compiler/encoders/arm8_asl                            2m09s   1GB
Aug 28 11:34:56 Starting compiler/encoders/mips
Aug 28 11:34:57 Finished compiler/encoders/mips                                   0s 105MB
Aug 28 11:34:58 Starting compiler/encoders/riscv
Aug 28 11:34:59 Finished compiler/encoders/riscv                                  0s 103MB
Aug 28 11:35:00 Starting compiler/encoders/ag32
Aug 28 11:35:02 Finished compiler/encoders/ag32                                   0s  92MB
Aug 28 11:35:03 Starting compiler/backend/x64
Aug 28 11:35:04 Finished compiler/backend/x64                                     0s 145MB
Aug 28 11:35:05 Starting compiler/backend/arm7
Aug 28 11:35:07 Finished compiler/backend/arm7                                    0s 145MB
Aug 28 11:35:08 Starting compiler/backend/arm8
Aug 28 11:35:10 Finished compiler/backend/arm8                                    0s 140MB
Aug 28 11:35:11 Starting compiler/backend/mips
Aug 28 11:35:12 Finished compiler/backend/mips                                    0s 135MB
Aug 28 11:35:13 Starting compiler/backend/riscv
Aug 28 11:35:15 Finished compiler/backend/riscv                                   0s 134MB
Aug 28 11:35:16 Starting compiler/backend/ag32
Aug 28 11:36:42 Finished compiler/backend/ag32                                 1m25s   3GB
Aug 28 11:36:43 Starting compiler/parsing/proofs
Aug 28 11:36:45 Finished compiler/parsing/proofs                                  0s  75MB
Aug 28 11:36:46 Starting compiler/inference/proofs
Aug 28 11:36:47 Finished compiler/inference/proofs                                0s  95MB
Aug 28 11:36:48 Starting compiler/backend/semantics
Aug 28 11:40:00 Finished compiler/backend/semantics                            3m10s   3GB
Aug 28 11:40:01 Starting compiler/backend/reg_alloc/proofs
Aug 28 11:40:02 Finished compiler/backend/reg_alloc/proofs                        0s  93MB
Aug 28 11:40:03 Starting compiler/backend/proofs
Aug 28 11:40:55 Finished compiler/backend/proofs                                 51s   3GB
Aug 28 11:40:56 Starting compiler/backend/serialiser
Aug 28 11:40:58 Finished compiler/backend/serialiser                              0s 142MB
Aug 28 11:40:59 Starting compiler/encoders/x64/proofs
Aug 28 11:51:06 Finished compiler/encoders/x64/proofs                         10m05s   5GB
Aug 28 11:51:07 Starting compiler/encoders/arm7/proofs
Aug 28 12:04:04 Finished compiler/encoders/arm7/proofs                        12m56s   9GB
Aug 28 12:04:05 Starting compiler/encoders/arm8/proofs
Aug 28 12:11:03 Finished compiler/encoders/arm8/proofs                         6m57s   6GB
Aug 28 12:11:04 Starting compiler/encoders/arm8_asl/proofs
Aug 28 12:26:11 Finished compiler/encoders/arm8_asl/proofs                    15m06s   4GB
Aug 28 12:26:12 Starting compiler/encoders/mips/proofs
Aug 28 12:36:24 Finished compiler/encoders/mips/proofs                        10m10s   7GB
Aug 28 12:36:25 Starting compiler/encoders/riscv/proofs
Aug 28 12:45:20 Finished compiler/encoders/riscv/proofs                        8m53s   4GB
Aug 28 12:45:20 Starting compiler/encoders/ag32/proofs
Aug 28 12:48:16 Finished compiler/encoders/ag32/proofs                         2m54s   2GB
Aug 28 12:48:17 Starting compiler/backend/x64/proofs
Aug 28 12:48:59 Finished compiler/backend/x64/proofs                             41s   3GB
Aug 28 12:49:00 Starting compiler/backend/arm7/proofs
Aug 28 12:49:46 Finished compiler/backend/arm7/proofs                            44s   3GB
Aug 28 12:49:47 Starting compiler/backend/arm8/proofs
Aug 28 12:50:30 Finished compiler/backend/arm8/proofs                            42s   3GB
Aug 28 12:50:31 Starting compiler/backend/arm8_asl
Aug 28 12:50:59 Finished compiler/backend/arm8_asl                               27s   2GB
Aug 28 12:51:00 Starting compiler/backend/mips/proofs
Aug 28 12:51:46 Finished compiler/backend/mips/proofs                            45s   3GB
Aug 28 12:51:47 Starting compiler/backend/riscv/proofs
Aug 28 12:52:42 Finished compiler/backend/riscv/proofs                           52s   4GB
Aug 28 12:52:43 Starting compiler/backend/ag32/proofs
Aug 28 13:06:59 Finished compiler/backend/ag32/proofs                         14m15s   6GB
Aug 28 13:07:00 Starting compiler/backend/cv_compute
Aug 28 13:08:39 Finished compiler/backend/cv_compute                           1m38s   3GB
Aug 28 13:08:40 Starting cv_translator
Aug 28 13:28:19 Finished cv_translator                                        19m38s  12GB
Aug 28 13:28:20 Starting candle/set-theory
Aug 28 13:29:09 Finished candle/set-theory                                       47s   1GB
Aug 28 13:29:10 Starting candle/syntax-lib
Aug 28 13:29:11 Finished candle/syntax-lib                                        0s  76MB
Aug 28 13:29:12 Starting candle/standard/syntax
Aug 28 13:29:31 Finished candle/standard/syntax                                  18s   1GB
Aug 28 13:29:32 Starting candle/standard/semantics
Aug 28 13:32:12 Finished candle/standard/semantics                             2m39s   4GB
Aug 28 13:32:13 Starting candle/standard/monadic
Aug 28 13:32:15 Finished candle/standard/monadic                                  0s 104MB
Aug 28 13:32:16 Starting candle/standard/ml_kernel
Aug 28 13:34:14 Finished candle/standard/ml_kernel                             1m57s   5GB
Aug 28 13:34:15 Starting candle/overloading/syntax
Aug 28 13:37:57 Finished candle/overloading/syntax                             3m40s   3GB
Aug 28 13:37:58 Starting candle/overloading/semantics
Aug 28 13:49:25 Finished candle/overloading/semantics                         11m26s   7GB
Aug 28 13:49:26 Starting candle/overloading/monadic
Aug 28 13:52:02 Finished candle/overloading/monadic                            2m34s   2GB
Aug 28 13:52:03 Starting candle/overloading/ml_kernel
Aug 28 13:59:52 Finished candle/overloading/ml_kernel                          7m48s   6GB
Aug 28 13:59:53 Starting candle/overloading/ml_checker
Aug 28 14:02:30 Finished candle/overloading/ml_checker                         2m36s   6GB
Aug 28 14:02:31 Starting candle/prover
Aug 28 14:12:51 Finished candle/prover                                        10m19s   5GB
Aug 28 14:12:52 Starting pancake
Aug 28 14:13:18 Finished pancake                                                 25s 983MB
Aug 28 14:13:19 Starting pancake/ffi
Aug 28 14:13:20 Finished pancake/ffi                                              0s  22MB
Aug 28 14:13:21 Starting pancake/semantics
Aug 28 14:15:28 Finished pancake/semantics                                     2m06s   2GB
Aug 28 14:15:29 Starting pancake/parser
Aug 28 14:15:43 FAILED: pancake/parser
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)/examples/machine-code/hoare-triple
Scanning $(HOLDIR)/src/ring/src
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/examples/machine-code/multiword
Scanning $(HOLDIR)/examples/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
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 $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(HOLDIR)/examples/algorithms
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
Scanning $(HOLDIR)/src/algebra/base
Scanning $(HOLDIR)/src/algebra/construction
Scanning $(HOLDIR)/src/algebra
Scanning $(HOLDIR)/src/hol88
Scanning $(HOLDIR)/src/rational
Scanning $(HOLDIR)/src/real
Scanning $(HOLDIR)/src/floating-point
Scanning $(HOLDIR)/src/monad/more_monads
Scanning $(HOLDIR)/src/update
Scanning $(HOLDIR)/examples/l3-machine-code/common
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/pancake
Scanned 44 directories
Starting work on README.md
Starting work on panConcreteExamplesTheory
README.md                                                           (0s)     OK
panConcreteExamplesTheory                                          (11s)FAIL<1>
 <<HOL message: Created theory "panConcreteExamples">>
 error in quse /scratch/cakeml/regression/cakeml-2587/pancake/parser/panConcreteExamplesScript.sml : HOL_ERR {message = "predicate not true", origin_function = "assert", origin_structure = "Lib"}
 error in load /scratch/cakeml/regression/cakeml-2587/pancake/parser/panConcreteExamplesScript : HOL_ERR {message = "predicate not true", origin_function = "assert", origin_structure = "Lib"}
 Uncaught exception: HOL_ERR {message = "predicate not true", origin_function = "assert", origin_structure = "Lib"}