Job 2978

CakeML:4809f91a58f68e48a5f258d1b282dae03efca687
  Ban TheoryPP.include_docs [Sep 20 12:57:16]
#1240 (use-no_sig_docs)
Merging into:44490100e4a5734a0542a63b3062e0f74b3651c9
  Merge pull request #1238 from CakeML/dafny-vcg-heap [Sep 16 07:30:14]
HOL:8217cc7588905bc0246e2dc8211ed4ce501245e8
  Remove binary_ieee's reservation of "sign" name [Sep 18 02:17:02]
Machine:pavlova

Sep 20 13:54:23 Claimed job
Sep 20 13:54:27 Reusing HOL
Sep 20 13:54:34 Starting developers
Sep 20 13:54:38 Finished developers                                               3s 202MB
Sep 20 13:54:39 Starting developers/bin
Sep 20 13:54:43 Finished developers/bin                                           3s  89MB
Sep 20 13:54:44 Starting misc
Sep 20 13:55:22 Finished misc                                                    37s   1GB
Sep 20 13:55:23 Starting compiler/proofs
Sep 20 15:06:32 Finished compiler/proofs                                    1h11m08s  43GB
Sep 20 15:06:33 Starting compiler/bootstrap/compilation/x64/64/proofs
Sep 20 21:17:15 Finished compiler/bootstrap/compilation/x64/64/proofs       6h10m39s  94GB
Sep 20 21:17:15 Starting semantics/ffi
Sep 20 21:17:25 Finished semantics/ffi                                            8s 517MB
Sep 20 21:17:25 Starting semantics
Sep 20 21:17:27 Finished semantics                                                0s  61MB
Sep 20 21:17:28 Starting semantics/proofs
Sep 20 21:17:50 Finished semantics/proofs                                        21s 734MB
Sep 20 21:17:51 Starting semantics/alt_semantics
Sep 20 21:18:07 Finished semantics/alt_semantics                                 15s 718MB
Sep 20 21:18:08 Starting semantics/alt_semantics/proofs
Sep 20 21:21:16 Finished semantics/alt_semantics/proofs                        3m07s   2GB
Sep 20 21:21:17 Starting basis/pure
Sep 20 21:21:19 Finished basis/pure                                               0s 103MB
Sep 20 21:21:19 Starting translator
Sep 20 21:22:43 Finished translator                                            1m22s   3GB
Sep 20 21:22:44 Starting compiler/parsing
Sep 20 21:22:45 Finished compiler/parsing                                         0s  62MB
Sep 20 21:22:46 Starting characteristic
Sep 20 21:22:48 Finished characteristic                                           1s 117MB
Sep 20 21:22:49 Starting translator/monadic
Sep 20 21:22:51 Finished translator/monadic                                       1s 122MB
Sep 20 21:22:52 Starting translator/monadic/monad_base
Sep 20 21:22:53 Finished translator/monadic/monad_base                            0s  61MB
Sep 20 21:22:54 Starting basis
Sep 20 21:25:05 Finished basis                                                 2m10s   5GB
Sep 20 21:25:06 Starting compiler
Sep 20 21:25:09 Finished compiler                                                 2s 213MB
Sep 20 21:25:10 Starting compiler/inference
Sep 20 21:25:12 Finished compiler/inference                                       1s 122MB
Sep 20 21:25:12 Starting compiler/backend/reg_alloc
Sep 20 21:25:14 Finished compiler/backend/reg_alloc                               0s 100MB
Sep 20 21:25:15 Starting compiler/backend/gc
Sep 20 21:25:17 Finished compiler/backend/gc                                      1s 140MB
Sep 20 21:25:18 Starting compiler/backend
Sep 20 21:25:23 Finished compiler/backend                                         4s 256MB
Sep 20 21:25:24 Starting compiler/encoders/asm
Sep 20 21:25:26 Finished compiler/encoders/asm                                    0s  91MB
Sep 20 21:25:27 Starting compiler/encoders/x64
Sep 20 21:25:28 Finished compiler/encoders/x64                                    0s  92MB
Sep 20 21:25:29 Starting compiler/encoders/arm7
Sep 20 21:25:31 Finished compiler/encoders/arm7                                   0s  92MB
Sep 20 21:25:32 Starting compiler/encoders/arm8
Sep 20 21:25:33 Finished compiler/encoders/arm8                                   0s  97MB
Sep 20 21:25:34 Starting compiler/encoders/arm8_asl
Sep 20 21:25:47 Finished compiler/encoders/arm8_asl                              12s   1GB
Sep 20 21:25:48 Starting compiler/encoders/mips
Sep 20 21:25:50 Finished compiler/encoders/mips                                   0s  95MB
Sep 20 21:25:50 Starting compiler/encoders/riscv
Sep 20 21:25:52 Finished compiler/encoders/riscv                                  0s  99MB
Sep 20 21:25:53 Starting compiler/encoders/ag32
Sep 20 21:25:55 Finished compiler/encoders/ag32                                   0s  91MB
Sep 20 21:25:55 Starting compiler/encoders/tests
Sep 20 21:25:57 Finished compiler/encoders/tests                                  0s 108MB
Sep 20 21:25:58 Starting compiler/encoders/monadic_enc
Sep 20 21:26:17 Finished compiler/encoders/monadic_enc                           18s   1GB
Sep 20 21:26:18 Starting compiler/backend/x64
Sep 20 21:26:20 Finished compiler/backend/x64                                     1s 152MB
Sep 20 21:26:21 Starting compiler/backend/arm7
Sep 20 21:26:24 Finished compiler/backend/arm7                                    1s 152MB
Sep 20 21:26:24 Starting compiler/backend/arm8
Sep 20 21:26:27 Finished compiler/backend/arm8                                    1s 152MB
Sep 20 21:26:27 Starting compiler/backend/mips
Sep 20 21:26:30 Finished compiler/backend/mips                                    1s 152MB
Sep 20 21:26:30 Starting compiler/backend/riscv
Sep 20 21:26:33 Finished compiler/backend/riscv                                   1s 151MB
Sep 20 21:26:34 Starting compiler/backend/ag32
Sep 20 21:27:37 Finished compiler/backend/ag32                                 1m02s   2GB
Sep 20 21:27:37 Starting compiler/backend/pattern_matching
Sep 20 21:27:39 Finished compiler/backend/pattern_matching                        0s  63MB
Sep 20 21:27:40 Starting compiler/parsing/ocaml
Sep 20 21:29:22 Finished compiler/parsing/ocaml                                1m41s   1GB
Sep 20 21:29:23 Starting compiler/printing
Sep 20 21:29:25 Finished compiler/printing                                        1s 122MB
Sep 20 21:29:26 Starting compiler/parsing/proofs
Sep 20 21:29:27 Finished compiler/parsing/proofs                                  0s  67MB
Sep 20 21:29:28 Starting compiler/inference/proofs
Sep 20 21:29:30 Finished compiler/inference/proofs                                1s 127MB
Sep 20 21:29:31 Starting compiler/backend/semantics
Sep 20 21:32:19 Finished compiler/backend/semantics                            2m47s   2GB
Sep 20 21:32:20 Starting compiler/backend/reg_alloc/proofs
Sep 20 21:32:22 Finished compiler/backend/reg_alloc/proofs                        1s 133MB
Sep 20 21:32:23 Starting compiler/backend/proofs
Sep 20 21:33:09 Finished compiler/backend/proofs                                 45s   3GB
Sep 20 21:33:10 Starting compiler/backend/serialiser
Sep 20 21:33:12 Finished compiler/backend/serialiser                              1s 153MB
Sep 20 21:33:13 Starting compiler/encoders/x64/proofs
Sep 20 21:33:14 Finished compiler/encoders/x64/proofs                             0s  99MB
Sep 20 21:33:15 Starting compiler/encoders/arm7/proofs
Sep 20 21:45:13 Finished compiler/encoders/arm7/proofs                        11m57s   7GB
Sep 20 21:45:14 Starting compiler/encoders/arm8/proofs
Sep 20 21:52:16 Finished compiler/encoders/arm8/proofs                         7m00s   3GB
Sep 20 21:52:16 Starting compiler/encoders/arm8_asl/proofs
Sep 20 22:08:32 Finished compiler/encoders/arm8_asl/proofs                    16m14s   4GB
Sep 20 22:08:33 Starting compiler/encoders/mips/proofs
Sep 20 22:18:22 Finished compiler/encoders/mips/proofs                         9m48s   7GB
Sep 20 22:18:23 Starting compiler/encoders/riscv/proofs
Sep 20 22:26:37 Finished compiler/encoders/riscv/proofs                        8m12s   6GB
Sep 20 22:26:37 Starting compiler/encoders/ag32/proofs
Sep 20 22:29:27 Finished compiler/encoders/ag32/proofs                         2m48s   1GB
Sep 20 22:29:28 Starting compiler/backend/x64/proofs
Sep 20 22:29:31 Finished compiler/backend/x64/proofs                              2s 221MB
Sep 20 22:29:32 Starting compiler/backend/arm7/proofs
Sep 20 22:30:06 Finished compiler/backend/arm7/proofs                            32s   2GB
Sep 20 22:30:07 Starting compiler/backend/arm8/proofs
Sep 20 22:30:41 Finished compiler/backend/arm8/proofs                            33s   2GB
Sep 20 22:30:42 Starting compiler/backend/arm8_asl
Sep 20 22:31:04 Finished compiler/backend/arm8_asl                               21s   2GB
Sep 20 22:31:05 Starting compiler/backend/mips/proofs
Sep 20 22:31:38 Finished compiler/backend/mips/proofs                            32s   2GB
Sep 20 22:31:39 Starting compiler/backend/riscv/proofs
Sep 20 22:32:14 Finished compiler/backend/riscv/proofs                           34s   2GB
Sep 20 22:32:15 Starting compiler/backend/ag32/proofs
Sep 20 22:44:16 Finished compiler/backend/ag32/proofs                         12m00s   6GB
Sep 20 22:44:17 Starting compiler/backend/cv_compute
Sep 20 22:44:42 Finished compiler/backend/cv_compute                             23s   1GB
Sep 20 22:44:42 Starting cv_translator
Sep 20 22:49:43 Finished cv_translator                                         4m59s   4GB
Sep 20 22:49:44 Starting candle
Sep 20 22:49:45 Finished candle                                                   0s  13MB
Sep 20 22:49:45 Starting candle/set-theory
Sep 20 22:50:11 Finished candle/set-theory                                       24s 920MB
Sep 20 22:50:11 Starting candle/syntax-lib
Sep 20 22:50:13 Finished candle/syntax-lib                                        0s 104MB
Sep 20 22:50:14 Starting candle/standard
Sep 20 22:50:15 Finished candle/standard                                          0s  16MB
Sep 20 22:50:16 Starting candle/standard/syntax
Sep 20 22:50:28 Finished candle/standard/syntax                                  11s 764MB
Sep 20 22:50:29 Starting candle/standard/semantics
Sep 20 22:52:27 Finished candle/standard/semantics                             1m57s   2GB
Sep 20 22:52:28 Starting candle/standard/monadic
Sep 20 22:52:30 Finished candle/standard/monadic                                  1s 135MB
Sep 20 22:52:31 Starting candle/standard/ml_kernel
Sep 20 22:54:11 Finished candle/standard/ml_kernel                             1m39s   4GB
Sep 20 22:54:12 Starting candle/standard/ml_kernel/lisp
Sep 20 22:54:14 Finished candle/standard/ml_kernel/lisp                           0s  56MB
Sep 20 22:54:14 Starting candle/overloading
Sep 20 22:54:15 Finished candle/overloading                                       0s  15MB
Sep 20 22:54:16 Starting candle/overloading/syntax
Sep 20 22:57:17 Finished candle/overloading/syntax                             3m00s   2GB
Sep 20 22:57:18 Starting candle/overloading/semantics
Sep 20 23:08:18 Finished candle/overloading/semantics                         10m58s   6GB
Sep 20 23:08:19 Starting candle/overloading/monadic
Sep 20 23:10:31 Finished candle/overloading/monadic                            2m11s   1GB
Sep 20 23:10:32 Starting candle/overloading/ml_kernel
Sep 20 23:17:14 Finished candle/overloading/ml_kernel                          6m41s   6GB
Sep 20 23:17:15 Starting candle/overloading/ml_checker
Sep 20 23:19:27 Finished candle/overloading/ml_checker                         2m09s   6GB
Sep 20 23:19:27 Starting candle/prover
Sep 20 23:19:30 Finished candle/prover                                            1s 165MB
Sep 20 23:19:31 Starting candle/prover/compute
Sep 20 23:19:33 Finished candle/prover/compute                                    1s 157MB
Sep 20 23:19:34 Starting pancake
Sep 20 23:19:36 Finished pancake                                                  1s 154MB
Sep 20 23:19:37 Starting pancake/semantics
Sep 20 23:22:18 Finished pancake/semantics                                     2m40s   1GB
Sep 20 23:22:19 Starting pancake/parser
Sep 20 23:22:48 Finished pancake/parser                                          28s 465MB
Sep 20 23:22:49 Starting pancake/static_checker
Sep 20 23:23:52 Finished pancake/static_checker                                1m02s   1GB
Sep 20 23:23:53 Starting pancake/proofs
Sep 20 23:39:19 Finished pancake/proofs                                       15m23s   4GB
Sep 20 23:39:19 Starting compiler/dafny
Sep 20 23:39:44 Finished compiler/dafny                                          23s 754MB
Sep 20 23:39:45 Starting compiler/dafny/translation
Sep 20 23:48:37 Finished compiler/dafny/translation                            8m51s   5GB
Sep 20 23:48:38 Starting compiler/dafny/compilation
Sep 20 23:50:15 Finished compiler/dafny/compilation                            1m36s   5GB
Sep 20 23:50:16 Starting compiler/dafny/semantics
Sep 20 23:50:48 Finished compiler/dafny/semantics                                31s 568MB
Sep 20 23:50:49 Starting compiler/dafny/proofs
Sep 20 23:52:14 Finished compiler/dafny/proofs                                 1m24s   1GB
Sep 20 23:52:15 Starting compiler/dafny/vcg
Sep 20 23:53:27 Finished compiler/dafny/vcg                                    1m10s   1GB
Sep 20 23:53:27 Starting compiler/scheme
Sep 20 23:53:53 Finished compiler/scheme                                         25s   1GB
Sep 20 23:53:54 Starting compiler/scheme/translation
Sep 21 00:00:44 Finished compiler/scheme/translation                           6m49s   8GB
Sep 21 00:00:45 Starting compiler/scheme/compilation
Sep 21 00:01:55 Finished compiler/scheme/compilation                           1m09s   4GB
Sep 21 00:01:56 Starting compiler/scheme/proofs
Sep 21 00:18:20 Finished compiler/scheme/proofs                               16m22s  51GB
Sep 21 00:18:20 Starting characteristic/examples
Sep 21 00:19:42 Finished characteristic/examples                               1m20s   4GB
Sep 21 00:19:43 Starting tutorial/solutions
Sep 21 00:21:59 Finished tutorial/solutions                                    2m14s   3GB
Sep 21 00:21:59 Starting translator/monadic/examples
Sep 21 00:24:46 Finished translator/monadic/examples                           2m45s   3GB
Sep 21 00:24:47 Starting examples
Sep 21 00:25:03 FAILED: examples
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/examples/Crypto/AES
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/bag
Scanning $(HOLDIR)/src/TeX
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/src/integer
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/real/analysis
Scanning $(HOLDIR)/src/probability
Scanning $(HOLDIR)/examples/Crypto/DES
Scanning $(HOLDIR)/examples/Crypto/IDEA
Scanning $(HOLDIR)/src/num/theories/cv_compute/automation
Scanning $(HOLDIR)/examples/Crypto/Keccak
Scanning $(HOLDIR)/examples/Crypto/MARS
Scanning $(HOLDIR)/examples/Crypto/MD5
Scanning $(HOLDIR)/examples/Crypto/RC6
Scanning $(HOLDIR)/examples/Crypto/MD
Scanning $(HOLDIR)/examples/Crypto/RIPEMD
Scanning $(HOLDIR)/examples/Crypto/SHA-1
Scanning $(HOLDIR)/examples/Crypto/SHA-2
Scanning $(HOLDIR)/examples/Crypto/Serpent/Bitslice
Scanning $(HOLDIR)/examples/Crypto/Serpent/Reference
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/src/monad/more_monads
Scanning $(HOLDIR)/src/emit
Scanning $(HOLDIR)/examples/Crypto/TEA
Scanning $(HOLDIR)/examples/Crypto/TWOFISH
Scanning $(HOLDIR)/examples/Crypto
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(HOLDIR)/examples/bootstrap
Scanning $(HOLDIR)/examples/misc
Scanning $(HOLDIR)/examples/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/src/search
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 60 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                                                           (6s)     OK
Starting work on diffTheory
diffTheory                                                          (5s)FAIL<1>
 <<HOL message: mk_functional: 
   pattern completion has added 1 clause to the original specification.>>
 <<HOL message: mk_functional: 
   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 ____ "parse_patch_header_def"
 Saved definition ____ "depatch_line_def"
 Saved definition ____ "depatch_lines_def"
 <<HOL message: mk_functional: 
   pattern completion has added 2 clauses to the original specification.>>
 Saved definition ____ "patch_aux_def"
 Saved induction _____ "patch_aux_ind"
 Saved definition ____ "patch_alg_def"
 Saved definition ____ "patch_alg_offs_def"
 Saved theorem _______ "tokens_append_strlit"
 Saved theorem _______ "tokens_append_right_strlit"
 Proved triviality ___ "one_to_ten"
 Proved triviality ___ "SPLITP_HEX"
 Proved triviality ___ "SPLITP_num_toString"
 Proved triviality ___ "SPLITP_int_toString"
 Proved triviality ___ "TOKENS_tostring"
 Proved triviality ___ "num_le_10"
 Proved triviality ___ "tokens_toString"
 Proved triviality ___ "tokens_strcat"
 Proved triviality ___ "tokens_strcat'"
 Proved triviality ___ "strsub_strcat"
 Proved triviality ___ "strsub_str"
 Proved triviality ___ "acd_simps"
 Proved triviality ___ "HEX_isDigit"
 Saved theorem _______ "toString_isDigit"
 Saved theorem _______ "int_abs_toString_num"
 Proved triviality ___ "substring_adhoc_simps"
 Proved triviality ___ "depatch_lines_strcat_cancel"
 Proved triviality ___ "depatch_lines_diff_add_prefix_cancel"
 Proved triviality ___ "patch_aux_nil"
 Proved triviality ___ "line_numbers_not_empty"
 Saved theorem _______ "tokens_eq_sing"
 Proof of 
 
 tokens ($= #",") (ml_num_toString n) = [ml_num_toString n]
 
 failed.
 Failed to prove theorem tokens_toString_comma.
 
 Exception raised at Q.EXISTS_TAC:
 goal not an exists
 error in quse /scratch/cakeml/regression/cakeml-2978/examples/diffScript.sml : HOL_ERR {message = "goal not an exists", origin_function = "EXISTS_TAC", origin_structure = "Q", source_location = Loc_Unknown}
 error in load /scratch/cakeml/regression/cakeml-2978/examples/diffScript : HOL_ERR {message = "goal not an exists", origin_function = "EXISTS_TAC", origin_structure = "Q", source_location = Loc_Unknown}
 Uncaught exception at /scratch/cakeml/regression/HOL-8217cc7588905bc0246e2dc8211ed4ce501245e8/src/prekernel/Feedback.sml:124: HOL_ERR {message = "goal not an exists", origin_function = "EXISTS_TAC", origin_structure = "Q", source_location = Loc_Unknown}
 Full log: /scratch/cakeml/regression/cakeml-2978/examples/.hol/logs/diffTheory
quicksortProgTheory                                                (12s)MKILLED
catProgTheory                                                      (12s)MKILLED
divTheory                                                          (12s)MKILLED