Job 3427

CakeML:c75888c080da3885147d572a8e2f5a622d049a2b
  Clean up more holproject.toml files under examples/ [Jul 20 03:42:24]
#1427 (holprojs)
Merging into:8bc1398735a2018e9c6c6bcb92c58737f1aacaa9
  monadic translator: read the current theory only when it is needed [Aug 04 00:40:52]
HOL:fac52534ceb43806d35b11f91dafd558266bcbb6
  Remove yet one more same_const instance in Compute.sml [Aug 02 03:13:23]
Machine:pavlova

Aug 04 00:56:18 Claimed job
Aug 04 00:56:23 Reusing HOL
Aug 04 00:57:16 Starting developers
Aug 04 00:58:03 Finished developers                                              45s   1GB
Aug 04 00:58:04 Starting developers/bin
Aug 04 00:58:12 Finished developers/bin                                           7s   1GB
Aug 04 00:58:14 Starting misc
Aug 04 00:59:04 Finished misc                                                    48s   1GB
Aug 04 00:59:05 Starting compiler/proofs
Aug 04 02:13:21 Finished compiler/proofs                                    1h14m14s  11GB
Aug 04 02:13:22 Starting compiler/bootstrap/compilation/x64/64/proofs
Aug 04 08:33:30 Finished compiler/bootstrap/compilation/x64/64/proofs       6h20m06s  98GB
Aug 04 08:33:31 Starting semantics/ffi
Aug 04 08:33:53 Finished semantics/ffi                                           20s   1GB
Aug 04 08:33:54 Starting semantics
Aug 04 08:33:59 Finished semantics                                                4s   1GB
Aug 04 08:34:00 Starting semantics/proofs
Aug 04 08:34:31 Finished semantics/proofs                                        29s   1GB
Aug 04 08:34:32 Starting semantics/alt_semantics
Aug 04 08:34:54 Finished semantics/alt_semantics                                 21s   1GB
Aug 04 08:34:55 Starting semantics/alt_semantics/proofs
Aug 04 08:38:55 Finished semantics/alt_semantics/proofs                        3m59s   1GB
Aug 04 08:38:56 Starting basis/pure
Aug 04 08:39:02 Finished basis/pure                                               5s   1GB
Aug 04 08:39:02 Starting translator
Aug 04 08:40:22 Finished translator                                            1m17s   1GB
Aug 04 08:40:23 Starting compiler/parsing
Aug 04 08:41:14 Finished compiler/parsing                                        50s   2GB
Aug 04 08:41:15 Starting characteristic
Aug 04 08:41:21 Finished characteristic                                           4s   1GB
Aug 04 08:41:22 Starting translator/monadic
Aug 04 08:41:27 Finished translator/monadic                                       4s   1GB
Aug 04 08:41:28 Starting translator/monadic/monad_base
Aug 04 08:41:33 Finished translator/monadic/monad_base                            4s   1GB
Aug 04 08:41:34 Starting profiler
Aug 04 08:42:08 Finished profiler                                                32s   1GB
Aug 04 08:42:08 Starting basis
Aug 04 08:43:54 Finished basis                                                 1m44s   4GB
Aug 04 08:43:54 Starting compiler
Aug 04 08:44:00 Finished compiler                                                 4s   1GB
Aug 04 08:44:01 Starting compiler/inference
Aug 04 08:44:06 Finished compiler/inference                                       4s   1GB
Aug 04 08:44:07 Starting compiler/backend/reg_alloc
Aug 04 08:44:13 Finished compiler/backend/reg_alloc                               4s   1GB
Aug 04 08:44:13 Starting compiler/backend/gc
Aug 04 08:44:19 Finished compiler/backend/gc                                      4s   1GB
Aug 04 08:44:20 Starting compiler/backend
Aug 04 08:44:25 Finished compiler/backend                                         4s   1GB
Aug 04 08:44:26 Starting compiler/encoders/asm
Aug 04 08:44:32 Finished compiler/encoders/asm                                    4s   1GB
Aug 04 08:44:33 Starting compiler/encoders/x64
Aug 04 08:44:38 Finished compiler/encoders/x64                                    4s   1GB
Aug 04 08:44:39 Starting compiler/encoders/arm7
Aug 04 08:44:45 Finished compiler/encoders/arm7                                   4s   1GB
Aug 04 08:44:45 Starting compiler/encoders/arm8
Aug 04 08:44:51 Finished compiler/encoders/arm8                                   4s   1GB
Aug 04 08:44:52 Starting compiler/encoders/arm8_asl
Aug 04 11:11:21 Finished compiler/encoders/arm8_asl                         2h26m27s  39GB
Aug 04 11:11:22 Starting compiler/encoders/mips
Aug 04 11:11:30 Finished compiler/encoders/mips                                   6s   1GB
Aug 04 11:11:31 Starting compiler/encoders/riscv
Aug 04 11:11:36 Finished compiler/encoders/riscv                                  4s   1GB
Aug 04 11:11:37 Starting compiler/encoders/ag32
Aug 04 11:11:43 Finished compiler/encoders/ag32                                   4s   1GB
Aug 04 11:11:43 Starting compiler/encoders/tests
Aug 04 11:11:49 Finished compiler/encoders/tests                                  4s   1GB
Aug 04 11:11:50 Starting compiler/encoders/monadic_enc
Aug 04 11:12:16 Finished compiler/encoders/monadic_enc                           25s   1GB
Aug 04 11:12:17 Starting compiler/backend/x64
Aug 04 11:12:23 Finished compiler/backend/x64                                     4s   1GB
Aug 04 11:12:24 Starting compiler/backend/arm7
Aug 04 11:12:29 Finished compiler/backend/arm7                                    4s   1GB
Aug 04 11:12:30 Starting compiler/backend/arm8
Aug 04 11:12:35 Finished compiler/backend/arm8                                    4s   1GB
Aug 04 11:12:36 Starting compiler/backend/mips
Aug 04 11:12:42 Finished compiler/backend/mips                                    4s   1GB
Aug 04 11:12:42 Starting compiler/backend/riscv
Aug 04 11:12:48 Finished compiler/backend/riscv                                   4s   1GB
Aug 04 11:12:49 Starting compiler/backend/ag32
Aug 04 11:13:54 Finished compiler/backend/ag32                                 1m03s   1GB
Aug 04 11:13:54 Starting compiler/backend/pattern_matching
Aug 04 11:14:00 Finished compiler/backend/pattern_matching                        4s   1GB
Aug 04 11:14:01 Starting compiler/parsing/ocaml
Aug 04 11:16:12 Finished compiler/parsing/ocaml                                2m10s   1GB
Aug 04 11:16:13 Starting compiler/printing
Aug 04 11:17:11 Finished compiler/printing                                       57s   1GB
Aug 04 11:17:12 Starting compiler/parsing/proofs
Aug 04 11:17:18 Finished compiler/parsing/proofs                                  4s   1GB
Aug 04 11:17:19 Starting compiler/inference/proofs
Aug 04 11:17:24 Finished compiler/inference/proofs                                4s   1GB
Aug 04 11:17:25 Starting compiler/backend/semantics
Aug 04 11:20:29 Finished compiler/backend/semantics                            3m03s   3GB
Aug 04 11:20:30 Starting compiler/backend/reg_alloc/proofs
Aug 04 11:20:36 Finished compiler/backend/reg_alloc/proofs                        4s   1GB
Aug 04 11:20:36 Starting compiler/backend/proofs
Aug 04 11:21:25 Finished compiler/backend/proofs                                 47s   2GB
Aug 04 11:21:26 Starting compiler/backend/serialiser
Aug 04 11:21:31 Finished compiler/backend/serialiser                              4s   1GB
Aug 04 11:21:32 Starting compiler/encoders/x64/proofs
Aug 04 11:21:38 Finished compiler/encoders/x64/proofs                             4s   1GB
Aug 04 11:21:39 Starting compiler/encoders/arm7/proofs
Aug 04 11:33:59 Finished compiler/encoders/arm7/proofs                        12m19s   4GB
Aug 04 11:33:59 Starting compiler/encoders/arm8/proofs
Aug 04 11:41:46 Finished compiler/encoders/arm8/proofs                         7m46s   3GB
Aug 04 11:41:47 Starting compiler/encoders/arm8_asl/proofs
Aug 04 12:38:00 Finished compiler/encoders/arm8_asl/proofs                    56m11s  11GB
Aug 04 12:38:01 Starting compiler/encoders/mips/proofs
Aug 04 12:48:44 Finished compiler/encoders/mips/proofs                        10m42s   8GB
Aug 04 12:48:45 Starting compiler/encoders/riscv/proofs
Aug 04 12:58:18 Finished compiler/encoders/riscv/proofs                        9m32s   3GB
Aug 04 12:58:19 Starting compiler/encoders/ag32/proofs
Aug 04 13:01:28 Finished compiler/encoders/ag32/proofs                         3m07s   1GB
Aug 04 13:01:29 Starting compiler/backend/x64/proofs
Aug 04 13:01:34 Finished compiler/backend/x64/proofs                              4s   1GB
Aug 04 13:01:35 Starting compiler/backend/arm7/proofs
Aug 04 13:02:21 Finished compiler/backend/arm7/proofs                            44s   2GB
Aug 04 13:02:21 Starting compiler/backend/arm8/proofs
Aug 04 13:03:06 Finished compiler/backend/arm8/proofs                            44s   2GB
Aug 04 13:03:07 Starting compiler/backend/arm8_asl
Aug 04 13:03:40 Finished compiler/backend/arm8_asl                               31s   1GB
Aug 04 13:03:41 Starting compiler/backend/mips/proofs
Aug 04 13:04:25 Finished compiler/backend/mips/proofs                            43s   2GB
Aug 04 13:04:26 Starting compiler/backend/riscv/proofs
Aug 04 13:05:13 Finished compiler/backend/riscv/proofs                           46s   2GB
Aug 04 13:05:14 Starting compiler/backend/ag32/proofs
Aug 04 13:14:50 Finished compiler/backend/ag32/proofs                          9m34s   5GB
Aug 04 13:14:51 Starting compiler/backend/cv_compute
Aug 04 13:15:28 Finished compiler/backend/cv_compute                             36s   1GB
Aug 04 13:15:29 Starting cv_translator
Aug 04 13:20:40 Finished cv_translator                                         5m10s   3GB
Aug 04 13:20:41 Starting candle
Aug 04 13:20:47 Finished candle                                                   4s   1GB
Aug 04 13:20:48 Starting candle/set-theory
Aug 04 13:21:24 Finished candle/set-theory                                       35s   1GB
Aug 04 13:21:25 Starting candle/syntax-lib
Aug 04 13:21:31 Finished candle/syntax-lib                                        4s   1GB
Aug 04 13:21:31 Starting candle/standard
Aug 04 13:21:37 Finished candle/standard                                          4s   1GB
Aug 04 13:21:38 Starting candle/standard/syntax
Aug 04 13:21:57 Finished candle/standard/syntax                                  18s   1GB
Aug 04 13:21:58 Starting candle/standard/syntax/little_theories
Aug 04 13:23:16 Finished candle/standard/syntax/little_theories                1m17s   1GB
Aug 04 13:23:17 Starting candle/standard/semantics
Aug 04 13:25:39 Finished candle/standard/semantics                             2m21s   2GB
Aug 04 13:25:40 Starting candle/standard/monadic
Aug 04 13:25:46 Finished candle/standard/monadic                                  4s   1GB
Aug 04 13:25:47 Starting candle/standard/ml_kernel
Aug 04 13:28:08 Finished candle/standard/ml_kernel                             2m19s   4GB
Aug 04 13:28:08 Starting candle/overloading
Aug 04 13:28:14 Finished candle/overloading                                       4s   1GB
Aug 04 13:28:15 Starting candle/overloading/syntax
Aug 04 13:28:20 Finished candle/overloading/syntax                                4s   1GB
Aug 04 13:28:21 Starting candle/overloading/semantics
Aug 04 13:28:27 Finished candle/overloading/semantics                             4s   1GB
Aug 04 13:28:28 Starting candle/overloading/monadic
Aug 04 13:28:33 Finished candle/overloading/monadic                               4s   1GB
Aug 04 13:28:34 Starting candle/overloading/ml_kernel
Aug 04 13:28:39 Finished candle/overloading/ml_kernel                             4s   1GB
Aug 04 13:28:40 Starting candle/overloading/ml_checker
Aug 04 13:28:46 Finished candle/overloading/ml_checker                            4s   1GB
Aug 04 13:28:47 Starting candle/prover
Aug 04 13:28:52 Finished candle/prover                                            4s   1GB
Aug 04 13:28:53 Starting candle/prover/compute
Aug 04 13:28:59 Finished candle/prover/compute                                    4s   1GB
Aug 04 13:29:00 Starting pancake
Aug 04 13:29:05 Finished pancake                                                  4s   1GB
Aug 04 13:29:06 Starting pancake/semantics
Aug 04 13:32:06 Finished pancake/semantics                                     2m59s   2GB
Aug 04 13:32:07 Starting pancake/parser
Aug 04 13:32:51 Finished pancake/parser                                          42s   1GB
Aug 04 13:32:52 Starting pancake/static_checker
Aug 04 13:35:29 Finished pancake/static_checker                                2m36s   1GB
Aug 04 13:35:29 Starting pancake/proofs
Aug 04 13:52:42 Finished pancake/proofs                                       17m11s   5GB
Aug 04 13:52:43 Starting compiler/dafny
Aug 04 13:53:12 Finished compiler/dafny                                          28s   1GB
Aug 04 13:53:13 Starting compiler/dafny/translation
Aug 04 14:04:39 Finished compiler/dafny/translation                           11m25s   7GB
Aug 04 14:04:39 Starting compiler/dafny/compilation
Aug 04 14:06:49 Finished compiler/dafny/compilation                            2m08s   6GB
Aug 04 14:06:50 Starting compiler/dafny/semantics
Aug 04 14:07:33 Finished compiler/dafny/semantics                                42s   1GB
Aug 04 14:07:34 Starting compiler/dafny/proofs
Aug 04 14:09:20 Finished compiler/dafny/proofs                                 1m45s   1GB
Aug 04 14:09:21 Starting compiler/dafny/vcg
Aug 04 14:09:27 Finished compiler/dafny/vcg                                       5s   1GB
Aug 04 14:09:28 Starting compiler/dafny/vcg/examples
Aug 04 14:10:01 Finished compiler/dafny/vcg/examples                             31s   1GB
Aug 04 14:10:01 Starting compiler/scheme
Aug 04 14:10:33 Finished compiler/scheme                                         31s   1GB
Aug 04 14:10:34 Starting compiler/scheme/translation
Aug 04 14:17:24 Finished compiler/scheme/translation                           6m48s   7GB
Aug 04 14:17:25 Starting compiler/scheme/compilation
Aug 04 14:19:06 Finished compiler/scheme/compilation                           1m40s   5GB
Aug 04 14:19:07 Starting compiler/scheme/proofs
Aug 04 14:25:58 Finished compiler/scheme/proofs                                6m50s   3GB
Aug 04 14:25:59 Starting characteristic/examples
Aug 04 14:27:39 Finished characteristic/examples                               1m38s   5GB
Aug 04 14:27:40 Starting tutorial/solutions
Aug 04 14:27:45 Finished tutorial/solutions                                       4s   1GB
Aug 04 14:27:46 Starting translator/monadic/examples
Aug 04 14:27:52 Finished translator/monadic/examples                              4s   1GB
Aug 04 14:27:53 Starting examples
Aug 04 14:32:26 Finished examples                                              4m32s   3GB
Aug 04 14:32:27 Starting examples/compilation
Aug 04 14:32:33 Finished examples/compilation                                     5s   1GB
Aug 04 14:32:34 Starting examples/compilation/x64
Aug 04 14:41:28 Finished examples/compilation/x64                              8m52s   4GB
Aug 04 14:41:28 Starting examples/compilation/x64/proofs
Aug 04 14:45:00 Finished examples/compilation/x64/proofs                       3m30s   4GB
Aug 04 14:45:00 Starting examples/compilation/ag32
Aug 04 14:47:47 Finished examples/compilation/ag32                             2m45s   3GB
Aug 04 14:47:48 Starting examples/compilation/ag32/proofs
Aug 04 14:49:13 Finished examples/compilation/ag32/proofs                      1m24s   5GB
Aug 04 14:49:14 Starting examples/lpr_checker
Aug 04 14:49:58 Finished examples/lpr_checker                                    43s   1GB
Aug 04 14:49:59 Starting examples/lpr_checker/array
Aug 04 15:02:50 Finished examples/lpr_checker/array                           12m49s   5GB
Aug 04 15:02:51 Starting examples/lpr_checker/array/compilation
Aug 04 15:06:35 Finished examples/lpr_checker/array/compilation                3m43s   6GB
Aug 04 15:06:36 Starting examples/lpr_checker/array/compilation/proofs
Aug 04 15:08:19 Finished examples/lpr_checker/array/compilation/proofs         1m42s   6GB
Aug 04 15:08:20 Starting examples/lpr_checker/array/compilation/proofsARM8
Aug 04 15:09:42 FAILED: examples/lpr_checker/array/compilation/proofsARM8
  HOLORIG=/scratch/cakeml/regression/cakeml-3427/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                                   (68s)        FAIL<1>
*** Holmake aborted - 1 target failed:
*** lpr_arrayProofARM8Theory (status 1)
 /scratch/cakeml/regression/cakeml-3427/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-3427/examples/lpr_checker/array/compilation/proofsARM8/lpr_arrayProofARM8Script.sml : Fail "Static Errors"
 error in load /scratch/cakeml/regression/cakeml-3427/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-3427/examples/lpr_checker/array/compilation/proofsARM8/.hol/logs/lpr_arrayProofARM8Theory