Job 3415

CakeML:df715c2ff9adf859244333eee41a5add7c289e7a
  Merge pull request #1426 from CakeML/no-substring-output [Jun 26 01:47:12]
HOL:1d9f33ad168d3823cc070223d83ea660d86dcb58
  Invert ParoundPrec, and use it to bracket stacked suffixes [Jun 24 01:00:44]
Machine:lammmington

Jun 27 07:54:09 Claimed job
Jun 27 07:54:14 Building HOL
Jun 27 08:07:40 Starting developers
Jun 27 08:07:45 Finished developers                                               4s 137MB
Jun 27 08:07:46 Starting developers/bin
Jun 27 08:07:50 Finished developers/bin                                           2s  94MB
Jun 27 08:07:51 Starting misc
Jun 27 08:08:50 Finished misc                                                    58s   1GB
Jun 27 08:08:51 Starting compiler/proofs
Jun 27 09:22:56 Finished compiler/proofs                                    1h14m04s  12GB
Jun 27 09:22:57 Starting compiler/bootstrap/compilation/x64/64/proofs
Jun 27 16:08:22 Finished compiler/bootstrap/compilation/x64/64/proofs       6h45m24s 101GB
Jun 27 16:08:23 Starting semantics/ffi
Jun 27 16:08:35 Finished semantics/ffi                                           10s 541MB
Jun 27 16:08:36 Starting semantics
Jun 27 16:08:37 Finished semantics                                                0s  91MB
Jun 27 16:08:38 Starting semantics/proofs
Jun 27 16:09:02 Finished semantics/proofs                                        22s 729MB
Jun 27 16:09:03 Starting semantics/alt_semantics
Jun 27 16:09:20 Finished semantics/alt_semantics                                 16s 496MB
Jun 27 16:09:20 Starting semantics/alt_semantics/proofs
Jun 27 16:13:13 Finished semantics/alt_semantics/proofs                        3m51s   1GB
Jun 27 16:13:14 Starting basis/pure
Jun 27 16:13:15 Finished basis/pure                                               0s  78MB
Jun 27 16:13:16 Starting translator
Jun 27 16:14:29 Finished translator                                            1m12s   2GB
Jun 27 16:14:30 Starting compiler/parsing
Jun 27 16:15:16 Finished compiler/parsing                                        45s   2GB
Jun 27 16:15:17 Starting characteristic
Jun 27 16:15:19 Finished characteristic                                           0s 117MB
Jun 27 16:15:20 Starting translator/monadic
Jun 27 16:15:22 Finished translator/monadic                                       0s 112MB
Jun 27 16:15:22 Starting translator/monadic/monad_base
Jun 27 16:15:24 Finished translator/monadic/monad_base                            0s  89MB
Jun 27 16:15:25 Starting profiler
Jun 27 16:15:56 Finished profiler                                                30s   1GB
Jun 27 16:15:57 Starting basis
Jun 27 16:17:38 Finished basis                                                 1m40s   4GB
Jun 27 16:17:39 Starting compiler
Jun 27 16:17:42 Finished compiler                                                 1s 228MB
Jun 27 16:17:43 Starting compiler/inference
Jun 27 16:17:44 Finished compiler/inference                                       0s 112MB
Jun 27 16:17:45 Starting compiler/backend/reg_alloc
Jun 27 16:17:47 Finished compiler/backend/reg_alloc                               0s  92MB
Jun 27 16:17:48 Starting compiler/backend/gc
Jun 27 16:17:49 Finished compiler/backend/gc                                      1s 137MB
Jun 27 16:17:50 Starting compiler/backend
Jun 27 16:17:52 Finished compiler/backend                                         1s 138MB
Jun 27 16:17:53 Starting compiler/encoders/asm
Jun 27 16:17:55 Finished compiler/encoders/asm                                    0s  90MB
Jun 27 16:17:56 Starting compiler/encoders/x64
Jun 27 16:17:57 Finished compiler/encoders/x64                                    0s 101MB
Jun 27 16:17:58 Starting compiler/encoders/arm7
Jun 27 16:18:00 Finished compiler/encoders/arm7                                   0s 105MB
Jun 27 16:18:01 Starting compiler/encoders/arm8
Jun 27 16:18:02 Finished compiler/encoders/arm8                                   0s 106MB
Jun 27 16:18:03 Starting compiler/encoders/arm8_asl
Jun 27 18:10:10 Finished compiler/encoders/arm8_asl                         1h52m06s  29GB
Jun 27 18:10:11 Starting compiler/encoders/mips
Jun 27 18:10:13 Finished compiler/encoders/mips                                   0s 105MB
Jun 27 18:10:14 Starting compiler/encoders/riscv
Jun 27 18:10:15 Finished compiler/encoders/riscv                                  0s 103MB
Jun 27 18:10:16 Starting compiler/encoders/ag32
Jun 27 18:10:18 Finished compiler/encoders/ag32                                   0s  98MB
Jun 27 18:10:19 Starting compiler/encoders/tests
Jun 27 18:10:21 Finished compiler/encoders/tests                                  1s 131MB
Jun 27 18:10:22 Starting compiler/encoders/monadic_enc
Jun 27 18:10:45 Finished compiler/encoders/monadic_enc                           22s   1GB
Jun 27 18:10:45 Starting compiler/backend/x64
Jun 27 18:10:47 Finished compiler/backend/x64                                     1s 136MB
Jun 27 18:10:48 Starting compiler/backend/arm7
Jun 27 18:10:50 Finished compiler/backend/arm7                                    1s 141MB
Jun 27 18:10:51 Starting compiler/backend/arm8
Jun 27 18:10:53 Finished compiler/backend/arm8                                    1s 136MB
Jun 27 18:10:54 Starting compiler/backend/mips
Jun 27 18:10:56 Finished compiler/backend/mips                                    1s 137MB
Jun 27 18:10:57 Starting compiler/backend/riscv
Jun 27 18:10:58 Finished compiler/backend/riscv                                   1s 141MB
Jun 27 18:10:59 Starting compiler/backend/ag32
Jun 27 18:12:01 Finished compiler/backend/ag32                                 1m00s   1GB
Jun 27 18:12:02 Starting compiler/backend/pattern_matching
Jun 27 18:12:03 Finished compiler/backend/pattern_matching                        0s  89MB
Jun 27 18:12:04 Starting compiler/parsing/ocaml
Jun 27 18:14:10 Finished compiler/parsing/ocaml                                2m05s   1GB
Jun 27 18:14:11 Starting compiler/printing
Jun 27 18:15:06 Finished compiler/printing                                       54s   1GB
Jun 27 18:15:07 Starting compiler/parsing/proofs
Jun 27 18:15:08 Finished compiler/parsing/proofs                                  0s  96MB
Jun 27 18:15:09 Starting compiler/inference/proofs
Jun 27 18:15:11 Finished compiler/inference/proofs                                0s 111MB
Jun 27 18:15:12 Starting compiler/backend/semantics
Jun 27 18:18:16 Finished compiler/backend/semantics                            3m03s   3GB
Jun 27 18:18:17 Starting compiler/backend/reg_alloc/proofs
Jun 27 18:18:19 Finished compiler/backend/reg_alloc/proofs                        1s 116MB
Jun 27 18:18:20 Starting compiler/backend/proofs
Jun 27 18:19:03 Finished compiler/backend/proofs                                 43s   2GB
Jun 27 18:19:04 Starting compiler/backend/serialiser
Jun 27 18:19:06 Finished compiler/backend/serialiser                              1s 147MB
Jun 27 18:19:07 Starting compiler/encoders/x64/proofs
Jun 27 18:19:09 Finished compiler/encoders/x64/proofs                             0s 107MB
Jun 27 18:19:10 Starting compiler/encoders/arm7/proofs
Jun 27 18:31:46 Finished compiler/encoders/arm7/proofs                        12m35s   9GB
Jun 27 18:31:47 Starting compiler/encoders/arm8/proofs
Jun 27 18:39:44 Finished compiler/encoders/arm8/proofs                         7m55s   4GB
Jun 27 18:39:44 Starting compiler/encoders/arm8_asl/proofs
Jun 27 19:37:03 Finished compiler/encoders/arm8_asl/proofs                    57m17s  15GB
Jun 27 19:37:04 Starting compiler/encoders/mips/proofs
Jun 27 19:47:45 Finished compiler/encoders/mips/proofs                        10m39s   6GB
Jun 27 19:47:45 Starting compiler/encoders/riscv/proofs
Jun 27 19:57:27 Finished compiler/encoders/riscv/proofs                        9m40s   3GB
Jun 27 19:57:28 Starting compiler/encoders/ag32/proofs
Jun 27 20:00:36 Finished compiler/encoders/ag32/proofs                         3m07s   1GB
Jun 27 20:00:37 Starting compiler/backend/x64/proofs
Jun 27 20:00:39 Finished compiler/backend/x64/proofs                              1s 218MB
Jun 27 20:00:40 Starting compiler/backend/arm7/proofs
Jun 27 20:01:19 Finished compiler/backend/arm7/proofs                            38s   2GB
Jun 27 20:01:20 Starting compiler/backend/arm8/proofs
Jun 27 20:01:57 Finished compiler/backend/arm8/proofs                            35s   2GB
Jun 27 20:01:57 Starting compiler/backend/arm8_asl
Jun 27 20:02:25 Finished compiler/backend/arm8_asl                               26s   2GB
Jun 27 20:02:25 Starting compiler/backend/mips/proofs
Jun 27 20:03:07 Finished compiler/backend/mips/proofs                            40s   2GB
Jun 27 20:03:08 Starting compiler/backend/riscv/proofs
Jun 27 20:03:50 Finished compiler/backend/riscv/proofs                           41s   2GB
Jun 27 20:03:51 Starting compiler/backend/ag32/proofs
Jun 27 20:13:21 Finished compiler/backend/ag32/proofs                          9m29s   5GB
Jun 27 20:13:22 Starting compiler/backend/cv_compute
Jun 27 20:13:51 Finished compiler/backend/cv_compute                             28s   1GB
Jun 27 20:13:52 Starting cv_translator
Jun 27 20:18:52 Finished cv_translator                                         4m59s   4GB
Jun 27 20:18:53 Starting candle
Jun 27 20:18:54 Finished candle                                                   0s   7MB
Jun 27 20:18:55 Starting candle/set-theory
Jun 27 20:19:27 Finished candle/set-theory                                       31s 908MB
Jun 27 20:19:27 Starting candle/syntax-lib
Jun 27 20:19:29 Finished candle/syntax-lib                                        0s  77MB
Jun 27 20:19:30 Starting candle/standard
Jun 27 20:19:31 Finished candle/standard                                          0s   7MB
Jun 27 20:19:31 Starting candle/standard/syntax
Jun 27 20:19:46 Finished candle/standard/syntax                                  14s 756MB
Jun 27 20:19:47 Starting candle/standard/syntax/little_theories
Jun 27 20:20:59 Finished candle/standard/syntax/little_theories                1m11s 836MB
Jun 27 20:21:00 Starting candle/standard/semantics
Jun 27 20:23:12 Finished candle/standard/semantics                             2m11s   2GB
Jun 27 20:23:13 Starting candle/standard/monadic
Jun 27 20:23:15 Finished candle/standard/monadic                                  0s 122MB
Jun 27 20:23:16 Starting candle/standard/ml_kernel
Jun 27 20:25:18 Finished candle/standard/ml_kernel                             2m01s   4GB
Jun 27 20:25:19 Starting candle/overloading
Jun 27 20:25:20 Finished candle/overloading                                       0s   7MB
Jun 27 20:25:21 Starting candle/overloading/syntax
Jun 27 20:28:30 Finished candle/overloading/syntax                             3m08s   2GB
Jun 27 20:28:31 Starting candle/overloading/semantics
Jun 27 20:38:23 Finished candle/overloading/semantics                          9m50s  11GB
Jun 27 20:38:23 Starting candle/overloading/monadic
Jun 27 20:40:27 Finished candle/overloading/monadic                            2m02s   1GB
Jun 27 20:40:28 Starting candle/overloading/ml_kernel
Jun 27 20:47:14 Finished candle/overloading/ml_kernel                          6m45s   6GB
Jun 27 20:47:15 Starting candle/overloading/ml_checker
Jun 27 20:49:56 Finished candle/overloading/ml_checker                         2m39s   6GB
Jun 27 20:49:57 Starting candle/prover
Jun 27 20:49:59 Finished candle/prover                                            1s 182MB
Jun 27 20:50:00 Starting candle/prover/compute
Jun 27 20:50:02 Finished candle/prover/compute                                    1s 170MB
Jun 27 20:50:03 Starting pancake
Jun 27 20:50:05 Finished pancake                                                  1s 137MB
Jun 27 20:50:06 Starting pancake/semantics
Jun 27 20:53:01 Finished pancake/semantics                                     2m54s   2GB
Jun 27 20:53:02 Starting pancake/parser
Jun 27 20:53:42 Finished pancake/parser                                          39s 497MB
Jun 27 20:53:43 Starting pancake/static_checker
Jun 27 20:56:17 Finished pancake/static_checker                                2m32s   1GB
Jun 27 20:56:17 Starting pancake/proofs
Jun 27 21:13:33 Finished pancake/proofs                                       17m15s   5GB
Jun 27 21:13:34 Starting compiler/dafny
Jun 27 21:13:58 Finished compiler/dafny                                          23s 660MB
Jun 27 21:13:59 Starting compiler/dafny/translation
Jun 27 21:23:54 Finished compiler/dafny/translation                            9m53s   6GB
Jun 27 21:23:54 Starting compiler/dafny/compilation
Jun 27 21:25:43 Finished compiler/dafny/compilation                            1m47s   6GB
Jun 27 21:25:44 Starting compiler/dafny/semantics
Jun 27 21:26:22 Finished compiler/dafny/semantics                                36s 516MB
Jun 27 21:26:23 Starting compiler/dafny/proofs
Jun 27 21:28:00 Finished compiler/dafny/proofs                                 1m36s   1GB
Jun 27 21:28:01 Starting compiler/dafny/vcg
Jun 27 21:28:02 Finished compiler/dafny/vcg                                       0s 105MB
Jun 27 21:28:03 Starting compiler/dafny/vcg/examples
Jun 27 21:28:31 Finished compiler/dafny/vcg/examples                             26s   1GB
Jun 27 21:28:32 Starting compiler/scheme
Jun 27 21:28:58 Finished compiler/scheme                                         25s   1GB
Jun 27 21:28:59 Starting compiler/scheme/translation
Jun 27 21:35:41 Finished compiler/scheme/translation                           6m40s   8GB
Jun 27 21:35:41 Starting compiler/scheme/compilation
Jun 27 21:37:03 Finished compiler/scheme/compilation                           1m21s   4GB
Jun 27 21:37:04 Starting compiler/scheme/proofs
Jun 27 21:43:54 Finished compiler/scheme/proofs                                6m48s   2GB
Jun 27 21:43:54 Starting characteristic/examples
Jun 27 21:45:28 Finished characteristic/examples                               1m32s   5GB
Jun 27 21:45:28 Starting tutorial/solutions
Jun 27 21:48:16 Finished tutorial/solutions                                    2m46s   3GB
Jun 27 21:48:17 Starting translator/monadic/examples
Jun 27 21:51:19 Finished translator/monadic/examples                           3m01s   4GB
Jun 27 21:51:20 Starting examples
Jun 27 21:53:57 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)/compiler/inference
Scanning $(CAKEMLDIR)/compiler/printing
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/basis
Scanned 66 directories
Building 28 theory files
Starting work on md5Theory
Starting work on source_valuesTheory
Starting work on regexp_parserTheory
Starting work on README.md
README.md                                         examples  (0s)             OK
Starting work on quicksortProgTheory
source_valuesTheory                     examples/bootstrap  (1s)  [1/28]     OK
Starting work on source_syntaxTheory
source_syntaxTheory                     examples/bootstrap  (0s)  [2/28]     OK
Starting work on parsingTheory
md5Theory                              examples/Crypto/MD5  (7s)  [3/28]     OK
Finished $(HOLDIR)/examples/Crypto/MD5 [#theories: 1]                  (7.570s) 
Starting work on printingTheory
parsingTheory                           examples/bootstrap  (8s)  [4/28]     OK
Starting work on catProgTheory
printingTheory                          examples/bootstrap  (4s)  [5/28]     OK
Finished $(HOLDIR)/examples/bootstrap [#theories: 4]                  (15.730s) 
Starting work on lcsTheory
regexp_parserTheory      examples/formal-languages/regular (12s)  [6/28]     OK
Finished $(HOLDIR)/examples/formal-languages/regular [#theories: 1]   (12.820s) 
Starting work on divTheory
lcsTheory                                         examples  (6s)  [7/28]     OK
Starting work on diffTheory
quicksortProgTheory                               examples (48s)  [8/28]     OK
Starting work on array_searchProgTheory
diffTheory                                        examples (31s)  [9/28]     OK
Starting work on diffProgTheory
catProgTheory                                     examples (47s) [10/28]     OK
Starting work on doubleArgProgTheory
divTheory                                         examples (56s) [11/28]     OK
Starting work on echoProgTheory
doubleArgProgTheory                               examples (30s) [12/28]     OK
Starting work on filterProgTheory
array_searchProgTheory                            examples (44s) [13/28]     OK
Starting work on grepProgTheory
diffProgTheory                                    examples (54s) [14/28]     OK
Starting work on helloErrProgTheory
echoProgTheory                                    examples (38s) [15/28]     OK
Starting work on helloProgTheory
filterProgTheory                                  examples (50s)        FAIL<1>
grepProgTheory                                    examples (48s)         killed
helloErrProgTheory                                examples (32s)         killed
helloProgTheory                                   examples (33s)         killed
*** Holmake aborted - 1 target failed:
*** filterProgTheory in examples (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.4s to build
 Full log: /scratch/cakeml/regression3/cakeml-3415/examples/.hol/logs/filterProgTheory