Job 3424

CakeML:c75888c080da3885147d572a8e2f5a622d049a2b
  Clean up more holproject.toml files under examples/ [Jul 20 03:42:24]
#1427 (holprojs)
Merging into:150b633c4a079a8520ac3dcb684463b706ed290b
  Merge pull request #1440 from CakeML/thunks [Jul 30 11:35:47]
HOL:f18e6e7277c2648d40c2491d87f09083c909e6e9
  OT logging: stop re-stripping already-undecorated retired names [Jul 19 03:05:49]
Machine:pavlova

Aug 03 08:06:07 Claimed job
Aug 03 08:06:45 Building HOL
Aug 03 08:21:07 Starting developers
Aug 03 08:21:52 Finished developers                                              44s   1GB
Aug 03 08:21:53 Starting developers/bin
Aug 03 08:22:00 Finished developers/bin                                           6s   1GB
Aug 03 08:22:01 Starting misc
Aug 03 08:23:06 Finished misc                                                  1m03s   1GB
Aug 03 08:23:07 Starting compiler/proofs
Aug 03 09:40:44 Finished compiler/proofs                                    1h17m36s  11GB
Aug 03 09:40:45 Starting compiler/bootstrap/compilation/x64/64/proofs
Aug 03 15:48:18 Finished compiler/bootstrap/compilation/x64/64/proofs       6h07m32s  71GB
Aug 03 15:48:19 Starting semantics/ffi
Aug 03 15:48:40 Finished semantics/ffi                                           20s   1GB
Aug 03 15:48:41 Starting semantics
Aug 03 15:48:47 Finished semantics                                                4s   1GB
Aug 03 15:48:48 Starting semantics/proofs
Aug 03 15:49:17 Finished semantics/proofs                                        28s   1GB
Aug 03 15:49:18 Starting semantics/alt_semantics
Aug 03 15:49:40 Finished semantics/alt_semantics                                 21s   1GB
Aug 03 15:49:41 Starting semantics/alt_semantics/proofs
Aug 03 15:53:40 Finished semantics/alt_semantics/proofs                        3m57s   1GB
Aug 03 15:53:41 Starting basis/pure
Aug 03 15:53:46 Finished basis/pure                                               5s   1GB
Aug 03 15:53:47 Starting translator
Aug 03 15:55:00 Finished translator                                            1m12s   1GB
Aug 03 15:55:01 Starting compiler/parsing
Aug 03 15:55:53 Finished compiler/parsing                                        50s   2GB
Aug 03 15:55:54 Starting characteristic
Aug 03 15:55:59 Finished characteristic                                           4s   1GB
Aug 03 15:56:00 Starting translator/monadic
Aug 03 15:56:06 Finished translator/monadic                                       4s   1GB
Aug 03 15:56:07 Starting translator/monadic/monad_base
Aug 03 15:56:12 Finished translator/monadic/monad_base                            4s   1GB
Aug 03 15:56:13 Starting profiler
Aug 03 15:56:47 Finished profiler                                                33s   1GB
Aug 03 15:56:48 Starting basis
Aug 03 15:58:38 Finished basis                                                 1m49s   4GB
Aug 03 15:58:39 Starting compiler
Aug 03 15:58:45 Finished compiler                                                 4s   1GB
Aug 03 15:58:45 Starting compiler/inference
Aug 03 15:58:51 Finished compiler/inference                                       4s   1GB
Aug 03 15:58:52 Starting compiler/backend/reg_alloc
Aug 03 15:58:57 Finished compiler/backend/reg_alloc                               4s   1GB
Aug 03 15:58:58 Starting compiler/backend/gc
Aug 03 15:59:04 Finished compiler/backend/gc                                      4s   1GB
Aug 03 15:59:04 Starting compiler/backend
Aug 03 15:59:10 Finished compiler/backend                                         4s   1GB
Aug 03 15:59:11 Starting compiler/encoders/asm
Aug 03 15:59:16 Finished compiler/encoders/asm                                    4s   1GB
Aug 03 15:59:17 Starting compiler/encoders/x64
Aug 03 15:59:22 Finished compiler/encoders/x64                                    4s   1GB
Aug 03 15:59:23 Starting compiler/encoders/arm7
Aug 03 15:59:29 Finished compiler/encoders/arm7                                   4s   1GB
Aug 03 15:59:29 Starting compiler/encoders/arm8
Aug 03 15:59:36 Finished compiler/encoders/arm8                                   4s   1GB
Aug 03 15:59:37 Starting compiler/encoders/arm8_asl
Aug 03 18:23:31 Finished compiler/encoders/arm8_asl                         2h23m53s  23GB
Aug 03 18:23:32 Starting compiler/encoders/mips
Aug 03 18:23:40 Finished compiler/encoders/mips                                   6s   1GB
Aug 03 18:23:41 Starting compiler/encoders/riscv
Aug 03 18:23:46 Finished compiler/encoders/riscv                                  4s   1GB
Aug 03 18:23:47 Starting compiler/encoders/ag32
Aug 03 18:23:53 Finished compiler/encoders/ag32                                   4s   1GB
Aug 03 18:23:53 Starting compiler/encoders/tests
Aug 03 18:23:59 Finished compiler/encoders/tests                                  4s   1GB
Aug 03 18:24:00 Starting compiler/encoders/monadic_enc
Aug 03 18:24:27 Finished compiler/encoders/monadic_enc                           26s   1GB
Aug 03 18:24:28 Starting compiler/backend/x64
Aug 03 18:24:33 Finished compiler/backend/x64                                     4s   1GB
Aug 03 18:24:34 Starting compiler/backend/arm7
Aug 03 18:24:39 Finished compiler/backend/arm7                                    4s   1GB
Aug 03 18:24:40 Starting compiler/backend/arm8
Aug 03 18:24:46 Finished compiler/backend/arm8                                    4s   1GB
Aug 03 18:24:47 Starting compiler/backend/mips
Aug 03 18:24:52 Finished compiler/backend/mips                                    4s   1GB
Aug 03 18:24:53 Starting compiler/backend/riscv
Aug 03 18:24:58 Finished compiler/backend/riscv                                   4s   1GB
Aug 03 18:24:59 Starting compiler/backend/ag32
Aug 03 18:26:06 Finished compiler/backend/ag32                                 1m06s   2GB
Aug 03 18:26:07 Starting compiler/backend/pattern_matching
Aug 03 18:26:13 Finished compiler/backend/pattern_matching                        4s   1GB
Aug 03 18:26:13 Starting compiler/parsing/ocaml
Aug 03 18:28:28 Finished compiler/parsing/ocaml                                2m13s   1GB
Aug 03 18:28:28 Starting compiler/printing
Aug 03 18:29:30 Finished compiler/printing                                     1m00s   1GB
Aug 03 18:29:31 Starting compiler/parsing/proofs
Aug 03 18:29:36 Finished compiler/parsing/proofs                                  4s   1GB
Aug 03 18:29:37 Starting compiler/inference/proofs
Aug 03 18:29:43 Finished compiler/inference/proofs                                4s   1GB
Aug 03 18:29:44 Starting compiler/backend/semantics
Aug 03 18:32:55 Finished compiler/backend/semantics                            3m10s   3GB
Aug 03 18:32:56 Starting compiler/backend/reg_alloc/proofs
Aug 03 18:33:01 Finished compiler/backend/reg_alloc/proofs                        4s   1GB
Aug 03 18:33:02 Starting compiler/backend/proofs
Aug 03 18:33:51 Finished compiler/backend/proofs                                 47s   2GB
Aug 03 18:33:52 Starting compiler/backend/serialiser
Aug 03 18:33:57 Finished compiler/backend/serialiser                              4s   1GB
Aug 03 18:33:58 Starting compiler/encoders/x64/proofs
Aug 03 18:34:04 Finished compiler/encoders/x64/proofs                             4s   1GB
Aug 03 18:34:05 Starting compiler/encoders/arm7/proofs
Aug 03 18:46:40 Finished compiler/encoders/arm7/proofs                        12m34s   9GB
Aug 03 18:46:41 Starting compiler/encoders/arm8/proofs
Aug 03 18:54:37 Finished compiler/encoders/arm8/proofs                         7m54s   4GB
Aug 03 18:54:38 Starting compiler/encoders/arm8_asl/proofs
Aug 03 19:51:05 Finished compiler/encoders/arm8_asl/proofs                    56m25s   9GB
Aug 03 19:51:06 Starting compiler/encoders/mips/proofs
Aug 03 20:01:40 Finished compiler/encoders/mips/proofs                        10m33s   8GB
Aug 03 20:01:41 Starting compiler/encoders/riscv/proofs
Aug 03 20:11:24 Finished compiler/encoders/riscv/proofs                        9m41s   3GB
Aug 03 20:11:25 Starting compiler/encoders/ag32/proofs
Aug 03 20:14:32 Finished compiler/encoders/ag32/proofs                         3m06s   1GB
Aug 03 20:14:33 Starting compiler/backend/x64/proofs
Aug 03 20:14:39 Finished compiler/backend/x64/proofs                              4s   1GB
Aug 03 20:14:40 Starting compiler/backend/arm7/proofs
Aug 03 20:15:23 Finished compiler/backend/arm7/proofs                            42s   2GB
Aug 03 20:15:24 Starting compiler/backend/arm8/proofs
Aug 03 20:16:03 Finished compiler/backend/arm8/proofs                            38s   1GB
Aug 03 20:16:04 Starting compiler/backend/arm8_asl
Aug 03 20:16:37 Finished compiler/backend/arm8_asl                               32s   1GB
Aug 03 20:16:38 Starting compiler/backend/mips/proofs
Aug 03 20:17:21 Finished compiler/backend/mips/proofs                            41s   2GB
Aug 03 20:17:22 Starting compiler/backend/riscv/proofs
Aug 03 20:18:07 Finished compiler/backend/riscv/proofs                           44s   2GB
Aug 03 20:18:08 Starting compiler/backend/ag32/proofs
Aug 03 20:27:53 Finished compiler/backend/ag32/proofs                          9m44s   5GB
Aug 03 20:27:54 Starting compiler/backend/cv_compute
Aug 03 20:28:30 Finished compiler/backend/cv_compute                             34s   1GB
Aug 03 20:28:31 Starting cv_translator
Aug 03 20:33:45 Finished cv_translator                                         5m14s   4GB
Aug 03 20:33:46 Starting candle
Aug 03 20:33:52 Finished candle                                                   4s   1GB
Aug 03 20:33:53 Starting candle/set-theory
Aug 03 20:34:30 Finished candle/set-theory                                       36s   1GB
Aug 03 20:34:31 Starting candle/syntax-lib
Aug 03 20:34:36 Finished candle/syntax-lib                                        4s   1GB
Aug 03 20:34:37 Starting candle/standard
Aug 03 20:34:42 Finished candle/standard                                          4s   1GB
Aug 03 20:34:43 Starting candle/standard/syntax
Aug 03 20:35:03 Finished candle/standard/syntax                                  18s   1GB
Aug 03 20:35:04 Starting candle/standard/syntax/little_theories
Aug 03 20:36:21 Finished candle/standard/syntax/little_theories                1m16s   1GB
Aug 03 20:36:22 Starting candle/standard/semantics
Aug 03 20:38:43 Finished candle/standard/semantics                             2m20s   1GB
Aug 03 20:38:44 Starting candle/standard/monadic
Aug 03 20:38:50 Finished candle/standard/monadic                                  5s   1GB
Aug 03 20:38:51 Starting candle/standard/ml_kernel
Aug 03 20:41:03 Finished candle/standard/ml_kernel                             2m11s   4GB
Aug 03 20:41:04 Starting candle/overloading
Aug 03 20:41:10 Finished candle/overloading                                       4s   1GB
Aug 03 20:41:11 Starting candle/overloading/syntax
Aug 03 20:41:16 Finished candle/overloading/syntax                                4s   1GB
Aug 03 20:41:17 Starting candle/overloading/semantics
Aug 03 20:41:23 Finished candle/overloading/semantics                             4s   1GB
Aug 03 20:41:24 Starting candle/overloading/monadic
Aug 03 20:41:29 Finished candle/overloading/monadic                               4s   1GB
Aug 03 20:41:30 Starting candle/overloading/ml_kernel
Aug 03 20:41:36 Finished candle/overloading/ml_kernel                             4s   1GB
Aug 03 20:41:36 Starting candle/overloading/ml_checker
Aug 03 20:41:42 Finished candle/overloading/ml_checker                            4s   1GB
Aug 03 20:41:43 Starting candle/prover
Aug 03 20:41:48 Finished candle/prover                                            4s   1GB
Aug 03 20:41:49 Starting candle/prover/compute
Aug 03 20:41:55 Finished candle/prover/compute                                    4s   1GB
Aug 03 20:41:56 Starting pancake
Aug 03 20:42:01 Finished pancake                                                  4s   1GB
Aug 03 20:42:02 Starting pancake/semantics
Aug 03 20:45:03 Finished pancake/semantics                                     2m59s   3GB
Aug 03 20:45:04 Starting pancake/parser
Aug 03 20:45:49 Finished pancake/parser                                          44s   1GB
Aug 03 20:45:50 Starting pancake/static_checker
Aug 03 20:48:27 Finished pancake/static_checker                                2m35s   1GB
Aug 03 20:48:27 Starting pancake/proofs
Aug 03 21:05:43 Finished pancake/proofs                                       17m15s   4GB
Aug 03 21:05:44 Starting compiler/dafny
Aug 03 21:06:14 Finished compiler/dafny                                          28s   1GB
Aug 03 21:06:15 Starting compiler/dafny/translation
Aug 03 21:16:52 Finished compiler/dafny/translation                           10m36s   6GB
Aug 03 21:16:53 Starting compiler/dafny/compilation
Aug 03 21:19:02 Finished compiler/dafny/compilation                            2m07s   7GB
Aug 03 21:19:03 Starting compiler/dafny/semantics
Aug 03 21:19:46 Finished compiler/dafny/semantics                                42s   1GB
Aug 03 21:19:46 Starting compiler/dafny/proofs
Aug 03 21:21:31 Finished compiler/dafny/proofs                                 1m43s   1GB
Aug 03 21:21:32 Starting compiler/dafny/vcg
Aug 03 21:21:38 Finished compiler/dafny/vcg                                       5s   1GB
Aug 03 21:21:38 Starting compiler/dafny/vcg/examples
Aug 03 21:22:11 Finished compiler/dafny/vcg/examples                             31s   1GB
Aug 03 21:22:12 Starting compiler/scheme
Aug 03 21:22:43 Finished compiler/scheme                                         30s   1GB
Aug 03 21:22:44 Starting compiler/scheme/translation
Aug 03 21:29:38 Finished compiler/scheme/translation                           6m53s   8GB
Aug 03 21:29:39 Starting compiler/scheme/compilation
Aug 03 21:31:19 Finished compiler/scheme/compilation                           1m38s   3GB
Aug 03 21:31:20 Starting compiler/scheme/proofs
Aug 03 21:38:16 Finished compiler/scheme/proofs                                6m55s   2GB
Aug 03 21:38:17 Starting characteristic/examples
Aug 03 21:39:57 Finished characteristic/examples                               1m39s   5GB
Aug 03 21:39:58 Starting tutorial/solutions
Aug 03 21:40:03 Finished tutorial/solutions                                       4s   1GB
Aug 03 21:40:04 Starting translator/monadic/examples
Aug 03 21:40:10 Finished translator/monadic/examples                              4s   1GB
Aug 03 21:40:11 Starting examples
Aug 03 21:44:39 Finished examples                                              4m27s   3GB
Aug 03 21:44:40 Starting examples/compilation
Aug 03 21:44:50 Finished examples/compilation                                     5s   1GB
Aug 03 21:44:51 Starting examples/compilation/x64
Aug 03 21:53:48 Finished examples/compilation/x64                              8m55s   4GB
Aug 03 21:53:49 Starting examples/compilation/x64/proofs
Aug 03 21:57:28 Finished examples/compilation/x64/proofs                       3m38s   4GB
Aug 03 21:57:29 Starting examples/compilation/ag32
Aug 03 22:00:09 Finished examples/compilation/ag32                             2m39s   3GB
Aug 03 22:00:10 Starting examples/compilation/ag32/proofs
Aug 03 22:01:38 Finished examples/compilation/ag32/proofs                      1m27s   4GB
Aug 03 22:01:39 Starting examples/lpr_checker
Aug 03 22:02:22 Finished examples/lpr_checker                                    42s   1GB
Aug 03 22:02:23 Starting examples/lpr_checker/array
Aug 03 22:15:16 Finished examples/lpr_checker/array                           12m52s   5GB
Aug 03 22:15:17 Starting examples/lpr_checker/array/compilation
Aug 03 22:19:03 Finished examples/lpr_checker/array/compilation                3m45s   6GB
Aug 03 22:19:04 Starting examples/lpr_checker/array/compilation/proofs
Aug 03 22:20:47 Finished examples/lpr_checker/array/compilation/proofs         1m42s   5GB
Aug 03 22:20:48 Starting examples/lpr_checker/array/compilation/proofsARM8
Aug 03 22:22:09 FAILED: examples/lpr_checker/array/compilation/proofsARM8
  HOLORIG=/scratch/cakeml/regression/cakeml-3424/examples/lpr_checker/array/compilation/proofsARM8 [ -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)/examples/algorithms
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/algebra/base
Scanning $(HOLDIR)/src/algebra/construction
Scanning $(HOLDIR)/src/algebra
Scanning $(HOLDIR)/src/hol88
Scanning $(HOLDIR)/src/rational
Scanning $(HOLDIR)/src/real
Scanning $(HOLDIR)/examples/data-structures/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/src/search
Scanning $(HOLDIR)/examples/formal-languages/regular
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/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/model
Scanning $(HOLDIR)/examples/machine-code/decompiler
Scanning $(HOLDIR)/examples/l3-machine-code
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/step
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv
Scanning $(HOLDIR)/examples/machine-code/multiword
Scanning $(CAKEMLDIR)/basis
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/candle
Scanning $(CAKEMLDIR)/candle/standard/syntax
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/pl-semantics/lprefix_lub
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/candle/syntax-lib
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/candle/standard/monadic
Scanning $(CAKEMLDIR)/candle/standard/ml_kernel
Scanning $(CAKEMLDIR)/candle/standard/semantics
Scanning $(CAKEMLDIR)/candle/prover/compute
Scanning $(CAKEMLDIR)/candle/prover
Scanning $(CAKEMLDIR)/candle/set-theory
Scanning $(CAKEMLDIR)/candle/standard
Scanning $(CAKEMLDIR)/candle/standard/syntax/little_theories
Scanning $(CAKEMLDIR)/characteristic/examples
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/compiler/encoders/ag32
Scanning $(CAKEMLDIR)/compiler/backend/ag32
Scanning $(HOLDIR)/examples/l3-machine-code/arm/model
Scanning $(HOLDIR)/examples/l3-machine-code/arm/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm7
Scanning $(CAKEMLDIR)/compiler/backend/arm7
Scanning $(CAKEMLDIR)/compiler/encoders/arm8
Scanning $(CAKEMLDIR)/compiler/backend/arm8
Scanning $(HOLDIR)/examples/l3-machine-code/mips/model
Scanning $(HOLDIR)/examples/l3-machine-code/mips/step
Scanning $(CAKEMLDIR)/compiler/encoders/mips
Scanning $(CAKEMLDIR)/compiler/backend/mips
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/model
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/step
Scanning $(CAKEMLDIR)/compiler/encoders/riscv
Scanning $(CAKEMLDIR)/compiler/backend/riscv
Scanning $(HOLDIR)/examples/l3-machine-code/x64/model
Scanning $(HOLDIR)/examples/l3-machine-code/x64/step
Scanning $(CAKEMLDIR)/compiler/encoders/x64
Scanning $(CAKEMLDIR)/compiler/backend/x64
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)/pancake
Scanning $(CAKEMLDIR)/pancake/parser
Scanning $(CAKEMLDIR)/compiler
Scanning $(CAKEMLDIR)/semantics/alt_semantics
Scanning $(CAKEMLDIR)/semantics/alt_semantics/proofs
Scanning $(CAKEMLDIR)/compiler/backend/semantics
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/prog
Scanning $(CAKEMLDIR)/compiler/encoders/riscv/proofs
Scanning $(CAKEMLDIR)/compiler/backend/San
Scanning $(CAKEMLDIR)/compiler/backend/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/ag32/proofs
Scanning $(CAKEMLDIR)/compiler/backend/ag32/proofs
Scanning $(HOLDIR)/examples/l3-machine-code/arm/prog
Scanning $(CAKEMLDIR)/compiler/encoders/arm7/proofs
Scanning $(CAKEMLDIR)/compiler/backend/arm7/proofs
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/prog
Scanning $(CAKEMLDIR)/compiler/encoders/arm8/proofs
Scanning $(CAKEMLDIR)/compiler/backend/arm8/proofs
Scanning $(CAKEMLDIR)/compiler/backend/serialiser
Scanning $(CAKEMLDIR)/compiler/backend/cv_compute
Scanning $(CAKEMLDIR)/compiler/backend/gc
Scanning $(HOLDIR)/examples/l3-machine-code/mips/prog
Scanning $(CAKEMLDIR)/compiler/encoders/mips/proofs
Scanning $(CAKEMLDIR)/compiler/backend/mips/proofs
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/compiler/backend/riscv/proofs
Scanning $(HOLDIR)/examples/l3-machine-code/x64/prog
Scanning $(CAKEMLDIR)/compiler/encoders/x64/proofs
Scanning $(CAKEMLDIR)/compiler/backend/x64/proofs
Scanning $(CAKEMLDIR)/compiler/bootstrap
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/ag32
Scanning $(CAKEMLDIR)/compiler/encoders/monadic_enc
Scanning $(CAKEMLDIR)/compiler/parsing/ocaml
Scanning $(CAKEMLDIR)/compiler/inference/proofs
Scanning $(CAKEMLDIR)/compiler/printing
Scanning $(CAKEMLDIR)/compiler/repl
Scanning $(CAKEMLDIR)/compiler/bootstrap/translation
Scanning $(HOLDIR)/src/num/theories/cv_compute/automation
Scanning $(HOLDIR)/examples/bootstrap
Scanning $(CAKEMLDIR)/cv_translator
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)/unverified/sexpr-bootstrap
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64/64
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64/64/proofs
Scanning $(CAKEMLDIR)/compiler/dafny
Scanning $(CAKEMLDIR)/compiler/dafny/translation
Scanning $(CAKEMLDIR)/compiler/dafny/compilation
Scanning $(CAKEMLDIR)/compiler/dafny/examples
Scanning $(CAKEMLDIR)/compiler/dafny/examples/output
Scanning $(CAKEMLDIR)/compiler/dafny/semantics
Scanning $(CAKEMLDIR)/compiler/dafny/vcg
Scanning $(CAKEMLDIR)/compiler/dafny/proofs
Scanning $(CAKEMLDIR)/compiler/dafny/vcg/examples
Scanning $(CAKEMLDIR)/compiler/encoders
Scanning $(CAKEMLDIR)/compiler/encoders/tests
Scanning $(CAKEMLDIR)/compiler/inference/tests
Scanning $(CAKEMLDIR)/compiler/parsing/proofs
Scanning $(CAKEMLDIR)/compiler/parsing/tests
Scanning $(CAKEMLDIR)/compiler/printing/test
Scanning $(CAKEMLDIR)/compiler/proofs
Scanning $(CAKEMLDIR)/compiler/scheme
Scanning $(CAKEMLDIR)/compiler/scheme/translation
Scanning $(CAKEMLDIR)/developers/bin
Scanning $(CAKEMLDIR)/compiler/scheme/compilation
Scanning $(CAKEMLDIR)/compiler/scheme/examples
Scanning $(CAKEMLDIR)/compiler/scheme/proofs
Scanning $(CAKEMLDIR)/compiler/scheme/unverified
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/cnf
Scanning $(CAKEMLDIR)/examples/cnf/array
Scanning $(CAKEMLDIR)/examples/cnf/dist
Scanning $(CAKEMLDIR)/examples/cnf/dist/array
Scanning $(CAKEMLDIR)/examples/cnf/dist/array/compilation
Scanning $(CAKEMLDIR)/examples/cnf/dist/array/compilation/proofs
Scanning $(CAKEMLDIR)/examples/compilation
Scanning $(CAKEMLDIR)/examples/compilation/ag32
Scanning $(CAKEMLDIR)/examples/compilation/ag32/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/Infra
Scanning $(CAKEMLDIR)/examples/flover/semantics
Scanning $(CAKEMLDIR)/examples/flover
Scanning $(CAKEMLDIR)/examples/lpr_checker
Scanning $(lpr_checker)/array
Scanning $(lpr_checker)/array/compilation
Scanning $(lpr_checker)/array/compilation/proofs
Scanning $(CAKEMLDIR)/examples/template
Scanning $(CAKEMLDIR)/examples/template/translation
Scanning $(CAKEMLDIR)/examples/template/compilation
Scanning $(CAKEMLDIR)/examples/vipr
Scanning $(CAKEMLDIR)/examples/vipr/compilation
Scanning $(CAKEMLDIR)/examples/xlrup_checker
Scanning $(CAKEMLDIR)/examples/xlrup_checker/array
Scanning $(CAKEMLDIR)/examples/xlrup_checker/array/compilation
Scanning $(CAKEMLDIR)/examples/xlrup_checker/array/compilation/proofs
Scanning $(CAKEMLDIR)/pancake/semantics
Scanning $(CAKEMLDIR)/pancake/proofs
Scanning $(CAKEMLDIR)/pancake/static_checker
Scanning $(CAKEMLDIR)/pancake/temp
Scanning $(CAKEMLDIR)/profiler
Scanning $(CAKEMLDIR)/translator/okasaki-examples
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/sexpr-bootstrap/x64
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/x64/64
Scanned 231 directories
Building 1 theory file
Starting work on README.md
Starting work on lpr_arrayProofARM8Theory
README.md                                                   (0s)             OK
lpr_arrayProofARM8Theory                                   (66s)        FAIL<1>
*** Holmake aborted - 1 target failed:
*** lpr_arrayProofARM8Theory (status 1)
 /scratch/cakeml/regression/cakeml-3424/examples/lpr_checker/array/compilation/proofsARM8/lpr_arrayProofARM8Script.sml:8: error: Structure (arm8_asl_configProofTheory) has not been declared
 Found near open holTheory HolKernel boolLib bossLib Parse ...
 error in quse /scratch/cakeml/regression/cakeml-3424/examples/lpr_checker/array/compilation/proofsARM8/lpr_arrayProofARM8Script.sml : Fail "Static Errors"
 error in load /scratch/cakeml/regression/cakeml-3424/examples/lpr_checker/array/compilation/proofsARM8/lpr_arrayProofARM8Script : Fail "Static Errors"
 Uncaught exception at ./basis/FinalPolyML.sml:492: Fail "Static Errors"
 Full log: /scratch/cakeml/regression/cakeml-3424/examples/lpr_checker/array/compilation/proofsARM8/.hol/logs/lpr_arrayProofARM8Theory