Job 3417

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

Jun 29 01:30:54 Claimed job
Jun 29 01:31:01 Reusing HOL
Jun 29 01:31:53 Starting developers
Jun 29 01:32:43 Finished developers                                              48s   1GB
Jun 29 01:32:44 Starting developers/bin
Jun 29 01:32:53 Finished developers/bin                                           7s   1GB
Jun 29 01:32:53 Starting misc
Jun 29 01:34:00 Finished misc                                                  1m05s   1GB
Jun 29 01:34:01 Starting compiler/proofs
Jun 29 02:49:57 Finished compiler/proofs                                    1h15m53s  11GB
Jun 29 02:49:57 Starting compiler/bootstrap/compilation/x64/64/proofs
Jun 29 09:36:25 Finished compiler/bootstrap/compilation/x64/64/proofs       6h46m26s 105GB
Jun 29 09:36:26 Starting semantics/ffi
Jun 29 09:36:47 Finished semantics/ffi                                           20s   1GB
Jun 29 09:36:48 Starting semantics
Jun 29 09:36:54 Finished semantics                                                4s   1GB
Jun 29 09:36:55 Starting semantics/proofs
Jun 29 09:37:23 Finished semantics/proofs                                        26s   1GB
Jun 29 09:37:23 Starting semantics/alt_semantics
Jun 29 09:37:43 Finished semantics/alt_semantics                                 19s   1GB
Jun 29 09:37:44 Starting semantics/alt_semantics/proofs
Jun 29 09:41:38 Finished semantics/alt_semantics/proofs                        3m52s   1GB
Jun 29 09:41:39 Starting basis/pure
Jun 29 09:41:45 Finished basis/pure                                               5s   1GB
Jun 29 09:41:45 Starting translator
Jun 29 09:42:59 Finished translator                                            1m12s   2GB
Jun 29 09:43:00 Starting compiler/parsing
Jun 29 09:43:48 Finished compiler/parsing                                        47s   2GB
Jun 29 09:43:49 Starting characteristic
Jun 29 09:43:55 Finished characteristic                                           5s   1GB
Jun 29 09:43:56 Starting translator/monadic
Jun 29 09:44:01 Finished translator/monadic                                       4s   1GB
Jun 29 09:44:02 Starting translator/monadic/monad_base
Jun 29 09:44:08 Finished translator/monadic/monad_base                            4s   1GB
Jun 29 09:44:08 Starting profiler
Jun 29 09:44:42 Finished profiler                                                32s   1GB
Jun 29 09:44:43 Starting basis
Jun 29 09:46:29 Finished basis                                                 1m45s   4GB
Jun 29 09:46:30 Starting compiler
Jun 29 09:46:35 Finished compiler                                                 4s   1GB
Jun 29 09:46:36 Starting compiler/inference
Jun 29 09:46:42 Finished compiler/inference                                       4s   1GB
Jun 29 09:46:43 Starting compiler/backend/reg_alloc
Jun 29 09:46:48 Finished compiler/backend/reg_alloc                               4s   1GB
Jun 29 09:46:49 Starting compiler/backend/gc
Jun 29 09:46:55 Finished compiler/backend/gc                                      4s   1GB
Jun 29 09:46:55 Starting compiler/backend
Jun 29 09:47:01 Finished compiler/backend                                         4s   1GB
Jun 29 09:47:02 Starting compiler/encoders/asm
Jun 29 09:47:07 Finished compiler/encoders/asm                                    4s   1GB
Jun 29 09:47:08 Starting compiler/encoders/x64
Jun 29 09:47:14 Finished compiler/encoders/x64                                    4s   1GB
Jun 29 09:47:15 Starting compiler/encoders/arm7
Jun 29 09:47:20 Finished compiler/encoders/arm7                                   4s   1GB
Jun 29 09:47:21 Starting compiler/encoders/arm8
Jun 29 09:47:27 Finished compiler/encoders/arm8                                   4s   1GB
Jun 29 09:47:27 Starting compiler/encoders/arm8_asl
Jun 29 11:39:05 Finished compiler/encoders/arm8_asl                         1h51m36s  28GB
Jun 29 11:39:06 Starting compiler/encoders/mips
Jun 29 11:39:14 Finished compiler/encoders/mips                                   7s   1GB
Jun 29 11:39:15 Starting compiler/encoders/riscv
Jun 29 11:39:20 Finished compiler/encoders/riscv                                  4s   1GB
Jun 29 11:39:21 Starting compiler/encoders/ag32
Jun 29 11:39:26 Finished compiler/encoders/ag32                                   4s   1GB
Jun 29 11:39:27 Starting compiler/encoders/tests
Jun 29 11:39:33 Finished compiler/encoders/tests                                  4s   1GB
Jun 29 11:39:34 Starting compiler/encoders/monadic_enc
Jun 29 11:40:00 Finished compiler/encoders/monadic_enc                           24s   1GB
Jun 29 11:40:00 Starting compiler/backend/x64
Jun 29 11:40:06 Finished compiler/backend/x64                                     4s   1GB
Jun 29 11:40:07 Starting compiler/backend/arm7
Jun 29 11:40:12 Finished compiler/backend/arm7                                    4s   1GB
Jun 29 11:40:13 Starting compiler/backend/arm8
Jun 29 11:40:19 Finished compiler/backend/arm8                                    4s   1GB
Jun 29 11:40:20 Starting compiler/backend/mips
Jun 29 11:40:25 Finished compiler/backend/mips                                    4s   1GB
Jun 29 11:40:26 Starting compiler/backend/riscv
Jun 29 11:40:32 Finished compiler/backend/riscv                                   4s   1GB
Jun 29 11:40:32 Starting compiler/backend/ag32
Jun 29 11:41:36 Finished compiler/backend/ag32                                 1m02s   1GB
Jun 29 11:41:37 Starting compiler/backend/pattern_matching
Jun 29 11:41:43 Finished compiler/backend/pattern_matching                        4s   1GB
Jun 29 11:41:43 Starting compiler/parsing/ocaml
Jun 29 11:43:56 Finished compiler/parsing/ocaml                                2m11s   1GB
Jun 29 11:43:57 Starting compiler/printing
Jun 29 11:44:56 Finished compiler/printing                                       58s   1GB
Jun 29 11:44:57 Starting compiler/parsing/proofs
Jun 29 11:45:03 Finished compiler/parsing/proofs                                  4s   1GB
Jun 29 11:45:03 Starting compiler/inference/proofs
Jun 29 11:45:09 Finished compiler/inference/proofs                                4s   1GB
Jun 29 11:45:10 Starting compiler/backend/semantics
Jun 29 11:48:19 Finished compiler/backend/semantics                            3m08s   3GB
Jun 29 11:48:20 Starting compiler/backend/reg_alloc/proofs
Jun 29 11:48:26 Finished compiler/backend/reg_alloc/proofs                        4s   1GB
Jun 29 11:48:27 Starting compiler/backend/proofs
Jun 29 11:49:14 Finished compiler/backend/proofs                                 46s   2GB
Jun 29 11:49:15 Starting compiler/backend/serialiser
Jun 29 11:49:21 Finished compiler/backend/serialiser                              4s   1GB
Jun 29 11:49:21 Starting compiler/encoders/x64/proofs
Jun 29 11:49:27 Finished compiler/encoders/x64/proofs                             4s   1GB
Jun 29 11:49:28 Starting compiler/encoders/arm7/proofs
Jun 29 12:01:53 Finished compiler/encoders/arm7/proofs                        12m24s   5GB
Jun 29 12:01:54 Starting compiler/encoders/arm8/proofs
Jun 29 12:09:57 Finished compiler/encoders/arm8/proofs                         8m02s   3GB
Jun 29 12:09:58 Starting compiler/encoders/arm8_asl/proofs
Jun 29 13:07:08 Finished compiler/encoders/arm8_asl/proofs                    57m09s  11GB
Jun 29 13:07:09 Starting compiler/encoders/mips/proofs
Jun 29 13:18:09 Finished compiler/encoders/mips/proofs                        10m59s   6GB
Jun 29 13:18:10 Starting compiler/encoders/riscv/proofs
Jun 29 13:27:51 Finished compiler/encoders/riscv/proofs                        9m39s   3GB
Jun 29 13:27:52 Starting compiler/encoders/ag32/proofs
Jun 29 13:31:05 Finished compiler/encoders/ag32/proofs                         3m12s   2GB
Jun 29 13:31:06 Starting compiler/backend/x64/proofs
Jun 29 13:31:11 Finished compiler/backend/x64/proofs                              4s   1GB
Jun 29 13:31:12 Starting compiler/backend/arm7/proofs
Jun 29 13:31:52 Finished compiler/backend/arm7/proofs                            38s   2GB
Jun 29 13:31:53 Starting compiler/backend/arm8/proofs
Jun 29 13:32:33 Finished compiler/backend/arm8/proofs                            39s   2GB
Jun 29 13:32:34 Starting compiler/backend/arm8_asl
Jun 29 13:33:02 Finished compiler/backend/arm8_asl                               26s   2GB
Jun 29 13:33:02 Starting compiler/backend/mips/proofs
Jun 29 13:33:44 Finished compiler/backend/mips/proofs                            41s   2GB
Jun 29 13:33:45 Starting compiler/backend/riscv/proofs
Jun 29 13:34:28 Finished compiler/backend/riscv/proofs                           42s   2GB
Jun 29 13:34:29 Starting compiler/backend/ag32/proofs
Jun 29 13:44:26 Finished compiler/backend/ag32/proofs                          9m56s   4GB
Jun 29 13:44:27 Starting compiler/backend/cv_compute
Jun 29 13:45:01 Finished compiler/backend/cv_compute                             32s   1GB
Jun 29 13:45:02 Starting cv_translator
Jun 29 13:50:13 Finished cv_translator                                         5m10s   3GB
Jun 29 13:50:14 Starting candle
Jun 29 13:50:20 Finished candle                                                   4s   1GB
Jun 29 13:50:21 Starting candle/set-theory
Jun 29 13:50:57 Finished candle/set-theory                                       35s   1GB
Jun 29 13:50:57 Starting candle/syntax-lib
Jun 29 13:51:03 Finished candle/syntax-lib                                        4s   1GB
Jun 29 13:51:04 Starting candle/standard
Jun 29 13:51:10 Finished candle/standard                                          5s   1GB
Jun 29 13:51:11 Starting candle/standard/syntax
Jun 29 13:51:30 Finished candle/standard/syntax                                  18s   1GB
Jun 29 13:51:31 Starting candle/standard/syntax/little_theories
Jun 29 13:52:50 Finished candle/standard/syntax/little_theories                1m18s   1GB
Jun 29 13:52:51 Starting candle/standard/semantics
Jun 29 13:55:11 Finished candle/standard/semantics                             2m18s   2GB
Jun 29 13:55:12 Starting candle/standard/monadic
Jun 29 13:55:18 Finished candle/standard/monadic                                  5s   1GB
Jun 29 13:55:19 Starting candle/standard/ml_kernel
Jun 29 13:57:28 Finished candle/standard/ml_kernel                             2m08s   4GB
Jun 29 13:57:29 Starting candle/overloading
Jun 29 13:57:34 Finished candle/overloading                                       4s   1GB
Jun 29 13:57:35 Starting candle/overloading/syntax
Jun 29 13:57:41 Finished candle/overloading/syntax                                4s   1GB
Jun 29 13:57:41 Starting candle/overloading/semantics
Jun 29 13:57:47 Finished candle/overloading/semantics                             4s   1GB
Jun 29 13:57:48 Starting candle/overloading/monadic
Jun 29 13:57:53 Finished candle/overloading/monadic                               4s   1GB
Jun 29 13:57:54 Starting candle/overloading/ml_kernel
Jun 29 13:58:00 Finished candle/overloading/ml_kernel                             4s   1GB
Jun 29 13:58:01 Starting candle/overloading/ml_checker
Jun 29 13:58:07 Finished candle/overloading/ml_checker                            4s   1GB
Jun 29 13:58:07 Starting candle/prover
Jun 29 13:58:13 Finished candle/prover                                            4s   1GB
Jun 29 13:58:14 Starting candle/prover/compute
Jun 29 13:58:20 Finished candle/prover/compute                                    4s   1GB
Jun 29 13:58:20 Starting pancake
Jun 29 13:58:26 Finished pancake                                                  4s   1GB
Jun 29 13:58:27 Starting pancake/semantics
Jun 29 14:01:24 Finished pancake/semantics                                     2m56s   2GB
Jun 29 14:01:25 Starting pancake/parser
Jun 29 14:02:10 Finished pancake/parser                                          44s   1GB
Jun 29 14:02:11 Starting pancake/static_checker
Jun 29 14:04:48 Finished pancake/static_checker                                2m36s   1GB
Jun 29 14:04:49 Starting pancake/proofs
Jun 29 14:22:08 Finished pancake/proofs                                       17m17s   6GB
Jun 29 14:22:09 Starting compiler/dafny
Jun 29 14:22:38 Finished compiler/dafny                                          27s   1GB
Jun 29 14:22:39 Starting compiler/dafny/translation
Jun 29 14:32:46 Finished compiler/dafny/translation                           10m06s   6GB
Jun 29 14:32:47 Starting compiler/dafny/compilation
Jun 29 14:34:35 Finished compiler/dafny/compilation                            1m47s   5GB
Jun 29 14:34:36 Starting compiler/dafny/semantics
Jun 29 14:35:19 Finished compiler/dafny/semantics                                41s   1GB
Jun 29 14:35:20 Starting compiler/dafny/proofs
Jun 29 14:37:01 Finished compiler/dafny/proofs                                 1m40s   1GB
Jun 29 14:37:02 Starting compiler/dafny/vcg
Jun 29 14:37:08 Finished compiler/dafny/vcg                                       5s   1GB
Jun 29 14:37:09 Starting compiler/dafny/vcg/examples
Jun 29 14:37:43 Finished compiler/dafny/vcg/examples                             33s   1GB
Jun 29 14:37:44 Starting compiler/scheme
Jun 29 14:38:15 Finished compiler/scheme                                         29s   1GB
Jun 29 14:38:16 Starting compiler/scheme/translation
Jun 29 14:45:01 Finished compiler/scheme/translation                           6m44s   7GB
Jun 29 14:45:01 Starting compiler/scheme/compilation
Jun 29 14:46:27 Finished compiler/scheme/compilation                           1m24s   4GB
Jun 29 14:46:28 Starting compiler/scheme/proofs
Jun 29 14:53:24 Finished compiler/scheme/proofs                                6m55s   2GB
Jun 29 14:53:25 Starting characteristic/examples
Jun 29 14:55:03 Finished characteristic/examples                               1m37s   5GB
Jun 29 14:55:04 Starting tutorial/solutions
Jun 29 14:55:09 Finished tutorial/solutions                                       5s   1GB
Jun 29 14:55:10 Starting translator/monadic/examples
Jun 29 14:55:16 Finished translator/monadic/examples                              4s   1GB
Jun 29 14:55:17 Starting examples
Jun 29 14:57:58 FAILED: examples
  HOLORIG=/scratch/cakeml/regression/cakeml-3417/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 28 theory files
Starting work on regexp_parserTheory
Starting work on source_valuesTheory
Starting work on md5Theory
Starting work on README.md
README.md                                         examples  (0s)             OK
Starting work on quicksortProgTheory
source_valuesTheory                     examples/bootstrap  (2s)  [1/28]     OK
Starting work on source_syntaxTheory
source_syntaxTheory                     examples/bootstrap  (0s)  [2/28]     OK
Starting work on parsingTheory
md5Theory                              examples/Crypto/MD5  (7s)  [3/28]     OK
Starting work on printingTheory
parsingTheory                           examples/bootstrap  (7s)  [4/28]     OK
Finished $(HOLDIR)/examples/Crypto/MD5 [#theories: 1]                  (7.490s) 
Starting work on catProgTheory
regexp_parserTheory      examples/formal-languages/regular (12s)  [5/28]     OK
Finished $(HOLDIR)/examples/formal-languages/regular [#theories: 1]   (12.940s) 
Starting work on lcsTheory
printingTheory                          examples/bootstrap  (5s)  [6/28]     OK
Finished $(HOLDIR)/examples/bootstrap [#theories: 4]                  (15.750s) 
Starting work on divTheory
lcsTheory                                         examples  (6s)  [7/28]     OK
Starting work on diffTheory
quicksortProgTheory                               examples (48s)  [8/28]     OK
Starting work on array_searchProgTheory
diffTheory                                        examples (31s)  [9/28]     OK
Starting work on diffProgTheory
catProgTheory                                     examples (46s) [10/28]     OK
Starting work on doubleArgProgTheory
divTheory                                         examples (56s) [11/28]     OK
Starting work on echoProgTheory
doubleArgProgTheory                               examples (30s) [12/28]     OK
Starting work on filterProgTheory
array_searchProgTheory                            examples (43s) [13/28]     OK
Starting work on grepProgTheory
echoProgTheory                                    examples (37s) [14/28]     OK
Starting work on helloErrProgTheory
diffProgTheory                                    examples (54s) [15/28]     OK
Starting work on helloProgTheory
filterProgTheory                                  examples (52s)        FAIL<1>
grepProgTheory                                    examples (52s)         killed
helloErrProgTheory                                examples (33s)         killed
helloProgTheory                                   examples (33s)         killed
*** Holmake aborted - 1 target failed:
*** filterProgTheory in examples (status 1)
                     DROP (LENGTH (... ... )) (nth_arr i input))))))) bv
 Saved theorem _______ "forward_matching_lines_div_spec"
 Saved theorem _______ "LTAKE_LLENGTH_SOME2"
 Using translator specification word8_fromint_v_thm from theory Word8Prog
 Post condition: POSTv v. seL4_IO input [] * W8ARRAY dummyarr_loc [] * &WORD8 0w v
 Using CF specification w8array_alloc_spec from theory Word8ArrayProof
 Post condition: POSTv v'.
   W8ARRAY v' (REPLICATE 256 0w) * seL4_IO input [] * W8ARRAY dummyarr_loc []
 Using CF specification w8array_substring_spec from theory Word8ArrayProof
 Post condition: POSTv sv.
   W8ARRAY v' (TAKE 256 h ++ DROP (LENGTH h) init) * W8ARRAY dummyarr_loc [] *
   seL4_IO (fromList l)
     (SNOC (IO_event (ExtCall accept_call) [] (ZIP (init,newinit))) events) *
   &STRING_TYPE
     (implode
        (MAP (CHR  w2n) (TAKE 256 (TAKE 256 h ++ DROP (LENGTH h) init)))) sv
 Using translator specification cut_at_null_v_thm from theory filterProg
 Post condition: POSTv sv1.
   W8ARRAY v' (TAKE 256 h ++ DROP (LENGTH h) init) * W8ARRAY dummyarr_loc [] *
   seL4_IO (fromList l)
     (SNOC (IO_event (ExtCall accept_call) [] (ZIP (init,newinit))) events) *
   &STRING_TYPE
     (cut_at_null
        (implode
           (MAP (CHR  w2n) (TAKE 256 (TAKE 256 h ++ DROP (LENGTH h) init)))))
     sv1
 Using translator specification match_string_v_thm from theory filterProg
 Post condition: POSTv bv.
   W8ARRAY v' (TAKE 256 h ++ DROP (LENGTH h) init) * W8ARRAY dummyarr_loc [] *
   seL4_IO (fromList l)
     (SNOC (IO_event (ExtCall accept_call) [] (ZIP (init,newinit))) events) *
   &BOOL
     (match_string
        (cut_at_null
           (implode
              (MAP (CHR  w2n) (TAKE 256 (TAKE 256 h ++ DROP (LENGTH h) init))))))
     bv
 Using a CF specification from the assumptions
 Saved theorem _______ "forward_matching_lines_ffidiv_spec"
 Saved definition ____ "seL4_proj1_def"
 Saved definition ____ "seL4_proj2"
 Saved definition ____ "filter_ffi_state_def"
 Saved theorem _______ "limited_parts_proj"
 Saved theorem _______ "parts_ok_filter"
 Saved theorem _______ "forward_matching_lines_semantics"
 Saved theorem _______ "forward_matching_lines_ffidiv_semantics"
 Saved theorem _______ "semantics_diverge_filter"
 Saved theorem _______ "semantics_finite_filter"
 Exporting theory "filterProg" ... done.
 Theory "filterProg" took 46.1s to build
 Full log: /scratch/cakeml/regression/cakeml-3417/examples/.hol/logs/filterProgTheory