Job 3591

CakeML:f6d96365e2f3f9bc13120522e3d69d208ad4a85c
  Remove old_drule, var_eq_old and temp_loose_equality retrofits [Oct 07 09:06:51]
#1536 (issue-sniping)
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:bikkie

Oct 07 12:36:12 Claimed job
Oct 07 12:36:25 Building HOL
Oct 07 12:48:46 Starting developers
Oct 07 12:49:42 Finished developers                                              55s   1GB
Oct 07 12:49:43 Starting developers/bin
Oct 07 12:49:53 Finished developers/bin                                           8s   1GB
Oct 07 12:49:54 Starting misc
Oct 07 12:50:55 Finished misc                                                  1m00s   1GB
Oct 07 12:50:56 Starting compiler/proofs
Oct 07 14:13:43 Finished compiler/proofs                                    1h22m45s  11GB
Oct 07 14:13:44 Starting compiler/bootstrap/compilation/x64/64/proofs
Oct 07 21:51:03 Finished compiler/bootstrap/compilation/x64/64/proofs       7h37m17s  86GB
Oct 07 21:51:04 Starting semantics/ffi
Oct 07 21:51:27 Finished semantics/ffi                                           22s   1GB
Oct 07 21:51:29 Starting semantics
Oct 07 21:51:40 Finished semantics                                                6s   1GB
Oct 07 21:51:40 Starting semantics/proofs
Oct 07 21:52:12 Finished semantics/proofs                                        30s   1GB
Oct 07 21:52:13 Starting semantics/alt_semantics
Oct 07 21:52:37 Finished semantics/alt_semantics                                 22s   1GB
Oct 07 21:52:38 Starting semantics/alt_semantics/proofs
Oct 07 21:56:50 Finished semantics/alt_semantics/proofs                        4m11s   2GB
Oct 07 21:56:51 Starting basis/pure
Oct 07 21:56:59 Finished basis/pure                                               6s   1GB
Oct 07 21:57:00 Starting translator
Oct 07 21:58:20 Finished translator                                            1m18s   2GB
Oct 07 21:58:21 Starting compiler/parsing
Oct 07 21:59:16 Finished compiler/parsing                                        54s   1GB
Oct 07 21:59:17 Starting characteristic
Oct 07 21:59:25 Finished characteristic                                           6s   1GB
Oct 07 21:59:26 Starting translator/monadic
Oct 07 21:59:33 Finished translator/monadic                                       6s   1GB
Oct 07 21:59:34 Starting translator/monadic/monad_base
Oct 07 21:59:41 Finished translator/monadic/monad_base                            6s   1GB
Oct 07 21:59:42 Starting profiler
Oct 07 22:00:18 Finished profiler                                                34s   2GB
Oct 07 22:00:19 Starting basis
Oct 07 22:02:14 Finished basis                                                 1m54s   4GB
Oct 07 22:02:15 Starting compiler
Oct 07 22:02:22 Finished compiler                                                 6s   1GB
Oct 07 22:02:23 Starting compiler/inference
Oct 07 22:02:30 Finished compiler/inference                                       6s   1GB
Oct 07 22:02:31 Starting compiler/backend/reg_alloc
Oct 07 22:02:39 Finished compiler/backend/reg_alloc                               6s   1GB
Oct 07 22:02:40 Starting compiler/backend/gc
Oct 07 22:02:47 Finished compiler/backend/gc                                      6s   1GB
Oct 07 22:02:48 Starting compiler/backend
Oct 07 22:02:58 Finished compiler/backend                                         9s   1GB
Oct 07 22:02:59 Starting compiler/encoders/asm
Oct 07 22:03:06 Finished compiler/encoders/asm                                    6s   1GB
Oct 07 22:03:07 Starting compiler/encoders/x64
Oct 07 22:03:15 Finished compiler/encoders/x64                                    6s   1GB
Oct 07 22:03:16 Starting compiler/encoders/arm7
Oct 07 22:03:23 Finished compiler/encoders/arm7                                   6s   1GB
Oct 07 22:03:24 Starting compiler/encoders/arm8
Oct 07 22:03:31 Finished compiler/encoders/arm8                                   6s   1GB
Oct 07 22:03:32 Starting compiler/encoders/arm8_asl
Oct 08 00:33:18 Finished compiler/encoders/arm8_asl                         2h29m43s  22GB
Oct 08 00:33:19 Starting compiler/encoders/mips
Oct 08 00:33:26 Finished compiler/encoders/mips                                   6s   1GB
Oct 08 00:33:27 Starting compiler/encoders/riscv
Oct 08 00:33:35 Finished compiler/encoders/riscv                                  6s   1GB
Oct 08 00:33:36 Starting compiler/encoders/ag32
Oct 08 00:33:43 Finished compiler/encoders/ag32                                   6s   1GB
Oct 08 00:33:44 Starting compiler/encoders/tests
Oct 08 00:34:26 Finished compiler/encoders/tests                                 40s   2GB
Oct 08 00:34:27 Starting compiler/encoders/monadic_enc
Oct 08 00:34:53 Finished compiler/encoders/monadic_enc                           25s   1GB
Oct 08 00:34:54 Starting compiler/backend/x64
Oct 08 00:35:02 Finished compiler/backend/x64                                     6s   1GB
Oct 08 00:35:03 Starting compiler/backend/arm7
Oct 08 00:35:10 Finished compiler/backend/arm7                                    6s   1GB
Oct 08 00:35:11 Starting compiler/backend/arm8
Oct 08 00:35:18 Finished compiler/backend/arm8                                    6s   1GB
Oct 08 00:35:19 Starting compiler/backend/mips
Oct 08 00:35:26 Finished compiler/backend/mips                                    6s   1GB
Oct 08 00:35:27 Starting compiler/backend/riscv
Oct 08 00:35:35 Finished compiler/backend/riscv                                   6s   1GB
Oct 08 00:35:36 Starting compiler/backend/ag32
Oct 08 00:36:46 Finished compiler/backend/ag32                                 1m08s   1GB
Oct 08 00:36:47 Starting compiler/backend/pattern_matching
Oct 08 00:37:09 Finished compiler/backend/pattern_matching                       21s   1GB
Oct 08 00:37:10 Starting compiler/parsing/ocaml
Oct 08 00:39:41 Finished compiler/parsing/ocaml                                2m30s   1GB
Oct 08 00:39:42 Starting compiler/printing
Oct 08 00:40:39 Finished compiler/printing                                       56s   1GB
Oct 08 00:40:40 Starting compiler/parsing/proofs
Oct 08 00:40:48 Finished compiler/parsing/proofs                                  6s   1GB
Oct 08 00:40:49 Starting compiler/inference/proofs
Oct 08 00:40:56 Finished compiler/inference/proofs                                6s   1GB
Oct 08 00:40:57 Starting compiler/backend/semantics
Oct 08 00:44:23 Finished compiler/backend/semantics                            3m25s   3GB
Oct 08 00:44:24 Starting compiler/backend/reg_alloc/proofs
Oct 08 00:44:32 Finished compiler/backend/reg_alloc/proofs                        6s   1GB
Oct 08 00:44:33 Starting compiler/backend/proofs
Oct 08 00:45:26 Finished compiler/backend/proofs                                 52s   2GB
Oct 08 00:45:27 Starting compiler/backend/serialiser
Oct 08 00:45:35 Finished compiler/backend/serialiser                              6s   1GB
Oct 08 00:45:36 Starting compiler/encoders/x64/proofs
Oct 08 00:45:43 Finished compiler/encoders/x64/proofs                             6s   1GB
Oct 08 00:45:44 Starting compiler/encoders/arm7/proofs
Oct 08 00:59:03 Finished compiler/encoders/arm7/proofs                        13m18s   4GB
Oct 08 00:59:04 Starting compiler/encoders/arm8/proofs
Oct 08 01:11:21 Finished compiler/encoders/arm8/proofs                        12m16s  13GB
Oct 08 01:11:22 Starting compiler/encoders/arm8_asl/proofs
Oct 08 02:20:34 Finished compiler/encoders/arm8_asl/proofs                  1h09m10s  41GB
Oct 08 02:20:35 Starting compiler/encoders/mips/proofs
Oct 08 02:32:37 Finished compiler/encoders/mips/proofs                        12m00s   5GB
Oct 08 02:32:38 Starting compiler/encoders/riscv/proofs
Oct 08 02:42:40 Finished compiler/encoders/riscv/proofs                       10m01s   3GB
Oct 08 02:42:41 Starting compiler/encoders/ag32/proofs
Oct 08 02:46:10 Finished compiler/encoders/ag32/proofs                         3m27s   1GB
Oct 08 02:46:11 Starting compiler/backend/x64/proofs
Oct 08 02:46:18 Finished compiler/backend/x64/proofs                              6s   1GB
Oct 08 02:46:19 Starting compiler/backend/arm7/proofs
Oct 08 02:47:04 Finished compiler/backend/arm7/proofs                            44s   2GB
Oct 08 02:47:05 Starting compiler/backend/arm8/proofs
Oct 08 02:47:53 Finished compiler/backend/arm8/proofs                            47s   2GB
Oct 08 02:47:54 Starting compiler/backend/arm8_asl
Oct 08 02:48:42 Finished compiler/backend/arm8_asl                               46s   2GB
Oct 08 02:48:43 Starting compiler/backend/mips/proofs
Oct 08 02:49:34 Finished compiler/backend/mips/proofs                            50s   2GB
Oct 08 02:49:35 Starting compiler/backend/riscv/proofs
Oct 08 02:50:26 Finished compiler/backend/riscv/proofs                           49s   2GB
Oct 08 02:50:26 Starting compiler/backend/ag32/proofs
Oct 08 03:00:12 Finished compiler/backend/ag32/proofs                          9m44s   5GB
Oct 08 03:00:13 Starting compiler/backend/cv_compute
Oct 08 03:00:50 Finished compiler/backend/cv_compute                             35s   1GB
Oct 08 03:00:51 Starting cv_translator
Oct 08 03:07:10 Finished cv_translator                                         6m18s   3GB
Oct 08 03:07:11 Starting candle
Oct 08 03:07:18 Finished candle                                                   6s   1GB
Oct 08 03:07:19 Starting candle/set-theory
Oct 08 03:07:43 Finished candle/set-theory                                       22s   1GB
Oct 08 03:07:44 Starting candle/syntax-lib
Oct 08 03:07:51 Finished candle/syntax-lib                                        6s   1GB
Oct 08 03:07:52 Starting candle/standard
Oct 08 03:07:59 Finished candle/standard                                          6s   1GB
Oct 08 03:08:00 Starting candle/standard/syntax
Oct 08 03:08:20 Finished candle/standard/syntax                                  19s   1GB
Oct 08 03:08:21 Starting candle/standard/syntax/little_theories
Oct 08 03:10:29 Finished candle/standard/syntax/little_theories                2m06s   1GB
Oct 08 03:10:30 Starting candle/standard/semantics
Oct 08 03:10:37 Finished candle/standard/semantics                                6s   1GB
Oct 08 03:10:38 Starting candle/standard/monadic
Oct 08 03:10:45 Finished candle/standard/monadic                                  6s   1GB
Oct 08 03:10:46 Starting candle/standard/ml_kernel
Oct 08 03:13:03 Finished candle/standard/ml_kernel                             2m15s   4GB
Oct 08 03:13:04 Starting candle/overloading
Oct 08 03:13:11 Finished candle/overloading                                       6s   1GB
Oct 08 03:13:12 Starting candle/overloading/syntax
Oct 08 03:16:41 Finished candle/overloading/syntax                             3m27s   2GB
Oct 08 03:16:42 Starting candle/overloading/semantics
Oct 08 03:25:32 Finished candle/overloading/semantics                          8m49s   4GB
Oct 08 03:25:33 Starting candle/overloading/monadic
Oct 08 03:27:47 Finished candle/overloading/monadic                            2m12s   1GB
Oct 08 03:27:48 Starting candle/overloading/ml_kernel
Oct 08 03:35:14 Finished candle/overloading/ml_kernel                          7m25s   6GB
Oct 08 03:35:15 Starting candle/overloading/ml_checker
Oct 08 03:37:28 Finished candle/overloading/ml_checker                         2m11s   6GB
Oct 08 03:37:29 Starting candle/prover
Oct 08 03:37:36 Finished candle/prover                                            6s   1GB
Oct 08 03:37:37 Starting candle/prover/compute
Oct 08 03:37:45 Finished candle/prover/compute                                    6s   1GB
Oct 08 03:37:46 Starting pancake
Oct 08 03:37:53 Finished pancake                                                  6s   1GB
Oct 08 03:37:54 Starting pancake/semantics
Oct 08 03:41:16 Finished pancake/semantics                                     3m21s   2GB
Oct 08 03:41:17 Starting pancake/parser
Oct 08 03:42:13 Finished pancake/parser                                          48s   1GB
Oct 08 03:42:14 Starting pancake/static_checker
Oct 08 03:45:00 Finished pancake/static_checker                                2m45s   1GB
Oct 08 03:45:01 Starting pancake/proofs
Oct 08 04:02:25 Finished pancake/proofs                                       17m22s   5GB
Oct 08 04:02:26 Starting pancake/decompiler
Oct 08 04:03:21 Finished pancake/decompiler                                      53s   2GB
Oct 08 04:03:22 Starting pancake/decompiler/examples
Oct 08 04:04:12 Finished pancake/decompiler/examples                             48s   1GB
Oct 08 04:04:17 Starting compiler/dafny
Oct 08 04:04:47 Finished compiler/dafny                                          27s   1GB
Oct 08 04:04:48 Starting compiler/dafny/translation
Oct 08 04:15:41 Finished compiler/dafny/translation                           10m52s   6GB
Oct 08 04:15:42 Starting compiler/dafny/compilation
Oct 08 04:18:07 Finished compiler/dafny/compilation                            2m23s   6GB
Oct 08 04:18:08 Starting compiler/dafny/semantics
Oct 08 04:18:54 Finished compiler/dafny/semantics                                45s   1GB
Oct 08 04:18:55 Starting compiler/dafny/proofs
Oct 08 04:20:42 Finished compiler/dafny/proofs                                 1m46s   1GB
Oct 08 04:20:43 Starting compiler/dafny/vcg
Oct 08 04:20:51 Finished compiler/dafny/vcg                                       7s   1GB
Oct 08 04:20:52 Starting compiler/dafny/vcg/examples
Oct 08 04:21:29 Finished compiler/dafny/vcg/examples                             35s   1GB
Oct 08 04:21:30 Starting compiler/scheme
Oct 08 04:22:02 Finished compiler/scheme                                         31s   1GB
Oct 08 04:22:03 Starting compiler/scheme/translation
Oct 08 04:29:10 Finished compiler/scheme/translation                           7m05s   7GB
Oct 08 04:29:11 Starting compiler/scheme/compilation
Oct 08 04:30:57 Finished compiler/scheme/compilation                           1m44s   5GB
Oct 08 04:30:58 Starting compiler/scheme/proofs
Oct 08 04:38:02 Finished compiler/scheme/proofs                                7m03s   2GB
Oct 08 04:38:03 Starting characteristic/examples
Oct 08 04:39:28 Finished characteristic/examples                               1m24s   5GB
Oct 08 04:39:30 Starting tutorial
Oct 08 04:39:38 Finished tutorial                                                 6s   1GB
Oct 08 04:39:39 Starting tutorial/solutions
Oct 08 04:42:47 Finished tutorial/solutions                                    3m06s   3GB
Oct 08 04:42:48 Starting translator/monadic/examples
Oct 08 04:44:21 FAILED: translator/monadic/examples
  HOLORIG=/scratch/regbox/regression3/cakeml-3591/translator/monadic/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/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 15 theory files
Starting work on README.md
Starting work on array_global_stateProgTheory
Starting work on array_local_stateProgTheory
Starting work on exceptionProgTheory
README.md                                                   (0s)             OK
Starting work on exception_arity_testProgTheory
exceptionProgTheory                                        (29s)  [1/15]     OK
Starting work on fibProgTheory
exception_arity_testProgTheory                             (31s)  [2/15]     OK
Starting work on floyd_warshallProgTheory
array_global_stateProgTheory                               (49s)  [3/15]     OK
Starting work on monadic_array_searchProgTheory
floyd_warshallProgTheory                                   (36s)  [4/15]     OK
Starting work on monadic_doubleArgProgTheory
array_local_stateProgTheory                                (75s)  [5/15]     OK
Starting work on monadic_helloProgTheory
fibProgTheory                                              (45s)        FAIL<1>
monadic_array_searchProgTheory                             (28s)         killed
monadic_doubleArgProgTheory                                 (7s)         killed
monadic_helloProgTheory                                     (5s)         killed
*** Holmake aborted - 1 target failed:
*** fibProgTheory (status 1)
     ADD<fibProg$STATE_EXN_TYPE_def>
   invalidated by NewBinding("STATE_EXN_TYPE_def", {private=false,loc=Unknown,class=Thm})>>
 Saved theorem _______ "STATE_EXN_TYPE_def"
 Attempting proof of: EqualityType STATE_EXN_TYPE
 Doing EqualityType proof via ONTO thm: a. r. a = num2state_exn r  r < 1
 .. done EqualityType proof.
 Adding type :state_exn.
 Saved theorem _______ "nsLookup_fibProg_env_pfun_eqs"
 Overloaded parser on: ``stdio``.
 Overloaded parser on: ``commandline``.
 Saved definition ____ "STATE_REFERENCES_def"
 Saved theorem _______ "EvalM_raise_Fail"
 Saved theorem __ "EvalM_raise_Fail"
 Saved theorem _______ "EvalM_handle_Fail"
 Saved theorem __ "EvalM_handle_Fail"
 <<HOL warning: Context.snapshot: ambient context read while a proof was running (in fibProg)>>
 Saved theorem _______ "stdio_INTRO"
 Saved intro theorem for stdio: stdio_INTRO.
 
 Saved theorem _______ "EvalM_print_stdio"
 Saved EvalM theorem for stdio: EvalM_print_stdio.
 Added access patterns for stdio: EvalM_print_stdio.
 
 Saved theorem _______ "EvalM_print_err_stdio"
 Saved EvalM theorem for stdio: EvalM_print_err_stdio.
 Added access patterns for stdio: EvalM_print_err_stdio.
 
 Saved theorem _______ "commandline_INTRO"
 Saved intro theorem for commandline: commandline_INTRO.
 
 Saved theorem _______ "EvalM_arguments_commandline"
 Saved EvalM theorem for commandline: EvalM_arguments_commandline.
 Added access patterns for commandline: EvalM_arguments_commandline.
 
 Saved theorem _______ "EvalM_name_commandline"
 Saved EvalM theorem for commandline: EvalM_name_commandline.
 Added access patterns for commandline: EvalM_name_commandline.
 
 Saved definition ____ "hd_def"
 Saved definition ____ "str_to_num_def"
 Saved definition ____ "fiba_def"
 Saved induction _____ "fiba_ind"
 Saved definition ____ "num_to_str_def"
 
 Exception raised at TotalDefn.xDefine:
 at Defn.Hol_defn: between line 65, character 2 and line 75, character 11:
 at Defn.parse_quote:
 at Defn.multi_dest_eq:
   between line 65, character 2 and line 75, character 11:
   Expected an equality
 Full log: /scratch/regbox/regression3/cakeml-3591/translator/monadic/examples/.hol/logs/fibProgTheory