CakeML Regression Test

Job 3421

CakeML:ad5fbb61e3c7b92981fda381bc617a75b9f5d0e3
  Remove more INCLUDES lines [Jun 25 07:17:34]
#1427 (holprojs)
Merging into:d4ce405e105cef3b7901d0f89694c41597bb8b22
  Merge pull request #1431 from CakeML/pb_str_to_core [Jul 04 16:05:56]
HOL:1d9f33ad168d3823cc070223d83ea660d86dcb58
  Invert ParoundPrec, and use it to bracket stacked suffixes [Jun 24 01:00:44]
Machine:timtam

Jul 04 16:09:13 Claimed job
Jul 04 16:09:21 Reusing HOL
Jul 04 16:09:29 Starting developers
Jul 04 16:10:17 Finished developers                                              47s   1GB
Jul 04 16:10:18 Starting developers/bin
Jul 04 16:10:29 Finished developers/bin                                           9s   1GB
Jul 04 16:10:29 Starting misc
Jul 04 16:11:19 Finished misc                                                    48s   1GB
Jul 04 16:11:20 Starting compiler/proofs
Jul 04 17:23:58 Finished compiler/proofs                                    1h12m37s   8GB
Jul 04 17:23:59 Starting compiler/bootstrap/compilation/x64/64/proofs
Jul 05 00:10:18 Finished compiler/bootstrap/compilation/x64/64/proofs       6h46m18s 101GB
Aug 03 08:06:53 Resuming semantics/ffi
Aug 03 08:07:14 Finished semantics/ffi                                           20s   1GB
Aug 03 08:07:15 Starting semantics
Aug 03 08:07:21 Finished semantics                                                4s   1GB
Aug 03 08:07:22 Starting semantics/proofs
Aug 03 08:07:50 Finished semantics/proofs                                        27s   1GB
Aug 03 08:07:51 Starting semantics/alt_semantics
Aug 03 08:08:12 Finished semantics/alt_semantics                                 20s   1GB
Aug 03 08:08:13 Starting semantics/alt_semantics/proofs
Aug 03 08:12:03 Finished semantics/alt_semantics/proofs                        3m49s   1GB
Aug 03 08:12:04 Starting basis/pure
Aug 03 08:12:10 Finished basis/pure                                               5s   1GB
Aug 03 08:12:11 Starting translator
Aug 03 08:13:24 Finished translator                                            1m11s   2GB
Aug 03 08:13:24 Starting compiler/parsing
Aug 03 08:14:14 Finished compiler/parsing                                        48s   2GB
Aug 03 08:14:15 Starting characteristic
Aug 03 08:14:21 Finished characteristic                                           4s   1GB
Aug 03 08:14:22 Starting translator/monadic
Aug 03 08:14:27 Finished translator/monadic                                       4s   1GB
Aug 03 08:14:28 Starting translator/monadic/monad_base
Aug 03 08:14:34 Finished translator/monadic/monad_base                            4s   1GB
Aug 03 08:14:35 Starting profiler
Aug 03 08:15:06 Finished profiler                                                30s   1GB
Aug 03 08:15:07 Starting basis
Aug 03 08:16:56 Finished basis                                                 1m47s   4GB
Aug 03 08:16:57 Starting compiler
Aug 03 08:17:02 Finished compiler                                                 4s   1GB
Aug 03 08:17:03 Starting compiler/inference
Aug 03 08:17:09 Finished compiler/inference                                       4s   1GB
Aug 03 08:17:10 Starting compiler/backend/reg_alloc
Aug 03 08:17:16 Finished compiler/backend/reg_alloc                               4s   1GB
Aug 03 08:17:17 Starting compiler/backend/gc
Aug 03 08:17:22 Finished compiler/backend/gc                                      4s   1GB
Aug 03 08:17:23 Starting compiler/backend
Aug 03 08:17:29 Finished compiler/backend                                         4s   1GB
Aug 03 08:17:30 Starting compiler/encoders/asm
Aug 03 08:17:35 Finished compiler/encoders/asm                                    4s   1GB
Aug 03 08:17:36 Starting compiler/encoders/x64
Aug 03 08:17:42 Finished compiler/encoders/x64                                    4s   1GB
Aug 03 08:17:43 Starting compiler/encoders/arm7
Aug 03 08:17:48 Finished compiler/encoders/arm7                                   4s   1GB
Aug 03 08:17:49 Starting compiler/encoders/arm8
Aug 03 08:17:55 Finished compiler/encoders/arm8                                   4s   1GB
Aug 03 08:17:56 Starting compiler/encoders/arm8_asl
Aug 03 08:18:12 Finished compiler/encoders/arm8_asl                              15s   1GB
Aug 03 08:18:13 Starting compiler/encoders/mips
Aug 03 08:18:19 Finished compiler/encoders/mips                                   4s   1GB
Aug 03 08:18:19 Starting compiler/encoders/riscv
Aug 03 08:18:25 Finished compiler/encoders/riscv                                  4s   1GB
Aug 03 08:18:26 Starting compiler/encoders/ag32
Aug 03 08:18:32 Finished compiler/encoders/ag32                                   4s   1GB
Aug 03 08:18:32 Starting compiler/encoders/tests
Aug 03 08:18:38 Finished compiler/encoders/tests                                  4s   1GB
Aug 03 08:18:39 Starting compiler/encoders/monadic_enc
Aug 03 08:19:04 Finished compiler/encoders/monadic_enc                           24s   1GB
Aug 03 08:19:05 Starting compiler/backend/x64
Aug 03 08:19:11 Finished compiler/backend/x64                                     4s   1GB
Aug 03 08:19:12 Starting compiler/backend/arm7
Aug 03 08:19:17 Finished compiler/backend/arm7                                    4s   1GB
Aug 03 08:19:18 Starting compiler/backend/arm8
Aug 03 08:19:24 Finished compiler/backend/arm8                                    4s   1GB
Aug 03 08:19:25 Starting compiler/backend/mips
Aug 03 08:19:31 Finished compiler/backend/mips                                    4s   1GB
Aug 03 08:19:31 Starting compiler/backend/riscv
Aug 03 08:19:37 Finished compiler/backend/riscv                                   4s   1GB
Aug 03 08:19:38 Starting compiler/backend/ag32
Aug 03 08:20:44 Finished compiler/backend/ag32                                 1m04s   1GB
Aug 03 08:20:45 Starting compiler/backend/pattern_matching
Aug 03 08:20:50 Finished compiler/backend/pattern_matching                        4s   1GB
Aug 03 08:20:51 Starting compiler/parsing/ocaml
Aug 03 08:23:06 Finished compiler/parsing/ocaml                                2m13s   1GB
Aug 03 08:23:07 Starting compiler/printing
Aug 03 08:24:08 Finished compiler/printing                                     1m00s   1GB
Aug 03 08:24:09 Starting compiler/parsing/proofs
Aug 03 08:24:15 Finished compiler/parsing/proofs                                  5s   1GB
Aug 03 08:24:16 Starting compiler/inference/proofs
Aug 03 08:24:22 Finished compiler/inference/proofs                                5s   1GB
Aug 03 08:24:23 Starting compiler/backend/semantics
Aug 03 08:27:38 Finished compiler/backend/semantics                            3m14s   3GB
Aug 03 08:27:39 Starting compiler/backend/reg_alloc/proofs
Aug 03 08:27:45 Finished compiler/backend/reg_alloc/proofs                        5s   1GB
Aug 03 08:27:46 Starting compiler/backend/proofs
Aug 03 08:28:34 Finished compiler/backend/proofs                                 47s   2GB
Aug 03 08:28:34 Starting compiler/backend/serialiser
Aug 03 08:28:40 Finished compiler/backend/serialiser                              4s   1GB
Aug 03 08:28:41 Starting compiler/encoders/x64/proofs
Aug 03 08:28:47 Finished compiler/encoders/x64/proofs                             4s   1GB
Aug 03 08:28:48 Starting compiler/encoders/arm7/proofs
Aug 03 08:41:55 Finished compiler/encoders/arm7/proofs                        13m05s   8GB
Aug 03 08:41:55 Starting compiler/encoders/arm8/proofs
Aug 03 08:50:19 Finished compiler/encoders/arm8/proofs                         8m22s   3GB
Aug 03 08:50:20 Starting compiler/encoders/arm8_asl/proofs
Aug 03 09:08:03 Finished compiler/encoders/arm8_asl/proofs                    17m41s   3GB
Aug 03 09:08:04 Starting compiler/encoders/mips/proofs
Aug 03 09:19:26 Finished compiler/encoders/mips/proofs                        11m20s   5GB
Aug 03 09:19:27 Starting compiler/encoders/riscv/proofs
Aug 03 09:29:23 Finished compiler/encoders/riscv/proofs                        9m55s   4GB
Aug 03 09:29:24 Starting compiler/encoders/ag32/proofs
Aug 03 09:32:35 Finished compiler/encoders/ag32/proofs                         3m09s   1GB
Aug 03 09:32:36 Starting compiler/backend/x64/proofs
Aug 03 09:32:41 Finished compiler/backend/x64/proofs                              4s   1GB
Aug 03 09:32:42 Starting compiler/backend/arm7/proofs
Aug 03 09:33:22 Finished compiler/backend/arm7/proofs                            39s   2GB
Aug 03 09:33:23 Starting compiler/backend/arm8/proofs
Aug 03 09:34:02 Finished compiler/backend/arm8/proofs                            38s   2GB
Aug 03 09:34:03 Starting compiler/backend/arm8_asl
Aug 03 09:34:28 Finished compiler/backend/arm8_asl                               24s   1GB
Aug 03 09:34:29 Starting compiler/backend/mips/proofs
Aug 03 09:35:11 Finished compiler/backend/mips/proofs                            41s   2GB
Aug 03 09:35:12 Starting compiler/backend/riscv/proofs
Aug 03 09:35:56 Finished compiler/backend/riscv/proofs                           42s   2GB
Aug 03 09:35:57 Starting compiler/backend/ag32/proofs
Aug 03 09:45:46 Finished compiler/backend/ag32/proofs                          9m48s   5GB
Aug 03 09:45:47 Starting compiler/backend/cv_compute
Aug 03 09:46:20 Finished compiler/backend/cv_compute                             32s   1GB
Aug 03 09:46:21 Starting cv_translator
Aug 03 09:51:42 Finished cv_translator                                         5m20s   4GB
Aug 03 09:51:43 Starting candle
Aug 03 09:51:49 Finished candle                                                   4s   1GB
Aug 03 09:51:50 Starting candle/set-theory
Aug 03 09:52:26 Finished candle/set-theory                                       35s   1GB
Aug 03 09:52:27 Starting candle/syntax-lib
Aug 03 09:52:33 Finished candle/syntax-lib                                        5s   1GB
Aug 03 09:52:34 Starting candle/standard
Aug 03 09:52:39 Finished candle/standard                                          4s   1GB
Aug 03 09:52:40 Starting candle/standard/syntax
Aug 03 09:52:59 Finished candle/standard/syntax                                  18s   1GB
Aug 03 09:53:00 Starting candle/standard/syntax/little_theories
Aug 03 09:54:18 Finished candle/standard/syntax/little_theories                1m17s   1GB
Aug 03 09:54:19 Starting candle/standard/semantics
Aug 03 09:56:40 Finished candle/standard/semantics                             2m19s   2GB
Aug 03 09:56:41 Starting candle/standard/monadic
Aug 03 09:56:47 Finished candle/standard/monadic                                  5s   1GB
Aug 03 09:56:48 Starting candle/standard/ml_kernel
Aug 03 09:58:59 Finished candle/standard/ml_kernel                             2m10s   5GB
Aug 03 09:59:00 Starting candle/overloading
Aug 03 09:59:06 Finished candle/overloading                                       5s   1GB
Aug 03 09:59:06 Starting candle/overloading/syntax
Aug 03 09:59:12 Finished candle/overloading/syntax                                4s   1GB
Aug 03 09:59:13 Starting candle/overloading/semantics
Aug 03 09:59:19 Finished candle/overloading/semantics                             4s   1GB
Aug 03 09:59:20 Starting candle/overloading/monadic
Aug 03 09:59:25 Finished candle/overloading/monadic                               4s   1GB
Aug 03 09:59:26 Starting candle/overloading/ml_kernel
Aug 03 09:59:32 Finished candle/overloading/ml_kernel                             4s   1GB
Aug 03 09:59:33 Starting candle/overloading/ml_checker
Aug 03 09:59:39 Finished candle/overloading/ml_checker                            4s   1GB
Aug 03 09:59:40 Starting candle/prover
Aug 03 09:59:45 Finished candle/prover                                            4s   1GB
Aug 03 09:59:46 Starting candle/prover/compute
Aug 03 09:59:52 Finished candle/prover/compute                                    4s   1GB
Aug 03 09:59:53 Starting pancake
Aug 03 09:59:59 Finished pancake                                                  4s   1GB
Aug 03 09:59:59 Starting pancake/semantics
Aug 03 10:03:06 Finished pancake/semantics                                     3m05s   2GB
Aug 03 10:03:06 Starting pancake/parser
Aug 03 10:03:50 Finished pancake/parser                                          42s   1GB
Aug 03 10:03:51 Starting pancake/static_checker
Aug 03 10:06:28 Finished pancake/static_checker                                2m36s   1GB
Aug 03 10:06:29 Starting pancake/proofs
Aug 03 10:24:00 Finished pancake/proofs                                       17m29s   5GB
Aug 03 10:24:00 Starting compiler/dafny
Aug 03 10:24:29 Finished compiler/dafny                                          28s   1GB
Aug 03 10:24:30 Starting compiler/dafny/translation
Aug 03 10:34:35 Finished compiler/dafny/translation                           10m03s   7GB
Aug 03 10:34:36 Starting compiler/dafny/compilation
Aug 03 10:36:27 Finished compiler/dafny/compilation                            1m50s   5GB
Aug 03 10:36:28 Starting compiler/dafny/semantics
Aug 03 10:37:10 Finished compiler/dafny/semantics                                41s   1GB
Aug 03 10:37:11 Starting compiler/dafny/proofs
Aug 03 10:38:56 Finished compiler/dafny/proofs                                 1m43s   1GB
Aug 03 10:38:57 Starting compiler/dafny/vcg
Aug 03 10:39:03 Finished compiler/dafny/vcg                                       5s   1GB
Aug 03 10:39:04 Starting compiler/dafny/vcg/examples
Aug 03 10:39:36 Finished compiler/dafny/vcg/examples                             31s   1GB
Aug 03 10:39:37 Starting compiler/scheme
Aug 03 10:40:07 Finished compiler/scheme                                         29s   1GB
Aug 03 10:40:08 Starting compiler/scheme/translation
Aug 03 10:46:52 Finished compiler/scheme/translation                           6m42s   6GB
Aug 03 10:46:53 Starting compiler/scheme/compilation
Aug 03 10:48:17 Finished compiler/scheme/compilation                           1m23s   4GB
Aug 03 10:48:18 Starting compiler/scheme/proofs
Aug 03 10:55:10 Finished compiler/scheme/proofs                                6m51s   2GB
Aug 03 10:55:11 Starting characteristic/examples
Aug 03 10:56:47 Finished characteristic/examples                               1m35s   5GB
Aug 03 10:56:48 Starting tutorial/solutions
Aug 03 10:56:54 Finished tutorial/solutions                                       4s   1GB
Aug 03 10:56:54 Starting translator/monadic/examples
Aug 03 10:57:00 Finished translator/monadic/examples                              4s   1GB
Aug 03 10:57:01 Starting examples
Aug 03 10:59:30 FAILED: examples
  HOLORIG=/scratch/cakeml/regression2/cakeml-3421/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                                                 (32s)  [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                                                  (57s)  [5/22]     OK
Starting work on echoProgTheory
doubleArgProgTheory                                        (30s)  [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                                             (39s)  [9/22]     OK
Starting work on helloProgTheory
filterProgTheory                                           (51s)        FAIL<1>
grepProgTheory                                             (42s)         killed
helloErrProgTheory                                         (34s)         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 45.4s to build
 Full log: /scratch/cakeml/regression2/cakeml-3421/examples/.hol/logs/filterProgTheory