Job 3506

CakeML:350825dba48fdf37b931e7a914fb4d9c9f3bceb2
  proofs: adapt Dafny, Scheme and filter to scoped constructor checks [Sep 09 19:03:40]
#1482 (dopen-new)
Merging into:e6bb97e7b11423ddb00b92e00b7dc972de361e89
  Merge pull request #1481 from CakeML/mcandidate-fix [Sep 09 14:45:46]
HOL:e395eb6e69054ff6f7cef9d1107fd1a04dd5848f
  A Quote body is verbatim material [Sep 02 10:49:13]
Machine:pavlova

Sep 09 20:04:37 Claimed job
Sep 09 20:04:45 Reusing HOL
Sep 09 20:05:41 Starting developers
Sep 09 20:06:32 Finished developers                                              49s   1GB
Sep 09 20:06:33 Starting developers/bin
Sep 09 20:06:43 Finished developers/bin                                           9s   1GB
Sep 09 20:06:44 Starting misc
Sep 09 20:07:34 Finished misc                                                    49s   1GB
Sep 09 20:07:35 Starting compiler/proofs
Sep 09 21:27:26 Finished compiler/proofs                                    1h19m49s  11GB
Sep 09 21:27:27 Starting compiler/bootstrap/compilation/x64/64/proofs
Sep 10 04:04:59 Finished compiler/bootstrap/compilation/x64/64/proofs       6h37m30s  86GB
Sep 10 04:05:00 Starting semantics/ffi
Sep 10 04:05:23 Finished semantics/ffi                                           22s   1GB
Sep 10 04:05:24 Starting semantics
Sep 10 04:05:31 Finished semantics                                                5s   1GB
Sep 10 04:05:32 Starting semantics/proofs
Sep 10 04:06:02 Finished semantics/proofs                                        29s   1GB
Sep 10 04:06:02 Starting semantics/alt_semantics
Sep 10 04:06:27 Finished semantics/alt_semantics                                 23s   1GB
Sep 10 04:06:28 Starting semantics/alt_semantics/proofs
Sep 10 04:10:32 Finished semantics/alt_semantics/proofs                        4m03s   2GB
Sep 10 04:10:33 Starting basis/pure
Sep 10 04:10:40 Finished basis/pure                                               6s   1GB
Sep 10 04:10:41 Starting translator
Sep 10 04:11:58 Finished translator                                            1m16s   2GB
Sep 10 04:11:59 Starting compiler/parsing
Sep 10 04:12:53 Finished compiler/parsing                                        53s   2GB
Sep 10 04:12:54 Starting characteristic
Sep 10 04:13:01 Finished characteristic                                           5s   1GB
Sep 10 04:13:02 Starting translator/monadic
Sep 10 04:13:08 Finished translator/monadic                                       5s   1GB
Sep 10 04:13:09 Starting translator/monadic/monad_base
Sep 10 04:13:16 Finished translator/monadic/monad_base                            5s   1GB
Sep 10 04:13:17 Starting profiler
Sep 10 04:13:55 Finished profiler                                                37s   1GB
Sep 10 04:13:56 Starting basis
Sep 10 04:15:50 Finished basis                                                 1m53s   4GB
Sep 10 04:15:51 Starting compiler
Sep 10 04:15:58 Finished compiler                                                 5s   1GB
Sep 10 04:15:59 Starting compiler/inference
Sep 10 04:16:05 Finished compiler/inference                                       5s   1GB
Sep 10 04:16:06 Starting compiler/backend/reg_alloc
Sep 10 04:16:13 Finished compiler/backend/reg_alloc                               5s   1GB
Sep 10 04:16:14 Starting compiler/backend/gc
Sep 10 04:16:20 Finished compiler/backend/gc                                      5s   1GB
Sep 10 04:16:21 Starting compiler/backend
Sep 10 04:16:28 Finished compiler/backend                                         5s   1GB
Sep 10 04:16:29 Starting compiler/encoders/asm
Sep 10 04:16:35 Finished compiler/encoders/asm                                    5s   1GB
Sep 10 04:16:36 Starting compiler/encoders/x64
Sep 10 04:16:43 Finished compiler/encoders/x64                                    5s   1GB
Sep 10 04:16:44 Starting compiler/encoders/arm7
Sep 10 04:16:50 Finished compiler/encoders/arm7                                   5s   1GB
Sep 10 04:16:51 Starting compiler/encoders/arm8
Sep 10 04:16:58 Finished compiler/encoders/arm8                                   5s   1GB
Sep 10 04:16:59 Starting compiler/encoders/arm8_asl
Sep 10 04:17:25 Finished compiler/encoders/arm8_asl                              25s   1GB
Sep 10 04:17:26 Starting compiler/encoders/mips
Sep 10 04:17:33 Finished compiler/encoders/mips                                   5s   1GB
Sep 10 04:17:33 Starting compiler/encoders/riscv
Sep 10 04:17:40 Finished compiler/encoders/riscv                                  5s   1GB
Sep 10 04:17:41 Starting compiler/encoders/ag32
Sep 10 04:17:47 Finished compiler/encoders/ag32                                   5s   1GB
Sep 10 04:17:48 Starting compiler/encoders/tests
Sep 10 04:17:55 Finished compiler/encoders/tests                                  5s   1GB
Sep 10 04:17:56 Starting compiler/encoders/monadic_enc
Sep 10 04:18:24 Finished compiler/encoders/monadic_enc                           27s   1GB
Sep 10 04:18:25 Starting compiler/backend/x64
Sep 10 04:18:31 Finished compiler/backend/x64                                     5s   1GB
Sep 10 04:18:32 Starting compiler/backend/arm7
Sep 10 04:18:39 Finished compiler/backend/arm7                                    5s   1GB
Sep 10 04:18:39 Starting compiler/backend/arm8
Sep 10 04:18:46 Finished compiler/backend/arm8                                    5s   1GB
Sep 10 04:18:47 Starting compiler/backend/mips
Sep 10 04:18:54 Finished compiler/backend/mips                                    5s   1GB
Sep 10 04:18:54 Starting compiler/backend/riscv
Sep 10 04:19:01 Finished compiler/backend/riscv                                   5s   1GB
Sep 10 04:19:02 Starting compiler/backend/ag32
Sep 10 04:20:08 Finished compiler/backend/ag32                                 1m05s   1GB
Sep 10 04:20:09 Starting compiler/backend/pattern_matching
Sep 10 04:20:31 Finished compiler/backend/pattern_matching                       20s   1GB
Sep 10 04:20:32 Starting compiler/parsing/ocaml
Sep 10 04:22:45 Finished compiler/parsing/ocaml                                2m12s   1GB
Sep 10 04:22:46 Starting compiler/printing
Sep 10 04:23:48 Finished compiler/printing                                     1m00s   1GB
Sep 10 04:23:49 Starting compiler/parsing/proofs
Sep 10 04:23:55 Finished compiler/parsing/proofs                                  5s   1GB
Sep 10 04:23:56 Starting compiler/inference/proofs
Sep 10 04:24:03 Finished compiler/inference/proofs                                5s   1GB
Sep 10 04:24:04 Starting compiler/backend/semantics
Sep 10 04:27:24 Finished compiler/backend/semantics                            3m19s   3GB
Sep 10 04:27:25 Starting compiler/backend/reg_alloc/proofs
Sep 10 04:27:31 Finished compiler/backend/reg_alloc/proofs                        5s   1GB
Sep 10 04:27:32 Starting compiler/backend/proofs
Sep 10 04:28:23 Finished compiler/backend/proofs                                 49s   2GB
Sep 10 04:28:24 Starting compiler/backend/serialiser
Sep 10 04:28:30 Finished compiler/backend/serialiser                              5s   1GB
Sep 10 04:28:31 Starting compiler/encoders/x64/proofs
Sep 10 04:28:38 Finished compiler/encoders/x64/proofs                             5s   1GB
Sep 10 04:28:39 Starting compiler/encoders/arm7/proofs
Sep 10 04:41:08 Finished compiler/encoders/arm7/proofs                        12m28s   5GB
Sep 10 04:41:09 Starting compiler/encoders/arm8/proofs
Sep 10 04:49:27 Finished compiler/encoders/arm8/proofs                         8m16s   3GB
Sep 10 04:49:28 Starting compiler/encoders/arm8_asl/proofs
Sep 10 05:07:15 Finished compiler/encoders/arm8_asl/proofs                    17m45s   3GB
Sep 10 05:07:15 Starting compiler/encoders/mips/proofs
Sep 10 05:18:06 Finished compiler/encoders/mips/proofs                        10m49s   4GB
Sep 10 05:18:07 Starting compiler/encoders/riscv/proofs
Sep 10 05:27:34 Finished compiler/encoders/riscv/proofs                        9m25s   3GB
Sep 10 05:27:35 Starting compiler/encoders/ag32/proofs
Sep 10 05:30:49 Finished compiler/encoders/ag32/proofs                         3m13s   1GB
Sep 10 05:30:50 Starting compiler/backend/x64/proofs
Sep 10 05:30:57 Finished compiler/backend/x64/proofs                              5s   1GB
Sep 10 05:30:58 Starting compiler/backend/arm7/proofs
Sep 10 05:31:44 Finished compiler/backend/arm7/proofs                            45s   2GB
Sep 10 05:31:45 Starting compiler/backend/arm8/proofs
Sep 10 05:32:27 Finished compiler/backend/arm8/proofs                            40s   1GB
Sep 10 05:32:28 Starting compiler/backend/arm8_asl
Sep 10 05:33:05 Finished compiler/backend/arm8_asl                               36s   1GB
Sep 10 05:33:06 Starting compiler/backend/mips/proofs
Sep 10 05:33:51 Finished compiler/backend/mips/proofs                            44s   2GB
Sep 10 05:33:52 Starting compiler/backend/riscv/proofs
Sep 10 05:34:40 Finished compiler/backend/riscv/proofs                           47s   2GB
Sep 10 05:34:41 Starting compiler/backend/ag32/proofs
Sep 10 05:44:43 Finished compiler/backend/ag32/proofs                         10m01s   5GB
Sep 10 05:44:44 Starting compiler/backend/cv_compute
Sep 10 05:45:21 Finished compiler/backend/cv_compute                             36s   1GB
Sep 10 05:45:22 Starting cv_translator
Sep 10 05:50:39 Finished cv_translator                                         5m14s   4GB
Sep 10 05:50:40 Starting candle
Sep 10 05:50:47 Finished candle                                                   5s   1GB
Sep 10 05:50:48 Starting candle/set-theory
Sep 10 05:51:10 Finished candle/set-theory                                       21s   1GB
Sep 10 05:51:11 Starting candle/syntax-lib
Sep 10 05:51:18 Finished candle/syntax-lib                                        5s   1GB
Sep 10 05:51:19 Starting candle/standard
Sep 10 05:51:25 Finished candle/standard                                          5s   1GB
Sep 10 05:51:26 Starting candle/standard/syntax
Sep 10 05:51:47 Finished candle/standard/syntax                                  19s   1GB
Sep 10 05:51:48 Starting candle/standard/syntax/little_theories
Sep 10 05:53:10 Finished candle/standard/syntax/little_theories                1m20s   1GB
Sep 10 05:53:11 Starting candle/standard/semantics
Sep 10 05:53:17 Finished candle/standard/semantics                                5s   1GB
Sep 10 05:53:18 Starting candle/standard/monadic
Sep 10 05:53:25 Finished candle/standard/monadic                                  5s   1GB
Sep 10 05:53:26 Starting candle/standard/ml_kernel
Sep 10 05:55:45 Finished candle/standard/ml_kernel                             2m18s   5GB
Sep 10 05:55:46 Starting candle/overloading
Sep 10 05:55:52 Finished candle/overloading                                       5s   1GB
Sep 10 05:55:53 Starting candle/overloading/syntax
Sep 10 05:59:18 Finished candle/overloading/syntax                             3m24s   2GB
Sep 10 05:59:19 Starting candle/overloading/semantics
Sep 10 06:09:07 Finished candle/overloading/semantics                          9m46s   5GB
Sep 10 06:09:08 Starting candle/overloading/monadic
Sep 10 06:11:20 Finished candle/overloading/monadic                            2m10s   1GB
Sep 10 06:11:21 Starting candle/overloading/ml_kernel
Sep 10 06:18:44 Finished candle/overloading/ml_kernel                          7m22s   7GB
Sep 10 06:18:45 Starting candle/overloading/ml_checker
Sep 10 06:21:39 Finished candle/overloading/ml_checker                         2m53s   6GB
Sep 10 06:21:40 Starting candle/prover
Sep 10 06:21:47 Finished candle/prover                                            5s   1GB
Sep 10 06:21:48 Starting candle/prover/compute
Sep 10 06:21:54 Finished candle/prover/compute                                    5s   1GB
Sep 10 06:21:55 Starting pancake
Sep 10 06:22:02 Finished pancake                                                  6s   1GB
Sep 10 06:22:03 Starting pancake/semantics
Sep 10 06:25:26 Finished pancake/semantics                                     3m21s   2GB
Sep 10 06:25:27 Starting pancake/parser
Sep 10 06:26:14 Finished pancake/parser                                          46s   1GB
Sep 10 06:26:15 Starting pancake/static_checker
Sep 10 06:28:57 Finished pancake/static_checker                                2m40s   1GB
Sep 10 06:28:58 Starting pancake/proofs
Sep 10 06:45:44 Finished pancake/proofs                                       16m45s   5GB
Sep 10 06:45:45 Starting compiler/dafny
Sep 10 06:46:17 Finished compiler/dafny                                          30s   1GB
Sep 10 06:46:17 Starting compiler/dafny/translation
Sep 10 06:57:30 Finished compiler/dafny/translation                           11m11s   7GB
Sep 10 06:57:31 Starting compiler/dafny/compilation
Sep 10 06:59:53 Finished compiler/dafny/compilation                            2m20s   6GB
Sep 10 06:59:53 Starting compiler/dafny/semantics
Sep 10 07:00:38 Finished compiler/dafny/semantics                                43s   1GB
Sep 10 07:00:39 Starting compiler/dafny/proofs
Sep 10 07:02:28 Finished compiler/dafny/proofs                                 1m47s   1GB
Sep 10 07:02:29 Starting compiler/dafny/vcg
Sep 10 07:02:36 Finished compiler/dafny/vcg                                       6s   1GB
Sep 10 07:02:36 Starting compiler/dafny/vcg/examples
Sep 10 07:03:11 Finished compiler/dafny/vcg/examples                             33s   1GB
Sep 10 07:03:12 Starting compiler/scheme
Sep 10 07:03:45 Finished compiler/scheme                                         32s   1GB
Sep 10 07:03:46 Starting compiler/scheme/translation
Sep 10 07:10:57 Finished compiler/scheme/translation                           7m09s   8GB
Sep 10 07:10:58 Starting compiler/scheme/compilation
Sep 10 07:12:47 Finished compiler/scheme/compilation                           1m48s   5GB
Sep 10 07:12:48 Starting compiler/scheme/proofs
Sep 10 07:19:58 Finished compiler/scheme/proofs                                7m08s   2GB
Sep 10 07:19:59 Starting characteristic/examples
Sep 10 07:21:42 Finished characteristic/examples                               1m41s   5GB
Sep 10 07:21:43 Starting tutorial
Sep 10 07:21:50 Finished tutorial                                                 6s   1GB
Sep 10 07:21:51 Starting tutorial/solutions
Sep 10 07:24:55 Finished tutorial/solutions                                    3m03s   5GB
Sep 10 07:24:56 Starting translator/monadic/examples
Sep 10 07:28:12 Finished translator/monadic/examples                           3m13s   4GB
Sep 10 07:28:13 Starting examples
Sep 10 07:32:37 Finished examples                                              4m22s   3GB
Sep 10 07:32:38 Starting examples/compilation
Sep 10 07:32:45 Finished examples/compilation                                     6s   1GB
Sep 10 07:32:46 Starting examples/compilation/x64
Sep 10 07:41:48 Finished examples/compilation/x64                              9m01s   5GB
Sep 10 07:41:49 Starting examples/compilation/x64/proofs
Sep 10 07:45:46 Finished examples/compilation/x64/proofs                       3m54s   4GB
Sep 10 07:45:47 Starting examples/compilation/ag32
Sep 10 07:48:38 Finished examples/compilation/ag32                             2m50s   3GB
Sep 10 07:48:39 Starting examples/compilation/ag32/proofs
Sep 10 07:50:10 Finished examples/compilation/ag32/proofs                      1m30s   5GB
Sep 10 07:50:11 Starting examples/lpr_checker
Sep 10 07:50:56 Finished examples/lpr_checker                                    44s   1GB
Sep 10 07:50:57 Starting examples/lpr_checker/array
Sep 10 08:04:10 Finished examples/lpr_checker/array                           13m12s   6GB
Sep 10 08:04:11 Starting examples/lpr_checker/array/compilation
Sep 10 08:08:16 Finished examples/lpr_checker/array/compilation                4m04s   6GB
Sep 10 08:08:17 Starting examples/lpr_checker/array/compilation/proofs
Sep 10 08:10:05 Finished examples/lpr_checker/array/compilation/proofs         1m47s   6GB
Sep 10 08:10:06 Starting examples/lpr_checker/array/compilation/proofsARM8
Sep 10 08:11:56 Finished examples/lpr_checker/array/compilation/proofsARM8     1m49s   6GB
Sep 10 08:11:57 Starting .
Sep 10 08:12:04 Finished .                                                        5s   1GB
Sep 10 08:12:05 Starting examples/xlrup_checker
Sep 10 08:13:03 Finished examples/xlrup_checker                                  57s   1GB
Sep 10 08:13:04 Starting examples/xlrup_checker/array
Sep 10 08:22:49 Finished examples/xlrup_checker/array                          9m43s   6GB
Sep 10 08:22:50 Starting examples/xlrup_checker/array/compilation
Sep 10 08:24:34 Finished examples/xlrup_checker/array/compilation              1m43s   5GB
Sep 10 08:24:35 Starting examples/xlrup_checker/array/compilation/proofs
Sep 10 08:26:15 Finished examples/xlrup_checker/array/compilation/proofs       1m38s   5GB
Sep 10 08:26:16 Starting examples/cnf
Sep 10 08:26:50 Finished examples/cnf                                            33s   1GB
Sep 10 08:26:51 Starting examples/cnf/array
Sep 10 08:30:00 Finished examples/cnf/array                                    3m07s   2GB
Sep 10 08:30:00 Starting examples/cnf/dist
Sep 10 08:30:12 Finished examples/cnf/dist                                       10s   1GB
Sep 10 08:30:13 Starting examples/cnf/dist/array
Sep 10 08:34:35 FAILED: examples/cnf/dist/array
  HOLORIG=/scratch/cakeml/regression/cakeml-3506/examples/cnf/dist/array [ -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)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/pl-semantics/lprefix_lub
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/src/rational
Scanning $(HOLDIR)/src/num/theories/cv_compute/automation
Scanning $(HOLDIR)/src/algebra/base
Scanning $(HOLDIR)/src/algebra/construction
Scanning $(HOLDIR)/src/algebra
Scanning $(HOLDIR)/src/hol88
Scanning $(HOLDIR)/src/real
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/src/search
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/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/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 $(CAKEMLDIR)/basis
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/candle
Scanning $(CAKEMLDIR)/candle/prover
Scanning $(CAKEMLDIR)/candle/prover/compute
Scanning $(CAKEMLDIR)/candle/set-theory
Scanning $(CAKEMLDIR)/candle/standard
Scanning $(CAKEMLDIR)/candle/standard/ml_kernel
Scanning $(CAKEMLDIR)/candle/standard/monadic
Scanning $(CAKEMLDIR)/candle/standard/semantics
Scanning $(CAKEMLDIR)/candle/standard/syntax
Scanning $(CAKEMLDIR)/candle/standard/syntax/little_theories
Scanning $(CAKEMLDIR)/candle/syntax-lib
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/characteristic/examples
Scanning $(CAKEMLDIR)/compiler
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/backend/ag32
Scanning $(CAKEMLDIR)/compiler/backend/ag32/proofs
Scanning $(CAKEMLDIR)/compiler/backend/arm7
Scanning $(CAKEMLDIR)/compiler/backend/arm7/proofs
Scanning $(CAKEMLDIR)/compiler/backend/arm8
Scanning $(CAKEMLDIR)/compiler/backend/arm8/proofs
Scanning $(CAKEMLDIR)/compiler/backend/arm8_asl
Scanning $(CAKEMLDIR)/compiler/backend/cv_compute
Scanning $(CAKEMLDIR)/compiler/backend/gc
Scanning $(CAKEMLDIR)/compiler/backend/mips
Scanning $(CAKEMLDIR)/compiler/backend/mips/proofs
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/compiler/backend/proofs
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/compiler/backend/riscv
Scanning $(CAKEMLDIR)/compiler/backend/riscv/proofs
Scanning $(CAKEMLDIR)/compiler/backend/semantics
Scanning $(CAKEMLDIR)/compiler/backend/serialiser
Scanning $(CAKEMLDIR)/compiler/backend/x64
Scanning $(CAKEMLDIR)/compiler/backend/x64/proofs
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/x64/64
Scanning $(CAKEMLDIR)/compiler/benchmarks/cakeml_benchmarks/cakeml
Scanning $(CAKEMLDIR)/compiler/benchmarks/mlton_benchmarks/cakeml
Scanning $(CAKEMLDIR)/compiler/benchmarks
Scanning $(CAKEMLDIR)/compiler/benchmarks/cakeml_benchmarks
Scanning $(CAKEMLDIR)/compiler/benchmarks/cakeml_benchmarks/ocaml
Scanning $(CAKEMLDIR)/compiler/benchmarks/mlton_benchmarks
Scanning $(CAKEMLDIR)/compiler/bootstrap
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/ag32
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)/compiler/bootstrap/compilation/x64/32
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64/32/proofs
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64/64
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64/64/proofs
Scanning $(CAKEMLDIR)/compiler/bootstrap/translation
Scanning $(CAKEMLDIR)/compiler/dafny
Scanning $(CAKEMLDIR)/compiler/dafny/compilation
Scanning $(CAKEMLDIR)/compiler/dafny/examples
Scanning $(CAKEMLDIR)/compiler/dafny/examples/output
Scanning $(CAKEMLDIR)/compiler/dafny/proofs
Scanning $(CAKEMLDIR)/compiler/dafny/semantics
Scanning $(CAKEMLDIR)/compiler/dafny/translation
Scanning $(CAKEMLDIR)/compiler/dafny/vcg
Scanning $(CAKEMLDIR)/compiler/dafny/vcg/examples
Scanning $(CAKEMLDIR)/compiler/encoders
Scanning $(CAKEMLDIR)/compiler/encoders/ag32
Scanning $(CAKEMLDIR)/compiler/encoders/ag32/proofs
Scanning $(HOLDIR)/examples/l3-machine-code/arm/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm7
Scanning $(HOLDIR)/examples/l3-machine-code/arm/prog
Scanning $(CAKEMLDIR)/compiler/encoders/arm7/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/arm8
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/prog
Scanning $(CAKEMLDIR)/compiler/encoders/arm8/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/arm8_asl
Scanning $(CAKEMLDIR)/compiler/encoders/arm8_asl/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(HOLDIR)/examples/l3-machine-code/mips/step
Scanning $(CAKEMLDIR)/compiler/encoders/mips
Scanning $(HOLDIR)/examples/l3-machine-code/mips/prog
Scanning $(CAKEMLDIR)/compiler/encoders/mips/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/monadic_enc
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/step
Scanning $(CAKEMLDIR)/compiler/encoders/riscv
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/prog
Scanning $(CAKEMLDIR)/compiler/encoders/riscv/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/tests
Scanning $(HOLDIR)/examples/l3-machine-code/x64/step
Scanning $(CAKEMLDIR)/compiler/encoders/x64
Scanning $(HOLDIR)/examples/l3-machine-code/x64/prog
Scanning $(CAKEMLDIR)/compiler/encoders/x64/proofs
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)/compiler/inference/proofs
Scanning $(CAKEMLDIR)/compiler/inference/tests
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/compiler/parsing/ocaml
Scanning $(CAKEMLDIR)/compiler/parsing/proofs
Scanning $(CAKEMLDIR)/compiler/parsing/tests
Scanning $(CAKEMLDIR)/compiler/printing
Scanning $(CAKEMLDIR)/compiler/printing/test
Scanning $(CAKEMLDIR)/compiler/proofs
Scanning $(CAKEMLDIR)/compiler/repl
Scanning $(CAKEMLDIR)/compiler/scheme
Scanning $(CAKEMLDIR)/compiler/scheme/compilation
Scanning $(CAKEMLDIR)/compiler/scheme/examples
Scanning $(CAKEMLDIR)/compiler/scheme/proofs
Scanning $(CAKEMLDIR)/compiler/scheme/translation
Scanning $(CAKEMLDIR)/compiler/scheme/unverified
Scanning $(CAKEMLDIR)/cv_translator
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/developers/bin
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/compilation
Scanning $(CAKEMLDIR)/examples/compilation/ag32
Scanning $(CAKEMLDIR)/examples/compilation/ag32/proofs
Scanning $(CAKEMLDIR)/examples/compilation/x64
Scanning $(CAKEMLDIR)/examples/compilation/x64/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
Scanning $(CAKEMLDIR)/examples/flover/Infra
Scanning $(CAKEMLDIR)/examples/flover/semantics
Scanning $(CAKEMLDIR)/examples/template
Scanning $(CAKEMLDIR)/examples/template/compilation
Scanning $(CAKEMLDIR)/examples/template/translation
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)/misc
Scanning $(CAKEMLDIR)/pancake
Scanning $(CAKEMLDIR)/pancake/parser
Scanning $(CAKEMLDIR)/pancake/proofs
Scanning $(CAKEMLDIR)/pancake/semantics
Scanning $(CAKEMLDIR)/pancake/static_checker
Scanning $(CAKEMLDIR)/pancake/temp
Scanning $(CAKEMLDIR)/profiler
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/semantics/alt_semantics
Scanning $(CAKEMLDIR)/semantics/alt_semantics/proofs
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/translator/monadic/examples
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/translator/okasaki-examples
Scanning $(HOLDIR)/examples/Crypto/RSA
Scanning $(HOLDIR)/examples/miller/ho_prover
Scanning $(HOLDIR)/examples/miller/subtypes
Scanning $(HOLDIR)/examples/miller/formalize
Scanning $(HOLDIR)/examples/miller/groups
Scanning $(HOLDIR)/examples/probability/legacy
Scanning $(HOLDIR)/examples/miller/prob
Scanning $(HOLDIR)/examples/miller/miller
Scanning $(CAKEMLDIR)/translator/other-examples
Scanning $(CAKEMLDIR)/translator/other-examples/auxiliary
Scanning $(CAKEMLDIR)/tutorial
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/reg_alloc
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/x64
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/x64/32
Scanning $(candle_overloading)/ml_checker
Scanning $(candle_overloading)/ml_kernel
Scanning $(candle_overloading)/monadic
Scanning $(candle_overloading)/semantics
Scanning $(candle_overloading)/syntax
Scanning $(cnf)/array
Scanning $(cnf)/dist
Scanning $(cnf)/dist/array
Scanning $(cnf)/dist/array/compilation
Scanning $(cnf)/dist/array/compilation/proofs
Scanning $(cnf)/lrup
Scanning $(cnf)/lrup/array
Scanning $(cnf)/lrup/array/compilation
Scanning $(cnf)/lrup/array/compilation/proofs
Scanning $(lpr_checker)/array
Scanning $(lpr_checker)/array/compilation
Scanning $(lpr_checker)/array/compilation/proofs
Scanning $(lpr_checker)/array/compilation/proofsARM8
Scanning $(opentheory)/compilation
Scanning $(opentheory)/compilation/ag32
Scanning $(opentheory)/compilation/ag32/proofs
Scanning $(opentheory)/compilation/proofs
Scanning $(pseudo_bool)/array
Scanning $(pseudo_bool)/array/compilation
Scanning $(pseudo_bool)/array/compilation/proofs
Scanning $(pseudo_bool)/array/compilation/proofsARM8
Scanning $(pseudo_bool)/cnf_encoding
Scanning $(pseudo_bool)/cnf_encoding/array
Scanning $(pseudo_bool)/cnf_encoding/array/compilation
Scanning $(pseudo_bool)/cnf_encoding/array/compilation/proofs
Scanning $(pseudo_bool)/cp_encoding
Scanning $(pseudo_bool)/cp_encoding/array
Scanning $(pseudo_bool)/cp_encoding/array/compilation
Scanning $(pseudo_bool)/cp_encoding/array/compilation/proofs
Scanning $(pseudo_bool)/graph_encoding
Scanning $(pseudo_bool)/graph_encoding/array
Scanning $(pseudo_bool)/graph_encoding/array/compilation
Scanning $(pseudo_bool)/graph_encoding/array/compilation/proofs
Scanning $(sat_encodings)/case_studies
Scanning $(sat_encodings)/demo
Scanning $(sat_encodings)/translation
Scanning $(sat_encodings)/translation/compilation
Scanning $(scpog_checker)/array
Scanning $(scpog_checker)/array/compilation
Scanning $(scpog_checker)/array/compilation/proofs
Scanned 298 directories
Building 4 theory files
Starting work on README.md
Starting work on distrup_listTheory
README.md                                                   (0s)             OK
distrup_listTheory                                          (3s)   [1/4]     OK
Starting work on distrup_arrayProgTheory
distrup_arrayProgTheory                                    (36s)   [2/4]     OK
Starting work on distrup_fullProgTheory
distrup_fullProgTheory                                    (202s)        FAIL<1>
*** Holmake aborted - 1 target failed:
*** distrup_fullProgTheory (status 1)
    CUSTOM_FFI Step inputs [] tb)
 Post condition: POSTv v''.
   &(v'' = Conv (SOME (TypeStamp Some 2)) [v'']) *
   (W8ARRAY v'' (REPLICATE 1024 0w) * ARRAY av (REPLICATE 4096 vcc_none_v) *
    W8ARRAY v'' [] * W8ARRAY v' (REPLICATE 17 0w) *
    CUSTOM_FFI Step inputs [] tb)
 Saved theorem _______ "main_spec"
 <<HOL message: mk_functional: 
   pattern completion has added 1 clause to the original specification.>>
 Saved definition ____ "update_oracle_def"
 Saved definition ____ "custom_ffi_def"
 Saved definition ____ "ffi_proj_def"
 Saved theorem _______ "parts_ok_custom_ffi"
 Proved triviality ___ "SPLIT_heaps_lemma"
 Saved theorem _______ "FILTER_SKIP"
 Saved theorem _______ "main_st_ffi_events"
 Adding nsLookup representation thms for [distrup_fullProg_env_14]
 Proof of 
 
 semantics_prog (init_state (custom_ffi (State Step inputs tb))) init_env
   distrup_prog (Terminate Success (main_events tb inputs))
 
 failed.
 First unsolved sub-goal is
 
 v ffi.
   ((st',r). (st'.ffi,r))
     (case
        if
          check_exp_constructors
            (nsAppend distrup_fullProg_env_14.c init_env.c)
            (App Opapp [Var (Short main); Con NONE []])
        then
          (main_st tb inputs,Rval <|v := nsEmpty; c := nsEmpty|>)
        else
          (distrup_arrayProg_st (custom_ffi (State Step inputs tb)) with
           clock := main_ck tb inputs + 1,Rerr (Rabort Rtype_error))
      of
        (s2,r) =>
          (s2,
           case r of
             Rval env' =>
               Rval
                 <|v := nsAppend env'.v distrup_fullProg_env_14.v;
                   c := nsAppend env'.c distrup_fullProg_env_14.c|>
           | Rerr e => Rerr e)) = (ffi,Rval v) 
   main_events tb inputs = ffi.io_events
 
 Tactic failure proving "semantics_prog_distrup_prog"; heap saved to distrup_fullProg.semantics_prog_distrup_prog.dumpedheap.
 Resume with: bin/hol --holstate=distrup_fullProg.semantics_prog_distrup_prog.dumpedheap
 Full log: /scratch/cakeml/regression/cakeml-3506/examples/cnf/dist/array/.hol/logs/distrup_fullProgTheory