Job 3416

CakeML: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

Jun 29 01:15:21 Claimed job
Jun 29 01:15:29 Reusing HOL
Jun 29 01:15:36 Starting developers
Jun 29 01:15:42 Finished developers                                               4s 201MB
Jun 29 01:15:43 Starting developers/bin
Jun 29 01:15:48 Finished developers/bin                                           4s  94MB
Jun 29 01:15:48 Starting misc
Jun 29 01:16:31 Finished misc                                                    42s   1GB
Jun 29 01:16:32 Starting compiler/proofs
Jun 29 02:28:21 Finished compiler/proofs                                    1h11m46s   9GB
Jun 29 02:28:22 Starting compiler/bootstrap/compilation/x64/64/proofs
Jun 29 09:12:46 Finished compiler/bootstrap/compilation/x64/64/proofs       6h44m22s  81GB
Jun 29 09:12:46 Starting semantics/ffi
Jun 29 09:12:58 Finished semantics/ffi                                           10s 541MB
Jun 29 09:12:59 Starting semantics
Jun 29 09:13:00 Finished semantics                                                0s  91MB
Jun 29 09:13:01 Starting semantics/proofs
Jun 29 09:13:25 Finished semantics/proofs                                        23s 702MB
Jun 29 09:13:26 Starting semantics/alt_semantics
Jun 29 09:13:43 Finished semantics/alt_semantics                                 16s 495MB
Jun 29 09:13:44 Starting semantics/alt_semantics/proofs
Jun 29 09:17:28 Finished semantics/alt_semantics/proofs                        3m43s   1GB
Jun 29 09:17:29 Starting basis/pure
Jun 29 09:17:31 Finished basis/pure                                               0s  86MB
Jun 29 09:17:31 Starting translator
Jun 29 09:18:44 Finished translator                                            1m12s   2GB
Jun 29 09:18:45 Starting compiler/parsing
Jun 29 09:19:30 Finished compiler/parsing                                        44s   2GB
Jun 29 09:19:31 Starting characteristic
Jun 29 09:19:33 Finished characteristic                                           1s 113MB
Jun 29 09:19:34 Starting translator/monadic
Jun 29 09:19:35 Finished translator/monadic                                       0s 119MB
Jun 29 09:19:36 Starting translator/monadic/monad_base
Jun 29 09:19:38 Finished translator/monadic/monad_base                            0s  84MB
Jun 29 09:19:39 Starting profiler
Jun 29 09:20:09 Finished profiler                                                29s   1GB
Jun 29 09:20:10 Starting basis
Jun 29 09:21:51 Finished basis                                                 1m38s   4GB
Jun 29 09:21:52 Starting compiler
Jun 29 09:21:54 Finished compiler                                                 1s 219MB
Jun 29 09:21:55 Starting compiler/inference
Jun 29 09:21:57 Finished compiler/inference                                       0s 115MB
Jun 29 09:21:58 Starting compiler/backend/reg_alloc
Jun 29 09:21:59 Finished compiler/backend/reg_alloc                               0s  89MB
Jun 29 09:22:00 Starting compiler/backend/gc
Jun 29 09:22:02 Finished compiler/backend/gc                                      1s 136MB
Jun 29 09:22:03 Starting compiler/backend
Jun 29 09:22:05 Finished compiler/backend                                         1s 138MB
Jun 29 09:22:06 Starting compiler/encoders/asm
Jun 29 09:22:07 Finished compiler/encoders/asm                                    0s  94MB
Jun 29 09:22:08 Starting compiler/encoders/x64
Jun 29 09:22:10 Finished compiler/encoders/x64                                    0s 103MB
Jun 29 09:22:11 Starting compiler/encoders/arm7
Jun 29 09:22:12 Finished compiler/encoders/arm7                                   0s 106MB
Jun 29 09:22:13 Starting compiler/encoders/arm8
Jun 29 09:22:15 Finished compiler/encoders/arm8                                   0s 102MB
Jun 29 09:22:16 Starting compiler/encoders/arm8_asl
Jun 29 09:22:34 Finished compiler/encoders/arm8_asl                              17s   1GB
Jun 29 09:22:34 Starting compiler/encoders/mips
Jun 29 09:22:36 Finished compiler/encoders/mips                                   0s 103MB
Jun 29 09:22:37 Starting compiler/encoders/riscv
Jun 29 09:22:39 Finished compiler/encoders/riscv                                  0s 101MB
Jun 29 09:22:39 Starting compiler/encoders/ag32
Jun 29 09:22:41 Finished compiler/encoders/ag32                                   0s 102MB
Jun 29 09:22:42 Starting compiler/encoders/tests
Jun 29 09:22:44 Finished compiler/encoders/tests                                  1s 132MB
Jun 29 09:22:45 Starting compiler/encoders/monadic_enc
Jun 29 09:23:07 Finished compiler/encoders/monadic_enc                           21s   1GB
Jun 29 09:23:08 Starting compiler/backend/x64
Jun 29 09:23:10 Finished compiler/backend/x64                                     1s 140MB
Jun 29 09:23:10 Starting compiler/backend/arm7
Jun 29 09:23:12 Finished compiler/backend/arm7                                    1s 143MB
Jun 29 09:23:13 Starting compiler/backend/arm8
Jun 29 09:23:15 Finished compiler/backend/arm8                                    1s 143MB
Jun 29 09:23:16 Starting compiler/backend/mips
Jun 29 09:23:18 Finished compiler/backend/mips                                    1s 145MB
Jun 29 09:23:19 Starting compiler/backend/riscv
Jun 29 09:23:21 Finished compiler/backend/riscv                                   1s 143MB
Jun 29 09:23:21 Starting compiler/backend/ag32
Jun 29 09:24:25 Finished compiler/backend/ag32                                 1m02s   2GB
Jun 29 09:24:25 Starting compiler/backend/pattern_matching
Jun 29 09:24:27 Finished compiler/backend/pattern_matching                        0s  91MB
Jun 29 09:24:28 Starting compiler/parsing/ocaml
Jun 29 09:26:35 Finished compiler/parsing/ocaml                                2m06s   1GB
Jun 29 09:26:36 Starting compiler/printing
Jun 29 09:27:31 Finished compiler/printing                                       53s   1GB
Jun 29 09:27:32 Starting compiler/parsing/proofs
Jun 29 09:27:33 Finished compiler/parsing/proofs                                  0s 104MB
Jun 29 09:27:34 Starting compiler/inference/proofs
Jun 29 09:27:36 Finished compiler/inference/proofs                                0s 114MB
Jun 29 09:27:37 Starting compiler/backend/semantics
Jun 29 09:30:40 Finished compiler/backend/semantics                            3m02s   2GB
Jun 29 09:30:41 Starting compiler/backend/reg_alloc/proofs
Jun 29 09:30:43 Finished compiler/backend/reg_alloc/proofs                        1s 115MB
Jun 29 09:30:44 Starting compiler/backend/proofs
Jun 29 09:31:28 Finished compiler/backend/proofs                                 43s   3GB
Jun 29 09:31:29 Starting compiler/backend/serialiser
Jun 29 09:31:31 Finished compiler/backend/serialiser                              1s 148MB
Jun 29 09:31:32 Starting compiler/encoders/x64/proofs
Jun 29 09:31:34 Finished compiler/encoders/x64/proofs                             0s  97MB
Jun 29 09:31:35 Starting compiler/encoders/arm7/proofs
Jun 29 09:43:55 Finished compiler/encoders/arm7/proofs                        12m19s   5GB
Jun 29 09:43:56 Starting compiler/encoders/arm8/proofs
Jun 29 09:51:42 Finished compiler/encoders/arm8/proofs                         7m44s   5GB
Jun 29 09:51:43 Starting compiler/encoders/arm8_asl/proofs
Jun 29 10:08:38 Finished compiler/encoders/arm8_asl/proofs                    16m53s   4GB
Jun 29 10:08:38 Starting compiler/encoders/mips/proofs
Jun 29 10:19:22 Finished compiler/encoders/mips/proofs                        10m42s   6GB
Jun 29 10:19:23 Starting compiler/encoders/riscv/proofs
Jun 29 10:28:37 Finished compiler/encoders/riscv/proofs                        9m13s   5GB
Jun 29 10:28:38 Starting compiler/encoders/ag32/proofs
Jun 29 10:31:45 Finished compiler/encoders/ag32/proofs                         3m05s   2GB
Jun 29 10:31:45 Starting compiler/backend/x64/proofs
Jun 29 10:31:48 Finished compiler/backend/x64/proofs                              1s 232MB
Jun 29 10:31:49 Starting compiler/backend/arm7/proofs
Jun 29 10:32:27 Finished compiler/backend/arm7/proofs                            37s   2GB
Jun 29 10:32:28 Starting compiler/backend/arm8/proofs
Jun 29 10:33:07 Finished compiler/backend/arm8/proofs                            37s   2GB
Jun 29 10:33:08 Starting compiler/backend/arm8_asl
Jun 29 10:33:36 Finished compiler/backend/arm8_asl                               27s   2GB
Jun 29 10:33:37 Starting compiler/backend/mips/proofs
Jun 29 10:34:15 Finished compiler/backend/mips/proofs                            38s   2GB
Jun 29 10:34:16 Starting compiler/backend/riscv/proofs
Jun 29 10:34:55 Finished compiler/backend/riscv/proofs                           37s   2GB
Jun 29 10:34:56 Starting compiler/backend/ag32/proofs
Jun 29 10:44:22 Finished compiler/backend/ag32/proofs                          9m24s   5GB
Jun 29 10:44:23 Starting compiler/backend/cv_compute
Jun 29 10:44:52 Finished compiler/backend/cv_compute                             28s   1GB
Jun 29 10:44:53 Starting cv_translator
Jun 29 10:49:45 Finished cv_translator                                         4m51s   3GB
Jun 29 10:49:46 Starting candle
Jun 29 10:49:46 Finished candle                                                   0s   7MB
Jun 29 10:49:47 Starting candle/set-theory
Jun 29 10:50:19 Finished candle/set-theory                                       30s 913MB
Jun 29 10:50:19 Starting candle/syntax-lib
Jun 29 10:50:21 Finished candle/syntax-lib                                        0s  81MB
Jun 29 10:50:22 Starting candle/standard
Jun 29 10:50:23 Finished candle/standard                                          0s   7MB
Jun 29 10:50:23 Starting candle/standard/syntax
Jun 29 10:50:39 Finished candle/standard/syntax                                  14s 773MB
Jun 29 10:50:40 Starting candle/standard/syntax/little_theories
Jun 29 10:51:54 Finished candle/standard/syntax/little_theories                1m12s   1GB
Jun 29 10:51:54 Starting candle/standard/semantics
Jun 29 10:54:07 Finished candle/standard/semantics                             2m11s   2GB
Jun 29 10:54:08 Starting candle/standard/monadic
Jun 29 10:54:10 Finished candle/standard/monadic                                  0s 125MB
Jun 29 10:54:11 Starting candle/standard/ml_kernel
Jun 29 10:56:15 Finished candle/standard/ml_kernel                             2m03s   4GB
Jun 29 10:56:16 Starting candle/overloading
Jun 29 10:56:17 Finished candle/overloading                                       0s   7MB
Jun 29 10:56:17 Starting candle/overloading/syntax
Jun 29 10:59:31 Finished candle/overloading/syntax                             3m13s   2GB
Jun 29 10:59:32 Starting candle/overloading/semantics
Jun 29 11:09:03 Finished candle/overloading/semantics                          9m30s   5GB
Jun 29 11:09:04 Starting candle/overloading/monadic
Jun 29 11:11:07 Finished candle/overloading/monadic                            2m02s   1GB
Jun 29 11:11:08 Starting candle/overloading/ml_kernel
Jun 29 11:17:50 Finished candle/overloading/ml_kernel                          6m41s   6GB
Jun 29 11:17:51 Starting candle/overloading/ml_checker
Jun 29 11:20:28 Finished candle/overloading/ml_checker                         2m35s   6GB
Jun 29 11:20:28 Starting candle/prover
Jun 29 11:20:31 Finished candle/prover                                            1s 180MB
Jun 29 11:20:32 Starting candle/prover/compute
Jun 29 11:20:34 Finished candle/prover/compute                                    1s 153MB
Jun 29 11:20:35 Starting pancake
Jun 29 11:20:37 Finished pancake                                                  1s 139MB
Jun 29 11:20:37 Starting pancake/semantics
Jun 29 11:23:33 Finished pancake/semantics                                     2m54s   2GB
Jun 29 11:23:33 Starting pancake/parser
Jun 29 11:24:13 Finished pancake/parser                                          38s 534MB
Jun 29 11:24:14 Starting pancake/static_checker
Jun 29 11:26:48 Finished pancake/static_checker                                2m32s   1GB
Jun 29 11:26:49 Starting pancake/proofs
Jun 29 11:44:12 Finished pancake/proofs                                       17m21s   4GB
Jun 29 11:44:13 Starting compiler/dafny
Jun 29 11:44:36 Finished compiler/dafny                                          22s 651MB
Jun 29 11:44:37 Starting compiler/dafny/translation
Jun 29 11:54:41 Finished compiler/dafny/translation                           10m03s   7GB
Jun 29 11:54:42 Starting compiler/dafny/compilation
Jun 29 11:56:27 Finished compiler/dafny/compilation                            1m43s   6GB
Jun 29 11:56:28 Starting compiler/dafny/semantics
Jun 29 11:57:05 Finished compiler/dafny/semantics                                36s 507MB
Jun 29 11:57:06 Starting compiler/dafny/proofs
Jun 29 11:58:45 Finished compiler/dafny/proofs                                 1m38s   1GB
Jun 29 11:58:46 Starting compiler/dafny/vcg
Jun 29 11:58:48 Finished compiler/dafny/vcg                                       0s 108MB
Jun 29 11:58:49 Starting compiler/dafny/vcg/examples
Jun 29 11:59:19 Finished compiler/dafny/vcg/examples                             29s   2GB
Jun 29 11:59:20 Starting compiler/scheme
Jun 29 11:59:47 Finished compiler/scheme                                         26s   1GB
Jun 29 11:59:48 Starting compiler/scheme/translation
Jun 29 12:06:30 Finished compiler/scheme/translation                           6m41s   8GB
Jun 29 12:06:31 Starting compiler/scheme/compilation
Jun 29 12:07:45 Finished compiler/scheme/compilation                           1m13s   3GB
Jun 29 12:07:45 Starting compiler/scheme/proofs
Jun 29 12:14:29 Finished compiler/scheme/proofs                                6m42s   2GB
Jun 29 12:14:29 Starting characteristic/examples
Jun 29 12:16:02 Finished characteristic/examples                               1m31s   5GB
Jun 29 12:16:03 Starting tutorial/solutions
Jun 29 12:18:49 Finished tutorial/solutions                                    2m45s   7GB
Jun 29 12:18:50 Starting translator/monadic/examples
Jun 29 12:21:56 Finished translator/monadic/examples                           3m04s   4GB
Jun 29 12:21:57 Starting examples
Jun 29 12:24:22 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
catProgTheory                                              (46s)  [3/22]     OK
Starting work on doubleArgProgTheory
quicksortProgTheory                                        (49s)  [4/22]     OK
Starting work on array_searchProgTheory
divTheory                                                  (55s)  [5/22]     OK
Starting work on echoProgTheory
doubleArgProgTheory                                        (31s)  [6/22]     OK
Starting work on filterProgTheory
array_searchProgTheory                                     (42s)  [7/22]     OK
Starting work on grepProgTheory
echoProgTheory                                             (37s)  [8/22]     OK
Starting work on helloErrProgTheory
diffProgTheory                                             (55s)  [9/22]     OK
Starting work on helloProgTheory
filterProgTheory                                           (51s)        FAIL<1>
grepProgTheory                                             (39s)         killed
helloErrProgTheory                                         (36s)         killed
helloProgTheory                                            (33s)         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.7s to build
 Full log: /scratch/cakeml/regression3/cakeml-3416/examples/.hol/logs/filterProgTheory