Job 3422

CakeML:d4ce405e105cef3b7901d0f89694c41597bb8b22
  Merge pull request #1431 from CakeML/pb_str_to_core [Jul 04 16:05:56]
HOL:1d9f33ad168d3823cc070223d83ea660d86dcb58
  Invert ParoundPrec, and use it to bracket stacked suffixes [Jun 24 01:00:44]
Machine:pavlova

Jul 04 16:20:07 Claimed job
Jul 04 16:20:11 Reusing HOL
Jul 04 16:21:06 Starting developers
Jul 04 16:21:11 Finished developers                                               4s 159MB
Jul 04 16:21:12 Starting developers/bin
Jul 04 16:21:15 Finished developers/bin                                           2s  93MB
Jul 04 16:21:16 Starting misc
Jul 04 16:21:59 Finished misc                                                    42s   1GB
Jul 04 16:22:00 Starting compiler/proofs
Jul 04 17:33:04 Finished compiler/proofs                                    1h11m02s  11GB
Jul 04 17:33:04 Starting compiler/bootstrap/compilation/x64/64/proofs
Jul 05 00:16:19 Finished compiler/bootstrap/compilation/x64/64/proofs       6h43m13s  85GB
Jul 05 00:16:20 Starting semantics/ffi
Jul 05 00:16:32 Finished semantics/ffi                                           11s 538MB
Jul 05 00:16:32 Starting semantics
Jul 05 00:16:34 Finished semantics                                                0s  87MB
Jul 05 00:16:35 Starting semantics/proofs
Jul 05 00:16:59 Finished semantics/proofs                                        22s 722MB
Jul 05 00:16:59 Starting semantics/alt_semantics
Jul 05 00:17:16 Finished semantics/alt_semantics                                 15s 574MB
Jul 05 00:17:17 Starting semantics/alt_semantics/proofs
Jul 05 00:21:04 Finished semantics/alt_semantics/proofs                        3m46s   1GB
Jul 05 00:21:05 Starting basis/pure
Jul 05 00:21:06 Finished basis/pure                                               0s  79MB
Jul 05 00:21:07 Starting translator
Jul 05 00:22:16 Finished translator                                            1m07s   2GB
Jul 05 00:22:16 Starting compiler/parsing
Jul 05 00:23:02 Finished compiler/parsing                                        45s   2GB
Jul 05 00:23:03 Starting characteristic
Jul 05 00:23:05 Finished characteristic                                           1s 118MB
Jul 05 00:23:06 Starting translator/monadic
Jul 05 00:23:08 Finished translator/monadic                                       0s 112MB
Jul 05 00:23:09 Starting translator/monadic/monad_base
Jul 05 00:23:10 Finished translator/monadic/monad_base                            0s  86MB
Jul 05 00:23:11 Starting profiler
Jul 05 00:23:40 Finished profiler                                                28s   1GB
Jul 05 00:23:41 Starting basis
Jul 05 00:25:25 Finished basis                                                 1m42s   4GB
Jul 05 00:25:25 Starting compiler
Jul 05 00:25:28 Finished compiler                                                 1s 228MB
Jul 05 00:25:29 Starting compiler/inference
Jul 05 00:25:31 Finished compiler/inference                                       0s 117MB
Jul 05 00:25:31 Starting compiler/backend/reg_alloc
Jul 05 00:25:33 Finished compiler/backend/reg_alloc                               0s  86MB
Jul 05 00:25:34 Starting compiler/backend/gc
Jul 05 00:25:36 Finished compiler/backend/gc                                      1s 134MB
Jul 05 00:25:37 Starting compiler/backend
Jul 05 00:25:39 Finished compiler/backend                                         1s 133MB
Jul 05 00:25:39 Starting compiler/encoders/asm
Jul 05 00:25:41 Finished compiler/encoders/asm                                    0s 100MB
Jul 05 00:25:42 Starting compiler/encoders/x64
Jul 05 00:25:44 Finished compiler/encoders/x64                                    0s 103MB
Jul 05 00:25:44 Starting compiler/encoders/arm7
Jul 05 00:25:46 Finished compiler/encoders/arm7                                   0s 106MB
Jul 05 00:25:47 Starting compiler/encoders/arm8
Jul 05 00:25:49 Finished compiler/encoders/arm8                                   0s  95MB
Jul 05 00:25:49 Starting compiler/encoders/arm8_asl
Jul 05 00:26:07 Finished compiler/encoders/arm8_asl                              16s   1GB
Jul 05 00:26:08 Starting compiler/encoders/mips
Jul 05 00:26:10 Finished compiler/encoders/mips                                   0s  99MB
Jul 05 00:26:10 Starting compiler/encoders/riscv
Jul 05 00:26:12 Finished compiler/encoders/riscv                                  0s  99MB
Jul 05 00:26:13 Starting compiler/encoders/ag32
Jul 05 00:26:15 Finished compiler/encoders/ag32                                   0s 101MB
Jul 05 00:26:16 Starting compiler/encoders/tests
Jul 05 00:26:17 Finished compiler/encoders/tests                                  1s 126MB
Jul 05 00:26:18 Starting compiler/encoders/monadic_enc
Jul 05 00:26:41 Finished compiler/encoders/monadic_enc                           21s   1GB
Jul 05 00:26:41 Starting compiler/backend/x64
Jul 05 00:26:43 Finished compiler/backend/x64                                     1s 133MB
Jul 05 00:26:44 Starting compiler/backend/arm7
Jul 05 00:26:46 Finished compiler/backend/arm7                                    1s 132MB
Jul 05 00:26:47 Starting compiler/backend/arm8
Jul 05 00:26:49 Finished compiler/backend/arm8                                    1s 133MB
Jul 05 00:26:50 Starting compiler/backend/mips
Jul 05 00:26:52 Finished compiler/backend/mips                                    1s 133MB
Jul 05 00:26:52 Starting compiler/backend/riscv
Jul 05 00:26:54 Finished compiler/backend/riscv                                   1s 134MB
Jul 05 00:26:55 Starting compiler/backend/ag32
Jul 05 00:27:57 Finished compiler/backend/ag32                                 1m00s   1GB
Jul 05 00:27:58 Starting compiler/backend/pattern_matching
Jul 05 00:27:59 Finished compiler/backend/pattern_matching                        0s  91MB
Jul 05 00:28:00 Starting compiler/parsing/ocaml
Jul 05 00:30:08 Finished compiler/parsing/ocaml                                2m07s   1GB
Jul 05 00:30:09 Starting compiler/printing
Jul 05 00:31:05 Finished compiler/printing                                       55s   1GB
Jul 05 00:31:06 Starting compiler/parsing/proofs
Jul 05 00:31:08 Finished compiler/parsing/proofs                                  0s  98MB
Jul 05 00:31:09 Starting compiler/inference/proofs
Jul 05 00:31:11 Finished compiler/inference/proofs                                0s 114MB
Jul 05 00:31:12 Starting compiler/backend/semantics
Jul 05 00:34:17 Finished compiler/backend/semantics                            3m04s   3GB
Jul 05 00:34:17 Starting compiler/backend/reg_alloc/proofs
Jul 05 00:34:19 Finished compiler/backend/reg_alloc/proofs                        1s 116MB
Jul 05 00:34:20 Starting compiler/backend/proofs
Jul 05 00:35:03 Finished compiler/backend/proofs                                 41s   1GB
Jul 05 00:35:04 Starting compiler/backend/serialiser
Jul 05 00:35:06 Finished compiler/backend/serialiser                              1s 144MB
Jul 05 00:35:07 Starting compiler/encoders/x64/proofs
Jul 05 00:35:09 Finished compiler/encoders/x64/proofs                             0s 108MB
Jul 05 00:35:09 Starting compiler/encoders/arm7/proofs
Jul 05 00:47:30 Finished compiler/encoders/arm7/proofs                        12m20s   5GB
Jul 05 00:47:31 Starting compiler/encoders/arm8/proofs
Jul 05 00:55:25 Finished compiler/encoders/arm8/proofs                         7m52s   3GB
Jul 05 00:55:25 Starting compiler/encoders/arm8_asl/proofs
Jul 05 01:12:48 Finished compiler/encoders/arm8_asl/proofs                    17m21s   3GB
Jul 05 01:12:49 Starting compiler/encoders/mips/proofs
Jul 05 01:23:36 Finished compiler/encoders/mips/proofs                        10m44s   8GB
Jul 05 01:23:36 Starting compiler/encoders/riscv/proofs
Jul 05 01:33:04 Finished compiler/encoders/riscv/proofs                        9m26s   4GB
Jul 05 01:33:05 Starting compiler/encoders/ag32/proofs
Jul 05 01:36:12 Finished compiler/encoders/ag32/proofs                         3m06s   1GB
Jul 05 01:36:12 Starting compiler/backend/x64/proofs
Jul 05 01:36:15 Finished compiler/backend/x64/proofs                              1s 216MB
Jul 05 01:36:16 Starting compiler/backend/arm7/proofs
Jul 05 01:36:53 Finished compiler/backend/arm7/proofs                            36s   2GB
Jul 05 01:36:54 Starting compiler/backend/arm8/proofs
Jul 05 01:37:33 Finished compiler/backend/arm8/proofs                            37s   2GB
Jul 05 01:37:33 Starting compiler/backend/arm8_asl
Jul 05 01:37:58 Finished compiler/backend/arm8_asl                               24s   1GB
Jul 05 01:37:59 Starting compiler/backend/mips/proofs
Jul 05 01:38:41 Finished compiler/backend/mips/proofs                            41s   2GB
Jul 05 01:38:42 Starting compiler/backend/riscv/proofs
Jul 05 01:39:23 Finished compiler/backend/riscv/proofs                           39s   2GB
Jul 05 01:39:24 Starting compiler/backend/ag32/proofs
Jul 05 01:48:55 Finished compiler/backend/ag32/proofs                          9m30s   5GB
Jul 05 01:48:56 Starting compiler/backend/cv_compute
Jul 05 01:49:26 Finished compiler/backend/cv_compute                             29s   1GB
Jul 05 01:49:27 Starting cv_translator
Jul 05 01:54:23 Finished cv_translator                                         4m55s   3GB
Jul 05 01:54:24 Starting candle
Jul 05 01:54:25 Finished candle                                                   0s   7MB
Jul 05 01:54:26 Starting candle/set-theory
Jul 05 01:54:57 Finished candle/set-theory                                       30s 937MB
Jul 05 01:54:57 Starting candle/syntax-lib
Jul 05 01:54:59 Finished candle/syntax-lib                                        0s  78MB
Jul 05 01:55:00 Starting candle/standard
Jul 05 01:55:01 Finished candle/standard                                          0s   7MB
Jul 05 01:55:01 Starting candle/standard/syntax
Jul 05 01:55:16 Finished candle/standard/syntax                                  14s 811MB
Jul 05 01:55:17 Starting candle/standard/syntax/little_theories
Jul 05 01:56:29 Finished candle/standard/syntax/little_theories                1m11s 985MB
Jul 05 01:56:30 Starting candle/standard/semantics
Jul 05 01:58:44 Finished candle/standard/semantics                             2m13s   1GB
Jul 05 01:58:45 Starting candle/standard/monadic
Jul 05 01:58:47 Finished candle/standard/monadic                                  0s 122MB
Jul 05 01:58:48 Starting candle/standard/ml_kernel
Jul 05 02:01:14 Finished candle/standard/ml_kernel                             2m25s   3GB
Jul 05 02:01:15 Starting candle/overloading
Jul 05 02:01:16 Finished candle/overloading                                       0s   6MB
Jul 05 02:01:17 Starting candle/overloading/syntax
Jul 05 02:04:26 Finished candle/overloading/syntax                             3m08s   2GB
Jul 05 02:04:27 Starting candle/overloading/semantics
Jul 05 02:14:05 Finished candle/overloading/semantics                          9m37s   4GB
Jul 05 02:14:06 Starting candle/overloading/monadic
Jul 05 02:16:09 Finished candle/overloading/monadic                            2m02s   1GB
Jul 05 02:16:10 Starting candle/overloading/ml_kernel
Jul 05 02:22:52 Finished candle/overloading/ml_kernel                          6m41s   6GB
Jul 05 02:22:53 Starting candle/overloading/ml_checker
Jul 05 02:25:36 Finished candle/overloading/ml_checker                         2m42s   6GB
Jul 05 02:25:37 Starting candle/prover
Jul 05 02:25:39 Finished candle/prover                                            1s 183MB
Jul 05 02:25:40 Starting candle/prover/compute
Jul 05 02:25:42 Finished candle/prover/compute                                    1s 157MB
Jul 05 02:25:43 Starting pancake
Jul 05 02:25:45 Finished pancake                                                  1s 148MB
Jul 05 02:25:46 Starting pancake/semantics
Jul 05 02:28:41 Finished pancake/semantics                                     2m54s   2GB
Jul 05 02:28:42 Starting pancake/parser
Jul 05 02:29:24 Finished pancake/parser                                          41s 487MB
Jul 05 02:29:25 Starting pancake/static_checker
Jul 05 02:31:58 Finished pancake/static_checker                                2m33s   1GB
Jul 05 02:31:59 Starting pancake/proofs
Jul 05 02:49:22 Finished pancake/proofs                                       17m22s   4GB
Jul 05 02:49:23 Starting compiler/dafny
Jul 05 02:49:46 Finished compiler/dafny                                          22s 664MB
Jul 05 02:49:47 Starting compiler/dafny/translation
Jul 05 03:00:51 Finished compiler/dafny/translation                           11m02s   7GB
Jul 05 03:00:52 Starting compiler/dafny/compilation
Jul 05 03:02:39 Finished compiler/dafny/compilation                            1m46s   6GB
Jul 05 03:02:40 Starting compiler/dafny/semantics
Jul 05 03:03:19 Finished compiler/dafny/semantics                                37s 492MB
Jul 05 03:03:20 Starting compiler/dafny/proofs
Jul 05 03:04:59 Finished compiler/dafny/proofs                                 1m37s   1GB
Jul 05 03:04:59 Starting compiler/dafny/vcg
Jul 05 03:05:01 Finished compiler/dafny/vcg                                       0s  98MB
Jul 05 03:05:02 Starting compiler/dafny/vcg/examples
Jul 05 03:05:31 Finished compiler/dafny/vcg/examples                             28s   1GB
Jul 05 03:05:32 Starting compiler/scheme
Jul 05 03:05:58 Finished compiler/scheme                                         25s   1GB
Jul 05 03:05:59 Starting compiler/scheme/translation
Jul 05 03:12:42 Finished compiler/scheme/translation                           6m42s   7GB
Jul 05 03:12:43 Starting compiler/scheme/compilation
Jul 05 03:14:08 Finished compiler/scheme/compilation                           1m23s   4GB
Jul 05 03:14:09 Starting compiler/scheme/proofs
Jul 05 03:20:59 Finished compiler/scheme/proofs                                6m49s   2GB
Jul 05 03:21:00 Starting characteristic/examples
Jul 05 03:22:32 Finished characteristic/examples                               1m30s   5GB
Jul 05 03:22:32 Starting tutorial/solutions
Jul 05 03:25:15 Finished tutorial/solutions                                    2m42s   3GB
Jul 05 03:25:16 Starting translator/monadic/examples
Jul 05 03:28:19 Finished translator/monadic/examples                           3m02s   4GB
Jul 05 03:28:20 Starting examples
Jul 05 03:30:45 FAILED: examples
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/examples/Crypto/AES
Scanning $(HOLDIR)/src/TeX
Scanning $(HOLDIR)/src/bag
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
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/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/pl-semantics/lprefix_lub
Scanning $(HOLDIR)/examples/bootstrap
Scanning $(HOLDIR)/examples/data-structures/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)/basis/pure
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(HOLDIR)/examples/algorithms/unification/triangular
Scanning $(HOLDIR)/src/transfer/examples
Scanning $(HOLDIR)/examples/algorithms/unification/triangular/first-order
Scanning $(HOLDIR)/examples/algorithms/unification/triangular/first-order/compilation
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/compiler/inference
Scanning $(CAKEMLDIR)/compiler/printing
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/basis
Scanned 66 directories
Building 22 theory files
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)  [1/22]     OK
Starting work on diffTheory
diffTheory                                                 (32s)  [2/22]     OK
Starting work on diffProgTheory
quicksortProgTheory                                        (48s)  [3/22]     OK
Starting work on array_searchProgTheory
catProgTheory                                              (47s)  [4/22]     OK
Starting work on doubleArgProgTheory
divTheory                                                  (57s)  [5/22]     OK
Starting work on echoProgTheory
doubleArgProgTheory                                        (30s)  [6/22]     OK
Starting work on filterProgTheory
array_searchProgTheory                                     (41s)  [7/22]     OK
Starting work on grepProgTheory
echoProgTheory                                             (38s)  [8/22]     OK
Starting work on helloErrProgTheory
diffProgTheory                                             (54s)  [9/22]     OK
Starting work on helloProgTheory
filterProgTheory                                           (51s)        FAIL<1>
grepProgTheory                                             (41s)         killed
helloErrProgTheory                                         (32s)         killed
helloProgTheory                                            (34s)         killed
*** Holmake aborted - 1 target failed:
*** filterProgTheory (status 1)
                     DROP (LENGTH (... ... )) (nth_arr i input))))))) bv
 Saved theorem _______ "forward_matching_lines_div_spec"
 Saved theorem _______ "LTAKE_LLENGTH_SOME2"
 Using translator specification word8_fromint_v_thm from theory Word8Prog
 Post condition: POSTv v. seL4_IO input [] * W8ARRAY dummyarr_loc [] * &WORD8 0w v
 Using CF specification w8array_alloc_spec from theory Word8ArrayProof
 Post condition: POSTv v'.
   W8ARRAY v' (REPLICATE 256 0w) * seL4_IO input [] * W8ARRAY dummyarr_loc []
 Using CF specification w8array_substring_spec from theory Word8ArrayProof
 Post condition: POSTv sv.
   W8ARRAY v' (TAKE 256 h ++ DROP (LENGTH h) init) * W8ARRAY dummyarr_loc [] *
   seL4_IO (fromList l)
     (SNOC (IO_event (ExtCall accept_call) [] (ZIP (init,newinit))) events) *
   &STRING_TYPE
     (implode
        (MAP (CHR  w2n) (TAKE 256 (TAKE 256 h ++ DROP (LENGTH h) init)))) sv
 Using translator specification cut_at_null_v_thm from theory filterProg
 Post condition: POSTv sv1.
   W8ARRAY v' (TAKE 256 h ++ DROP (LENGTH h) init) * W8ARRAY dummyarr_loc [] *
   seL4_IO (fromList l)
     (SNOC (IO_event (ExtCall accept_call) [] (ZIP (init,newinit))) events) *
   &STRING_TYPE
     (cut_at_null
        (implode
           (MAP (CHR  w2n) (TAKE 256 (TAKE 256 h ++ DROP (LENGTH h) init)))))
     sv1
 Using translator specification match_string_v_thm from theory filterProg
 Post condition: POSTv bv.
   W8ARRAY v' (TAKE 256 h ++ DROP (LENGTH h) init) * W8ARRAY dummyarr_loc [] *
   seL4_IO (fromList l)
     (SNOC (IO_event (ExtCall accept_call) [] (ZIP (init,newinit))) events) *
   &BOOL
     (match_string
        (cut_at_null
           (implode
              (MAP (CHR  w2n) (TAKE 256 (TAKE 256 h ++ DROP (LENGTH h) init))))))
     bv
 Using a CF specification from the assumptions
 Saved theorem _______ "forward_matching_lines_ffidiv_spec"
 Saved definition ____ "seL4_proj1_def"
 Saved definition ____ "seL4_proj2"
 Saved definition ____ "filter_ffi_state_def"
 Saved theorem _______ "limited_parts_proj"
 Saved theorem _______ "parts_ok_filter"
 Saved theorem _______ "forward_matching_lines_semantics"
 Saved theorem _______ "forward_matching_lines_ffidiv_semantics"
 Saved theorem _______ "semantics_diverge_filter"
 Saved theorem _______ "semantics_finite_filter"
 Exporting theory "filterProg" ... done.
 Theory "filterProg" took 44.9s to build
 Full log: /scratch/cakeml/regression/cakeml-3422/examples/.hol/logs/filterProgTheory