Job 3567

CakeML:c87f05aad2c67f661098a2713194808ab751cc81
  add DecompIt to changes-since-release.md [Sep 24 10:39:04]
#1492 (pan_decompiler)
Merging into:6d0be5ffab23f1e6a9437cbaad3dfb0699c3f2ae
  Merge pull request #1511 from CakeML/mcandidate-fix [Oct 01 09:44:16]
HOL:652d1f0aad5cd537ed1e5d470ba3444e70ba470e
  Merge remote-tracking branch 'origin/master' into develop [Sep 27 02:14:15]
Machine:pavlova

Oct 01 17:03:55 Claimed job
Oct 01 17:04:00 Reusing HOL
Oct 01 17:05:01 Starting developers
Oct 01 17:05:54 Finished developers                                              51s   1GB
Oct 01 17:05:55 Starting developers/bin
Oct 01 17:06:04 Finished developers/bin                                           8s   1GB
Oct 01 17:06:05 Starting misc
Oct 01 17:06:51 Finished misc                                                    45s   1GB
Oct 01 17:06:52 Starting compiler/proofs
Oct 01 18:22:15 Finished compiler/proofs                                    1h15m21s  12GB
Oct 01 18:22:16 Starting compiler/bootstrap/compilation/x64/64/proofs
Oct 02 01:04:47 Finished compiler/bootstrap/compilation/x64/64/proofs       6h42m28s  80GB
Oct 02 01:04:47 Starting semantics/ffi
Oct 02 01:05:10 Finished semantics/ffi                                           21s   1GB
Oct 02 01:05:11 Starting semantics
Oct 02 01:05:18 Finished semantics                                                6s   1GB
Oct 02 01:05:19 Starting semantics/proofs
Oct 02 01:05:50 Finished semantics/proofs                                        30s   1GB
Oct 02 01:05:51 Starting semantics/alt_semantics
Oct 02 01:06:13 Finished semantics/alt_semantics                                 21s   1GB
Oct 02 01:06:14 Starting semantics/alt_semantics/proofs
Oct 02 01:10:26 Finished semantics/alt_semantics/proofs                        4m11s   1GB
Oct 02 01:10:27 Starting basis/pure
Oct 02 01:10:35 Finished basis/pure                                               6s   1GB
Oct 02 01:10:36 Starting translator
Oct 02 01:11:54 Finished translator                                            1m17s   2GB
Oct 02 01:11:55 Starting compiler/parsing
Oct 02 01:12:46 Finished compiler/parsing                                        50s   1GB
Oct 02 01:12:47 Starting characteristic
Oct 02 01:12:55 Finished characteristic                                           6s   1GB
Oct 02 01:12:56 Starting translator/monadic
Oct 02 01:13:03 Finished translator/monadic                                       6s   1GB
Oct 02 01:13:04 Starting translator/monadic/monad_base
Oct 02 01:13:11 Finished translator/monadic/monad_base                            6s   1GB
Oct 02 01:13:12 Starting profiler
Oct 02 01:13:47 Finished profiler                                                33s   1GB
Oct 02 01:13:48 Starting basis
Oct 02 01:15:36 Finished basis                                                 1m46s   4GB
Oct 02 01:15:37 Starting compiler
Oct 02 01:15:44 Finished compiler                                                 6s   1GB
Oct 02 01:15:45 Starting compiler/inference
Oct 02 01:15:52 Finished compiler/inference                                       6s   1GB
Oct 02 01:15:53 Starting compiler/backend/reg_alloc
Oct 02 01:16:00 Finished compiler/backend/reg_alloc                               6s   1GB
Oct 02 01:16:01 Starting compiler/backend/gc
Oct 02 01:16:08 Finished compiler/backend/gc                                      6s   1GB
Oct 02 01:16:09 Starting compiler/backend
Oct 02 01:16:20 Finished compiler/backend                                         9s   1GB
Oct 02 01:16:21 Starting compiler/encoders/asm
Oct 02 01:16:28 Finished compiler/encoders/asm                                    6s   1GB
Oct 02 01:16:29 Starting compiler/encoders/x64
Oct 02 01:16:36 Finished compiler/encoders/x64                                    6s   1GB
Oct 02 01:16:37 Starting compiler/encoders/arm7
Oct 02 01:16:44 Finished compiler/encoders/arm7                                   6s   1GB
Oct 02 01:16:45 Starting compiler/encoders/arm8
Oct 02 01:16:52 Finished compiler/encoders/arm8                                   6s   1GB
Oct 02 01:16:53 Starting compiler/encoders/arm8_asl
Oct 02 03:48:55 Finished compiler/encoders/arm8_asl                         2h31m59s  36GB
Oct 02 03:48:56 Starting compiler/encoders/mips
Oct 02 03:49:03 Finished compiler/encoders/mips                                   6s   1GB
Oct 02 03:49:04 Starting compiler/encoders/riscv
Oct 02 03:49:12 Finished compiler/encoders/riscv                                  6s   1GB
Oct 02 03:49:12 Starting compiler/encoders/ag32
Oct 02 03:49:20 Finished compiler/encoders/ag32                                   6s   1GB
Oct 02 03:49:20 Starting compiler/encoders/tests
Oct 02 03:49:28 Finished compiler/encoders/tests                                  6s   1GB
Oct 02 03:49:29 Starting compiler/encoders/monadic_enc
Oct 02 03:49:55 Finished compiler/encoders/monadic_enc                           24s   1GB
Oct 02 03:49:56 Starting compiler/backend/x64
Oct 02 03:50:03 Finished compiler/backend/x64                                     6s   1GB
Oct 02 03:50:04 Starting compiler/backend/arm7
Oct 02 03:50:11 Finished compiler/backend/arm7                                    6s   1GB
Oct 02 03:50:12 Starting compiler/backend/arm8
Oct 02 03:50:19 Finished compiler/backend/arm8                                    6s   1GB
Oct 02 03:50:20 Starting compiler/backend/mips
Oct 02 03:50:27 Finished compiler/backend/mips                                    6s   1GB
Oct 02 03:50:28 Starting compiler/backend/riscv
Oct 02 03:50:35 Finished compiler/backend/riscv                                   6s   1GB
Oct 02 03:50:36 Starting compiler/backend/ag32
Oct 02 03:51:45 Finished compiler/backend/ag32                                 1m08s   1GB
Oct 02 03:51:46 Starting compiler/backend/pattern_matching
Oct 02 03:52:07 Finished compiler/backend/pattern_matching                       20s   1GB
Oct 02 03:52:08 Starting compiler/parsing/ocaml
Oct 02 03:54:25 Finished compiler/parsing/ocaml                                2m16s   1GB
Oct 02 03:54:26 Starting compiler/printing
Oct 02 03:55:23 Finished compiler/printing                                       55s   1GB
Oct 02 03:55:24 Starting compiler/parsing/proofs
Oct 02 03:55:31 Finished compiler/parsing/proofs                                  6s   1GB
Oct 02 03:55:32 Starting compiler/inference/proofs
Oct 02 03:55:39 Finished compiler/inference/proofs                                6s   1GB
Oct 02 03:55:40 Starting compiler/backend/semantics
Oct 02 03:59:04 Finished compiler/backend/semantics                            3m23s   3GB
Oct 02 03:59:05 Starting compiler/backend/reg_alloc/proofs
Oct 02 03:59:13 Finished compiler/backend/reg_alloc/proofs                        6s   1GB
Oct 02 03:59:14 Starting compiler/backend/proofs
Oct 02 04:00:08 Finished compiler/backend/proofs                                 53s   3GB
Oct 02 04:00:09 Starting compiler/backend/serialiser
Oct 02 04:00:16 Finished compiler/backend/serialiser                              6s   1GB
Oct 02 04:00:17 Starting compiler/encoders/x64/proofs
Oct 02 04:00:24 Finished compiler/encoders/x64/proofs                             6s   1GB
Oct 02 04:00:25 Starting compiler/encoders/arm7/proofs
Oct 02 04:13:00 Finished compiler/encoders/arm7/proofs                        12m32s   5GB
Oct 02 04:13:01 Starting compiler/encoders/arm8/proofs
Oct 02 04:21:48 Finished compiler/encoders/arm8/proofs                         8m45s   3GB
Oct 02 04:21:49 Starting compiler/encoders/arm8_asl/proofs
Oct 02 05:18:46 Finished compiler/encoders/arm8_asl/proofs                    56m54s   8GB
Oct 02 05:18:47 Starting compiler/encoders/mips/proofs
Oct 02 05:29:27 Finished compiler/encoders/mips/proofs                        10m39s  10GB
Oct 02 05:29:28 Starting compiler/encoders/riscv/proofs
Oct 02 05:39:19 Finished compiler/encoders/riscv/proofs                        9m49s   3GB
Oct 02 05:39:20 Starting compiler/encoders/ag32/proofs
Oct 02 05:42:41 Finished compiler/encoders/ag32/proofs                         3m19s   1GB
Oct 02 05:42:41 Starting compiler/backend/x64/proofs
Oct 02 05:42:49 Finished compiler/backend/x64/proofs                              6s   1GB
Oct 02 05:42:50 Starting compiler/backend/arm7/proofs
Oct 02 05:43:31 Finished compiler/backend/arm7/proofs                            40s   2GB
Oct 02 05:43:32 Starting compiler/backend/arm8/proofs
Oct 02 05:44:16 Finished compiler/backend/arm8/proofs                            43s   2GB
Oct 02 05:44:17 Starting compiler/backend/arm8_asl
Oct 02 05:45:00 Finished compiler/backend/arm8_asl                               41s   2GB
Oct 02 05:45:01 Starting compiler/backend/mips/proofs
Oct 02 05:45:47 Finished compiler/backend/mips/proofs                            45s   2GB
Oct 02 05:45:48 Starting compiler/backend/riscv/proofs
Oct 02 05:46:33 Finished compiler/backend/riscv/proofs                           43s   2GB
Oct 02 05:46:34 Starting compiler/backend/ag32/proofs
Oct 02 05:56:04 Finished compiler/backend/ag32/proofs                          9m29s   4GB
Oct 02 05:56:05 Starting compiler/backend/cv_compute
Oct 02 05:56:42 Finished compiler/backend/cv_compute                             36s   1GB
Oct 02 05:56:43 Starting cv_translator
Oct 02 06:02:00 Finished cv_translator                                         5m15s   3GB
Oct 02 06:02:01 Starting candle
Oct 02 06:02:08 Finished candle                                                   6s   1GB
Oct 02 06:02:09 Starting candle/set-theory
Oct 02 06:02:33 Finished candle/set-theory                                       22s   1GB
Oct 02 06:02:34 Starting candle/syntax-lib
Oct 02 06:02:41 Finished candle/syntax-lib                                        6s   1GB
Oct 02 06:02:42 Starting candle/standard
Oct 02 06:02:49 Finished candle/standard                                          6s   1GB
Oct 02 06:02:50 Starting candle/standard/syntax
Oct 02 06:03:11 Finished candle/standard/syntax                                  19s   1GB
Oct 02 06:03:12 Starting candle/standard/syntax/little_theories
Oct 02 06:05:13 Finished candle/standard/syntax/little_theories                2m00s   1GB
Oct 02 06:05:14 Starting candle/standard/semantics
Oct 02 06:05:21 Finished candle/standard/semantics                                6s   1GB
Oct 02 06:05:22 Starting candle/standard/monadic
Oct 02 06:05:29 Finished candle/standard/monadic                                  6s   1GB
Oct 02 06:05:30 Starting candle/standard/ml_kernel
Oct 02 06:07:57 Finished candle/standard/ml_kernel                             2m25s   4GB
Oct 02 06:07:58 Starting candle/overloading
Oct 02 06:08:05 Finished candle/overloading                                       6s   1GB
Oct 02 06:08:06 Starting candle/overloading/syntax
Oct 02 06:11:38 Finished candle/overloading/syntax                             3m30s   1GB
Oct 02 06:11:39 Starting candle/overloading/semantics
Oct 02 06:21:14 Finished candle/overloading/semantics                          9m33s   6GB
Oct 02 06:21:15 Starting candle/overloading/monadic
Oct 02 06:23:27 Finished candle/overloading/monadic                            2m11s   1GB
Oct 02 06:23:28 Starting candle/overloading/ml_kernel
Oct 02 06:30:42 Finished candle/overloading/ml_kernel                          7m12s   6GB
Oct 02 06:30:43 Starting candle/overloading/ml_checker
Oct 02 06:32:54 Finished candle/overloading/ml_checker                         2m09s   6GB
Oct 02 06:32:55 Starting candle/prover
Oct 02 06:33:02 Finished candle/prover                                            6s   1GB
Oct 02 06:33:03 Starting candle/prover/compute
Oct 02 06:33:11 Finished candle/prover/compute                                    6s   1GB
Oct 02 06:33:12 Starting pancake
Oct 02 06:33:19 Finished pancake                                                  6s   1GB
Oct 02 06:33:20 Starting pancake/semantics
Oct 02 06:36:37 Finished pancake/semantics                                     3m15s   2GB
Oct 02 06:36:37 Starting pancake/parser
Oct 02 06:37:25 Finished pancake/parser                                          46s   1GB
Oct 02 06:37:26 Starting pancake/static_checker
Oct 02 06:40:06 Finished pancake/static_checker                                2m39s   1GB
Oct 02 06:40:08 Starting pancake/proofs
Oct 02 06:56:53 Finished pancake/proofs                                       16m44s   5GB
Oct 02 06:56:54 Starting pancake/decompiler
Oct 02 06:57:48 Finished pancake/decompiler                                      52s   2GB
Oct 02 06:57:49 Starting pancake/decompiler/examples
Oct 02 06:58:31 FAILED: pancake/decompiler/examples
  HOLORIG=/scratch/cakeml/regression/cakeml-3567/pancake/decompiler/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)/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)/misc
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
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 $(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 304 directories
Building 5 theory files
Starting work on README.md
Starting work on fibTheory
Starting work on initSharedArrayTheory
Starting work on revArrayTheory
README.md                                                   (0s)             OK
Starting work on sumFuncTheory
sumFuncTheory                                              (16s)   [1/5]     OK
Starting work on yesTheory
fibTheory                                                  (17s)   [2/5]     OK
yesTheory                                                  (13s)        FAIL<1>
initSharedArrayTheory                                      (31s)         killed
revArrayTheory                                             (31s)         killed
*** Holmake aborted - 1 target failed:
*** yesTheory (status 1)
 /scratch/cakeml/regression/cakeml-3567/pancake/decompiler/panItreeDecompilerLib.sml:423: warning: Pattern is not exhaustive.
 Found near val (eval_call, [state, ...]) = strip_comb trm
 /scratch/cakeml/regression/cakeml-3567/pancake/decompiler/panItreeDecompilerLib.sml:424: warning: Pattern is not exhaustive.
 Found near val (op_call, [w_op, ...]) = strip_comb op_exp
 /scratch/cakeml/regression/cakeml-3567/pancake/decompiler/panItreeDecompilerLib.sml:426: warning: Pattern is not exhaustive.
 Found near val [ty_arg] = ((state |> type_of) |> dest_type) |> snd
 /scratch/cakeml/regression/cakeml-3567/pancake/decompiler/panItreeDecompilerLib.sml:483: warning: Pattern is not exhaustive. Found near val [let_term] = let_list
 /scratch/cakeml/regression/cakeml-3567/pancake/decompiler/panItreeDecompilerLib.sml:743: warning: Pattern is not exhaustive. Found near val (itb, [lt, ...]) = strip_comb t
 /scratch/cakeml/regression/cakeml-3567/pancake/decompiler/panItreeDecompilerLib.sml:931: warning: Pattern is not exhaustive.
 Found near val [from, to] = ((rep_thm |> concl) |> strip_comb) |> snd
 /scratch/cakeml/regression/cakeml-3567/pancake/decompiler/panItreeDecompilerLib.sml:948: warning: Pattern is not exhaustive.
 Found near val [from, to] = ((rep_thm |> concl) |> strip_comb) |> snd
 /scratch/cakeml/regression/cakeml-3567/pancake/decompiler/panItreeDecompilerLib.sml:971: warning: Pattern is not exhaustive.
 Found near val [from, to] = ((rep_thm |> concl) |> strip_comb) |> snd
 /scratch/cakeml/regression/cakeml-3567/pancake/decompiler/panItreeDecompilerLib.sml:993: warning: Pattern is not exhaustive.
 Found near val [from, to] = ((rep_thm |> concl) |> strip_comb) |> snd
 /scratch/cakeml/regression/cakeml-3567/pancake/decompiler/panItreeDecompilerLib.sml:1125: warning: Pattern is not exhaustive.
 Found near val (itc, [progst]) = strip_comb prog_tree
 /scratch/cakeml/regression/cakeml-3567/pancake/decompiler/panItreeDecompilerLib.sml:1126: warning: Pattern is not exhaustive.
 Found near val (_, [prog, ...]) = strip_comb progst
 /scratch/cakeml/regression/cakeml-3567/pancake/decompiler/panItreeDecompilerLib.sml:1183: warning: Pattern is not exhaustive.
 Found near val (itc, [progst]) = strip_comb prog_tree
 /scratch/cakeml/regression/cakeml-3567/pancake/decompiler/panItreeDecompilerLib.sml:1184: warning: Pattern is not exhaustive.
 Found near val (_, [prog, ...]) = strip_comb progst
 /scratch/cakeml/regression/cakeml-3567/pancake/decompiler/panItreeDecompilerLib.sml:1392: warning: Pattern is not exhaustive.
 Found near val (itc, [progst]) = strip_comb prog_tree
 /scratch/cakeml/regression/cakeml-3567/pancake/decompiler/panItreeDecompilerLib.sml:1393: warning: Pattern is not exhaustive.
 Found near val (_, [cond_call, ...]) = strip_comb progst
 /scratch/cakeml/regression/cakeml-3567/pancake/decompiler/panItreeDecompilerLib.sml:1411: warning: Pattern is not exhaustive.
 Found near val (itc, [progst]) = strip_comb prog_tree
 /scratch/cakeml/regression/cakeml-3567/pancake/decompiler/panItreeDecompilerLib.sml:1412: warning: Pattern is not exhaustive.
 Found near val (_, [while_call, ...]) = strip_comb progst
 /scratch/cakeml/regression/cakeml-3567/pancake/decompiler/panItreeDecompilerLib.sml:1443: warning: Pattern is not exhaustive.
 Found near val (itc, [progst]) = strip_comb prog_tree
 /scratch/cakeml/regression/cakeml-3567/pancake/decompiler/panItreeDecompilerLib.sml:1444: warning: Pattern is not exhaustive.
 Found near val (_, [deccall, ...]) = strip_comb progst
 <<HOL message: Created theory "yes">>
 Saved definition ____ "yes_codes_def"
 Saved definition ____ "yes_body_def"
 Saved definition ____ "yes_while_1_def"
 <<HOL warning: Context.snapshot: ambient context read while a proof was running (in yes)>>
 Saved theorem _______ "event_satisfy_Tau"
 Saved theorem _______ "event_satisfy_FUNPOW"
 Saved theorem _______ "itree_wbisim_impl_event_satisfy"
 Saved theorem _______ "yes_while_1_safety"
 /scratch/cakeml/regression/cakeml-3567/pancake/decompiler/examples/yesScript.sml:177: error: Value or constructor (byte_align_extract) has not been declared
 Found near [read_bytearray_compute, mem_load_byte_def, byte_align_extract]
 error in quse /scratch/cakeml/regression/cakeml-3567/pancake/decompiler/examples/yesScript.sml : Fail "Static Errors"
 error in load /scratch/cakeml/regression/cakeml-3567/pancake/decompiler/examples/yesScript : Fail "Static Errors"
 Uncaught exception at ./basis/FinalPolyML.sml:492: Fail "Static Errors"
 Full log: /scratch/cakeml/regression/cakeml-3567/pancake/decompiler/examples/.hol/logs/yesTheory