Job 2597

CakeML:541fc6df534977922a4b2784532cc48a51886146
  Merge pull request #1050 from CakeML/pancake_annot_comments [Aug 31 06:10:48]
HOL:ba3052854752b85c309b047ba1e544f17084e071
  Add lemma prob_div_mul_relf, refactor code in proofs of BAYES_THEOREM [Sep 03 23:00:37]
Machine:stove 5.15.0-86-generic x86_64 GNU/Linux

Sep 09 17:57:28 Claimed job
Sep 09 17:57:35 Building HOL
Sep 09 18:11:28 Starting developers
Sep 09 18:11:33 Finished developers                                               5s 138MB
Sep 09 18:11:34 Starting developers/bin
Sep 09 18:11:40 Finished developers/bin                                           5s   1GB
Sep 09 18:11:40 Starting compiler/proofs
Sep 09 20:15:29 Finished compiler/proofs                                    2h03m49s  16GB
Sep 09 20:15:29 Starting compiler/bootstrap/translation
Sep 10 05:39:05 Finished compiler/bootstrap/translation                     9h23m36s  36GB
Sep 10 05:39:05 Starting semantics/ffi
Sep 10 05:39:11 Finished semantics/ffi                                            5s 410MB
Sep 10 05:39:11 Starting semantics
Sep 10 05:39:13 Finished semantics                                                1s  20MB
Sep 10 05:39:13 Starting semantics/proofs
Sep 10 05:39:39 Finished semantics/proofs                                        25s 421MB
Sep 10 05:39:39 Starting semantics/alt_semantics
Sep 10 05:40:05 Finished semantics/alt_semantics                                 25s 583MB
Sep 10 05:40:05 Starting semantics/alt_semantics/proofs
Sep 10 05:51:49 Finished semantics/alt_semantics/proofs                       11m44s   1GB
Sep 10 05:51:49 Starting basis/pure
Sep 10 05:51:51 Finished basis/pure                                               1s  18MB
Sep 10 05:51:51 Starting translator
Sep 10 05:53:34 Finished translator                                            1m43s   1GB
Sep 10 05:53:34 Starting compiler/parsing
Sep 10 05:53:36 Finished compiler/parsing                                         1s  19MB
Sep 10 05:53:36 Starting characteristic
Sep 10 05:53:38 Finished characteristic                                           1s  23MB
Sep 10 05:53:38 Starting translator/monadic
Sep 10 05:53:40 Finished translator/monadic                                       1s  22MB
Sep 10 05:53:40 Starting basis
Sep 10 05:56:14 Finished basis                                                 2m33s   2GB
Sep 10 05:56:14 Starting compiler/inference
Sep 10 05:56:16 Finished compiler/inference                                       1s  19MB
Sep 10 05:56:16 Starting compiler/backend/reg_alloc
Sep 10 05:56:18 Finished compiler/backend/reg_alloc                               1s  22MB
Sep 10 05:56:18 Starting compiler/backend/gc
Sep 10 05:56:20 Finished compiler/backend/gc                                      2s  26MB
Sep 10 05:56:20 Starting compiler/backend
Sep 10 05:56:26 Finished compiler/backend                                         5s 292MB
Sep 10 05:56:26 Starting compiler/encoders/asm
Sep 10 05:56:28 Finished compiler/encoders/asm                                    1s  21MB
Sep 10 05:56:28 Starting compiler/encoders/x64
Sep 10 05:56:30 Finished compiler/encoders/x64                                    1s  20MB
Sep 10 05:56:30 Starting compiler/encoders/arm7
Sep 10 05:56:32 Finished compiler/encoders/arm7                                   1s  25MB
Sep 10 05:56:32 Starting compiler/encoders/arm8
Sep 10 05:56:34 Finished compiler/encoders/arm8                                   1s  25MB
Sep 10 05:56:34 Starting compiler/encoders/arm8_asl
Sep 10 08:33:26 Finished compiler/encoders/arm8_asl                         2h36m51s  46GB
Sep 10 08:33:26 Starting compiler/encoders/mips
Sep 10 08:33:28 Finished compiler/encoders/mips                                   1s  24MB
Sep 10 08:33:28 Starting compiler/encoders/riscv
Sep 10 08:33:30 Finished compiler/encoders/riscv                                  1s  21MB
Sep 10 08:33:30 Starting compiler/encoders/ag32
Sep 10 08:33:32 Finished compiler/encoders/ag32                                   1s  24MB
Sep 10 08:33:32 Starting compiler/backend/x64
Sep 10 08:33:34 Finished compiler/backend/x64                                     2s  30MB
Sep 10 08:33:34 Starting compiler/backend/arm7
Sep 10 08:33:37 Finished compiler/backend/arm7                                    2s  32MB
Sep 10 08:33:37 Starting compiler/backend/arm8
Sep 10 08:33:39 Finished compiler/backend/arm8                                    2s  29MB
Sep 10 08:33:39 Starting compiler/backend/mips
Sep 10 08:33:42 Finished compiler/backend/mips                                    2s  30MB
Sep 10 08:33:42 Starting compiler/backend/riscv
Sep 10 08:33:44 Finished compiler/backend/riscv                                   2s  27MB
Sep 10 08:33:44 Starting compiler/backend/ag32
Sep 10 08:35:17 Finished compiler/backend/ag32                                 1m33s   1GB
Sep 10 08:35:17 Starting compiler/parsing/proofs
Sep 10 08:35:19 Finished compiler/parsing/proofs                                  1s  22MB
Sep 10 08:35:19 Starting compiler/inference/proofs
Sep 10 08:35:21 Finished compiler/inference/proofs                                1s  21MB
Sep 10 08:35:21 Starting compiler/backend/semantics
Sep 10 08:39:05 Finished compiler/backend/semantics                            3m43s   1GB
Sep 10 08:39:05 Starting compiler/backend/reg_alloc/proofs
Sep 10 08:39:07 Finished compiler/backend/reg_alloc/proofs                        1s  25MB
Sep 10 08:39:07 Starting compiler/backend/proofs
Sep 10 08:40:12 Finished compiler/backend/proofs                               1m04s   2GB
Sep 10 08:40:12 Starting compiler/backend/serialiser
Sep 10 08:40:15 Finished compiler/backend/serialiser                              2s  25MB
Sep 10 08:40:15 Starting compiler/encoders/x64/proofs
Sep 10 08:51:40 Finished compiler/encoders/x64/proofs                         11m25s   7GB
Sep 10 08:51:40 Starting compiler/encoders/arm7/proofs
Sep 10 09:05:57 Finished compiler/encoders/arm7/proofs                        14m16s   4GB
Sep 10 09:05:57 Starting compiler/encoders/arm8/proofs
Sep 10 09:13:40 Finished compiler/encoders/arm8/proofs                         7m43s   1GB
Sep 10 09:13:40 Starting compiler/encoders/arm8_asl/proofs
Sep 10 10:14:15 Finished compiler/encoders/arm8_asl/proofs                  1h00m34s   8GB
Sep 10 10:14:15 Starting compiler/encoders/mips/proofs
Sep 10 10:26:43 Finished compiler/encoders/mips/proofs                        12m27s   3GB
Sep 10 10:26:43 Starting compiler/encoders/riscv/proofs
Sep 10 10:37:24 Finished compiler/encoders/riscv/proofs                       10m41s   2GB
Sep 10 10:37:25 Starting compiler/encoders/ag32/proofs
Sep 10 10:41:11 Finished compiler/encoders/ag32/proofs                         3m45s   1GB
Sep 10 10:41:11 Starting compiler/backend/x64/proofs
Sep 10 10:41:49 Finished compiler/backend/x64/proofs                             37s   1GB
Sep 10 10:41:49 Starting compiler/backend/arm7/proofs
Sep 10 10:42:29 Finished compiler/backend/arm7/proofs                            40s   1GB
Sep 10 10:42:29 Starting compiler/backend/arm8/proofs
Sep 10 10:43:09 Finished compiler/backend/arm8/proofs                            39s   1GB
Sep 10 10:43:09 Starting compiler/backend/arm8_asl
Sep 10 10:43:37 Finished compiler/backend/arm8_asl                               28s   1GB
Sep 10 10:43:37 Starting compiler/backend/mips/proofs
Sep 10 10:44:17 Finished compiler/backend/mips/proofs                            39s   1GB
Sep 10 10:44:17 Starting compiler/backend/riscv/proofs
Sep 10 10:44:58 Finished compiler/backend/riscv/proofs                           40s   2GB
Sep 10 10:44:58 Starting compiler/backend/ag32/proofs
Sep 10 11:01:57 Finished compiler/backend/ag32/proofs                         16m58s   3GB
Sep 10 11:01:57 Starting compiler/backend/cv_compute
Sep 10 11:03:23 Finished compiler/backend/cv_compute                           1m26s   2GB
Sep 10 11:03:23 Starting cv_translator
Sep 10 11:25:50 Finished cv_translator                                        22m26s   6GB
Sep 10 11:25:50 Starting candle/set-theory
Sep 10 11:26:39 Finished candle/set-theory                                       49s   1GB
Sep 10 11:26:39 Starting candle/syntax-lib
Sep 10 11:26:41 Finished candle/syntax-lib                                        1s  29MB
Sep 10 11:26:41 Starting candle/standard/syntax
Sep 10 11:26:54 Finished candle/standard/syntax                                  13s 864MB
Sep 10 11:26:54 Starting candle/standard/semantics
Sep 10 11:29:14 Finished candle/standard/semantics                             2m19s   2GB
Sep 10 11:29:14 Starting candle/standard/monadic
Sep 10 11:29:16 Finished candle/standard/monadic                                  1s  26MB
Sep 10 11:29:16 Starting candle/standard/ml_kernel
Sep 10 11:31:17 Finished candle/standard/ml_kernel                             2m00s   3GB
Sep 10 11:31:17 Starting candle/overloading/syntax
Sep 10 11:34:59 Finished candle/overloading/syntax                             3m41s   1GB
Sep 10 11:34:59 Starting candle/overloading/semantics
Sep 10 11:48:09 Finished candle/overloading/semantics                         13m09s   2GB
Sep 10 11:48:09 Starting candle/overloading/monadic
Sep 10 11:51:21 Finished candle/overloading/monadic                            3m11s   2GB
Sep 10 11:51:21 Starting candle/overloading/ml_kernel
Sep 10 12:00:26 Finished candle/overloading/ml_kernel                          9m05s   3GB
Sep 10 12:00:26 Starting candle/overloading/ml_checker
Sep 10 12:03:14 Finished candle/overloading/ml_checker                         2m47s   3GB
Sep 10 12:03:14 Starting candle/prover
Sep 10 12:14:27 Finished candle/prover                                        11m13s   4GB
Sep 10 12:14:27 Starting pancake
Sep 10 12:14:53 Finished pancake                                                 25s 761MB
Sep 10 12:14:53 Starting pancake/ffi
Sep 10 12:14:54 Finished pancake/ffi                                              0s  14MB
Sep 10 12:14:54 Starting pancake/semantics
Sep 10 12:17:34 Finished pancake/semantics                                     2m39s   1GB
Sep 10 12:17:34 Starting pancake/parser
Sep 10 12:18:00 Finished pancake/parser                                          26s 467MB
Sep 10 12:18:01 Starting pancake/proofs
Sep 10 12:36:03 Finished pancake/proofs                                       18m02s   5GB
Sep 10 12:36:03 Starting characteristic/examples
Sep 10 12:37:37 Finished characteristic/examples                               1m33s   2GB
Sep 10 12:37:37 Starting tutorial/solutions
Sep 10 12:40:33 Finished tutorial/solutions                                    2m55s   5GB
Sep 10 12:40:33 Starting translator/monadic/examples
Sep 10 12:44:36 Finished translator/monadic/examples                           4m03s   3GB
Sep 10 12:44:37 Starting examples
Sep 10 12:45:57 FAILED: examples
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)/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$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/src/rational[0m
Scanning [1m$(HOLDIR)/src/num/theories/cv_compute/automation[0m
Scanning [1m$(HOLDIR)/examples/bootstrap[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)/examples/machine-code/hoare-triple[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)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/basis[0m
Scanned 34 directories
Starting work on source_valuesTheory
Starting work on regexp_parserTheory
Starting work on README.md
Starting work on quicksortProgTheory
README.md                                                                                         examples  (0s)     OK
Starting work on catProgTheory
source_valuesTheory                                                                     examples/bootstrap  (2s)     OK
Starting work on source_syntaxTheory
source_syntaxTheory                                                                     examples/bootstrap  (1s)     OK
Starting work on parsingTheory
regexp_parserTheory                                                      examples/formal-languages/regular (16s)     OK
Starting work on printingTheory
printingTheory                                                                          examples/bootstrap  (6s)     OK
Finished $(HOLDIR)/examples/formal-languages/regular [#theories: 1]                                           (16.179s) 
Starting work on lcsTheory
parsingTheory                                                                           examples/bootstrap (25s)     OK
Finished $(HOLDIR)/examples/bootstrap [#theories: 4]                                                          (35.052s) 
Starting work on divTheory
lcsTheory                                                                                         examples (18s)     OK
Starting work on diffTheory
catProgTheory                                                                                     examples (69s)     OK
Starting work on doubleArgProgTheory
diffTheory                                                                                        examples (32s)FAIL<1>
   sl. IS_SUFFIX l sl  P sl
 
 failed.
 error in quse /home/cug/hk324/cml-regression/cakeml-2597/examples/diffScript.sml : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
 error in load /home/cug/hk324/cml-regression/cakeml-2597/examples/diffScript : HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
 First unsolved sub-goal is
 
 P (h'::t)
 
 Uncaught exception: HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"}
quicksortProgTheory                                                                               examples (76s)MKILLED
divTheory                                                                                         examples (45s)MKILLED
doubleArgProgTheory                                                                               examples  (5s)MKILLED