Job 3457

CakeML:fc2757ca9983a47fd47dcbe5ef265be828801ca8
  Restrict backward reification to a single literal, and extend the par [Aug 14 09:59:03]
#1457 (pb-parse)
Merging into:d19e3eb4438d587a84b8f21ef0aac65327be46d3
  Merge pull request #1427 from CakeML/holprojs [Aug 15 13:11:56]
HOL:fac52534ceb43806d35b11f91dafd558266bcbb6
  Remove yet one more same_const instance in Compute.sml [Aug 02 03:13:23]
Machine:lammmington

Aug 16 04:26:51 Claimed job
Aug 16 04:26:55 Reusing HOL
Aug 16 04:27:03 Starting developers
Aug 16 04:27:51 Finished developers                                              46s   1GB
Aug 16 04:27:52 Starting developers/bin
Aug 16 04:27:59 Finished developers/bin                                           6s   1GB
Aug 16 04:28:00 Starting misc
Aug 16 04:28:49 Finished misc                                                    48s   1GB
Aug 16 04:28:50 Starting compiler/proofs
Aug 16 05:43:38 Finished compiler/proofs                                    1h14m47s  11GB
Aug 16 05:43:39 Starting compiler/bootstrap/compilation/x64/64/proofs
Aug 16 12:08:14 Finished compiler/bootstrap/compilation/x64/64/proofs       6h24m33s  98GB
Aug 16 12:08:14 Starting semantics/ffi
Aug 16 12:08:37 Finished semantics/ffi                                           21s   1GB
Aug 16 12:08:37 Starting semantics
Aug 16 12:08:43 Finished semantics                                                4s   1GB
Aug 16 12:08:44 Starting semantics/proofs
Aug 16 12:09:13 Finished semantics/proofs                                        28s   1GB
Aug 16 12:09:14 Starting semantics/alt_semantics
Aug 16 12:09:36 Finished semantics/alt_semantics                                 21s   1GB
Aug 16 12:09:37 Starting semantics/alt_semantics/proofs
Aug 16 12:13:36 Finished semantics/alt_semantics/proofs                        3m57s   1GB
Aug 16 12:13:37 Starting basis/pure
Aug 16 12:13:43 Finished basis/pure                                               5s   1GB
Aug 16 12:13:43 Starting translator
Aug 16 12:15:02 Finished translator                                            1m17s   2GB
Aug 16 12:15:03 Starting compiler/parsing
Aug 16 12:15:53 Finished compiler/parsing                                        49s   2GB
Aug 16 12:15:54 Starting characteristic
Aug 16 12:16:00 Finished characteristic                                           4s   1GB
Aug 16 12:16:01 Starting translator/monadic
Aug 16 12:16:06 Finished translator/monadic                                       4s   1GB
Aug 16 12:16:07 Starting translator/monadic/monad_base
Aug 16 12:16:13 Finished translator/monadic/monad_base                            4s   1GB
Aug 16 12:16:14 Starting profiler
Aug 16 12:16:50 Finished profiler                                                35s   1GB
Aug 16 12:16:51 Starting basis
Aug 16 12:18:45 Finished basis                                                 1m53s   4GB
Aug 16 12:18:46 Starting compiler
Aug 16 12:18:52 Finished compiler                                                 4s   1GB
Aug 16 12:18:53 Starting compiler/inference
Aug 16 12:18:59 Finished compiler/inference                                       4s   1GB
Aug 16 12:18:59 Starting compiler/backend/reg_alloc
Aug 16 12:19:05 Finished compiler/backend/reg_alloc                               4s   1GB
Aug 16 12:19:06 Starting compiler/backend/gc
Aug 16 12:19:11 Finished compiler/backend/gc                                      4s   1GB
Aug 16 12:19:12 Starting compiler/backend
Aug 16 12:19:18 Finished compiler/backend                                         4s   1GB
Aug 16 12:19:19 Starting compiler/encoders/asm
Aug 16 12:19:25 Finished compiler/encoders/asm                                    4s   1GB
Aug 16 12:19:25 Starting compiler/encoders/x64
Aug 16 12:19:31 Finished compiler/encoders/x64                                    4s   1GB
Aug 16 12:19:32 Starting compiler/encoders/arm7
Aug 16 12:19:37 Finished compiler/encoders/arm7                                   4s   1GB
Aug 16 12:19:38 Starting compiler/encoders/arm8
Aug 16 12:19:44 Finished compiler/encoders/arm8                                   4s   1GB
Aug 16 12:19:45 Starting compiler/encoders/arm8_asl
Aug 16 12:20:10 Finished compiler/encoders/arm8_asl                              24s   1GB
Aug 16 12:20:10 Starting compiler/encoders/mips
Aug 16 12:20:16 Finished compiler/encoders/mips                                   4s   1GB
Aug 16 12:20:17 Starting compiler/encoders/riscv
Aug 16 12:20:22 Finished compiler/encoders/riscv                                  4s   1GB
Aug 16 12:20:23 Starting compiler/encoders/ag32
Aug 16 12:20:29 Finished compiler/encoders/ag32                                   4s   1GB
Aug 16 12:20:30 Starting compiler/encoders/tests
Aug 16 12:20:35 Finished compiler/encoders/tests                                  4s   1GB
Aug 16 12:20:36 Starting compiler/encoders/monadic_enc
Aug 16 12:21:03 Finished compiler/encoders/monadic_enc                           25s   1GB
Aug 16 12:21:04 Starting compiler/backend/x64
Aug 16 12:21:09 Finished compiler/backend/x64                                     4s   1GB
Aug 16 12:21:10 Starting compiler/backend/arm7
Aug 16 12:21:16 Finished compiler/backend/arm7                                    4s   1GB
Aug 16 12:21:17 Starting compiler/backend/arm8
Aug 16 12:21:23 Finished compiler/backend/arm8                                    5s   1GB
Aug 16 12:21:23 Starting compiler/backend/mips
Aug 16 12:21:29 Finished compiler/backend/mips                                    4s   1GB
Aug 16 12:21:30 Starting compiler/backend/riscv
Aug 16 12:21:35 Finished compiler/backend/riscv                                   4s   1GB
Aug 16 12:21:36 Starting compiler/backend/ag32
Aug 16 12:22:41 Finished compiler/backend/ag32                                 1m03s   1GB
Aug 16 12:22:42 Starting compiler/backend/pattern_matching
Aug 16 12:23:02 Finished compiler/backend/pattern_matching                       19s   1GB
Aug 16 12:23:03 Starting compiler/parsing/ocaml
Aug 16 12:25:16 Finished compiler/parsing/ocaml                                2m12s   1GB
Aug 16 12:25:17 Starting compiler/printing
Aug 16 12:26:19 Finished compiler/printing                                     1m00s   1GB
Aug 16 12:26:19 Starting compiler/parsing/proofs
Aug 16 12:26:25 Finished compiler/parsing/proofs                                  4s   1GB
Aug 16 12:26:26 Starting compiler/inference/proofs
Aug 16 12:26:32 Finished compiler/inference/proofs                                4s   1GB
Aug 16 12:26:32 Starting compiler/backend/semantics
Aug 16 12:29:43 Finished compiler/backend/semantics                            3m09s   3GB
Aug 16 12:29:43 Starting compiler/backend/reg_alloc/proofs
Aug 16 12:29:49 Finished compiler/backend/reg_alloc/proofs                        4s   1GB
Aug 16 12:29:50 Starting compiler/backend/proofs
Aug 16 12:30:39 Finished compiler/backend/proofs                                 47s   2GB
Aug 16 12:30:39 Starting compiler/backend/serialiser
Aug 16 12:30:45 Finished compiler/backend/serialiser                              4s   1GB
Aug 16 12:30:46 Starting compiler/encoders/x64/proofs
Aug 16 12:30:52 Finished compiler/encoders/x64/proofs                             4s   1GB
Aug 16 12:30:52 Starting compiler/encoders/arm7/proofs
Aug 16 12:43:28 Finished compiler/encoders/arm7/proofs                        12m34s  10GB
Aug 16 12:43:29 Starting compiler/encoders/arm8/proofs
Aug 16 12:51:30 Finished compiler/encoders/arm8/proofs                         8m00s   3GB
Aug 16 12:51:31 Starting compiler/encoders/arm8_asl/proofs
Aug 16 13:08:31 Finished compiler/encoders/arm8_asl/proofs                    16m59s   3GB
Aug 16 13:08:32 Starting compiler/encoders/mips/proofs
Aug 16 13:19:17 Finished compiler/encoders/mips/proofs                        10m43s   6GB
Aug 16 13:19:18 Starting compiler/encoders/riscv/proofs
Aug 16 13:28:51 Finished compiler/encoders/riscv/proofs                        9m32s   4GB
Aug 16 13:28:52 Starting compiler/encoders/ag32/proofs
Aug 16 13:32:01 Finished compiler/encoders/ag32/proofs                         3m08s   1GB
Aug 16 13:32:02 Starting compiler/backend/x64/proofs
Aug 16 13:32:07 Finished compiler/backend/x64/proofs                              4s   1GB
Aug 16 13:32:08 Starting compiler/backend/arm7/proofs
Aug 16 13:32:51 Finished compiler/backend/arm7/proofs                            41s   2GB
Aug 16 13:32:51 Starting compiler/backend/arm8/proofs
Aug 16 13:33:37 Finished compiler/backend/arm8/proofs                            44s   2GB
Aug 16 13:33:38 Starting compiler/backend/arm8_asl
Aug 16 13:34:14 Finished compiler/backend/arm8_asl                               34s   1GB
Aug 16 13:34:15 Starting compiler/backend/mips/proofs
Aug 16 13:35:00 Finished compiler/backend/mips/proofs                            44s   2GB
Aug 16 13:35:01 Starting compiler/backend/riscv/proofs
Aug 16 13:35:48 Finished compiler/backend/riscv/proofs                           46s   2GB
Aug 16 13:35:49 Starting compiler/backend/ag32/proofs
Aug 16 13:45:29 Finished compiler/backend/ag32/proofs                          9m38s   5GB
Aug 16 13:45:30 Starting compiler/backend/cv_compute
Aug 16 13:46:06 Finished compiler/backend/cv_compute                             35s   1GB
Aug 16 13:46:06 Starting cv_translator
Aug 16 13:51:26 Finished cv_translator                                         5m18s   3GB
Aug 16 13:51:27 Starting candle
Aug 16 13:51:32 Finished candle                                                   4s   1GB
Aug 16 13:51:33 Starting candle/set-theory
Aug 16 13:51:55 Finished candle/set-theory                                       21s   1GB
Aug 16 13:51:56 Starting candle/syntax-lib
Aug 16 13:52:02 Finished candle/syntax-lib                                        4s   1GB
Aug 16 13:52:03 Starting candle/standard
Aug 16 13:52:09 Finished candle/standard                                          5s   1GB
Aug 16 13:52:09 Starting candle/standard/syntax
Aug 16 13:52:29 Finished candle/standard/syntax                                  18s   1GB
Aug 16 13:52:30 Starting candle/standard/syntax/little_theories
Aug 16 13:53:47 Finished candle/standard/syntax/little_theories                1m16s   1GB
Aug 16 13:53:48 Starting candle/standard/semantics
Aug 16 13:53:54 Finished candle/standard/semantics                                4s   1GB
Aug 16 13:53:54 Starting candle/standard/monadic
Aug 16 13:54:00 Finished candle/standard/monadic                                  4s   1GB
Aug 16 13:54:01 Starting candle/standard/ml_kernel
Aug 16 13:56:20 Finished candle/standard/ml_kernel                             2m17s   4GB
Aug 16 13:56:21 Starting candle/overloading
Aug 16 13:56:26 Finished candle/overloading                                       4s   1GB
Aug 16 13:56:27 Starting candle/overloading/syntax
Aug 16 13:56:33 Finished candle/overloading/syntax                                5s   1GB
Aug 16 13:56:34 Starting candle/overloading/semantics
Aug 16 13:56:40 Finished candle/overloading/semantics                             4s   1GB
Aug 16 13:56:41 Starting candle/overloading/monadic
Aug 16 13:56:46 Finished candle/overloading/monadic                               4s   1GB
Aug 16 13:56:47 Starting candle/overloading/ml_kernel
Aug 16 13:56:53 Finished candle/overloading/ml_kernel                             4s   1GB
Aug 16 13:56:54 Starting candle/overloading/ml_checker
Aug 16 13:56:59 Finished candle/overloading/ml_checker                            4s   1GB
Aug 16 13:57:00 Starting candle/prover
Aug 16 13:57:06 Finished candle/prover                                            4s   1GB
Aug 16 13:57:07 Starting candle/prover/compute
Aug 16 13:57:12 Finished candle/prover/compute                                    4s   1GB
Aug 16 13:57:13 Starting pancake
Aug 16 13:57:19 Finished pancake                                                  4s   1GB
Aug 16 13:57:20 Starting pancake/semantics
Aug 16 14:00:23 Finished pancake/semantics                                     3m02s   2GB
Aug 16 14:00:24 Starting pancake/parser
Aug 16 14:01:08 Finished pancake/parser                                          43s   1GB
Aug 16 14:01:09 Starting pancake/static_checker
Aug 16 14:03:46 Finished pancake/static_checker                                2m36s   1GB
Aug 16 14:03:47 Starting pancake/proofs
Aug 16 14:21:09 Finished pancake/proofs                                       17m20s   4GB
Aug 16 14:21:10 Starting compiler/dafny
Aug 16 14:21:40 Finished compiler/dafny                                          29s   1GB
Aug 16 14:21:41 Starting compiler/dafny/translation
Aug 16 14:32:34 Finished compiler/dafny/translation                           10m52s   6GB
Aug 16 14:32:35 Starting compiler/dafny/compilation
Aug 16 14:34:51 Finished compiler/dafny/compilation                            2m14s   7GB
Aug 16 14:34:52 Starting compiler/dafny/semantics
Aug 16 14:35:36 Finished compiler/dafny/semantics                                43s   1GB
Aug 16 14:35:37 Starting compiler/dafny/proofs
Aug 16 14:37:23 Finished compiler/dafny/proofs                                 1m44s   1GB
Aug 16 14:37:23 Starting compiler/dafny/vcg
Aug 16 14:37:30 Finished compiler/dafny/vcg                                       5s   1GB
Aug 16 14:37:30 Starting compiler/dafny/vcg/examples
Aug 16 14:38:03 Finished compiler/dafny/vcg/examples                             31s   1GB
Aug 16 14:38:04 Starting compiler/scheme
Aug 16 14:38:35 Finished compiler/scheme                                         30s   1GB
Aug 16 14:38:36 Starting compiler/scheme/translation
Aug 16 14:45:35 Finished compiler/scheme/translation                           6m57s   7GB
Aug 16 14:45:36 Starting compiler/scheme/compilation
Aug 16 14:47:22 Finished compiler/scheme/compilation                           1m45s   4GB
Aug 16 14:47:23 Starting compiler/scheme/proofs
Aug 16 14:54:17 Finished compiler/scheme/proofs                                6m53s   2GB
Aug 16 14:54:18 Starting characteristic/examples
Aug 16 14:55:58 Finished characteristic/examples                               1m38s   5GB
Aug 16 14:55:59 Starting tutorial/solutions
Aug 16 14:56:04 Finished tutorial/solutions                                       4s   1GB
Aug 16 14:56:05 Starting translator/monadic/examples
Aug 16 14:56:11 Finished translator/monadic/examples                              4s   1GB
Aug 16 14:56:12 Starting examples
Aug 16 15:00:29 Finished examples                                              4m16s   4GB
Aug 16 15:00:30 Starting examples/compilation
Aug 16 15:00:37 Finished examples/compilation                                     5s   1GB
Aug 16 15:00:37 Starting examples/compilation/x64
Aug 16 15:09:35 Finished examples/compilation/x64                              8m57s   4GB
Aug 16 15:09:36 Starting examples/compilation/x64/proofs
Aug 16 15:13:24 Finished examples/compilation/x64/proofs                       3m46s   4GB
Aug 16 15:13:25 Starting examples/compilation/ag32
Aug 16 15:16:16 Finished examples/compilation/ag32                             2m49s   3GB
Aug 16 15:16:16 Starting examples/compilation/ag32/proofs
Aug 16 15:17:44 Finished examples/compilation/ag32/proofs                      1m26s   4GB
Aug 16 15:17:45 Starting examples/lpr_checker
Aug 16 15:18:29 Finished examples/lpr_checker                                    43s   1GB
Aug 16 15:18:30 Starting examples/lpr_checker/array
Aug 16 15:31:26 Finished examples/lpr_checker/array                           12m55s   6GB
Aug 16 15:31:27 Starting examples/lpr_checker/array/compilation
Aug 16 15:35:22 Finished examples/lpr_checker/array/compilation                3m54s   6GB
Aug 16 15:35:23 Starting examples/lpr_checker/array/compilation/proofs
Aug 16 15:37:07 Finished examples/lpr_checker/array/compilation/proofs         1m43s   5GB
Aug 16 15:37:13 Starting examples/lpr_checker/array/compilation/proofsARM8
Aug 16 15:39:06 Finished examples/lpr_checker/array/compilation/proofsARM8     1m52s   6GB
Aug 16 15:39:07 Starting .
Aug 16 15:39:13 Finished .                                                        4s   1GB
Aug 16 15:39:14 Starting examples/xlrup_checker
Aug 16 15:40:12 Finished examples/xlrup_checker                                  57s   1GB
Aug 16 15:40:13 Starting examples/xlrup_checker/array
Aug 16 15:50:01 Finished examples/xlrup_checker/array                          9m46s   5GB
Aug 16 15:50:02 Starting examples/xlrup_checker/array/compilation
Aug 16 15:51:44 Finished examples/xlrup_checker/array/compilation              1m41s   5GB
Aug 16 15:51:45 Starting examples/xlrup_checker/array/compilation/proofs
Aug 16 15:53:18 Finished examples/xlrup_checker/array/compilation/proofs       1m32s   5GB
Aug 16 15:53:19 Starting examples/cnf
Aug 16 15:53:47 Finished examples/cnf                                            26s   1GB
Aug 16 15:53:47 Starting examples/cnf/array
Aug 16 15:56:20 Finished examples/cnf/array                                    2m31s   2GB
Aug 16 15:56:21 Starting examples/cnf/dist
Aug 16 15:56:32 Finished examples/cnf/dist                                        9s   1GB
Aug 16 15:56:32 Starting examples/cnf/dist/array
Aug 16 16:03:40 Finished examples/cnf/dist/array                               7m06s   6GB
Aug 16 16:03:41 Starting examples/cnf/dist/array/compilation
Aug 16 16:04:48 Finished examples/cnf/dist/array/compilation                   1m05s   3GB
Aug 16 16:04:49 Starting examples/cnf/dist/array/compilation/proofs
Aug 16 16:06:12 Finished examples/cnf/dist/array/compilation/proofs            1m22s   4GB
Aug 16 16:06:13 Starting examples/scpog_checker
Aug 16 16:07:07 Finished examples/scpog_checker                                  53s   1GB
Aug 16 16:07:08 Starting examples/scpog_checker/array
Aug 16 16:13:15 Finished examples/scpog_checker/array                          6m05s   2GB
Aug 16 16:13:15 Starting examples/scpog_checker/array/compilation
Aug 16 16:15:56 Finished examples/scpog_checker/array/compilation              2m39s   8GB
Aug 16 16:15:56 Starting examples/scpog_checker/array/compilation/proofs
Aug 16 16:17:50 Finished examples/scpog_checker/array/compilation/proofs       1m52s   6GB
Aug 16 16:17:51 Starting examples/pseudo_bool
Aug 16 16:20:14 Finished examples/pseudo_bool                                  2m22s   1GB
Aug 16 16:20:15 Starting examples/pseudo_bool/cnf_encoding
Aug 16 16:20:51 Finished examples/pseudo_bool/cnf_encoding                       35s   1GB
Aug 16 16:20:52 Starting examples/pseudo_bool/graph_encoding
Aug 16 16:21:40 Finished examples/pseudo_bool/graph_encoding                     47s   1GB
Aug 16 16:21:41 Starting examples/pseudo_bool/array
Aug 16 17:06:24 Finished examples/pseudo_bool/array                           44m41s  29GB
Aug 16 17:06:24 Starting examples/pseudo_bool/array/compilation
Aug 16 17:30:18 Finished examples/pseudo_bool/array/compilation               23m52s  22GB
Aug 16 17:30:19 Starting examples/pseudo_bool/array/compilation/proofs
Aug 16 17:38:10 Finished examples/pseudo_bool/array/compilation/proofs         7m50s   9GB
Aug 16 17:38:11 Starting examples/pseudo_bool/array/compilation/proofsARM8
Aug 16 17:40:50 Finished examples/pseudo_bool/array/compilation/proofsARM8     2m38s   6GB
Aug 16 17:40:51 Starting examples/pseudo_bool/cp_encoding
Aug 16 17:44:07 Finished examples/pseudo_bool/cp_encoding                      3m14s   1GB
Aug 16 17:44:08 Starting examples/pseudo_bool/cp_encoding/array
Aug 16 17:48:51 FAILED: examples/pseudo_bool/cp_encoding/array
  HOLORIG=/scratch/cakeml/regression3/cakeml-3457/examples/pseudo_bool/cp_encoding/array [ -d "armv8.6-asl-snapshot" ] || ./get-armv8.6-hol-snapshot
Scanning $(CAKEMLDIR)/basis
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(HOLDIR)/src/sort
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(HOLDIR)/src/TeX
Scanning $(HOLDIR)/src/bag
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/pl-semantics/lprefix_lub
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(HOLDIR)/examples/algorithms
Scanning $(HOLDIR)/examples/Crypto/AES
Scanning $(HOLDIR)/src/integer
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)/src/floating-point
Scanning $(HOLDIR)/src/real/analysis
Scanning $(HOLDIR)/src/probability
Scanning $(HOLDIR)/examples/Crypto/DES
Scanning $(HOLDIR)/examples/Crypto/IDEA
Scanning $(HOLDIR)/src/num/theories/cv_compute/automation
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/monad/more_monads
Scanning $(HOLDIR)/src/emit
Scanning $(HOLDIR)/examples/Crypto/TEA
Scanning $(HOLDIR)/examples/Crypto/TWOFISH
Scanning $(HOLDIR)/examples/Crypto
Scanning $(HOLDIR)/examples/bootstrap
Scanning $(HOLDIR)/examples/data-structures/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/src/search
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(CAKEMLDIR)/examples
Scanning $(CAKEMLDIR)/examples/lpr_checker
Scanning $(pseudo_bool)/cnf_encoding
Scanning $(pseudo_bool)/graph_encoding
Scanning $(pseudo_bool)/array
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(HOLDIR)/src/update
Scanning $(HOLDIR)/examples/l3-machine-code/common
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(CAKEMLDIR)/compiler/encoders/ag32
Scanning $(CAKEMLDIR)/compiler/backend/ag32
Scanning $(HOLDIR)/examples/l3-machine-code/lib
Scanning $(HOLDIR)/examples/l3-machine-code/arm/model
Scanning $(HOLDIR)/examples/machine-code/decompiler
Scanning $(HOLDIR)/examples/l3-machine-code
Scanning $(HOLDIR)/examples/l3-machine-code/arm/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm7
Scanning $(CAKEMLDIR)/compiler/backend/arm7
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/model
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/step
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)/translator/monadic/monad_base
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 $(HOLDIR)/examples/machine-code/multiword
Scanning $(CAKEMLDIR)/pancake
Scanning $(CAKEMLDIR)/pancake/parser
Scanning $(CAKEMLDIR)/compiler
Scanning $(CAKEMLDIR)/compiler/backend/serialiser
Scanning $(CAKEMLDIR)/compiler/backend/cv_compute
Scanning $(CAKEMLDIR)/cv_translator
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap
Scanning $(pseudo_bool)/array/compilation
Scanning $(CAKEMLDIR)/compiler/backend/proofs
Scanning $(CAKEMLDIR)/semantics/alt_semantics
Scanning $(CAKEMLDIR)/semantics/alt_semantics/proofs
Scanning $(CAKEMLDIR)/compiler/backend/semantics
Scanning $(HOLDIR)/examples/l3-machine-code/x64/prog
Scanning $(CAKEMLDIR)/compiler/encoders/x64/proofs
Scanning $(CAKEMLDIR)/compiler/backend/x64/proofs
Scanning $(pseudo_bool)/array/compilation/proofs
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/asl-equiv
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/prog
Scanning $(CAKEMLDIR)/compiler/encoders/arm8/proofs
Scanning $(CAKEMLDIR)/compiler/backend/arm8/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/arm8_asl
Scanning $(CAKEMLDIR)/compiler/encoders/arm8_asl/proofs
Scanning $(CAKEMLDIR)/compiler/backend/arm8_asl
Scanning $(pseudo_bool)/array/compilation/proofsARM8
Scanning $(CAKEMLDIR)/compiler/dafny
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
Scanned 134 directories
Building 1 theory file
Starting work on README.md
Starting work on cpProgTheory
README.md                                                   (0s)             OK
cpProgTheory                                              (272s)        FAIL<1>
*** Holmake aborted - 1 target failed:
*** cpProgTheory (status 1)
 Saved theorem _______ "encode_nivar_v_thm"
 Translating proj_ivar
 Adding nsLookup representation thms for [cpProg_env_474]
 Saved theorem _______ "nsLookup_cpProg_env_475_pfun_eqs"
 Saved theorem _______ "proj_ivar_v_thm"
 Translating encode_prob_type
 Adding nsLookup representation thms for [cpProg_env_475]
 Saved theorem _______ "nsLookup_cpProg_env_476_pfun_eqs"
 Saved theorem _______ "encode_prob_type_v_thm"
 Translating format_string
 Adding nsLookup representation thms for [cpProg_env_476]
 Saved theorem _______ "nsLookup_cpProg_env_477_pfun_eqs"
 Saved theorem _______ "format_string_v_thm"
 <<HOL warning: ThmSetData.revise_data: 
   Theorems in set "compute":
     ADD<cpProg$generated_definition_def>
   invalidated by DelConstant(cpProg$generated_definition)>>
 Translating full_encode
 Adding nsLookup representation thms for [cpProg_env_477]
 Saved theorem _______ "nsLookup_cpProg_env_478_pfun_eqs"
 Saved theorem _______ "full_encode_v_thm"
 Translating conv_concl
 Adding nsLookup representation thms for [cpProg_env_478]
 Saved theorem _______ "nsLookup_cpProg_env_479_pfun_eqs"
 Saved theorem _______ "conv_concl_v_thm"
 Saved definition ____ "get_cp_inst_def"
 Saved theorem _______ "nsLookup_cpProg_env_480_pfun_eqs"
 Adding nsLookup representation thms for [cpProg_env_480, cpProg_env_479]
 Post condition: POSTv v. &(v = Conv (SOME (TypeStamp Some 2)) [fv]) * STDIO fs
 Using translator specification notfound_string_v_thm from theory npbc_parseProg
 Post condition: POSTv sv. STDIO fs * &vomap_TYPE (notfound_string f) sv
 Using translator specification parse_cp_inst_v_thm from theory cpProg
 Saved theorem _______ "parse_cp_file_spec"
 Saved theorem _______ "nsLookup_cpProg_env_481_pfun_eqs"
 Adding nsLookup representation thms for [cpProg_env_481]
 
 Exception raised at Q.store_thm_at:
 at Preterm.type-analysis:
   between line 1016, character 8 and line 1022, character 32:
   
 Type error in case expression.
   case res :(mlstring prob_type #
  mlstring list option #
  (mlstring lin_term # int) option # (mlstring list # mlstring pbc) list)
 result
   of INL err => get_cp_inst fs f = NONE | INR (cpobj,prob) => inst.
   get_cp_inst fs f = SOME inst  SND (SND inst) = cpobj 
   full_encode inst = prob
   Reason: Attempt to unify different type operators: list$list and option$option
 
 Full log: /scratch/cakeml/regression3/cakeml-3457/examples/pseudo_bool/cp_encoding/array/.hol/logs/cpProgTheory