CakeML Regression Test

Job 3593

CakeML:5d87655e39f14a73e7eae69891cc252a6112f9ae
  Preserve metadata in stack display translation [Oct 08 02:56:40]
#1535 (metadata)
Merging into:f8da03aeecd4d58a35bb88286780ff7e7e4ca7d6
  Merge pull request #1508 from CakeML/source-dce [Oct 07 07:48:42]
HOL:652d1f0aad5cd537ed1e5d470ba3444e70ba470e
  Merge remote-tracking branch 'origin/master' into develop [Sep 27 02:14:15]
Machine:spagbol

Oct 08 06:02:18 Claimed job
Oct 08 06:02:23 Reusing HOL
Oct 08 06:02:32 Starting developers
Oct 08 06:03:30 Finished developers                                              56s   1GB
Oct 08 06:03:31 Starting developers/bin
Oct 08 06:03:40 Finished developers/bin                                           8s   1GB
Oct 08 06:03:41 Starting misc
Oct 08 06:04:27 Finished misc                                                    44s   1GB
Oct 08 06:04:28 Starting compiler/proofs
Oct 08 07:22:00 Finished compiler/proofs                                    1h17m31s  10GB
Oct 08 07:22:01 Starting compiler/bootstrap/compilation/x64/64/proofs
Oct 08 14:46:27 Finished compiler/bootstrap/compilation/x64/64/proofs       7h24m24s  79GB
Oct 08 14:46:28 Starting semantics/ffi
Oct 08 14:46:51 Finished semantics/ffi                                           22s   1GB
Oct 08 14:46:52 Starting semantics
Oct 08 14:47:00 Finished semantics                                                6s   1GB
Oct 08 14:47:01 Starting semantics/proofs
Oct 08 14:47:33 Finished semantics/proofs                                        31s   1GB
Oct 08 14:47:34 Starting semantics/alt_semantics
Oct 08 14:47:59 Finished semantics/alt_semantics                                 23s   1GB
Oct 08 14:47:59 Starting semantics/alt_semantics/proofs
Oct 08 14:52:07 Finished semantics/alt_semantics/proofs                        4m06s   1GB
Oct 08 14:52:08 Starting basis/pure
Oct 08 14:52:16 Finished basis/pure                                               6s   1GB
Oct 08 14:52:17 Starting translator
Oct 08 14:53:34 Finished translator                                            1m15s   3GB
Oct 08 14:53:35 Starting compiler/parsing
Oct 08 14:54:29 Finished compiler/parsing                                        53s   2GB
Oct 08 14:54:30 Starting characteristic
Oct 08 14:54:37 Finished characteristic                                           6s   1GB
Oct 08 14:54:38 Starting translator/monadic
Oct 08 14:54:45 Finished translator/monadic                                       6s   1GB
Oct 08 14:54:46 Starting translator/monadic/monad_base
Oct 08 14:54:54 Finished translator/monadic/monad_base                            6s   1GB
Oct 08 14:54:54 Starting profiler
Oct 08 14:55:30 Finished profiler                                                34s   1GB
Oct 08 14:55:31 Starting basis
Oct 08 14:57:24 Finished basis                                                 1m51s   4GB
Oct 08 14:57:25 Starting compiler
Oct 08 14:57:32 Finished compiler                                                 6s   1GB
Oct 08 14:57:33 Starting compiler/inference
Oct 08 14:57:41 Finished compiler/inference                                       6s   1GB
Oct 08 14:57:42 Starting compiler/backend/reg_alloc
Oct 08 14:57:49 Finished compiler/backend/reg_alloc                               6s   1GB
Oct 08 14:57:50 Starting compiler/backend/gc
Oct 08 14:57:57 Finished compiler/backend/gc                                      6s   1GB
Oct 08 14:57:58 Starting compiler/backend
Oct 08 14:58:09 Finished compiler/backend                                         9s   1GB
Oct 08 14:58:10 Starting compiler/encoders/asm
Oct 08 14:58:17 Finished compiler/encoders/asm                                    6s   1GB
Oct 08 14:58:18 Starting compiler/encoders/x64
Oct 08 14:58:25 Finished compiler/encoders/x64                                    6s   1GB
Oct 08 14:58:26 Starting compiler/encoders/arm7
Oct 08 14:58:34 Finished compiler/encoders/arm7                                   6s   1GB
Oct 08 14:58:35 Starting compiler/encoders/arm8
Oct 08 14:58:42 Finished compiler/encoders/arm8                                   6s   1GB
Oct 08 14:58:43 Starting compiler/encoders/arm8_asl
Oct 08 14:59:07 Finished compiler/encoders/arm8_asl                              23s   1GB
Oct 08 14:59:08 Starting compiler/encoders/mips
Oct 08 14:59:15 Finished compiler/encoders/mips                                   6s   1GB
Oct 08 14:59:16 Starting compiler/encoders/riscv
Oct 08 14:59:24 Finished compiler/encoders/riscv                                  6s   1GB
Oct 08 14:59:24 Starting compiler/encoders/ag32
Oct 08 14:59:32 Finished compiler/encoders/ag32                                   6s   1GB
Oct 08 14:59:33 Starting compiler/encoders/tests
Oct 08 15:00:16 Finished compiler/encoders/tests                                 42s   2GB
Oct 08 15:00:17 Starting compiler/encoders/monadic_enc
Oct 08 15:00:45 Finished compiler/encoders/monadic_enc                           26s   1GB
Oct 08 15:00:46 Starting compiler/backend/x64
Oct 08 15:00:53 Finished compiler/backend/x64                                     6s   1GB
Oct 08 15:00:54 Starting compiler/backend/arm7
Oct 08 15:01:01 Finished compiler/backend/arm7                                    6s   1GB
Oct 08 15:01:02 Starting compiler/backend/arm8
Oct 08 15:01:10 Finished compiler/backend/arm8                                    6s   1GB
Oct 08 15:01:11 Starting compiler/backend/mips
Oct 08 15:01:18 Finished compiler/backend/mips                                    6s   1GB
Oct 08 15:01:19 Starting compiler/backend/riscv
Oct 08 15:01:26 Finished compiler/backend/riscv                                   6s   1GB
Oct 08 15:01:27 Starting compiler/backend/ag32
Oct 08 15:02:34 Finished compiler/backend/ag32                                 1m05s   1GB
Oct 08 15:02:35 Starting compiler/backend/pattern_matching
Oct 08 15:02:57 Finished compiler/backend/pattern_matching                       20s   1GB
Oct 08 15:02:58 Starting compiler/parsing/ocaml
Oct 08 15:05:28 Finished compiler/parsing/ocaml                                2m29s   1GB
Oct 08 15:05:29 Starting compiler/printing
Oct 08 15:06:24 Finished compiler/printing                                       54s   1GB
Oct 08 15:06:25 Starting compiler/parsing/proofs
Oct 08 15:06:33 Finished compiler/parsing/proofs                                  6s   1GB
Oct 08 15:06:34 Starting compiler/inference/proofs
Oct 08 15:06:41 Finished compiler/inference/proofs                                6s   1GB
Oct 08 15:06:42 Starting compiler/backend/semantics
Oct 08 15:10:09 Finished compiler/backend/semantics                            3m26s   3GB
Oct 08 15:10:10 Starting compiler/backend/reg_alloc/proofs
Oct 08 15:10:18 Finished compiler/backend/reg_alloc/proofs                        6s   1GB
Oct 08 15:10:19 Starting compiler/backend/proofs
Oct 08 15:11:09 Finished compiler/backend/proofs                                 49s   2GB
Oct 08 15:11:10 Starting compiler/backend/serialiser
Oct 08 15:11:18 Finished compiler/backend/serialiser                              6s   1GB
Oct 08 15:11:19 Starting compiler/encoders/x64/proofs
Oct 08 15:11:26 Finished compiler/encoders/x64/proofs                             6s   1GB
Oct 08 15:11:27 Starting compiler/encoders/arm7/proofs
Oct 08 15:24:20 Finished compiler/encoders/arm7/proofs                        12m51s   8GB
Oct 08 15:24:21 Starting compiler/encoders/arm8/proofs
Oct 08 15:36:37 Finished compiler/encoders/arm8/proofs                        12m15s  14GB
Oct 08 15:36:38 Starting compiler/encoders/arm8_asl/proofs
Oct 08 16:04:53 Finished compiler/encoders/arm8_asl/proofs                    28m13s  34GB
Oct 08 16:04:54 Starting compiler/encoders/mips/proofs
Oct 08 16:16:38 Finished compiler/encoders/mips/proofs                        11m42s   8GB
Oct 08 16:16:39 Starting compiler/encoders/riscv/proofs
Oct 08 16:26:46 Finished compiler/encoders/riscv/proofs                       10m06s   3GB
Oct 08 16:26:47 Starting compiler/encoders/ag32/proofs
Oct 08 16:30:07 Finished compiler/encoders/ag32/proofs                         3m19s   1GB
Oct 08 16:30:08 Starting compiler/backend/x64/proofs
Oct 08 16:30:15 Finished compiler/backend/x64/proofs                              6s   1GB
Oct 08 16:30:16 Starting compiler/backend/arm7/proofs
Oct 08 16:30:59 Finished compiler/backend/arm7/proofs                            41s   2GB
Oct 08 16:31:00 Starting compiler/backend/arm8/proofs
Oct 08 16:31:43 Finished compiler/backend/arm8/proofs                            41s   2GB
Oct 08 16:31:43 Starting compiler/backend/arm8_asl
Oct 08 16:32:25 Finished compiler/backend/arm8_asl                               40s   2GB
Oct 08 16:32:26 Starting compiler/backend/mips/proofs
Oct 08 16:33:10 Finished compiler/backend/mips/proofs                            43s   2GB
Oct 08 16:33:11 Starting compiler/backend/riscv/proofs
Oct 08 16:33:56 Finished compiler/backend/riscv/proofs                           43s   2GB
Oct 08 16:33:57 Starting compiler/backend/ag32/proofs
Oct 08 16:43:22 Finished compiler/backend/ag32/proofs                          9m24s   4GB
Oct 08 16:43:23 Starting compiler/backend/cv_compute
Oct 08 16:43:58 Finished compiler/backend/cv_compute                             34s   1GB
Oct 08 16:43:59 Starting cv_translator
Oct 08 16:50:00 Finished cv_translator                                         5m59s   3GB
Oct 08 16:50:01 Starting candle
Oct 08 16:50:08 Finished candle                                                   6s   1GB
Oct 08 16:50:09 Starting candle/set-theory
Oct 08 16:50:32 Finished candle/set-theory                                       21s   1GB
Oct 08 16:50:33 Starting candle/syntax-lib
Oct 08 16:50:41 Finished candle/syntax-lib                                        6s   1GB
Oct 08 16:50:42 Starting candle/standard
Oct 08 16:50:49 Finished candle/standard                                          6s   1GB
Oct 08 16:50:50 Starting candle/standard/syntax
Oct 08 16:51:11 Finished candle/standard/syntax                                  20s   1GB
Oct 08 16:51:12 Starting candle/standard/syntax/little_theories
Oct 08 16:53:14 Finished candle/standard/syntax/little_theories                2m00s   1GB
Oct 08 16:53:15 Starting candle/standard/semantics
Oct 08 16:53:23 Finished candle/standard/semantics                                6s   1GB
Oct 08 16:53:24 Starting candle/standard/monadic
Oct 08 16:53:31 Finished candle/standard/monadic                                  6s   1GB
Oct 08 16:53:32 Starting candle/standard/ml_kernel
Oct 08 16:55:42 Finished candle/standard/ml_kernel                             2m09s   4GB
Oct 08 16:55:43 Starting candle/overloading
Oct 08 16:55:50 Finished candle/overloading                                       6s   1GB
Oct 08 16:55:51 Starting candle/overloading/syntax
Oct 08 16:59:11 Finished candle/overloading/syntax                             3m18s   1GB
Oct 08 16:59:12 Starting candle/overloading/semantics
Oct 08 17:08:52 Finished candle/overloading/semantics                          9m39s   7GB
Oct 08 17:08:53 Starting candle/overloading/monadic
Oct 08 17:11:00 Finished candle/overloading/monadic                            2m05s   1GB
Oct 08 17:11:01 Starting candle/overloading/ml_kernel
Oct 08 17:18:21 Finished candle/overloading/ml_kernel                          7m19s   6GB
Oct 08 17:18:22 Starting candle/overloading/ml_checker
Oct 08 17:20:36 Finished candle/overloading/ml_checker                         2m13s   6GB
Oct 08 17:20:37 Starting candle/prover
Oct 08 17:20:45 Finished candle/prover                                            6s   1GB
Oct 08 17:20:46 Starting candle/prover/compute
Oct 08 17:20:53 Finished candle/prover/compute                                    6s   1GB
Oct 08 17:20:54 Starting pancake
Oct 08 17:21:02 Finished pancake                                                  6s   1GB
Oct 08 17:21:03 Starting pancake/semantics
Oct 08 17:24:19 Finished pancake/semantics                                     3m14s   2GB
Oct 08 17:24:20 Starting pancake/parser
Oct 08 17:25:07 Finished pancake/parser                                          46s   1GB
Oct 08 17:25:08 Starting pancake/static_checker
Oct 08 17:27:51 Finished pancake/static_checker                                2m41s   1GB
Oct 08 17:27:52 Starting pancake/proofs
Oct 08 17:28:06 FAILED: pancake/proofs
  HOLORIG=/scratch/regbox/regression/cakeml-3593/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/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/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/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)/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 $(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
Scanning $(xlrup_checker)/array
Scanning $(xlrup_checker)/array/compilation
Scanning $(xlrup_checker)/array/compilation/proofs
Scanned 311 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
loop_to_wordProofTheory                                     (5s)        FAIL<1>
crep_arithProofTheory                                       (6s)         killed
crep_inlineProofTheory                                      (6s)         killed
loop_callProofTheory                                        (6s)         killed
*** Holmake aborted - 1 target failed:
*** loop_to_wordProofTheory (status 1)
 <<HOL message: Created theory "loop_to_wordProof">>
 Saved definition ____ "locals_rel_def"
 Saved definition ____ "globals_rel_def"
 Saved definition ____ "code_rel_def"
 
 Exception raised at TotalDefn.xDefine:
 at Defn.Hol_defn: between line 41, character 2 and line 53, character 25:
 at Defn.parse_quote:
 at Preterm.type-analysis: on line 53, characters 22-25:
   Couldn't infer type for overloaded name  _ record selectcode
 Full log: /scratch/regbox/regression/cakeml-3593/pancake/proofs/.hol/logs/loop_to_wordProofTheory