CakeML Regression Test

Job 3420

CakeML:ad5fbb61e3c7b92981fda381bc617a75b9f5d0e3
  Remove more INCLUDES lines [Jun 25 07:17:34]
#1427 (holprojs)
Merging into: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:pavlova

Jul 03 02:22:01 Claimed job
Jul 03 02:22:11 Reusing HOL
Jul 03 02:23:04 Starting developers
Jul 03 02:23:52 Finished developers                                              47s   1GB
Jul 03 02:23:53 Starting developers/bin
Jul 03 02:24:02 Finished developers/bin                                           8s   1GB
Jul 03 02:24:03 Starting misc
Jul 03 02:24:51 Finished misc                                                    47s   1GB
Jul 03 02:24:52 Starting compiler/proofs
Jul 03 03:37:51 Finished compiler/proofs                                    1h12m57s  10GB
Jul 03 03:37:52 Starting compiler/bootstrap/compilation/x64/64/proofs
Jul 03 10:29:34 Finished compiler/bootstrap/compilation/x64/64/proofs       6h51m40s 111GB
Jul 03 10:29:35 Starting semantics/ffi
Jul 03 10:29:57 Finished semantics/ffi                                           21s   1GB
Jul 03 10:29:58 Starting semantics
Jul 03 10:30:03 Finished semantics                                                4s   1GB
Jul 03 10:30:04 Starting semantics/proofs
Jul 03 10:30:32 Finished semantics/proofs                                        27s   1GB
Jul 03 10:30:33 Starting semantics/alt_semantics
Jul 03 10:30:54 Finished semantics/alt_semantics                                 20s   1GB
Jul 03 10:30:55 Starting semantics/alt_semantics/proofs
Jul 03 10:34:48 Finished semantics/alt_semantics/proofs                        3m51s   1GB
Jul 03 10:34:48 Starting basis/pure
Jul 03 10:34:54 Finished basis/pure                                               5s   1GB
Jul 03 10:34:55 Starting translator
Jul 03 10:36:11 Finished translator                                            1m14s   3GB
Jul 03 10:36:12 Starting compiler/parsing
Jul 03 10:37:01 Finished compiler/parsing                                        47s   2GB
Jul 03 10:37:01 Starting characteristic
Jul 03 10:37:07 Finished characteristic                                           4s   1GB
Jul 03 10:37:08 Starting translator/monadic
Jul 03 10:37:14 Finished translator/monadic                                       4s   1GB
Jul 03 10:37:15 Starting translator/monadic/monad_base
Jul 03 10:37:20 Finished translator/monadic/monad_base                            4s   1GB
Jul 03 10:37:21 Starting profiler
Jul 03 10:37:54 Finished profiler                                                32s   1GB
Jul 03 10:37:55 Starting basis
Jul 03 10:39:42 Finished basis                                                 1m46s   4GB
Jul 03 10:39:43 Starting compiler
Jul 03 10:39:49 Finished compiler                                                 5s   1GB
Jul 03 10:39:50 Starting compiler/inference
Jul 03 10:39:55 Finished compiler/inference                                       4s   1GB
Jul 03 10:39:56 Starting compiler/backend/reg_alloc
Jul 03 10:40:02 Finished compiler/backend/reg_alloc                               4s   1GB
Jul 03 10:40:03 Starting compiler/backend/gc
Jul 03 10:40:08 Finished compiler/backend/gc                                      4s   1GB
Jul 03 10:40:09 Starting compiler/backend
Jul 03 10:40:15 Finished compiler/backend                                         4s   1GB
Jul 03 10:40:16 Starting compiler/encoders/asm
Jul 03 10:40:22 Finished compiler/encoders/asm                                    4s   1GB
Jul 03 10:40:22 Starting compiler/encoders/x64
Jul 03 10:40:28 Finished compiler/encoders/x64                                    4s   1GB
Jul 03 10:40:29 Starting compiler/encoders/arm7
Jul 03 10:40:34 Finished compiler/encoders/arm7                                   4s   1GB
Jul 03 10:40:35 Starting compiler/encoders/arm8
Jul 03 10:40:41 Finished compiler/encoders/arm8                                   4s   1GB
Jul 03 10:40:42 Starting compiler/encoders/arm8_asl
Jul 03 10:40:58 Finished compiler/encoders/arm8_asl                              15s   1GB
Jul 03 10:40:59 Starting compiler/encoders/mips
Jul 03 10:41:05 Finished compiler/encoders/mips                                   4s   1GB
Jul 03 10:41:05 Starting compiler/encoders/riscv
Jul 03 10:41:11 Finished compiler/encoders/riscv                                  5s   1GB
Jul 03 10:41:12 Starting compiler/encoders/ag32
Jul 03 10:41:18 Finished compiler/encoders/ag32                                   4s   1GB
Jul 03 10:41:19 Starting compiler/encoders/tests
Jul 03 10:41:24 Finished compiler/encoders/tests                                  4s   1GB
Jul 03 10:41:25 Starting compiler/encoders/monadic_enc
Jul 03 10:41:50 Finished compiler/encoders/monadic_enc                           24s   1GB
Jul 03 10:41:51 Starting compiler/backend/x64
Jul 03 10:41:57 Finished compiler/backend/x64                                     4s   1GB
Jul 03 10:41:58 Starting compiler/backend/arm7
Jul 03 10:42:03 Finished compiler/backend/arm7                                    4s   1GB
Jul 03 10:42:04 Starting compiler/backend/arm8
Jul 03 10:42:10 Finished compiler/backend/arm8                                    4s   1GB
Jul 03 10:42:11 Starting compiler/backend/mips
Jul 03 10:42:16 Finished compiler/backend/mips                                    4s   1GB
Jul 03 10:42:17 Starting compiler/backend/riscv
Jul 03 10:42:23 Finished compiler/backend/riscv                                   4s   1GB
Jul 03 10:42:24 Starting compiler/backend/ag32
Jul 03 10:43:30 Finished compiler/backend/ag32                                 1m05s   2GB
Jul 03 10:43:31 Starting compiler/backend/pattern_matching
Jul 03 10:43:36 Finished compiler/backend/pattern_matching                        4s   1GB
Jul 03 10:43:37 Starting compiler/parsing/ocaml
Jul 03 10:45:51 Finished compiler/parsing/ocaml                                2m13s   1GB
Jul 03 10:45:52 Starting compiler/printing
Jul 03 10:46:53 Finished compiler/printing                                       59s   1GB
Jul 03 10:46:54 Starting compiler/parsing/proofs
Jul 03 10:46:59 Finished compiler/parsing/proofs                                  4s   1GB
Jul 03 10:47:00 Starting compiler/inference/proofs
Jul 03 10:47:06 Finished compiler/inference/proofs                                4s   1GB
Jul 03 10:47:07 Starting compiler/backend/semantics
Jul 03 10:50:14 Finished compiler/backend/semantics                            3m06s   2GB
Jul 03 10:50:15 Starting compiler/backend/reg_alloc/proofs
Jul 03 10:50:21 Finished compiler/backend/reg_alloc/proofs                        4s   1GB
Jul 03 10:50:22 Starting compiler/backend/proofs
Jul 03 10:51:09 Finished compiler/backend/proofs                                 46s   2GB
Jul 03 10:51:10 Starting compiler/backend/serialiser
Jul 03 10:51:15 Finished compiler/backend/serialiser                              4s   1GB
Jul 03 10:51:16 Starting compiler/encoders/x64/proofs
Jul 03 10:51:22 Finished compiler/encoders/x64/proofs                             4s   1GB
Jul 03 10:51:23 Starting compiler/encoders/arm7/proofs
Jul 03 11:04:05 Finished compiler/encoders/arm7/proofs                        12m41s   5GB
Jul 03 11:04:06 Starting compiler/encoders/arm8/proofs
Jul 03 11:11:51 Finished compiler/encoders/arm8/proofs                         7m44s   3GB
Jul 03 11:11:52 Starting compiler/encoders/arm8_asl/proofs
Jul 03 11:28:57 Finished compiler/encoders/arm8_asl/proofs                    17m03s   3GB
Jul 03 11:28:57 Starting compiler/encoders/mips/proofs
Jul 03 11:40:00 Finished compiler/encoders/mips/proofs                        11m01s   8GB
Jul 03 11:40:01 Starting compiler/encoders/riscv/proofs
Jul 03 11:49:26 Finished compiler/encoders/riscv/proofs                        9m24s   3GB
Jul 03 11:49:27 Starting compiler/encoders/ag32/proofs
Jul 03 11:52:37 Finished compiler/encoders/ag32/proofs                         3m08s   1GB
Jul 03 11:52:37 Starting compiler/backend/x64/proofs
Jul 03 11:52:43 Finished compiler/backend/x64/proofs                              4s   1GB
Jul 03 11:52:44 Starting compiler/backend/arm7/proofs
Jul 03 11:53:24 Finished compiler/backend/arm7/proofs                            39s   2GB
Jul 03 11:53:25 Starting compiler/backend/arm8/proofs
Jul 03 11:54:07 Finished compiler/backend/arm8/proofs                            41s   2GB
Jul 03 11:54:08 Starting compiler/backend/arm8_asl
Jul 03 11:54:34 Finished compiler/backend/arm8_asl                               25s   1GB
Jul 03 11:54:35 Starting compiler/backend/mips/proofs
Jul 03 11:55:17 Finished compiler/backend/mips/proofs                            41s   2GB
Jul 03 11:55:18 Starting compiler/backend/riscv/proofs
Jul 03 11:56:01 Finished compiler/backend/riscv/proofs                           41s   2GB
Jul 03 11:56:02 Starting compiler/backend/ag32/proofs
Jul 03 12:05:33 Finished compiler/backend/ag32/proofs                          9m30s   5GB
Jul 03 12:05:34 Starting compiler/backend/cv_compute
Jul 03 12:06:08 Finished compiler/backend/cv_compute                             32s   1GB
Jul 03 12:06:08 Starting cv_translator
Jul 03 12:11:13 Finished cv_translator                                         5m03s   3GB
Jul 03 12:11:14 Starting candle
Jul 03 12:11:19 Finished candle                                                   4s   1GB
Jul 03 12:11:20 Starting candle/set-theory
Jul 03 12:11:56 Finished candle/set-theory                                       34s   1GB
Jul 03 12:11:56 Starting candle/syntax-lib
Jul 03 12:12:02 Finished candle/syntax-lib                                        4s   1GB
Jul 03 12:12:03 Starting candle/standard
Jul 03 12:12:09 Finished candle/standard                                          4s   1GB
Jul 03 12:12:09 Starting candle/standard/syntax
Jul 03 12:12:29 Finished candle/standard/syntax                                  18s   1GB
Jul 03 12:12:30 Starting candle/standard/syntax/little_theories
Jul 03 12:13:46 Finished candle/standard/syntax/little_theories                1m15s   1GB
Jul 03 12:13:47 Starting candle/standard/semantics
Jul 03 12:16:09 Finished candle/standard/semantics                             2m20s   2GB
Jul 03 12:16:10 Starting candle/standard/monadic
Jul 03 12:16:16 Finished candle/standard/monadic                                  5s   1GB
Jul 03 12:16:17 Starting candle/standard/ml_kernel
Jul 03 12:18:24 Finished candle/standard/ml_kernel                             2m06s   4GB
Jul 03 12:18:25 Starting candle/overloading
Jul 03 12:18:30 Finished candle/overloading                                       4s   1GB
Jul 03 12:18:31 Starting candle/overloading/syntax
Jul 03 12:18:37 Finished candle/overloading/syntax                                4s   1GB
Jul 03 12:18:38 Starting candle/overloading/semantics
Jul 03 12:18:43 Finished candle/overloading/semantics                             4s   1GB
Jul 03 12:18:44 Starting candle/overloading/monadic
Jul 03 12:18:50 Finished candle/overloading/monadic                               4s   1GB
Jul 03 12:18:51 Starting candle/overloading/ml_kernel
Jul 03 12:18:56 Finished candle/overloading/ml_kernel                             4s   1GB
Jul 03 12:18:57 Starting candle/overloading/ml_checker
Jul 03 12:19:03 Finished candle/overloading/ml_checker                            4s   1GB
Jul 03 12:19:04 Starting candle/prover
Jul 03 12:19:09 Finished candle/prover                                            4s   1GB
Jul 03 12:19:10 Starting candle/prover/compute
Jul 03 12:19:16 Finished candle/prover/compute                                    4s   1GB
Jul 03 12:19:17 Starting pancake
Jul 03 12:19:22 Finished pancake                                                  4s   1GB
Jul 03 12:19:23 Starting pancake/semantics
Jul 03 12:22:27 Finished pancake/semantics                                     3m02s   2GB
Jul 03 12:22:28 Starting pancake/parser
Jul 03 12:23:12 Finished pancake/parser                                          43s   1GB
Jul 03 12:23:13 Starting pancake/static_checker
Jul 03 12:25:49 Finished pancake/static_checker                                2m35s   1GB
Jul 03 12:25:50 Starting pancake/proofs
Jul 03 12:43:05 Finished pancake/proofs                                       17m13s   5GB
Jul 03 12:43:06 Starting compiler/dafny
Jul 03 12:43:34 Finished compiler/dafny                                          27s   1GB
Jul 03 12:43:35 Starting compiler/dafny/translation
Jul 03 12:53:51 Finished compiler/dafny/translation                           10m15s   6GB
Jul 03 12:53:52 Starting compiler/dafny/compilation
Jul 03 12:55:43 Finished compiler/dafny/compilation                            1m50s   6GB
Jul 03 12:55:44 Starting compiler/dafny/semantics
Jul 03 12:56:27 Finished compiler/dafny/semantics                                41s   1GB
Jul 03 12:56:28 Starting compiler/dafny/proofs
Jul 03 12:58:11 Finished compiler/dafny/proofs                                 1m42s   1GB
Jul 03 12:58:12 Starting compiler/dafny/vcg
Jul 03 12:58:18 Finished compiler/dafny/vcg                                       5s   1GB
Jul 03 12:58:19 Starting compiler/dafny/vcg/examples
Jul 03 12:58:52 Finished compiler/dafny/vcg/examples                             31s   1GB
Jul 03 12:58:52 Starting compiler/scheme
Jul 03 12:59:23 Finished compiler/scheme                                         29s   1GB
Jul 03 12:59:24 Starting compiler/scheme/translation
Jul 03 13:06:14 Finished compiler/scheme/translation                           6m49s   6GB
Jul 03 13:06:15 Starting compiler/scheme/compilation
Jul 03 13:07:42 Finished compiler/scheme/compilation                           1m26s   4GB
Jul 03 13:07:43 Starting compiler/scheme/proofs
Jul 03 13:14:32 Finished compiler/scheme/proofs                                6m48s   2GB
Jul 03 13:14:33 Starting characteristic/examples
Jul 03 13:16:06 Finished characteristic/examples                               1m32s   5GB
Jul 03 13:16:07 Starting tutorial/solutions
Jul 03 13:16:13 Finished tutorial/solutions                                       4s   1GB
Jul 03 13:16:14 Starting translator/monadic/examples
Jul 03 13:16:19 Finished translator/monadic/examples                              4s   1GB
Jul 03 13:16:20 Starting examples
Jul 03 13:18:45 FAILED: examples
  HOLORIG=/scratch/cakeml/regression/cakeml-3420/examples [ -d "armv8.6-asl-snapshot" ] || ./get-armv8.6-hol-snapshot
Scanning $(HOLDIR)/src/TeX
Scanning $(HOLDIR)/src/bag
Scanning $(HOLDIR)/src/sort
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/examples/algorithms
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)/examples/data-structures/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/src/search
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/sail
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(HOLDIR)/src/floating-point
Scanning $(HOLDIR)/src/monad/more_monads
Scanning $(HOLDIR)/src/update
Scanning $(HOLDIR)/examples/l3-machine-code/common
Scanning $(HOLDIR)/examples/l3-machine-code/lib
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/model
Scanning $(HOLDIR)/examples/machine-code/decompiler
Scanning $(HOLDIR)/examples/l3-machine-code
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/step
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv
Scanning $(HOLDIR)/examples/machine-code/multiword
Scanning $(CAKEMLDIR)/basis
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/candle
Scanning $(CAKEMLDIR)/candle/standard/syntax
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/pl-semantics/lprefix_lub
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/candle/syntax-lib
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/candle/standard/monadic
Scanning $(CAKEMLDIR)/candle/standard/ml_kernel
Scanning $(CAKEMLDIR)/candle/standard/semantics
Scanning $(CAKEMLDIR)/candle/prover/compute
Scanning $(CAKEMLDIR)/candle/prover
Scanning $(CAKEMLDIR)/candle/set-theory
Scanning $(CAKEMLDIR)/candle/standard
Scanning $(CAKEMLDIR)/candle/standard/syntax/little_theories
Scanning $(CAKEMLDIR)/characteristic/examples
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/compiler/encoders/ag32
Scanning $(CAKEMLDIR)/compiler/backend/ag32
Scanning $(HOLDIR)/examples/l3-machine-code/arm/model
Scanning $(HOLDIR)/examples/l3-machine-code/arm/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm7
Scanning $(CAKEMLDIR)/compiler/backend/arm7
Scanning $(CAKEMLDIR)/compiler/encoders/arm8
Scanning $(CAKEMLDIR)/compiler/backend/arm8
Scanning $(HOLDIR)/examples/l3-machine-code/mips/model
Scanning $(HOLDIR)/examples/l3-machine-code/mips/step
Scanning $(CAKEMLDIR)/compiler/encoders/mips
Scanning $(CAKEMLDIR)/compiler/backend/mips
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/model
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/step
Scanning $(CAKEMLDIR)/compiler/encoders/riscv
Scanning $(CAKEMLDIR)/compiler/backend/riscv
Scanning $(HOLDIR)/examples/l3-machine-code/x64/model
Scanning $(HOLDIR)/examples/l3-machine-code/x64/step
Scanning $(CAKEMLDIR)/compiler/encoders/x64
Scanning $(CAKEMLDIR)/compiler/backend/x64
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)/pancake
Scanning $(CAKEMLDIR)/pancake/parser
Scanning $(CAKEMLDIR)/compiler
Scanning $(CAKEMLDIR)/semantics/alt_semantics
Scanning $(CAKEMLDIR)/semantics/alt_semantics/proofs
Scanning $(CAKEMLDIR)/compiler/backend/semantics
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/prog
Scanning $(CAKEMLDIR)/compiler/encoders/riscv/proofs
Scanning $(CAKEMLDIR)/compiler/backend/San
Scanning $(CAKEMLDIR)/compiler/backend/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/ag32/proofs
Scanning $(CAKEMLDIR)/compiler/backend/ag32/proofs
Scanning $(HOLDIR)/examples/l3-machine-code/arm/prog
Scanning $(CAKEMLDIR)/compiler/encoders/arm7/proofs
Scanning $(CAKEMLDIR)/compiler/backend/arm7/proofs
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/prog
Scanning $(CAKEMLDIR)/compiler/encoders/arm8/proofs
Scanning $(CAKEMLDIR)/compiler/backend/arm8/proofs
Scanning $(CAKEMLDIR)/compiler/backend/serialiser
Scanning $(CAKEMLDIR)/compiler/backend/cv_compute
Scanning $(CAKEMLDIR)/compiler/backend/gc
Scanning $(HOLDIR)/examples/l3-machine-code/mips/prog
Scanning $(CAKEMLDIR)/compiler/encoders/mips/proofs
Scanning $(CAKEMLDIR)/compiler/backend/mips/proofs
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/compiler/backend/riscv/proofs
Scanning $(HOLDIR)/examples/l3-machine-code/x64/prog
Scanning $(CAKEMLDIR)/compiler/encoders/x64/proofs
Scanning $(CAKEMLDIR)/compiler/backend/x64/proofs
Scanning $(CAKEMLDIR)/compiler/bootstrap
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/ag32
Scanning $(CAKEMLDIR)/compiler/encoders/monadic_enc
Scanning $(CAKEMLDIR)/compiler/parsing/ocaml
Scanning $(CAKEMLDIR)/compiler/inference/proofs
Scanning $(CAKEMLDIR)/compiler/printing
Scanning $(CAKEMLDIR)/compiler/repl
Scanning $(CAKEMLDIR)/compiler/bootstrap/translation
Scanning $(HOLDIR)/src/num/theories/cv_compute/automation
Scanning $(HOLDIR)/examples/bootstrap
Scanning $(CAKEMLDIR)/cv_translator
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/ag32/32
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/ag32/32/proofs
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/arm8
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/arm8/64
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/arm8/64/proofs
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64/64
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64/64/proofs
Scanning $(CAKEMLDIR)/compiler/dafny
Scanning $(CAKEMLDIR)/compiler/dafny/translation
Scanning $(CAKEMLDIR)/compiler/dafny/compilation
Scanning $(CAKEMLDIR)/compiler/dafny/examples
Scanning $(CAKEMLDIR)/compiler/dafny/examples/output
Scanning $(CAKEMLDIR)/compiler/dafny/semantics
Scanning $(CAKEMLDIR)/compiler/dafny/vcg
Scanning $(CAKEMLDIR)/compiler/dafny/proofs
Scanning $(CAKEMLDIR)/compiler/dafny/vcg/examples
Scanning $(CAKEMLDIR)/compiler/encoders
Scanning $(CAKEMLDIR)/compiler/encoders/tests
Scanning $(CAKEMLDIR)/compiler/inference/tests
Scanning $(CAKEMLDIR)/compiler/parsing/proofs
Scanning $(CAKEMLDIR)/compiler/parsing/tests
Scanning $(CAKEMLDIR)/compiler/printing/test
Scanning $(CAKEMLDIR)/compiler/proofs
Scanning $(CAKEMLDIR)/compiler/scheme
Scanning $(CAKEMLDIR)/compiler/scheme/translation
Scanning $(CAKEMLDIR)/developers/bin
Scanning $(CAKEMLDIR)/compiler/scheme/compilation
Scanning $(CAKEMLDIR)/compiler/scheme/examples
Scanning $(CAKEMLDIR)/compiler/scheme/proofs
Scanning $(CAKEMLDIR)/compiler/scheme/unverified
Scanning $(CAKEMLDIR)/examples/cnf
Scanning $(HOLDIR)/examples/Crypto/AES
Scanning $(HOLDIR)/src/real/analysis
Scanning $(HOLDIR)/src/probability
Scanning $(HOLDIR)/examples/Crypto/DES
Scanning $(HOLDIR)/examples/Crypto/IDEA
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/emit
Scanning $(HOLDIR)/examples/Crypto/TEA
Scanning $(HOLDIR)/examples/Crypto/TWOFISH
Scanning $(HOLDIR)/examples/Crypto
Scanning $(CAKEMLDIR)/examples
Scanning $(CAKEMLDIR)/examples/cnf/array
Scanning $(CAKEMLDIR)/examples/cnf/dist
Scanning $(CAKEMLDIR)/examples/cnf/dist/array
Scanning $(CAKEMLDIR)/examples/cnf/dist/array/compilation
Scanning $(CAKEMLDIR)/examples/cnf/dist/array/compilation/proofs
Scanning $(CAKEMLDIR)/examples/compilation
Scanning $(CAKEMLDIR)/examples/compilation/ag32
Scanning $(CAKEMLDIR)/examples/compilation/ag32/proofs
Scanning $(CAKEMLDIR)/examples/deflate
Scanning $(CAKEMLDIR)/examples/deflate/translation
Scanning $(CAKEMLDIR)/examples/deflate/translation/compilation
Scanning $(CAKEMLDIR)/examples/deflate/translation/compilation/tests
Scanning $(CAKEMLDIR)/examples/flover/Infra
Scanning $(CAKEMLDIR)/examples/flover/semantics
Scanning $(CAKEMLDIR)/examples/flover
Scanning $(CAKEMLDIR)/examples/lpr_checker
Scanning $(CAKEMLDIR)/examples/scpog_checker
Scanning $(CAKEMLDIR)/examples/scpog_checker/array
Scanning $(CAKEMLDIR)/examples/scpog_checker/array/compilation
Scanning $(CAKEMLDIR)/examples/scpog_checker/array/compilation/proofs
Scanning $(CAKEMLDIR)/examples/template
Scanning $(CAKEMLDIR)/examples/template/translation
Scanning $(CAKEMLDIR)/examples/template/compilation
Scanning $(CAKEMLDIR)/examples/vipr
Scanning $(CAKEMLDIR)/examples/vipr/compilation
Scanning $(CAKEMLDIR)/examples/xlrup_checker
Scanning $(CAKEMLDIR)/examples/xlrup_checker/array
Scanning $(CAKEMLDIR)/examples/xlrup_checker/array/compilation
Scanning $(CAKEMLDIR)/examples/xlrup_checker/array/compilation/proofs
Scanning $(CAKEMLDIR)/pancake/semantics
Scanning $(CAKEMLDIR)/pancake/proofs
Scanning $(CAKEMLDIR)/pancake/static_checker
Scanning $(CAKEMLDIR)/pancake/temp
Scanning $(CAKEMLDIR)/profiler
Scanning $(CAKEMLDIR)/translator/okasaki-examples
Scanning $(CAKEMLDIR)/unverified
Scanning $(CAKEMLDIR)/unverified/front-end
Scanning $(CAKEMLDIR)/unverified/hol-light-syntax
Scanning $(CAKEMLDIR)/unverified/ocaml-syntax
Scanning $(CAKEMLDIR)/unverified/ocaml-syntax/lib
Scanning $(CAKEMLDIR)/unverified/ocaml-syntax/tests
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/x64
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/x64/64
Scanned 231 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
catProgTheory                                              (44s)  [3/22]     OK
Starting work on doubleArgProgTheory
quicksortProgTheory                                        (47s)  [4/22]     OK
Starting work on array_searchProgTheory
divTheory                                                  (57s)  [5/22]     OK
Starting work on echoProgTheory
doubleArgProgTheory                                        (30s)  [6/22]     OK
Starting work on filterProgTheory
array_searchProgTheory                                     (42s)  [7/22]     OK
Starting work on grepProgTheory
diffProgTheory                                             (53s)  [8/22]     OK
Starting work on helloErrProgTheory
echoProgTheory                                             (37s)  [9/22]     OK
Starting work on helloProgTheory
filterProgTheory                                           (51s)        FAIL<1>
grepProgTheory                                             (37s)         killed
helloErrProgTheory                                         (33s)         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 44.5s to build
 Full log: /scratch/cakeml/regression/cakeml-3420/examples/.hol/logs/filterProgTheory