Job 2595

CakeML:b0fe517748249b0743f701c337ca6237e2ed536c
  remove trailing whitespaces [Sep 05 04:00:04]
#1051 (pancake_itree2)
Merging into:541fc6df534977922a4b2784532cc48a51886146
  Merge pull request #1050 from CakeML/pancake_annot_comments [Aug 31 06:10:48]
HOL:0027639d9586b620303c54f45954b93896dd4587
  [emacs-mode] Fix error in detection of structures caused by previous [Aug 29 06:24:20]
Machine:stove 5.15.0-86-generic x86_64 GNU/Linux

Sep 05 06:45:01 Claimed job
Sep 05 06:45:06 Reusing HOL
Sep 05 06:45:51 Starting developers
Sep 05 06:45:56 Finished developers                                               5s 142MB
Sep 05 06:45:56 Starting developers/bin
Sep 05 06:46:13 Finished developers/bin                                          16s   1GB
Sep 05 06:46:13 Starting compiler/proofs
Sep 05 08:43:31 Finished compiler/proofs                                    1h57m18s  28GB
Sep 05 08:43:31 Starting compiler/bootstrap/translation
Sep 05 17:38:33 Finished compiler/bootstrap/translation                     8h55m02s  37GB
Sep 05 17:38:33 Starting semantics/ffi
Sep 05 17:38:39 Finished semantics/ffi                                            5s 404MB
Sep 05 17:38:39 Starting semantics
Sep 05 17:38:41 Finished semantics                                                1s  21MB
Sep 05 17:38:41 Starting semantics/proofs
Sep 05 17:39:06 Finished semantics/proofs                                        25s 414MB
Sep 05 17:39:06 Starting semantics/alt_semantics
Sep 05 17:39:32 Finished semantics/alt_semantics                                 25s 583MB
Sep 05 17:39:32 Starting semantics/alt_semantics/proofs
Sep 05 17:51:13 Finished semantics/alt_semantics/proofs                       11m40s   1GB
Sep 05 17:51:13 Starting basis/pure
Sep 05 17:51:15 Finished basis/pure                                               1s  17MB
Sep 05 17:51:15 Starting translator
Sep 05 17:52:58 Finished translator                                            1m42s   1GB
Sep 05 17:52:58 Starting compiler/parsing
Sep 05 17:52:59 Finished compiler/parsing                                         1s  17MB
Sep 05 17:52:59 Starting characteristic
Sep 05 17:53:01 Finished characteristic                                           1s  21MB
Sep 05 17:53:01 Starting translator/monadic
Sep 05 17:53:03 Finished translator/monadic                                       1s  25MB
Sep 05 17:53:03 Starting basis
Sep 05 17:55:40 Finished basis                                                 2m36s   3GB
Sep 05 17:55:40 Starting compiler/inference
Sep 05 17:55:42 Finished compiler/inference                                       1s  21MB
Sep 05 17:55:43 Starting compiler/backend/reg_alloc
Sep 05 17:55:44 Finished compiler/backend/reg_alloc                               1s  17MB
Sep 05 17:55:44 Starting compiler/backend/gc
Sep 05 17:55:47 Finished compiler/backend/gc                                      2s  28MB
Sep 05 17:55:47 Starting compiler/backend
Sep 05 17:55:53 Finished compiler/backend                                         5s 296MB
Sep 05 17:55:53 Starting compiler/encoders/asm
Sep 05 17:55:55 Finished compiler/encoders/asm                                    1s  25MB
Sep 05 17:55:55 Starting compiler/encoders/x64
Sep 05 17:55:57 Finished compiler/encoders/x64                                    1s  23MB
Sep 05 17:55:57 Starting compiler/encoders/arm7
Sep 05 17:55:59 Finished compiler/encoders/arm7                                   1s  23MB
Sep 05 17:55:59 Starting compiler/encoders/arm8
Sep 05 17:56:01 Finished compiler/encoders/arm8                                   1s  20MB
Sep 05 17:56:01 Starting compiler/encoders/arm8_asl
Sep 05 17:59:06 Finished compiler/encoders/arm8_asl                            3m04s   1GB
Sep 05 17:59:06 Starting compiler/encoders/mips
Sep 05 17:59:08 Finished compiler/encoders/mips                                   1s  21MB
Sep 05 17:59:08 Starting compiler/encoders/riscv
Sep 05 17:59:10 Finished compiler/encoders/riscv                                  1s  23MB
Sep 05 17:59:10 Starting compiler/encoders/ag32
Sep 05 17:59:12 Finished compiler/encoders/ag32                                   1s  23MB
Sep 05 17:59:12 Starting compiler/backend/x64
Sep 05 17:59:15 Finished compiler/backend/x64                                     2s  24MB
Sep 05 17:59:15 Starting compiler/backend/arm7
Sep 05 17:59:17 Finished compiler/backend/arm7                                    2s  24MB
Sep 05 17:59:17 Starting compiler/backend/arm8
Sep 05 17:59:20 Finished compiler/backend/arm8                                    2s  21MB
Sep 05 17:59:20 Starting compiler/backend/mips
Sep 05 17:59:22 Finished compiler/backend/mips                                    2s  25MB
Sep 05 17:59:22 Starting compiler/backend/riscv
Sep 05 17:59:24 Finished compiler/backend/riscv                                   2s  24MB
Sep 05 17:59:24 Starting compiler/backend/ag32
Sep 05 18:00:54 Finished compiler/backend/ag32                                 1m29s   1GB
Sep 05 18:00:54 Starting compiler/parsing/proofs
Sep 05 18:00:56 Finished compiler/parsing/proofs                                  1s  19MB
Sep 05 18:00:56 Starting compiler/inference/proofs
Sep 05 18:00:58 Finished compiler/inference/proofs                                1s  25MB
Sep 05 18:00:58 Starting compiler/backend/semantics
Sep 05 18:04:27 Finished compiler/backend/semantics                            3m29s   1GB
Sep 05 18:04:27 Starting compiler/backend/reg_alloc/proofs
Sep 05 18:04:29 Finished compiler/backend/reg_alloc/proofs                        1s  21MB
Sep 05 18:04:29 Starting compiler/backend/proofs
Sep 05 18:05:25 Finished compiler/backend/proofs                                 55s   2GB
Sep 05 18:05:25 Starting compiler/backend/serialiser
Sep 05 18:05:27 Finished compiler/backend/serialiser                              2s  26MB
Sep 05 18:05:27 Starting compiler/encoders/x64/proofs
Sep 05 18:16:04 Finished compiler/encoders/x64/proofs                         10m37s   5GB
Sep 05 18:16:05 Starting compiler/encoders/arm7/proofs
Sep 05 18:30:11 Finished compiler/encoders/arm7/proofs                        14m06s   3GB
Sep 05 18:30:11 Starting compiler/encoders/arm8/proofs
Sep 05 18:37:39 Finished compiler/encoders/arm8/proofs                         7m27s   1GB
Sep 05 18:37:39 Starting compiler/encoders/arm8_asl/proofs
Sep 05 18:55:11 Finished compiler/encoders/arm8_asl/proofs                    17m32s   2GB
Sep 05 18:55:11 Starting compiler/encoders/mips/proofs
Sep 05 19:06:02 Finished compiler/encoders/mips/proofs                        10m50s   2GB
Sep 05 19:06:02 Starting compiler/encoders/riscv/proofs
Sep 05 19:15:06 Finished compiler/encoders/riscv/proofs                        9m04s   2GB
Sep 05 19:15:06 Starting compiler/encoders/ag32/proofs
Sep 05 19:18:22 Finished compiler/encoders/ag32/proofs                         3m15s   1GB
Sep 05 19:18:22 Starting compiler/backend/x64/proofs
Sep 05 19:18:54 Finished compiler/backend/x64/proofs                             31s   1GB
Sep 05 19:18:54 Starting compiler/backend/arm7/proofs
Sep 05 19:19:28 Finished compiler/backend/arm7/proofs                            33s   1GB
Sep 05 19:19:28 Starting compiler/backend/arm8/proofs
Sep 05 19:20:00 Finished compiler/backend/arm8/proofs                            31s   1GB
Sep 05 19:20:00 Starting compiler/backend/arm8_asl
Sep 05 19:20:24 Finished compiler/backend/arm8_asl                               23s   1GB
Sep 05 19:20:24 Starting compiler/backend/mips/proofs
Sep 05 19:20:58 Finished compiler/backend/mips/proofs                            34s   1GB
Sep 05 19:20:58 Starting compiler/backend/riscv/proofs
Sep 05 19:21:36 Finished compiler/backend/riscv/proofs                           38s   2GB
Sep 05 19:21:36 Starting compiler/backend/ag32/proofs
Sep 05 19:36:28 Finished compiler/backend/ag32/proofs                         14m51s   2GB
Sep 05 19:36:28 Starting compiler/backend/cv_compute
Sep 05 19:37:48 Finished compiler/backend/cv_compute                           1m20s   2GB
Sep 05 19:37:48 Starting cv_translator
Sep 05 19:58:43 Finished cv_translator                                        20m54s   8GB
Sep 05 19:58:43 Starting candle/set-theory
Sep 05 19:59:26 Finished candle/set-theory                                       43s   1GB
Sep 05 19:59:26 Starting candle/syntax-lib
Sep 05 19:59:28 Finished candle/syntax-lib                                        1s  19MB
Sep 05 19:59:28 Starting candle/standard/syntax
Sep 05 19:59:41 Finished candle/standard/syntax                                  12s 888MB
Sep 05 19:59:41 Starting candle/standard/semantics
Sep 05 20:01:55 Finished candle/standard/semantics                             2m14s   1GB
Sep 05 20:01:55 Starting candle/standard/monadic
Sep 05 20:01:57 Finished candle/standard/monadic                                  1s  22MB
Sep 05 20:01:57 Starting candle/standard/ml_kernel
Sep 05 20:03:47 Finished candle/standard/ml_kernel                             1m49s   3GB
Sep 05 20:03:47 Starting candle/overloading/syntax
Sep 05 20:07:24 Finished candle/overloading/syntax                             3m36s   1GB
Sep 05 20:07:24 Starting candle/overloading/semantics
Sep 05 20:19:58 Finished candle/overloading/semantics                         12m33s   2GB
Sep 05 20:19:58 Starting candle/overloading/monadic
Sep 05 20:22:42 Finished candle/overloading/monadic                            2m43s   2GB
Sep 05 20:22:42 Starting candle/overloading/ml_kernel
Sep 05 20:31:01 Finished candle/overloading/ml_kernel                          8m18s   4GB
Sep 05 20:31:01 Starting candle/overloading/ml_checker
Sep 05 20:33:41 Finished candle/overloading/ml_checker                         2m40s   3GB
Sep 05 20:33:41 Starting candle/prover
Sep 05 20:44:07 Finished candle/prover                                        10m25s   3GB
Sep 05 20:44:07 Starting pancake
Sep 05 20:44:31 Finished pancake                                                 24s 702MB
Sep 05 20:44:31 Starting pancake/ffi
Sep 05 20:44:32 Finished pancake/ffi                                              0s  13MB
Sep 05 20:44:32 Starting pancake/semantics
Sep 05 20:45:10 FAILED: pancake/semantics
Scanning [1m$(HOLDIR)/src/bag[0m
Scanning [1m$(HOLDIR)/src/sort[0m
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/algorithms[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(HOLDIR)/src/algebra/base[0m
Scanning [1m$(HOLDIR)/src/algebra/construction[0m
Scanning [1m$(HOLDIR)/src/algebra[0m
Scanning [1m$(HOLDIR)/src/hol88[0m
Scanning [1m$(HOLDIR)/src/rational[0m
Scanning [1m$(HOLDIR)/src/real[0m
Scanning [1m$(HOLDIR)/src/floating-point[0m
Scanning [1m$(HOLDIR)/src/monad/more_monads[0m
Scanning [1m$(HOLDIR)/src/update[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Scanning [1m$(CAKEMLDIR)/semantics/alt_semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/alt_semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/semantics[0m
Scanning [1m$(CAKEMLDIR)/pancake[0m
Scanned 47 directories
Starting work on README.md
Starting work on compactDSLSemTheory
Starting work on panSemTheory
Starting work on pan_commonPropsTheory
README.md                                                                                                   (0s)     OK
Starting work on loopSemTheory
compactDSLSemTheory                                                                                         (4s)     OK
Starting work on timeSemTheory
pan_commonPropsTheory                                                                                       (8s)     OK
loopSemTheory                                                                                              (11s)     OK
Starting work on loopPropsTheory
timeSemTheory                                                                                               (7s)     OK
Starting work on timeFunSemTheory
Starting work on timePropsTheory
timePropsTheory                                                                                             (2s)     OK
timeFunSemTheory                                                                                            (6s)     OK
panSemTheory                                                                                               (22s)     OK
Starting work on crepSemTheory
Starting work on panPropsTheory
Starting work on panItreeSemTheory
panItreeSemTheory                                                                                          (10s)FAIL<1>
   pattern completion has added 1 clause to the original specification.>>
 <<HOL message: mk_functional: 
   pattern completion has added 2 clauses to the original specification.>>
 Saved definition ____ "h_prog_sh_mem_load_def"
 <<HOL message: mk_functional: 
   pattern completion has added 5 clauses to the original specification.>>
 Saved definition ____ "h_prog_sh_mem_store_def"
 error in quse /home/cug/hk324/cml-regression/cakeml-2595/pancake/semantics/panItreeSemScript.sml : HOL_ERR {message = "between line 459, character 2 and line 478, character 33:\nat Defn.parse_quote:\nat Preterm.type-analysis:\nin unknown location:\nAttempt to unify different type operators: panLang$prog and min$fun", origin_function = "Hol_defn", origin_structure = "Defn"}
 error in load /home/cug/hk324/cml-regression/cakeml-2595/pancake/semantics/panItreeSemScript : HOL_ERR {message = "between line 459, character 2 and line 478, character 33:\nat Defn.parse_quote:\nat Preterm.type-analysis:\nin unknown location:\nAttempt to unify different type operators: panLang$prog and min$fun", origin_function = "Hol_defn", origin_structure = "Defn"}
 Uncaught exception: HOL_ERR {message = "between line 459, character 2 and line 478, character 33:\nat Defn.parse_quote:\nat Preterm.type-analysis:\nin unknown location:\nAttempt to unify different type operators: panLang$prog and min$fun", origin_function = "Hol_defn", origin_structure = "Defn"}
loopPropsTheory                                                                                            (21s)MKILLED
crepSemTheory                                                                                              (11s)MKILLED
panPropsTheory                                                                                             (11s)MKILLED