Job 3418

CakeML:7f71e73b095b6e19af29de810592291d950ee6ac
  Update changes-since-release.md [Jul 02 07:06:16]
#1430 (better-concatWith)
Merging into:ed31510b3b0d0523283b68ef7066882526d77df9
  Merge pull request #1429 from CakeML/use-monadsyntax-api [Jun 29 01:11:59]
HOL:1d9f33ad168d3823cc070223d83ea660d86dcb58
  Invert ParoundPrec, and use it to bracket stacked suffixes [Jun 24 01:00:44]
Machine:lammmington

Jul 02 09:28:14 Claimed job
Jul 02 09:28:18 Reusing HOL
Jul 02 09:28:26 Starting developers
Jul 02 09:28:33 Finished developers                                               6s 179MB
Jul 02 09:28:34 Starting developers/bin
Jul 02 09:28:38 Finished developers/bin                                           2s  93MB
Jul 02 09:28:39 Starting misc
Jul 02 09:29:23 Finished misc                                                    43s   1GB
Jul 02 09:29:24 Starting compiler/proofs
Jul 02 10:39:42 Finished compiler/proofs                                    1h10m16s   9GB
Jul 02 10:39:42 Starting compiler/bootstrap/compilation/x64/64/proofs
Jul 02 17:28:14 Finished compiler/bootstrap/compilation/x64/64/proofs       6h48m30s 103GB
Jul 02 17:28:14 Starting semantics/ffi
Jul 02 17:28:26 Finished semantics/ffi                                           11s 537MB
Jul 02 17:28:27 Starting semantics
Jul 02 17:28:29 Finished semantics                                                0s  92MB
Jul 02 17:28:30 Starting semantics/proofs
Jul 02 17:28:54 Finished semantics/proofs                                        23s 723MB
Jul 02 17:28:55 Starting semantics/alt_semantics
Jul 02 17:29:12 Finished semantics/alt_semantics                                 16s 491MB
Jul 02 17:29:13 Starting semantics/alt_semantics/proofs
Jul 02 17:32:59 Finished semantics/alt_semantics/proofs                        3m45s   1GB
Jul 02 17:33:00 Starting basis/pure
Jul 02 17:33:01 Finished basis/pure                                               0s  80MB
Jul 02 17:33:02 Starting translator
Jul 02 17:34:14 Finished translator                                            1m10s   2GB
Jul 02 17:34:15 Starting compiler/parsing
Jul 02 17:35:01 Finished compiler/parsing                                        45s   2GB
Jul 02 17:35:02 Starting characteristic
Jul 02 17:35:04 Finished characteristic                                           1s 113MB
Jul 02 17:35:05 Starting translator/monadic
Jul 02 17:35:07 Finished translator/monadic                                       0s 119MB
Jul 02 17:35:07 Starting translator/monadic/monad_base
Jul 02 17:35:09 Finished translator/monadic/monad_base                            0s  85MB
Jul 02 17:35:10 Starting profiler
Jul 02 17:35:41 Finished profiler                                                30s   1GB
Jul 02 17:35:42 Starting basis
Jul 02 17:37:26 Finished basis                                                 1m43s   4GB
Jul 02 17:37:27 Starting compiler
Jul 02 17:37:30 Finished compiler                                                 1s 217MB
Jul 02 17:37:31 Starting compiler/inference
Jul 02 17:37:32 Finished compiler/inference                                       0s 115MB
Jul 02 17:37:33 Starting compiler/backend/reg_alloc
Jul 02 17:37:35 Finished compiler/backend/reg_alloc                               0s  93MB
Jul 02 17:37:36 Starting compiler/backend/gc
Jul 02 17:37:38 Finished compiler/backend/gc                                      1s 139MB
Jul 02 17:37:39 Starting compiler/backend
Jul 02 17:37:41 Finished compiler/backend                                         1s 139MB
Jul 02 17:37:41 Starting compiler/encoders/asm
Jul 02 17:37:43 Finished compiler/encoders/asm                                    0s  95MB
Jul 02 17:37:44 Starting compiler/encoders/x64
Jul 02 17:37:46 Finished compiler/encoders/x64                                    0s 104MB
Jul 02 17:37:47 Starting compiler/encoders/arm7
Jul 02 17:37:48 Finished compiler/encoders/arm7                                   0s 107MB
Jul 02 17:37:49 Starting compiler/encoders/arm8
Jul 02 17:37:51 Finished compiler/encoders/arm8                                   0s 103MB
Jul 02 17:37:52 Starting compiler/encoders/arm8_asl
Jul 02 17:38:10 Finished compiler/encoders/arm8_asl                              17s   1GB
Jul 02 17:38:11 Starting compiler/encoders/mips
Jul 02 17:38:12 Finished compiler/encoders/mips                                   0s 103MB
Jul 02 17:38:13 Starting compiler/encoders/riscv
Jul 02 17:38:15 Finished compiler/encoders/riscv                                  0s 107MB
Jul 02 17:38:16 Starting compiler/encoders/ag32
Jul 02 17:38:17 Finished compiler/encoders/ag32                                   0s 104MB
Jul 02 17:38:18 Starting compiler/encoders/tests
Jul 02 17:38:20 Finished compiler/encoders/tests                                  1s 131MB
Jul 02 17:38:21 Starting compiler/encoders/monadic_enc
Jul 02 17:38:43 Finished compiler/encoders/monadic_enc                           21s   1GB
Jul 02 17:38:44 Starting compiler/backend/x64
Jul 02 17:38:46 Finished compiler/backend/x64                                     1s 141MB
Jul 02 17:38:47 Starting compiler/backend/arm7
Jul 02 17:38:49 Finished compiler/backend/arm7                                    1s 143MB
Jul 02 17:38:50 Starting compiler/backend/arm8
Jul 02 17:38:52 Finished compiler/backend/arm8                                    1s 142MB
Jul 02 17:38:53 Starting compiler/backend/mips
Jul 02 17:38:55 Finished compiler/backend/mips                                    1s 143MB
Jul 02 17:38:55 Starting compiler/backend/riscv
Jul 02 17:38:57 Finished compiler/backend/riscv                                   1s 143MB
Jul 02 17:38:58 Starting compiler/backend/ag32
Jul 02 17:40:00 Finished compiler/backend/ag32                                 1m01s   1GB
Jul 02 17:40:01 Starting compiler/backend/pattern_matching
Jul 02 17:40:03 Finished compiler/backend/pattern_matching                        0s  91MB
Jul 02 17:40:04 Starting compiler/parsing/ocaml
Jul 02 17:42:14 Finished compiler/parsing/ocaml                                2m09s   1GB
Jul 02 17:42:15 Starting compiler/printing
Jul 02 17:43:09 Finished compiler/printing                                       52s   1GB
Jul 02 17:43:10 Starting compiler/parsing/proofs
Jul 02 17:43:11 Finished compiler/parsing/proofs                                  0s 105MB
Jul 02 17:43:13 Starting compiler/inference/proofs
Jul 02 17:43:14 Finished compiler/inference/proofs                                0s 113MB
Jul 02 17:43:15 Starting compiler/backend/semantics
Jul 02 17:46:22 Finished compiler/backend/semantics                            3m05s   3GB
Jul 02 17:46:23 Starting compiler/backend/reg_alloc/proofs
Jul 02 17:46:24 Finished compiler/backend/reg_alloc/proofs                        1s 122MB
Jul 02 17:46:25 Starting compiler/backend/proofs
Jul 02 17:47:09 Finished compiler/backend/proofs                                 43s   2GB
Jul 02 17:47:10 Starting compiler/backend/serialiser
Jul 02 17:47:12 Finished compiler/backend/serialiser                              1s 149MB
Jul 02 17:47:13 Starting compiler/encoders/x64/proofs
Jul 02 17:47:15 Finished compiler/encoders/x64/proofs                             0s  99MB
Jul 02 17:47:16 Starting compiler/encoders/arm7/proofs
Jul 02 17:59:41 Finished compiler/encoders/arm7/proofs                        12m23s   5GB
Jul 02 17:59:41 Starting compiler/encoders/arm8/proofs
Jul 02 18:07:41 Finished compiler/encoders/arm8/proofs                         7m58s   3GB
Jul 02 18:07:42 Starting compiler/encoders/arm8_asl/proofs
Jul 02 18:24:59 Finished compiler/encoders/arm8_asl/proofs                    17m16s   3GB
Jul 02 18:25:00 Starting compiler/encoders/mips/proofs
Jul 02 18:35:45 Finished compiler/encoders/mips/proofs                        10m43s   5GB
Jul 02 18:35:46 Starting compiler/encoders/riscv/proofs
Jul 02 18:45:22 Finished compiler/encoders/riscv/proofs                        9m35s   3GB
Jul 02 18:45:23 Starting compiler/encoders/ag32/proofs
Jul 02 18:48:30 Finished compiler/encoders/ag32/proofs                         3m06s   1GB
Jul 02 18:48:30 Starting compiler/backend/x64/proofs
Jul 02 18:48:33 Finished compiler/backend/x64/proofs                              1s 227MB
Jul 02 18:48:34 Starting compiler/backend/arm7/proofs
Jul 02 18:49:14 Finished compiler/backend/arm7/proofs                            39s   2GB
Jul 02 18:49:15 Starting compiler/backend/arm8/proofs
Jul 02 18:49:51 Finished compiler/backend/arm8/proofs                            35s   1GB
Jul 02 18:49:52 Starting compiler/backend/arm8_asl
Jul 02 18:50:18 Finished compiler/backend/arm8_asl                               24s   1GB
Jul 02 18:50:19 Starting compiler/backend/mips/proofs
Jul 02 18:50:58 Finished compiler/backend/mips/proofs                            38s   2GB
Jul 02 18:50:59 Starting compiler/backend/riscv/proofs
Jul 02 18:51:39 Finished compiler/backend/riscv/proofs                           39s   2GB
Jul 02 18:51:40 Starting compiler/backend/ag32/proofs
Jul 02 19:01:13 Finished compiler/backend/ag32/proofs                          9m32s   5GB
Jul 02 19:01:14 Starting compiler/backend/cv_compute
Jul 02 19:01:43 Finished compiler/backend/cv_compute                             28s   1GB
Jul 02 19:01:44 Starting cv_translator
Jul 02 19:06:45 Finished cv_translator                                         4m59s   3GB
Jul 02 19:06:45 Starting candle
Jul 02 19:06:46 Finished candle                                                   0s   7MB
Jul 02 19:06:47 Starting candle/set-theory
Jul 02 19:07:19 Finished candle/set-theory                                       30s 937MB
Jul 02 19:07:19 Starting candle/syntax-lib
Jul 02 19:07:21 Finished candle/syntax-lib                                        0s  80MB
Jul 02 19:07:22 Starting candle/standard
Jul 02 19:07:23 Finished candle/standard                                          0s   7MB
Jul 02 19:07:24 Starting candle/standard/syntax
Jul 02 19:07:39 Finished candle/standard/syntax                                  14s 815MB
Jul 02 19:07:39 Starting candle/standard/syntax/little_theories
Jul 02 19:08:52 Finished candle/standard/syntax/little_theories                1m11s 905MB
Jul 02 19:08:53 Starting candle/standard/semantics
Jul 02 19:11:08 Finished candle/standard/semantics                             2m14s   2GB
Jul 02 19:11:09 Starting candle/standard/monadic
Jul 02 19:11:11 Finished candle/standard/monadic                                  0s 123MB
Jul 02 19:11:12 Starting candle/standard/ml_kernel
Jul 02 19:13:15 Finished candle/standard/ml_kernel                             2m02s   4GB
Jul 02 19:13:16 Starting candle/overloading
Jul 02 19:13:17 Finished candle/overloading                                       0s   7MB
Jul 02 19:13:18 Starting candle/overloading/syntax
Jul 02 19:16:24 Finished candle/overloading/syntax                             3m04s   2GB
Jul 02 19:16:25 Starting candle/overloading/semantics
Jul 02 19:25:59 Finished candle/overloading/semantics                          9m33s   3GB
Jul 02 19:26:00 Starting candle/overloading/monadic
Jul 02 19:28:01 Finished candle/overloading/monadic                            2m00s   1GB
Jul 02 19:28:02 Starting candle/overloading/ml_kernel
Jul 02 19:34:54 Finished candle/overloading/ml_kernel                          6m50s   6GB
Jul 02 19:34:55 Starting candle/overloading/ml_checker
Jul 02 19:37:40 Finished candle/overloading/ml_checker                         2m44s   6GB
Jul 02 19:37:41 Starting candle/prover
Jul 02 19:37:44 Finished candle/prover                                            1s 181MB
Jul 02 19:37:45 Starting candle/prover/compute
Jul 02 19:37:47 Finished candle/prover/compute                                    1s 153MB
Jul 02 19:37:48 Starting pancake
Jul 02 19:37:50 Finished pancake                                                  1s 137MB
Jul 02 19:37:50 Starting pancake/semantics
Jul 02 19:40:49 Finished pancake/semantics                                     2m58s   2GB
Jul 02 19:40:50 Starting pancake/parser
Jul 02 19:41:31 Finished pancake/parser                                          39s 483MB
Jul 02 19:41:32 Starting pancake/static_checker
Jul 02 19:44:06 Finished pancake/static_checker                                2m32s   1GB
Jul 02 19:44:07 Starting pancake/proofs
Jul 02 20:01:35 Finished pancake/proofs                                       17m27s   6GB
Jul 02 20:01:35 Starting compiler/dafny
Jul 02 20:01:59 Finished compiler/dafny                                          23s 662MB
Jul 02 20:02:00 Starting compiler/dafny/translation
Jul 02 20:12:05 Finished compiler/dafny/translation                           10m03s   6GB
Jul 02 20:12:05 Starting compiler/dafny/compilation
Jul 02 20:13:52 Finished compiler/dafny/compilation                            1m45s   5GB
Jul 02 20:13:52 Starting compiler/dafny/semantics
Jul 02 20:14:31 Finished compiler/dafny/semantics                                37s 493MB
Jul 02 20:14:31 Starting compiler/dafny/proofs
Jul 02 20:16:11 Finished compiler/dafny/proofs                                 1m38s   1GB
Jul 02 20:16:12 Starting compiler/dafny/vcg
Jul 02 20:16:13 Finished compiler/dafny/vcg                                       0s 108MB
Jul 02 20:16:14 Starting compiler/dafny/vcg/examples
Jul 02 20:16:44 Finished compiler/dafny/vcg/examples                             28s   1GB
Jul 02 20:16:44 Starting compiler/scheme
Jul 02 20:17:11 Finished compiler/scheme                                         26s   1GB
Jul 02 20:17:12 Starting compiler/scheme/translation
Jul 02 20:24:01 Finished compiler/scheme/translation                           6m47s   8GB
Jul 02 20:24:02 Starting compiler/scheme/compilation
Jul 02 20:25:27 Finished compiler/scheme/compilation                           1m21s   4GB
Jul 02 20:25:28 Starting compiler/scheme/proofs
Jul 02 20:32:18 Finished compiler/scheme/proofs                                6m49s   2GB
Jul 02 20:32:19 Starting characteristic/examples
Jul 02 20:33:51 Finished characteristic/examples                               1m31s   5GB
Jul 02 20:33:52 Starting tutorial/solutions
Jul 02 20:36:35 Finished tutorial/solutions                                    2m42s   3GB
Jul 02 20:36:36 Starting translator/monadic/examples
Jul 02 20:39:40 Finished translator/monadic/examples                           3m03s   4GB
Jul 02 20:39:41 Starting examples
Jul 02 20:42:07 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                                        (48s)  [3/22]     OK
Starting work on array_searchProgTheory
catProgTheory                                              (47s)  [4/22]     OK
Starting work on doubleArgProgTheory
divTheory                                                  (56s)  [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                                             (54s)  [8/22]     OK
Starting work on helloErrProgTheory
echoProgTheory                                             (38s)  [9/22]     OK
Starting work on helloProgTheory
filterProgTheory                                           (51s)        FAIL<1>
grepProgTheory                                             (41s)         killed
helloErrProgTheory                                         (35s)         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.6s to build
 Full log: /scratch/cakeml/regression3/cakeml-3418/examples/.hol/logs/filterProgTheory