Job 3639

CakeML:3ced4931e476ba1bb2668957b8da5ff1deba13f8
  Merge remote-tracking branch 'origin/master' into byte-array-scan [Oct 23 13:07:30]
#1559 (byte-array-scan)
Merging into:0f1aca3913a175c390f0fd0b3af04f43d49a0fde
  xlrup release message [Oct 23 03:33:35]
HOL:652d1f0aad5cd537ed1e5d470ba3444e70ba470e
  Merge remote-tracking branch 'origin/master' into develop [Sep 27 02:14:15]
Machine:spagbol

Oct 23 16:59:31 Claimed job
Oct 23 16:59:35 Reusing HOL
Oct 23 16:59:44 Starting developers
Oct 23 17:00:42 Finished developers                                              56s   1GB
Oct 23 17:00:43 Starting developers/bin
Oct 23 17:00:52 Finished developers/bin                                           8s   1GB
Oct 23 17:00:53 Starting misc
Oct 23 17:01:42 Finished misc                                                    47s   1GB
Oct 23 17:01:43 Starting compiler/proofs
Oct 23 18:32:29 Finished compiler/proofs                                    1h30m44s  11GB
Oct 23 18:32:30 Starting compiler/bootstrap/compilation/x64/64/proofs
Oct 24 00:53:46 Finished compiler/bootstrap/compilation/x64/64/proofs       6h21m15s  99GB
Oct 24 00:53:47 Starting semantics/ffi
Oct 24 00:54:12 Finished semantics/ffi                                           23s   1GB
Oct 24 00:54:13 Starting semantics
Oct 24 00:54:20 Finished semantics                                                6s   1GB
Oct 24 00:54:21 Starting semantics/proofs
Oct 24 00:54:53 Finished semantics/proofs                                        31s   1GB
Oct 24 00:54:54 Starting semantics/alt_semantics
Oct 24 00:55:19 Finished semantics/alt_semantics                                 24s   1GB
Oct 24 00:55:20 Starting semantics/alt_semantics/proofs
Oct 24 01:00:09 Finished semantics/alt_semantics/proofs                        4m47s   2GB
Oct 24 01:00:10 Starting basis/pure
Oct 24 01:00:18 Finished basis/pure                                               7s   1GB
Oct 24 01:00:19 Starting translator
Oct 24 01:01:42 Finished translator                                            1m22s   2GB
Oct 24 01:01:43 Starting compiler/parsing
Oct 24 01:02:40 Finished compiler/parsing                                        56s   1GB
Oct 24 01:02:41 Starting characteristic
Oct 24 01:02:49 Finished characteristic                                           6s   1GB
Oct 24 01:02:50 Starting translator/monadic
Oct 24 01:02:57 Finished translator/monadic                                       6s   1GB
Oct 24 01:02:58 Starting translator/monadic/monad_base
Oct 24 01:03:05 Finished translator/monadic/monad_base                            6s   1GB
Oct 24 01:03:06 Starting profiler
Oct 24 01:03:42 Finished profiler                                                34s   2GB
Oct 24 01:03:43 Starting basis
Oct 24 01:06:11 Finished basis                                                 2m27s   5GB
Oct 24 01:06:12 Starting compiler
Oct 24 01:06:20 Finished compiler                                                 6s   1GB
Oct 24 01:06:21 Starting compiler/inference
Oct 24 01:06:29 Finished compiler/inference                                       6s   1GB
Oct 24 01:06:30 Starting compiler/backend/reg_alloc
Oct 24 01:06:37 Finished compiler/backend/reg_alloc                               6s   1GB
Oct 24 01:06:38 Starting compiler/backend/gc
Oct 24 01:06:46 Finished compiler/backend/gc                                      6s   1GB
Oct 24 01:06:47 Starting compiler/backend
Oct 24 01:06:55 Finished compiler/backend                                         6s   1GB
Oct 24 01:06:56 Starting compiler/backend/tests
Oct 24 01:07:32 Finished compiler/backend/tests                                  35s   1GB
Oct 24 01:07:33 Starting compiler/encoders/asm
Oct 24 01:07:41 Finished compiler/encoders/asm                                    7s   1GB
Oct 24 01:07:42 Starting compiler/encoders/x64
Oct 24 01:07:50 Finished compiler/encoders/x64                                    6s   1GB
Oct 24 01:07:51 Starting compiler/encoders/arm7
Oct 24 01:07:58 Finished compiler/encoders/arm7                                   6s   1GB
Oct 24 01:07:59 Starting compiler/encoders/arm8
Oct 24 01:08:07 Finished compiler/encoders/arm8                                   6s   1GB
Oct 24 01:08:08 Starting compiler/encoders/arm8_asl
Oct 24 01:08:31 Finished compiler/encoders/arm8_asl                              22s   1GB
Oct 24 01:08:32 Starting compiler/encoders/mips
Oct 24 01:08:39 Finished compiler/encoders/mips                                   6s   1GB
Oct 24 01:08:40 Starting compiler/encoders/riscv
Oct 24 01:08:47 Finished compiler/encoders/riscv                                  6s   1GB
Oct 24 01:08:48 Starting compiler/encoders/ag32
Oct 24 01:08:56 Finished compiler/encoders/ag32                                   6s   1GB
Oct 24 01:08:57 Starting compiler/encoders/tests
Oct 24 01:09:40 Finished compiler/encoders/tests                                 42s   1GB
Oct 24 01:09:41 Starting compiler/encoders/monadic_enc
Oct 24 01:10:09 Finished compiler/encoders/monadic_enc                           27s   1GB
Oct 24 01:10:10 Starting compiler/backend/x64
Oct 24 01:10:18 Finished compiler/backend/x64                                     6s   1GB
Oct 24 01:10:19 Starting compiler/backend/arm7
Oct 24 01:10:26 Finished compiler/backend/arm7                                    6s   1GB
Oct 24 01:10:27 Starting compiler/backend/arm8
Oct 24 01:10:35 Finished compiler/backend/arm8                                    6s   1GB
Oct 24 01:10:35 Starting compiler/backend/mips
Oct 24 01:10:43 Finished compiler/backend/mips                                    6s   1GB
Oct 24 01:10:44 Starting compiler/backend/riscv
Oct 24 01:10:51 Finished compiler/backend/riscv                                   6s   1GB
Oct 24 01:10:52 Starting compiler/backend/ag32
Oct 24 01:12:09 Finished compiler/backend/ag32                                 1m16s   1GB
Oct 24 01:12:10 Starting compiler/backend/pattern_matching
Oct 24 01:12:32 Finished compiler/backend/pattern_matching                       20s   1GB
Oct 24 01:12:33 Starting compiler/printing
Oct 24 01:13:38 Finished compiler/printing                                     1m03s   1GB
Oct 24 01:13:39 Starting compiler/parsing/proofs
Oct 24 01:13:46 Finished compiler/parsing/proofs                                  6s   1GB
Oct 24 01:13:47 Starting compiler/inference/proofs
Oct 24 01:13:55 Finished compiler/inference/proofs                                6s   1GB
Oct 24 01:13:55 Starting compiler/backend/semantics
Oct 24 01:16:36 Finished compiler/backend/semantics                            2m39s   1GB
Oct 24 01:16:37 Starting compiler/backend/reg_alloc/proofs
Oct 24 01:16:44 Finished compiler/backend/reg_alloc/proofs                        6s   1GB
Oct 24 01:16:45 Starting compiler/backend/proofs
Oct 24 01:17:43 Finished compiler/backend/proofs                                 56s   3GB
Oct 24 01:17:44 Starting compiler/backend/serialiser
Oct 24 01:17:52 Finished compiler/backend/serialiser                              6s   1GB
Oct 24 01:17:52 Starting compiler/encoders/x64/proofs
Oct 24 01:18:00 Finished compiler/encoders/x64/proofs                             6s   1GB
Oct 24 01:18:01 Starting compiler/encoders/arm7/proofs
Oct 24 01:31:08 Finished compiler/encoders/arm7/proofs                        13m06s   6GB
Oct 24 01:31:09 Starting compiler/encoders/arm8/proofs
Oct 24 01:43:48 Finished compiler/encoders/arm8/proofs                        12m38s  16GB
Oct 24 01:43:49 Starting compiler/encoders/arm8_asl/proofs
Oct 24 02:12:19 Finished compiler/encoders/arm8_asl/proofs                    28m28s  33GB
Oct 24 02:12:20 Starting compiler/encoders/mips/proofs
Oct 24 02:24:19 Finished compiler/encoders/mips/proofs                        11m57s   5GB
Oct 24 02:24:20 Starting compiler/encoders/riscv/proofs
Oct 24 02:34:40 Finished compiler/encoders/riscv/proofs                       10m18s   3GB
Oct 24 02:34:41 Starting compiler/encoders/ag32/proofs
Oct 24 02:38:09 Finished compiler/encoders/ag32/proofs                         3m26s   1GB
Oct 24 02:38:10 Starting compiler/backend/x64/proofs
Oct 24 02:38:17 Finished compiler/backend/x64/proofs                              6s   1GB
Oct 24 02:38:18 Starting compiler/backend/arm7/proofs
Oct 24 02:39:04 Finished compiler/backend/arm7/proofs                            45s   2GB
Oct 24 02:39:05 Starting compiler/backend/arm8/proofs
Oct 24 02:39:55 Finished compiler/backend/arm8/proofs                            48s   2GB
Oct 24 02:39:55 Starting compiler/backend/arm8_asl
Oct 24 02:40:43 Finished compiler/backend/arm8_asl                               46s   2GB
Oct 24 02:40:43 Starting compiler/backend/mips/proofs
Oct 24 02:41:35 Finished compiler/backend/mips/proofs                            50s   2GB
Oct 24 02:41:36 Starting compiler/backend/riscv/proofs
Oct 24 02:42:29 Finished compiler/backend/riscv/proofs                           51s   2GB
Oct 24 02:42:30 Starting compiler/backend/San
Oct 24 02:43:47 Finished compiler/backend/San                                  1m15s   4GB
Oct 24 02:43:48 Starting compiler/backend/ag32/proofs
Oct 24 02:53:38 Finished compiler/backend/ag32/proofs                          9m49s   4GB
Oct 24 02:53:39 Starting compiler/backend/cv_compute
Oct 24 02:54:17 Finished compiler/backend/cv_compute                             36s   1GB
Oct 24 02:54:17 Starting cv_translator
Oct 24 02:57:28 Finished cv_translator                                         3m09s   3GB
Oct 24 02:57:29 Starting candle
Oct 24 02:57:36 Finished candle                                                   6s   1GB
Oct 24 02:57:37 Starting candle/set-theory
Oct 24 02:58:01 Finished candle/set-theory                                       23s   1GB
Oct 24 02:58:02 Starting candle/syntax-lib
Oct 24 02:58:10 Finished candle/syntax-lib                                        6s   1GB
Oct 24 02:58:11 Starting candle/standard
Oct 24 02:58:18 Finished candle/standard                                          6s   1GB
Oct 24 02:58:19 Starting candle/standard/syntax
Oct 24 02:58:41 Finished candle/standard/syntax                                  20s   1GB
Oct 24 02:58:42 Starting candle/standard/syntax/little_theories
Oct 24 03:00:53 Finished candle/standard/syntax/little_theories                2m09s   1GB
Oct 24 03:00:54 Starting candle/standard/semantics
Oct 24 03:01:01 Finished candle/standard/semantics                                6s   1GB
Oct 24 03:01:02 Starting candle/standard/monadic
Oct 24 03:01:10 Finished candle/standard/monadic                                  6s   1GB
Oct 24 03:01:11 Starting candle/standard/ml_kernel
Oct 24 03:04:01 Finished candle/standard/ml_kernel                             2m49s   6GB
Oct 24 03:04:02 Starting candle/overloading
Oct 24 03:04:09 Finished candle/overloading                                       6s   1GB
Oct 24 03:04:10 Starting candle/overloading/syntax
Oct 24 03:07:31 Finished candle/overloading/syntax                             3m19s   2GB
Oct 24 03:07:32 Starting candle/overloading/semantics
Oct 24 03:16:20 Finished candle/overloading/semantics                          8m47s   4GB
Oct 24 03:16:21 Starting candle/overloading/monadic
Oct 24 03:18:42 Finished candle/overloading/monadic                            2m20s   1GB
Oct 24 03:18:43 Starting candle/overloading/ml_kernel
Oct 24 03:26:59 Finished candle/overloading/ml_kernel                          8m14s   8GB
Oct 24 03:27:00 Starting candle/overloading/ml_checker
Oct 24 03:29:29 Finished candle/overloading/ml_checker                         2m27s   7GB
Oct 24 03:29:30 Starting candle/prover
Oct 24 03:29:37 Finished candle/prover                                            6s   1GB
Oct 24 03:29:38 Starting candle/prover/compute
Oct 24 03:29:46 Finished candle/prover/compute                                    6s   1GB
Oct 24 03:29:47 Starting candle/parser
Oct 24 03:29:54 Finished candle/parser                                            6s   1GB
Oct 24 03:29:55 Starting pancake
Oct 24 03:30:02 Finished pancake                                                  6s   1GB
Oct 24 03:30:03 Starting pancake/semantics
Oct 24 03:33:40 Finished pancake/semantics                                     3m35s   2GB
Oct 24 03:33:41 Starting pancake/parser
Oct 24 03:34:33 Finished pancake/parser                                          51s   1GB
Oct 24 03:34:34 Starting pancake/static_checker
Oct 24 03:37:23 Finished pancake/static_checker                                2m47s   1GB
Oct 24 03:37:23 Starting pancake/proofs
Oct 24 03:48:04 FAILED: pancake/proofs
  HOLORIG=/scratch/regbox/regression/cakeml-3639/pancake/proofs [ -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/parser
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/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/semantics
Scanning $(CAKEMLDIR)/compiler/encoders/asm
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)/misc
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/backend/San
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/proofs
Scanning $(CAKEMLDIR)/compiler/backend/riscv
Scanning $(CAKEMLDIR)/compiler/backend/riscv/proofs
Scanning $(CAKEMLDIR)/compiler/backend/serialiser
Scanning $(CAKEMLDIR)/compiler/backend/tests
Scanning $(CAKEMLDIR)/compiler/backend/x64
Scanning $(CAKEMLDIR)/compiler/backend/x64/proofs
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/export/x64/64
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)/unverified/sexpr-bootstrap/export/32
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/export/arm8/64
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 $(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 $(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/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)/pancake
Scanning $(CAKEMLDIR)/pancake/parser
Scanning $(CAKEMLDIR)/pancake/semantics
Scanning $(CAKEMLDIR)/pancake/decompiler
Scanning $(CAKEMLDIR)/pancake/decompiler/examples
Scanning $(CAKEMLDIR)/pancake/proofs
Scanning $(CAKEMLDIR)/pancake/static_checker
Scanning $(CAKEMLDIR)/pancake/temp
Scanning $(CAKEMLDIR)/profiler
Scanning $(CAKEMLDIR)/semantics/alt_semantics
Scanning $(CAKEMLDIR)/semantics/alt_semantics/proofs
Scanning $(CAKEMLDIR)/semantics/ffi
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/export
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/export/arm8
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/export/x64
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 $(cnf)/xlrup
Scanning $(cnf)/xlrup/array
Scanning $(cnf)/xlrup/array/compilation
Scanning $(cnf)/xlrup/array/compilation/proofs
Scanning $(hwmcc_checker)/compilation
Scanning $(hwmcc_checker)/compilation/proofs
Scanning $(hwmcc_checker)/examples
Scanning $(hwmcc_checker)/translation
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 313 directories
Building 13 theory files
Starting work on README.md
Starting work on crep_arithProofTheory
Starting work on crep_inlineProofTheory
Starting work on loop_callProofTheory
README.md                                                   (0s)             OK
Starting work on loop_to_wordProofTheory
crep_arithProofTheory                                      (10s)  [1/13]     OK
Starting work on pan_globalsProofTheory
loop_callProofTheory                                       (20s)  [2/13]     OK
Starting work on loop_liveProofTheory
loop_liveProofTheory                                       (19s)  [3/13]     OK
Starting work on crep_to_loopProofTheory
crep_inlineProofTheory                                     (72s)  [4/13]     OK
Starting work on pan_itreeEquivProofTheory
crep_to_loopProofTheory                                    (55s)  [5/13]     OK
Starting work on pan_simpProofTheory
loop_to_wordProofTheory                                    (99s)  [6/13]     OK
Starting work on pan_structsProofTheory
pan_globalsProofTheory                                     (87s)  [7/13]     OK
Starting work on pan_to_crepProofTheory
pan_structsProofTheory                                     (24s)  [8/13]     OK
pan_simpProofTheory                                        (30s)  [9/13]     OK
pan_to_crepProofTheory                                    (203s) [10/13]     OK
Starting work on pan_to_wordProofTheory
pan_to_wordProofTheory                                     (43s) [11/13]     OK
Starting work on pan_to_targetProofTheory
pan_to_targetProofTheory                                  (260s)        FAIL<1>
pan_itreeEquivProofTheory                                 (531s)         killed
*** Holmake aborted - 1 target failed:
*** pan_to_targetProofTheory (status 1)
 Saved theorem _______ "get_var_imm_const_memory"
 Saved theorem _______ "mem_load_const_memory"
 Saved theorem _______ "mem_store_const_memory"
 Saved theorem _______ "mem_load_32_const_memory"
 Saved theorem _______ "mem_store_32_const_memory"
 Saved theorem _______ "word_exp_const_memory"
 Saved theorem _______ "mem_load_byte_aux_const_memory"
 Saved theorem _______ "mem_store_byte_aux_const_memory"
 Saved theorem _______ "read_bytearray_const_memory"
 Saved theorem _______ "write_bytearray_const_memory"
 Saved theorem _______ "inst_const_memory"
 Saved theorem _______ "const_writes_const_memory"
 Saved theorem _______ "share_inst_const_memory"
 Proved triviality ___ "mem_upd_lemma"
 Proved triviality ___ "push_env_mem_upd"
 Proved triviality ___ "push_env_mem_const"
 Proved triviality ___ "cut_state_with_mem_const"
 <<HOL message: Stashing suspended theorem memory_swap_lemma1 with pending subgoal: Loop.>>
 <<HOL warning: boolLib.save_thm_attrs: Ignoring attributes on suspended theorem memory_swap_lemma1; apply them at Finalise time instead>>
 Saved theorem _______ "memory_swap_lemma1"
 Proved triviality ___ "memory_swap_lemma"
 Saved theorem _______ "word_semantics_memory_update"
 Saved theorem _______ "word_to_word_compile_no_install_no_alloc"
 Saved theorem _______ "no_alloc_word_evaluate"
 Saved theorem _______ "panLang_wordSem_neq_NotEnoughSpace"
 Saved theorem _______ "inst_stack_size_const_panLang"
 Saved theorem _______ "inst_stack_limit_const_panLang"
 Saved theorem _______ "inst_stack_max_const_panLang"
 Saved theorem _______ "share_inst_modifies"
 Saved theorem _______ "evaluate_stack_size_limit_const_panLang"
 Saved definition ____ "compile_prog_max_def"
 Saved definition ____ "option_lt_def"
 Saved induction _____ "option_lt_ind"
 Saved theorem _______ "option_lt_SOME"
 Saved theorem _______ "from_pan_to_lab_no_install"
 Proved triviality ___ "n2w_sub_alt"
 Proved triviality ___ "aligned_n2w_IMP"
 Saved theorem _______ "word_list_exists_addresses"
 Saved theorem _______ "good_dimindex_div_mul"
 Proof of 
 
 InitGlobals_location = first_name
 
 failed.
 First unsolved sub-goal is
 
 F
 
 Tactic failure proving "InitGlobals_location_eq_first_name"; heap saved to pan_to_targetProof.InitGlobals_location_eq_first_name.dumpedheap.
 Resume with: bin/hol --holstate=pan_to_targetProof.InitGlobals_location_eq_first_name.dumpedheap
 Full log: /scratch/regbox/regression/cakeml-3639/pancake/proofs/.hol/logs/pan_to_targetProofTheory