Job 3419

CakeML:1cd29d45aad69f59e4ac8fb164dedbd0dd862e6b
  Merge pull request #1430 from CakeML/better-concatWith [Jul 03 01:05:19]
HOL:1d9f33ad168d3823cc070223d83ea660d86dcb58
  Invert ParoundPrec, and use it to bracket stacked suffixes [Jun 24 01:00:44]
Machine:timtam

Jul 03 01:21:25 Claimed job
Jul 03 01:21:30 Reusing HOL
Jul 03 01:21:37 Starting developers
Jul 03 01:21:43 Finished developers                                               4s 205MB
Jul 03 01:21:44 Starting developers/bin
Jul 03 01:21:47 Finished developers/bin                                           2s  94MB
Jul 03 01:21:48 Starting misc
Jul 03 01:22:33 Finished misc                                                    44s   1GB
Jul 03 01:22:34 Starting compiler/proofs
Jul 03 02:33:13 Finished compiler/proofs                                    1h10m37s  11GB
Jul 03 02:33:13 Starting compiler/bootstrap/compilation/x64/64/proofs
Jul 03 09:15:36 Finished compiler/bootstrap/compilation/x64/64/proofs       6h42m21s  62GB
Jul 03 09:15:37 Starting semantics/ffi
Jul 03 09:15:49 Finished semantics/ffi                                           11s 538MB
Jul 03 09:15:50 Starting semantics
Jul 03 09:15:51 Finished semantics                                                0s  83MB
Jul 03 09:15:52 Starting semantics/proofs
Jul 03 09:16:16 Finished semantics/proofs                                        22s 721MB
Jul 03 09:16:17 Starting semantics/alt_semantics
Jul 03 09:16:34 Finished semantics/alt_semantics                                 16s 540MB
Jul 03 09:16:35 Starting semantics/alt_semantics/proofs
Jul 03 09:20:21 Finished semantics/alt_semantics/proofs                        3m44s   1GB
Jul 03 09:20:22 Starting basis/pure
Jul 03 09:20:23 Finished basis/pure                                               0s  85MB
Jul 03 09:20:24 Starting translator
Jul 03 09:21:33 Finished translator                                            1m08s   2GB
Jul 03 09:21:34 Starting compiler/parsing
Jul 03 09:22:20 Finished compiler/parsing                                        44s   2GB
Jul 03 09:22:21 Starting characteristic
Jul 03 09:22:22 Finished characteristic                                           0s 113MB
Jul 03 09:22:23 Starting translator/monadic
Jul 03 09:22:25 Finished translator/monadic                                       0s 120MB
Jul 03 09:22:26 Starting translator/monadic/monad_base
Jul 03 09:22:28 Finished translator/monadic/monad_base                            0s  88MB
Jul 03 09:22:28 Starting profiler
Jul 03 09:23:00 Finished profiler                                                30s   1GB
Jul 03 09:23:00 Starting basis
Jul 03 09:24:44 Finished basis                                                 1m42s   4GB
Jul 03 09:24:45 Starting compiler
Jul 03 09:24:47 Finished compiler                                                 1s 228MB
Jul 03 09:24:48 Starting compiler/inference
Jul 03 09:24:50 Finished compiler/inference                                       0s 115MB
Jul 03 09:24:51 Starting compiler/backend/reg_alloc
Jul 03 09:24:52 Finished compiler/backend/reg_alloc                               0s  88MB
Jul 03 09:24:53 Starting compiler/backend/gc
Jul 03 09:24:55 Finished compiler/backend/gc                                      1s 139MB
Jul 03 09:24:56 Starting compiler/backend
Jul 03 09:24:58 Finished compiler/backend                                         1s 143MB
Jul 03 09:24:59 Starting compiler/encoders/asm
Jul 03 09:25:01 Finished compiler/encoders/asm                                    0s  92MB
Jul 03 09:25:01 Starting compiler/encoders/x64
Jul 03 09:25:03 Finished compiler/encoders/x64                                    0s 102MB
Jul 03 09:25:04 Starting compiler/encoders/arm7
Jul 03 09:25:06 Finished compiler/encoders/arm7                                   0s 107MB
Jul 03 09:25:06 Starting compiler/encoders/arm8
Jul 03 09:25:08 Finished compiler/encoders/arm8                                   0s 103MB
Jul 03 09:25:09 Starting compiler/encoders/arm8_asl
Jul 03 09:25:27 Finished compiler/encoders/arm8_asl                              17s   1GB
Jul 03 09:25:28 Starting compiler/encoders/mips
Jul 03 09:25:30 Finished compiler/encoders/mips                                   0s 104MB
Jul 03 09:25:30 Starting compiler/encoders/riscv
Jul 03 09:25:32 Finished compiler/encoders/riscv                                  0s 100MB
Jul 03 09:25:33 Starting compiler/encoders/ag32
Jul 03 09:25:35 Finished compiler/encoders/ag32                                   0s 100MB
Jul 03 09:25:35 Starting compiler/encoders/tests
Jul 03 09:25:37 Finished compiler/encoders/tests                                  1s 130MB
Jul 03 09:25:38 Starting compiler/encoders/monadic_enc
Jul 03 09:26:02 Finished compiler/encoders/monadic_enc                           22s   1GB
Jul 03 09:26:03 Starting compiler/backend/x64
Jul 03 09:26:05 Finished compiler/backend/x64                                     1s 141MB
Jul 03 09:26:06 Starting compiler/backend/arm7
Jul 03 09:26:08 Finished compiler/backend/arm7                                    1s 143MB
Jul 03 09:26:08 Starting compiler/backend/arm8
Jul 03 09:26:10 Finished compiler/backend/arm8                                    1s 142MB
Jul 03 09:26:11 Starting compiler/backend/mips
Jul 03 09:26:13 Finished compiler/backend/mips                                    1s 145MB
Jul 03 09:26:14 Starting compiler/backend/riscv
Jul 03 09:26:16 Finished compiler/backend/riscv                                   1s 142MB
Jul 03 09:26:17 Starting compiler/backend/ag32
Jul 03 09:27:18 Finished compiler/backend/ag32                                 1m00s   1GB
Jul 03 09:27:19 Starting compiler/backend/pattern_matching
Jul 03 09:27:20 Finished compiler/backend/pattern_matching                        0s  88MB
Jul 03 09:27:21 Starting compiler/parsing/ocaml
Jul 03 09:29:27 Finished compiler/parsing/ocaml                                2m05s   1GB
Jul 03 09:29:28 Starting compiler/printing
Jul 03 09:30:21 Finished compiler/printing                                       52s   1GB
Jul 03 09:30:22 Starting compiler/parsing/proofs
Jul 03 09:30:24 Finished compiler/parsing/proofs                                  0s 103MB
Jul 03 09:30:25 Starting compiler/inference/proofs
Jul 03 09:30:27 Finished compiler/inference/proofs                                0s 118MB
Jul 03 09:30:28 Starting compiler/backend/semantics
Jul 03 09:33:36 Finished compiler/backend/semantics                            3m07s   2GB
Jul 03 09:33:37 Starting compiler/backend/reg_alloc/proofs
Jul 03 09:33:38 Finished compiler/backend/reg_alloc/proofs                        1s 115MB
Jul 03 09:33:39 Starting compiler/backend/proofs
Jul 03 09:34:25 Finished compiler/backend/proofs                                 45s   3GB
Jul 03 09:34:26 Starting compiler/backend/serialiser
Jul 03 09:34:28 Finished compiler/backend/serialiser                              1s 140MB
Jul 03 09:34:29 Starting compiler/encoders/x64/proofs
Jul 03 09:34:31 Finished compiler/encoders/x64/proofs                             0s  97MB
Jul 03 09:34:32 Starting compiler/encoders/arm7/proofs
Jul 03 09:47:01 Finished compiler/encoders/arm7/proofs                        12m28s   5GB
Jul 03 09:47:02 Starting compiler/encoders/arm8/proofs
Jul 03 09:54:41 Finished compiler/encoders/arm8/proofs                         7m37s   3GB
Jul 03 09:54:42 Starting compiler/encoders/arm8_asl/proofs
Jul 03 10:11:56 Finished compiler/encoders/arm8_asl/proofs                    17m13s   3GB
Jul 03 10:11:57 Starting compiler/encoders/mips/proofs
Jul 03 10:22:52 Finished compiler/encoders/mips/proofs                        10m54s   4GB
Jul 03 10:22:53 Starting compiler/encoders/riscv/proofs
Jul 03 10:32:14 Finished compiler/encoders/riscv/proofs                        9m20s   3GB
Jul 03 10:32:15 Starting compiler/encoders/ag32/proofs
Jul 03 10:35:20 Finished compiler/encoders/ag32/proofs                         3m04s   1GB
Jul 03 10:35:21 Starting compiler/backend/x64/proofs
Jul 03 10:35:23 Finished compiler/backend/x64/proofs                              1s 219MB
Jul 03 10:35:24 Starting compiler/backend/arm7/proofs
Jul 03 10:36:04 Finished compiler/backend/arm7/proofs                            38s   2GB
Jul 03 10:36:05 Starting compiler/backend/arm8/proofs
Jul 03 10:36:44 Finished compiler/backend/arm8/proofs                            38s   2GB
Jul 03 10:36:45 Starting compiler/backend/arm8_asl
Jul 03 10:37:11 Finished compiler/backend/arm8_asl                               24s   1GB
Jul 03 10:37:12 Starting compiler/backend/mips/proofs
Jul 03 10:37:51 Finished compiler/backend/mips/proofs                            38s   2GB
Jul 03 10:37:52 Starting compiler/backend/riscv/proofs
Jul 03 10:38:32 Finished compiler/backend/riscv/proofs                           39s   2GB
Jul 03 10:38:33 Starting compiler/backend/ag32/proofs
Jul 03 10:48:02 Finished compiler/backend/ag32/proofs                          9m28s   4GB
Jul 03 10:48:03 Starting compiler/backend/cv_compute
Jul 03 10:48:33 Finished compiler/backend/cv_compute                             29s   1GB
Jul 03 10:48:34 Starting cv_translator
Jul 03 10:53:32 Finished cv_translator                                         4m56s   3GB
Jul 03 10:53:33 Starting candle
Jul 03 10:53:34 Finished candle                                                   0s   7MB
Jul 03 10:53:35 Starting candle/set-theory
Jul 03 10:54:07 Finished candle/set-theory                                       31s 907MB
Jul 03 10:54:07 Starting candle/syntax-lib
Jul 03 10:54:09 Finished candle/syntax-lib                                        0s  80MB
Jul 03 10:54:10 Starting candle/standard
Jul 03 10:54:11 Finished candle/standard                                          0s   7MB
Jul 03 10:54:12 Starting candle/standard/syntax
Jul 03 10:54:26 Finished candle/standard/syntax                                  14s 814MB
Jul 03 10:54:27 Starting candle/standard/syntax/little_theories
Jul 03 10:55:39 Finished candle/standard/syntax/little_theories                1m10s 880MB
Jul 03 10:55:39 Starting candle/standard/semantics
Jul 03 10:57:54 Finished candle/standard/semantics                             2m13s   2GB
Jul 03 10:57:55 Starting candle/standard/monadic
Jul 03 10:57:57 Finished candle/standard/monadic                                  0s 123MB
Jul 03 10:57:58 Starting candle/standard/ml_kernel
Jul 03 11:00:03 Finished candle/standard/ml_kernel                             2m04s   4GB
Jul 03 11:00:04 Starting candle/overloading
Jul 03 11:00:05 Finished candle/overloading                                       0s   7MB
Jul 03 11:00:06 Starting candle/overloading/syntax
Jul 03 11:03:12 Finished candle/overloading/syntax                             3m05s   2GB
Jul 03 11:03:13 Starting candle/overloading/semantics
Jul 03 11:12:50 Finished candle/overloading/semantics                          9m35s   4GB
Jul 03 11:12:51 Starting candle/overloading/monadic
Jul 03 11:14:55 Finished candle/overloading/monadic                            2m03s   1GB
Jul 03 11:14:56 Starting candle/overloading/ml_kernel
Jul 03 11:21:36 Finished candle/overloading/ml_kernel                          6m39s   6GB
Jul 03 11:21:37 Starting candle/overloading/ml_checker
Jul 03 11:24:22 Finished candle/overloading/ml_checker                         2m44s   6GB
Jul 03 11:24:23 Starting candle/prover
Jul 03 11:24:25 Finished candle/prover                                            1s 170MB
Jul 03 11:24:26 Starting candle/prover/compute
Jul 03 11:24:28 Finished candle/prover/compute                                    1s 159MB
Jul 03 11:24:29 Starting pancake
Jul 03 11:24:31 Finished pancake                                                  1s 147MB
Jul 03 11:24:32 Starting pancake/semantics
Jul 03 11:27:28 Finished pancake/semantics                                     2m54s   2GB
Jul 03 11:27:28 Starting pancake/parser
Jul 03 11:28:09 Finished pancake/parser                                          39s 483MB
Jul 03 11:28:10 Starting pancake/static_checker
Jul 03 11:30:42 Finished pancake/static_checker                                2m31s   1GB
Jul 03 11:30:43 Starting pancake/proofs
Jul 03 11:47:52 Finished pancake/proofs                                       17m08s   5GB
Jul 03 11:47:53 Starting compiler/dafny
Jul 03 11:48:16 Finished compiler/dafny                                          22s 661MB
Jul 03 11:48:17 Starting compiler/dafny/translation
Jul 03 11:58:18 Finished compiler/dafny/translation                           10m00s   6GB
Jul 03 11:58:19 Starting compiler/dafny/compilation
Jul 03 12:00:07 Finished compiler/dafny/compilation                            1m46s   6GB
Jul 03 12:00:08 Starting compiler/dafny/semantics
Jul 03 12:00:45 Finished compiler/dafny/semantics                                36s 485MB
Jul 03 12:00:46 Starting compiler/dafny/proofs
Jul 03 12:02:24 Finished compiler/dafny/proofs                                 1m36s   1GB
Jul 03 12:02:24 Starting compiler/dafny/vcg
Jul 03 12:02:26 Finished compiler/dafny/vcg                                       0s 104MB
Jul 03 12:02:27 Starting compiler/dafny/vcg/examples
Jul 03 12:02:56 Finished compiler/dafny/vcg/examples                             27s   1GB
Jul 03 12:02:57 Starting compiler/scheme
Jul 03 12:03:23 Finished compiler/scheme                                         25s   1GB
Jul 03 12:03:24 Starting compiler/scheme/translation
Jul 03 12:10:02 Finished compiler/scheme/translation                           6m36s   8GB
Jul 03 12:10:03 Starting compiler/scheme/compilation
Jul 03 12:11:27 Finished compiler/scheme/compilation                           1m23s   4GB
Jul 03 12:11:27 Starting compiler/scheme/proofs
Jul 03 12:18:06 Finished compiler/scheme/proofs                                6m37s   2GB
Jul 03 12:18:06 Starting characteristic/examples
Jul 03 12:19:40 Finished characteristic/examples                               1m32s   5GB
Jul 03 12:19:41 Starting tutorial/solutions
Jul 03 12:22:21 Finished tutorial/solutions                                    2m39s   3GB
Jul 03 12:22:22 Starting translator/monadic/examples
Jul 03 12:25:24 Finished translator/monadic/examples                           3m01s   4GB
Jul 03 12:25:25 Starting examples
Jul 03 12:27:50 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                                                 (31s)  [2/22]     OK
Starting work on diffProgTheory
quicksortProgTheory                                        (47s)  [3/22]     OK
Starting work on array_searchProgTheory
catProgTheory                                              (46s)  [4/22]     OK
Starting work on doubleArgProgTheory
divTheory                                                  (58s)  [5/22]     OK
Starting work on echoProgTheory
doubleArgProgTheory                                        (31s)  [6/22]     OK
Starting work on filterProgTheory
array_searchProgTheory                                     (41s)  [7/22]     OK
Starting work on grepProgTheory
diffProgTheory                                             (55s)  [8/22]     OK
Starting work on helloErrProgTheory
echoProgTheory                                             (40s)  [9/22]     OK
Starting work on helloProgTheory
filterProgTheory                                           (52s)        FAIL<1>
grepProgTheory                                             (42s)         killed
helloErrProgTheory                                         (34s)         killed
helloProgTheory                                            (31s)         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 45.0s to build
 Full log: /scratch/cakeml/regression2/cakeml-3419/examples/.hol/logs/filterProgTheory