Job 3558

CakeML:5c570da1c5dc08930735b5fde54a866d10c8f9e3
  Merge remote-tracking branch 'origin/master' into fdiff [Sep 30 04:20:10]
#1444 (fdiff)
Merging into:530c7deec135ad421cce7ca768eed2f5801261b2
  Merge pull request #1502 from CakeML/bool_array_in_basis [Sep 28 20:21:18]
HOL:dfff742b1f89a43e9c1812a146e9a40d4c4d89fc
  Avoid Q.prove in Lib [Sep 16 11:12:56]
Machine:lammmington

Sep 30 07:44:47 Claimed job
Sep 30 07:44:51 Reusing HOL
Sep 30 07:45:01 Starting developers
Sep 30 07:45:53 Finished developers                                              51s   1GB
Sep 30 07:45:54 Starting developers/bin
Sep 30 07:46:04 Finished developers/bin                                           8s   1GB
Sep 30 07:46:04 Starting misc
Sep 30 07:46:52 Finished misc                                                    46s   1GB
Sep 30 07:46:53 Starting compiler/proofs
Sep 30 09:06:09 Finished compiler/proofs                                    1h19m15s  16GB
Sep 30 09:06:10 Starting compiler/bootstrap/compilation/x64/64/proofs
Sep 30 16:02:50 Finished compiler/bootstrap/compilation/x64/64/proofs       6h56m38s  95GB
Sep 30 16:02:51 Starting semantics/ffi
Sep 30 16:03:15 Finished semantics/ffi                                           22s   1GB
Sep 30 16:03:16 Starting semantics
Sep 30 16:03:23 Finished semantics                                                6s   1GB
Sep 30 16:03:24 Starting semantics/proofs
Sep 30 16:03:55 Finished semantics/proofs                                        30s   1GB
Sep 30 16:03:56 Starting semantics/alt_semantics
Sep 30 16:04:19 Finished semantics/alt_semantics                                 22s   1GB
Sep 30 16:04:20 Starting semantics/alt_semantics/proofs
Sep 30 16:08:33 Finished semantics/alt_semantics/proofs                        4m11s   1GB
Sep 30 16:08:34 Starting basis/pure
Sep 30 16:08:42 Finished basis/pure                                               6s   1GB
Sep 30 16:08:43 Starting translator
Sep 30 16:10:01 Finished translator                                            1m17s   3GB
Sep 30 16:10:02 Starting compiler/parsing
Sep 30 16:10:53 Finished compiler/parsing                                        50s   2GB
Sep 30 16:10:54 Starting characteristic
Sep 30 16:11:02 Finished characteristic                                           6s   1GB
Sep 30 16:11:03 Starting translator/monadic
Sep 30 16:11:10 Finished translator/monadic                                       6s   1GB
Sep 30 16:11:11 Starting translator/monadic/monad_base
Sep 30 16:11:18 Finished translator/monadic/monad_base                            6s   1GB
Sep 30 16:11:19 Starting profiler
Sep 30 16:11:55 Finished profiler                                                35s   2GB
Sep 30 16:11:56 Starting basis
Sep 30 16:13:52 Finished basis                                                 1m55s   4GB
Sep 30 16:13:53 Starting compiler
Sep 30 16:14:00 Finished compiler                                                 6s   1GB
Sep 30 16:14:01 Starting compiler/inference
Sep 30 16:14:08 Finished compiler/inference                                       6s   1GB
Sep 30 16:14:09 Starting compiler/backend/reg_alloc
Sep 30 16:14:16 Finished compiler/backend/reg_alloc                               6s   1GB
Sep 30 16:14:17 Starting compiler/backend/gc
Sep 30 16:14:24 Finished compiler/backend/gc                                      6s   1GB
Sep 30 16:14:25 Starting compiler/backend
Sep 30 16:14:36 Finished compiler/backend                                         9s   1GB
Sep 30 16:14:36 Starting compiler/encoders/asm
Sep 30 16:14:44 Finished compiler/encoders/asm                                    6s   1GB
Sep 30 16:14:45 Starting compiler/encoders/x64
Sep 30 16:14:52 Finished compiler/encoders/x64                                    6s   1GB
Sep 30 16:14:53 Starting compiler/encoders/arm7
Sep 30 16:15:00 Finished compiler/encoders/arm7                                   6s   1GB
Sep 30 16:15:01 Starting compiler/encoders/arm8
Sep 30 16:15:08 Finished compiler/encoders/arm8                                   6s   1GB
Sep 30 16:15:09 Starting compiler/encoders/arm8_asl
Sep 30 16:15:31 Finished compiler/encoders/arm8_asl                              21s   1GB
Sep 30 16:15:32 Starting compiler/encoders/mips
Sep 30 16:15:39 Finished compiler/encoders/mips                                   6s   1GB
Sep 30 16:15:40 Starting compiler/encoders/riscv
Sep 30 16:15:47 Finished compiler/encoders/riscv                                  6s   1GB
Sep 30 16:15:48 Starting compiler/encoders/ag32
Sep 30 16:15:55 Finished compiler/encoders/ag32                                   5s   1GB
Sep 30 16:15:56 Starting compiler/encoders/tests
Sep 30 16:16:03 Finished compiler/encoders/tests                                  6s   1GB
Sep 30 16:16:04 Starting compiler/encoders/monadic_enc
Sep 30 16:16:31 Finished compiler/encoders/monadic_enc                           25s   1GB
Sep 30 16:16:32 Starting compiler/backend/x64
Sep 30 16:16:39 Finished compiler/backend/x64                                     6s   1GB
Sep 30 16:16:40 Starting compiler/backend/arm7
Sep 30 16:16:47 Finished compiler/backend/arm7                                    5s   1GB
Sep 30 16:16:48 Starting compiler/backend/arm8
Sep 30 16:16:55 Finished compiler/backend/arm8                                    6s   1GB
Sep 30 16:16:56 Starting compiler/backend/mips
Sep 30 16:17:03 Finished compiler/backend/mips                                    6s   1GB
Sep 30 16:17:04 Starting compiler/backend/riscv
Sep 30 16:17:11 Finished compiler/backend/riscv                                   6s   1GB
Sep 30 16:17:12 Starting compiler/backend/ag32
Sep 30 16:18:20 Finished compiler/backend/ag32                                 1m07s   1GB
Sep 30 16:18:21 Starting compiler/backend/pattern_matching
Sep 30 16:18:42 Finished compiler/backend/pattern_matching                       20s   1GB
Sep 30 16:18:43 Starting compiler/parsing/ocaml
Sep 30 16:21:09 Finished compiler/parsing/ocaml                                2m25s   1GB
Sep 30 16:21:10 Starting compiler/printing
Sep 30 16:22:09 Finished compiler/printing                                       58s   1GB
Sep 30 16:22:10 Starting compiler/parsing/proofs
Sep 30 16:22:17 Finished compiler/parsing/proofs                                  6s   1GB
Sep 30 16:22:18 Starting compiler/inference/proofs
Sep 30 16:22:25 Finished compiler/inference/proofs                                6s   1GB
Sep 30 16:22:26 Starting compiler/backend/semantics
Sep 30 16:25:45 Finished compiler/backend/semantics                            3m18s   3GB
Sep 30 16:25:46 Starting compiler/backend/reg_alloc/proofs
Sep 30 16:25:54 Finished compiler/backend/reg_alloc/proofs                        6s   1GB
Sep 30 16:25:55 Starting compiler/backend/proofs
Sep 30 16:26:47 Finished compiler/backend/proofs                                 50s   2GB
Sep 30 16:26:48 Starting compiler/backend/serialiser
Sep 30 16:26:55 Finished compiler/backend/serialiser                              6s   1GB
Sep 30 16:26:56 Starting compiler/encoders/x64/proofs
Sep 30 16:27:03 Finished compiler/encoders/x64/proofs                             6s   1GB
Sep 30 16:27:04 Starting compiler/encoders/arm7/proofs
Sep 30 16:39:36 Finished compiler/encoders/arm7/proofs                        12m30s   4GB
Sep 30 16:39:37 Starting compiler/encoders/arm8/proofs
Sep 30 16:48:10 Finished compiler/encoders/arm8/proofs                         8m32s   3GB
Sep 30 16:48:11 Starting compiler/encoders/arm8_asl/proofs
Sep 30 17:05:56 Finished compiler/encoders/arm8_asl/proofs                    17m43s   3GB
Sep 30 17:05:57 Starting compiler/encoders/mips/proofs
Sep 30 17:17:09 Finished compiler/encoders/mips/proofs                        11m10s   5GB
Sep 30 17:17:10 Starting compiler/encoders/riscv/proofs
Sep 30 17:27:08 Finished compiler/encoders/riscv/proofs                        9m57s   3GB
Sep 30 17:27:09 Starting compiler/encoders/ag32/proofs
Sep 30 17:30:26 Finished compiler/encoders/ag32/proofs                         3m15s   1GB
Sep 30 17:30:27 Starting compiler/backend/x64/proofs
Sep 30 17:30:34 Finished compiler/backend/x64/proofs                              6s   1GB
Sep 30 17:30:35 Starting compiler/backend/arm7/proofs
Sep 30 17:31:23 Finished compiler/backend/arm7/proofs                            46s   2GB
Sep 30 17:31:24 Starting compiler/backend/arm8/proofs
Sep 30 17:32:07 Finished compiler/backend/arm8/proofs                            42s   2GB
Sep 30 17:32:08 Starting compiler/backend/arm8_asl
Sep 30 17:32:49 Finished compiler/backend/arm8_asl                               39s   2GB
Sep 30 17:32:50 Starting compiler/backend/mips/proofs
Sep 30 17:33:36 Finished compiler/backend/mips/proofs                            44s   2GB
Sep 30 17:33:37 Starting compiler/backend/riscv/proofs
Sep 30 17:34:25 Finished compiler/backend/riscv/proofs                           47s   2GB
Sep 30 17:34:26 Starting compiler/backend/ag32/proofs
Sep 30 17:44:25 Finished compiler/backend/ag32/proofs                          9m57s   4GB
Sep 30 17:44:26 Starting compiler/backend/cv_compute
Sep 30 17:45:02 Finished compiler/backend/cv_compute                             35s   1GB
Sep 30 17:45:03 Starting cv_translator
Sep 30 17:50:34 Finished cv_translator                                         5m30s   3GB
Sep 30 17:50:35 Starting candle
Sep 30 17:50:42 Finished candle                                                   6s   1GB
Sep 30 17:50:43 Starting candle/set-theory
Sep 30 17:51:06 Finished candle/set-theory                                       21s   1GB
Sep 30 17:51:07 Starting candle/syntax-lib
Sep 30 17:51:14 Finished candle/syntax-lib                                        6s   1GB
Sep 30 17:51:15 Starting candle/standard
Sep 30 17:51:22 Finished candle/standard                                          6s   1GB
Sep 30 17:51:23 Starting candle/standard/syntax
Sep 30 17:51:43 Finished candle/standard/syntax                                  18s   1GB
Sep 30 17:51:44 Starting candle/standard/syntax/little_theories
Sep 30 17:53:01 Finished candle/standard/syntax/little_theories                1m16s   1GB
Sep 30 17:53:02 Starting candle/standard/semantics
Sep 30 17:53:09 Finished candle/standard/semantics                                6s   1GB
Sep 30 17:53:10 Starting candle/standard/monadic
Sep 30 17:53:17 Finished candle/standard/monadic                                  6s   1GB
Sep 30 17:53:18 Starting candle/standard/ml_kernel
Sep 30 17:55:35 Finished candle/standard/ml_kernel                             2m15s   4GB
Sep 30 17:55:36 Starting candle/overloading
Sep 30 17:55:43 Finished candle/overloading                                       6s   1GB
Sep 30 17:55:44 Starting candle/overloading/syntax
Sep 30 17:59:01 Finished candle/overloading/syntax                             3m16s   1GB
Sep 30 17:59:02 Starting candle/overloading/semantics
Sep 30 18:08:41 Finished candle/overloading/semantics                          9m37s   4GB
Sep 30 18:08:42 Starting candle/overloading/monadic
Sep 30 18:10:59 Finished candle/overloading/monadic                            2m16s   1GB
Sep 30 18:11:00 Starting candle/overloading/ml_kernel
Sep 30 18:18:17 Finished candle/overloading/ml_kernel                          7m15s   7GB
Sep 30 18:18:18 Starting candle/overloading/ml_checker
Sep 30 18:21:15 Finished candle/overloading/ml_checker                         2m56s   6GB
Sep 30 18:21:16 Starting candle/prover
Sep 30 18:21:24 Finished candle/prover                                            6s   1GB
Sep 30 18:21:25 Starting candle/prover/compute
Sep 30 18:21:32 Finished candle/prover/compute                                    5s   1GB
Sep 30 18:21:33 Starting pancake
Sep 30 18:21:40 Finished pancake                                                  5s   1GB
Sep 30 18:21:41 Starting pancake/semantics
Sep 30 18:25:02 Finished pancake/semantics                                     3m20s   1GB
Sep 30 18:25:03 Starting pancake/parser
Sep 30 18:25:52 Finished pancake/parser                                          48s   1GB
Sep 30 18:25:53 Starting pancake/static_checker
Sep 30 18:28:33 Finished pancake/static_checker                                2m39s   1GB
Sep 30 18:28:34 Starting pancake/proofs
Sep 30 18:45:21 Finished pancake/proofs                                       16m45s   6GB
Sep 30 18:45:22 Starting compiler/dafny
Sep 30 18:45:52 Finished compiler/dafny                                          28s   1GB
Sep 30 18:45:53 Starting compiler/dafny/translation
Sep 30 18:57:08 Finished compiler/dafny/translation                           11m14s   7GB
Sep 30 18:57:09 Starting compiler/dafny/compilation
Sep 30 18:59:30 Finished compiler/dafny/compilation                            2m19s   7GB
Sep 30 18:59:31 Starting compiler/dafny/semantics
Sep 30 19:00:16 Finished compiler/dafny/semantics                                43s   1GB
Sep 30 19:00:17 Starting compiler/dafny/proofs
Sep 30 19:02:03 Finished compiler/dafny/proofs                                 1m44s   1GB
Sep 30 19:02:04 Starting compiler/dafny/vcg
Sep 30 19:02:12 Finished compiler/dafny/vcg                                       6s   1GB
Sep 30 19:02:13 Starting compiler/dafny/vcg/examples
Sep 30 19:02:47 Finished compiler/dafny/vcg/examples                             33s   1GB
Sep 30 19:02:48 Starting compiler/scheme
Sep 30 19:03:21 Finished compiler/scheme                                         32s   1GB
Sep 30 19:03:22 Starting compiler/scheme/translation
Sep 30 19:10:53 Finished compiler/scheme/translation                           7m29s   9GB
Sep 30 19:10:54 Starting compiler/scheme/compilation
Sep 30 19:12:45 Finished compiler/scheme/compilation                           1m49s   5GB
Sep 30 19:12:46 Starting compiler/scheme/proofs
Sep 30 19:19:59 Finished compiler/scheme/proofs                                7m12s   2GB
Sep 30 19:20:00 Starting characteristic/examples
Sep 30 19:21:43 Finished characteristic/examples                               1m42s   5GB
Sep 30 19:21:44 Starting tutorial
Sep 30 19:21:52 Finished tutorial                                                 6s   1GB
Sep 30 19:21:53 Starting tutorial/solutions
Sep 30 19:24:54 Finished tutorial/solutions                                    3m00s   4GB
Sep 30 19:24:55 Starting translator/monadic/examples
Sep 30 19:28:18 Finished translator/monadic/examples                           3m21s   4GB
Sep 30 19:28:19 Starting examples
Sep 30 19:32:46 Finished examples                                              4m26s   5GB
Sep 30 19:32:47 Starting examples/compilation
Sep 30 19:32:55 Finished examples/compilation                                     6s   1GB
Sep 30 19:32:56 Starting examples/compilation/x64
Sep 30 19:42:25 Finished examples/compilation/x64                              9m27s   4GB
Sep 30 19:42:26 Starting examples/compilation/x64/proofs
Sep 30 19:46:10 Finished examples/compilation/x64/proofs                       3m42s   4GB
Sep 30 19:46:11 Starting examples/compilation/ag32
Sep 30 19:49:04 Finished examples/compilation/ag32                             2m51s   3GB
Sep 30 19:49:05 Starting examples/compilation/ag32/proofs
Sep 30 19:50:39 Finished examples/compilation/ag32/proofs                      1m33s   5GB
Sep 30 19:50:40 Starting examples/lpr_checker
Sep 30 19:51:25 Finished examples/lpr_checker                                    44s   1GB
Sep 30 19:51:26 Starting examples/lpr_checker/array
Sep 30 20:04:44 Finished examples/lpr_checker/array                           13m16s   4GB
Sep 30 20:04:45 Starting examples/lpr_checker/array/compilation
Sep 30 20:08:39 Finished examples/lpr_checker/array/compilation                3m53s   7GB
Sep 30 20:08:40 Starting examples/lpr_checker/array/compilation/proofs
Sep 30 20:10:26 Finished examples/lpr_checker/array/compilation/proofs         1m44s   6GB
Sep 30 20:10:27 Starting examples/lpr_checker/array/compilation/proofsARM8
Sep 30 20:12:18 Finished examples/lpr_checker/array/compilation/proofsARM8     1m49s   6GB
Sep 30 20:12:19 Starting .
Sep 30 20:12:26 Finished .                                                        6s   1GB
Sep 30 20:12:27 Starting examples/xlrup_checker
Sep 30 20:13:26 Finished examples/xlrup_checker                                  58s   1GB
Sep 30 20:13:27 Starting examples/xlrup_checker/array
Sep 30 20:23:30 Finished examples/xlrup_checker/array                         10m01s   3GB
Sep 30 20:23:30 Starting examples/xlrup_checker/array/compilation
Sep 30 20:25:18 Finished examples/xlrup_checker/array/compilation              1m47s   5GB
Sep 30 20:25:19 Starting examples/xlrup_checker/array/compilation/proofs
Sep 30 20:26:57 Finished examples/xlrup_checker/array/compilation/proofs       1m36s   5GB
Sep 30 20:26:58 Starting examples/cnf
Sep 30 20:27:32 Finished examples/cnf                                            33s   1GB
Sep 30 20:27:33 Starting examples/cnf/array
Sep 30 20:30:49 Finished examples/cnf/array                                    3m15s   1GB
Sep 30 20:30:50 Starting examples/cnf/dist
Sep 30 20:31:02 Finished examples/cnf/dist                                       10s   1GB
Sep 30 20:31:03 Starting examples/cnf/dist/array
Sep 30 20:35:43 Finished examples/cnf/dist/array                               4m38s   3GB
Sep 30 20:35:43 Starting examples/cnf/dist/array/compilation
Sep 30 20:36:54 Finished examples/cnf/dist/array/compilation                   1m09s   3GB
Sep 30 20:36:55 Starting examples/cnf/dist/array/compilation/proofs
Sep 30 20:38:23 Finished examples/cnf/dist/array/compilation/proofs            1m27s   4GB
Sep 30 20:38:24 Starting examples/cnf/lrup
Sep 30 20:38:37 Finished examples/cnf/lrup                                       11s   1GB
Sep 30 20:38:38 Starting examples/cnf/lrup/array
Sep 30 20:41:59 Finished examples/cnf/lrup/array                               3m20s   1GB
Sep 30 20:42:00 Starting examples/cnf/lrup/array/compilation
Sep 30 20:43:21 Finished examples/cnf/lrup/array/compilation                   1m20s   4GB
Sep 30 20:43:22 Starting examples/cnf/lrup/array/compilation/proofs
Sep 30 20:44:52 Finished examples/cnf/lrup/array/compilation/proofs            1m28s   4GB
Sep 30 20:44:53 Starting examples/cnf/xlrup
Sep 30 20:45:37 Finished examples/cnf/xlrup                                      43s   1GB
Sep 30 20:45:38 Starting examples/cnf/xlrup/array
Sep 30 20:53:16 Finished examples/cnf/xlrup/array                              7m37s   2GB
Sep 30 20:53:17 Starting examples/cnf/xlrup/array/compilation
Sep 30 20:54:54 Finished examples/cnf/xlrup/array/compilation                  1m35s   5GB
Sep 30 20:54:55 Starting examples/cnf/xlrup/array/compilation/proofs
Sep 30 20:56:25 Finished examples/cnf/xlrup/array/compilation/proofs           1m29s   4GB
Sep 30 20:56:26 Starting examples/scpog_checker
Sep 30 20:57:22 Finished examples/scpog_checker                                  54s   1GB
Sep 30 20:57:23 Starting examples/scpog_checker/array
Sep 30 21:03:33 Finished examples/scpog_checker/array                          6m08s   2GB
Sep 30 21:03:34 Starting examples/scpog_checker/array/compilation
Sep 30 21:06:25 Finished examples/scpog_checker/array/compilation              2m50s   8GB
Sep 30 21:06:26 Starting examples/scpog_checker/array/compilation/proofs
Sep 30 21:08:17 Finished examples/scpog_checker/array/compilation/proofs       1m49s   6GB
Sep 30 21:08:18 Starting examples/pseudo_bool
Sep 30 21:10:54 Finished examples/pseudo_bool                                  2m35s   1GB
Sep 30 21:10:55 Starting examples/pseudo_bool/cnf_encoding
Sep 30 21:11:35 Finished examples/pseudo_bool/cnf_encoding                       38s   1GB
Sep 30 21:11:36 Starting examples/pseudo_bool/graph_encoding
Sep 30 21:12:26 Finished examples/pseudo_bool/graph_encoding                     49s   1GB
Sep 30 21:12:27 Starting examples/pseudo_bool/array
Sep 30 21:55:18 Finished examples/pseudo_bool/array                           42m49s  19GB
Sep 30 21:55:19 Starting examples/pseudo_bool/array/compilation
Sep 30 22:03:48 Finished examples/pseudo_bool/array/compilation                8m28s  21GB
Sep 30 22:03:49 Starting examples/pseudo_bool/array/compilation/proofs
Sep 30 22:06:38 Finished examples/pseudo_bool/array/compilation/proofs         2m47s   8GB
Sep 30 22:06:39 Starting examples/pseudo_bool/array/compilation/proofsARM8
Sep 30 22:09:30 Finished examples/pseudo_bool/array/compilation/proofsARM8     2m50s   8GB
Sep 30 22:09:31 Starting examples/pseudo_bool/cnf_encoding/array
Sep 30 22:11:57 Finished examples/pseudo_bool/cnf_encoding/array               2m24s   2GB
Sep 30 22:11:58 Starting examples/pseudo_bool/cnf_encoding/array/compilation
Sep 30 22:21:10 Finished examples/pseudo_bool/cnf_encoding/array/compilation     9m10s  21GB
Sep 30 22:21:11 Starting examples/pseudo_bool/cnf_encoding/array/compilation/proofs
Sep 30 22:24:02 Finished examples/pseudo_bool/cnf_encoding/array/compilation/proofs     2m50s   8GB
Sep 30 22:24:03 Starting examples/pseudo_bool/graph_encoding/array
Sep 30 22:28:44 Finished examples/pseudo_bool/graph_encoding/array             4m39s   3GB
Sep 30 22:28:45 Starting examples/pseudo_bool/graph_encoding/array/compilation
Sep 30 22:45:40 Finished examples/pseudo_bool/graph_encoding/array/compilation    16m53s  22GB
Sep 30 22:45:41 Starting examples/pseudo_bool/graph_encoding/array/compilation/proofs
Sep 30 22:51:15 Finished examples/pseudo_bool/graph_encoding/array/compilation/proofs     5m31s   8GB
Oct 01 02:00:07 Resuming examples/pseudo_bool/graph_encoding/array/compilation/proofs
Oct 01 02:00:14 Finished examples/pseudo_bool/graph_encoding/array/compilation/proofs        6s   1GB
Oct 01 02:00:15 Starting examples/pseudo_bool/cp_encoding
Oct 01 02:03:29 Finished examples/pseudo_bool/cp_encoding                      3m12s   1GB
Oct 01 02:03:30 Starting examples/pseudo_bool/cp_encoding/array
Oct 01 02:06:20 FAILED: examples/pseudo_bool/cp_encoding/array
  HOLORIG=/scratch/cakeml/regression3/cakeml-3558/examples/pseudo_bool/cp_encoding/array [ -d "armv8.6-asl-snapshot" ] || ./get-armv8.6-hol-snapshot
Scanning $(HOLDIR)/src/TeX
Scanning $(HOLDIR)/src/bag
Scanning $(HOLDIR)/src/sort
Scanning $(HOLDIR)/src/string
Scanning $(HOLDIR)/src/n-bit
Scanning $(HOLDIR)/src/res_quan/src
Scanning $(HOLDIR)/src/finite_maps
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/pl-semantics/lprefix_lub
Scanning $(HOLDIR)/src/integer
Scanning $(HOLDIR)/src/rational
Scanning $(HOLDIR)/src/num/theories/cv_compute/automation
Scanning $(HOLDIR)/src/algebra/base
Scanning $(HOLDIR)/src/algebra/construction
Scanning $(HOLDIR)/src/algebra
Scanning $(HOLDIR)/src/hol88
Scanning $(HOLDIR)/src/real
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/src/search
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(HOLDIR)/src/floating-point
Scanning $(HOLDIR)/src/monad/more_monads
Scanning $(HOLDIR)/src/update
Scanning $(HOLDIR)/examples/l3-machine-code/common
Scanning $(HOLDIR)/examples/l3-machine-code/lib
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/lem
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A/lib/sail
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/asl-equiv/armv8.6-asl-snapshot/A64_ISA_v86A
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/model
Scanning $(HOLDIR)/examples/machine-code/decompiler
Scanning $(HOLDIR)/examples/l3-machine-code
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/step
Scanning $(CAKEMLDIR)/basis
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/candle
Scanning $(CAKEMLDIR)/candle/prover
Scanning $(CAKEMLDIR)/candle/prover/compute
Scanning $(CAKEMLDIR)/candle/set-theory
Scanning $(CAKEMLDIR)/candle/standard
Scanning $(CAKEMLDIR)/candle/standard/ml_kernel
Scanning $(CAKEMLDIR)/candle/standard/monadic
Scanning $(CAKEMLDIR)/candle/standard/semantics
Scanning $(CAKEMLDIR)/candle/standard/syntax
Scanning $(CAKEMLDIR)/candle/standard/syntax/little_theories
Scanning $(CAKEMLDIR)/candle/syntax-lib
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/characteristic/examples
Scanning $(CAKEMLDIR)/compiler
Scanning $(CAKEMLDIR)/compiler/backend
Scanning $(CAKEMLDIR)/compiler/backend/ag32
Scanning $(CAKEMLDIR)/compiler/backend/ag32/proofs
Scanning $(CAKEMLDIR)/compiler/backend/arm7
Scanning $(CAKEMLDIR)/compiler/backend/arm7/proofs
Scanning $(CAKEMLDIR)/compiler/backend/arm8
Scanning $(CAKEMLDIR)/compiler/backend/arm8/proofs
Scanning $(CAKEMLDIR)/compiler/backend/arm8_asl
Scanning $(CAKEMLDIR)/compiler/backend/cv_compute
Scanning $(CAKEMLDIR)/compiler/backend/gc
Scanning $(CAKEMLDIR)/compiler/backend/mips
Scanning $(CAKEMLDIR)/compiler/backend/mips/proofs
Scanning $(CAKEMLDIR)/compiler/backend/pattern_matching
Scanning $(CAKEMLDIR)/compiler/backend/proofs
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/reg_alloc/proofs
Scanning $(CAKEMLDIR)/compiler/backend/riscv
Scanning $(CAKEMLDIR)/compiler/backend/riscv/proofs
Scanning $(CAKEMLDIR)/compiler/backend/semantics
Scanning $(CAKEMLDIR)/compiler/backend/serialiser
Scanning $(CAKEMLDIR)/compiler/backend/x64
Scanning $(CAKEMLDIR)/compiler/backend/x64/proofs
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/x64/64
Scanning $(CAKEMLDIR)/compiler/benchmarks/cakeml_benchmarks/cakeml
Scanning $(CAKEMLDIR)/compiler/benchmarks/mlton_benchmarks/cakeml
Scanning $(CAKEMLDIR)/compiler/benchmarks
Scanning $(CAKEMLDIR)/compiler/benchmarks/cakeml_benchmarks
Scanning $(CAKEMLDIR)/compiler/benchmarks/cakeml_benchmarks/ocaml
Scanning $(CAKEMLDIR)/compiler/benchmarks/mlton_benchmarks
Scanning $(CAKEMLDIR)/compiler/bootstrap
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/ag32
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/ag32/32
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/ag32/32/proofs
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/arm8
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/arm8/64
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/arm8/64/proofs
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64/32
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64/32/proofs
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64/64
Scanning $(CAKEMLDIR)/compiler/bootstrap/compilation/x64/64/proofs
Scanning $(CAKEMLDIR)/compiler/bootstrap/translation
Scanning $(CAKEMLDIR)/compiler/dafny
Scanning $(CAKEMLDIR)/compiler/dafny/compilation
Scanning $(CAKEMLDIR)/compiler/dafny/examples
Scanning $(CAKEMLDIR)/compiler/dafny/examples/output
Scanning $(CAKEMLDIR)/compiler/dafny/proofs
Scanning $(CAKEMLDIR)/compiler/dafny/semantics
Scanning $(CAKEMLDIR)/compiler/dafny/translation
Scanning $(CAKEMLDIR)/compiler/dafny/vcg
Scanning $(CAKEMLDIR)/compiler/dafny/vcg/examples
Scanning $(CAKEMLDIR)/compiler/encoders
Scanning $(CAKEMLDIR)/compiler/encoders/ag32
Scanning $(CAKEMLDIR)/compiler/encoders/ag32/proofs
Scanning $(HOLDIR)/examples/l3-machine-code/arm/step
Scanning $(CAKEMLDIR)/compiler/encoders/arm7
Scanning $(HOLDIR)/examples/l3-machine-code/arm/prog
Scanning $(CAKEMLDIR)/compiler/encoders/arm7/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/arm8
Scanning $(HOLDIR)/examples/l3-machine-code/arm8/prog
Scanning $(CAKEMLDIR)/compiler/encoders/arm8/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/arm8_asl
Scanning $(CAKEMLDIR)/compiler/encoders/arm8_asl/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/asm
Scanning $(HOLDIR)/examples/l3-machine-code/mips/step
Scanning $(CAKEMLDIR)/compiler/encoders/mips
Scanning $(HOLDIR)/examples/l3-machine-code/mips/prog
Scanning $(CAKEMLDIR)/compiler/encoders/mips/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/monadic_enc
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/step
Scanning $(CAKEMLDIR)/compiler/encoders/riscv
Scanning $(HOLDIR)/examples/l3-machine-code/riscv/prog
Scanning $(CAKEMLDIR)/compiler/encoders/riscv/proofs
Scanning $(CAKEMLDIR)/compiler/encoders/tests
Scanning $(HOLDIR)/examples/l3-machine-code/x64/step
Scanning $(CAKEMLDIR)/compiler/encoders/x64
Scanning $(HOLDIR)/examples/l3-machine-code/x64/prog
Scanning $(CAKEMLDIR)/compiler/encoders/x64/proofs
Scanning $(HOLDIR)/examples/algorithms/unification/triangular
Scanning $(HOLDIR)/src/transfer/examples
Scanning $(HOLDIR)/examples/algorithms/unification/triangular/first-order
Scanning $(HOLDIR)/examples/algorithms/unification/triangular/first-order/compilation
Scanning $(CAKEMLDIR)/compiler/inference
Scanning $(CAKEMLDIR)/compiler/inference/proofs
Scanning $(CAKEMLDIR)/compiler/inference/tests
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/compiler/parsing/ocaml
Scanning $(CAKEMLDIR)/compiler/parsing/proofs
Scanning $(CAKEMLDIR)/compiler/parsing/tests
Scanning $(CAKEMLDIR)/compiler/printing
Scanning $(CAKEMLDIR)/compiler/printing/test
Scanning $(CAKEMLDIR)/compiler/proofs
Scanning $(CAKEMLDIR)/compiler/repl
Scanning $(CAKEMLDIR)/compiler/scheme
Scanning $(CAKEMLDIR)/compiler/scheme/compilation
Scanning $(CAKEMLDIR)/compiler/scheme/examples
Scanning $(CAKEMLDIR)/compiler/scheme/proofs
Scanning $(CAKEMLDIR)/compiler/scheme/translation
Scanning $(CAKEMLDIR)/compiler/scheme/unverified
Scanning $(CAKEMLDIR)/cv_translator
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/developers/bin
Scanning $(HOLDIR)/examples/Crypto/AES
Scanning $(HOLDIR)/src/real/analysis
Scanning $(HOLDIR)/src/probability
Scanning $(HOLDIR)/examples/Crypto/DES
Scanning $(HOLDIR)/examples/Crypto/IDEA
Scanning $(HOLDIR)/examples/Crypto/Keccak
Scanning $(HOLDIR)/examples/Crypto/MARS
Scanning $(HOLDIR)/examples/Crypto/MD5
Scanning $(HOLDIR)/examples/Crypto/RC6
Scanning $(HOLDIR)/examples/Crypto/MD
Scanning $(HOLDIR)/examples/Crypto/RIPEMD
Scanning $(HOLDIR)/examples/Crypto/SHA-1
Scanning $(HOLDIR)/examples/Crypto/SHA-2
Scanning $(HOLDIR)/examples/Crypto/Serpent/Bitslice
Scanning $(HOLDIR)/examples/Crypto/Serpent/Reference
Scanning $(HOLDIR)/src/emit
Scanning $(HOLDIR)/examples/Crypto/TEA
Scanning $(HOLDIR)/examples/Crypto/TWOFISH
Scanning $(HOLDIR)/examples/Crypto
Scanning $(CAKEMLDIR)/examples
Scanning $(CAKEMLDIR)/examples/compilation
Scanning $(CAKEMLDIR)/examples/compilation/ag32
Scanning $(CAKEMLDIR)/examples/compilation/ag32/proofs
Scanning $(CAKEMLDIR)/examples/compilation/x64
Scanning $(CAKEMLDIR)/examples/compilation/x64/proofs
Scanning $(CAKEMLDIR)/examples/deflate
Scanning $(CAKEMLDIR)/examples/deflate/translation
Scanning $(CAKEMLDIR)/examples/deflate/translation/compilation
Scanning $(CAKEMLDIR)/examples/deflate/translation/compilation/tests
Scanning $(CAKEMLDIR)/examples/flover
Scanning $(CAKEMLDIR)/examples/flover/Infra
Scanning $(CAKEMLDIR)/examples/flover/semantics
Scanning $(CAKEMLDIR)/examples/template
Scanning $(CAKEMLDIR)/examples/template/compilation
Scanning $(CAKEMLDIR)/examples/template/translation
Scanning $(CAKEMLDIR)/examples/vipr
Scanning $(CAKEMLDIR)/examples/vipr/compilation
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/pancake
Scanning $(CAKEMLDIR)/pancake/parser
Scanning $(CAKEMLDIR)/pancake/proofs
Scanning $(CAKEMLDIR)/pancake/semantics
Scanning $(CAKEMLDIR)/pancake/static_checker
Scanning $(CAKEMLDIR)/pancake/temp
Scanning $(CAKEMLDIR)/profiler
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/semantics/alt_semantics
Scanning $(CAKEMLDIR)/semantics/alt_semantics/proofs
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/translator/monadic/examples
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/translator/okasaki-examples
Scanning $(HOLDIR)/examples/Crypto/RSA
Scanning $(HOLDIR)/examples/miller/ho_prover
Scanning $(HOLDIR)/examples/miller/subtypes
Scanning $(HOLDIR)/examples/miller/formalize
Scanning $(HOLDIR)/examples/miller/groups
Scanning $(HOLDIR)/examples/probability/legacy
Scanning $(HOLDIR)/examples/miller/prob
Scanning $(HOLDIR)/examples/miller/miller
Scanning $(CAKEMLDIR)/translator/other-examples
Scanning $(CAKEMLDIR)/translator/other-examples/auxiliary
Scanning $(CAKEMLDIR)/tutorial
Scanning $(CAKEMLDIR)/unverified
Scanning $(CAKEMLDIR)/unverified/front-end
Scanning $(CAKEMLDIR)/unverified/hol-light-syntax
Scanning $(CAKEMLDIR)/unverified/ocaml-syntax
Scanning $(CAKEMLDIR)/unverified/ocaml-syntax/lib
Scanning $(CAKEMLDIR)/unverified/ocaml-syntax/tests
Scanning $(CAKEMLDIR)/unverified/reg_alloc
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/x64
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/x64/32
Scanning $(candle_overloading)/ml_checker
Scanning $(candle_overloading)/ml_kernel
Scanning $(candle_overloading)/monadic
Scanning $(candle_overloading)/semantics
Scanning $(candle_overloading)/syntax
Scanning $(cnf)/array
Scanning $(cnf)/dist
Scanning $(cnf)/dist/array
Scanning $(cnf)/dist/array/compilation
Scanning $(cnf)/dist/array/compilation/proofs
Scanning $(cnf)/lrup
Scanning $(cnf)/lrup/array
Scanning $(cnf)/lrup/array/compilation
Scanning $(cnf)/lrup/array/compilation/proofs
Scanning $(cnf)/xlrup
Scanning $(cnf)/xlrup/array
Scanning $(cnf)/xlrup/array/compilation
Scanning $(cnf)/xlrup/array/compilation/proofs
Scanning $(lpr_checker)/array
Scanning $(lpr_checker)/array/compilation
Scanning $(lpr_checker)/array/compilation/proofs
Scanning $(lpr_checker)/array/compilation/proofsARM8
Scanning $(opentheory)/compilation
Scanning $(opentheory)/compilation/ag32
Scanning $(opentheory)/compilation/ag32/proofs
Scanning $(opentheory)/compilation/proofs
Scanning $(pseudo_bool)/array
Scanning $(pseudo_bool)/array/compilation
Scanning $(pseudo_bool)/array/compilation/proofs
Scanning $(pseudo_bool)/array/compilation/proofsARM8
Scanning $(pseudo_bool)/cnf_encoding
Scanning $(pseudo_bool)/cnf_encoding/array
Scanning $(pseudo_bool)/cnf_encoding/array/compilation
Scanning $(pseudo_bool)/cnf_encoding/array/compilation/proofs
Scanning $(pseudo_bool)/cp_encoding
Scanning $(pseudo_bool)/cp_encoding/array
Scanning $(pseudo_bool)/cp_encoding/array/compilation
Scanning $(pseudo_bool)/cp_encoding/array/compilation/proofs
Scanning $(pseudo_bool)/graph_encoding
Scanning $(pseudo_bool)/graph_encoding/array
Scanning $(pseudo_bool)/graph_encoding/array/compilation
Scanning $(pseudo_bool)/graph_encoding/array/compilation/proofs
Scanning $(sat_encodings)/case_studies
Scanning $(sat_encodings)/demo
Scanning $(sat_encodings)/translation
Scanning $(sat_encodings)/translation/compilation
Scanning $(scpog_checker)/array
Scanning $(scpog_checker)/array/compilation
Scanning $(scpog_checker)/array/compilation/proofs
Scanning $(xlrup_checker)/array
Scanning $(xlrup_checker)/array/compilation
Scanning $(xlrup_checker)/array/compilation/proofs
Scanned 302 directories
Building 1 theory file
Starting work on README.md
Starting work on cpProgTheory
README.md                                                   (0s)             OK
cpProgTheory                                              (153s)        FAIL<1>
*** Holmake aborted - 1 target failed:
*** cpProgTheory (status 1)
 Adding nsLookup representation thms for [cpProg_env_185, cpProg_env_184]
 Saved theorem _______ "nsLookup_cpProg_env_186_pfun_eqs"
 Saved theorem _______ "numint_v_thm"
 Translating numset_to_intlist
 Adding nsLookup representation thms for [cpProg_env_186]
 Saved theorem _______ "nsLookup_cpProg_env_187_pfun_eqs"
 Saved theorem _______ "numset_to_intlist_v_thm"
 Translating union_1
 Saved theorem _______ "nsLookup_cpProg_env_188_pfun_eqs"
 Adding nsLookup representation thms for [cpProg_env_187]
 Adding nsLookup representation thms for [cpProg_env_188]
 Saved theorem _______ "union_1_v_thm"
 Translating domlist
 Saved theorem _______ "nsLookup_cpProg_env_189_pfun_eqs"
 
 WARNING: domlist has a precondition.
 
 Saved theorem _______ "domlist_v_thm"
 Saved theorem _______ "domlist_side"
 Updating domlist_v_thm
 Saved theorem _______ "domlist_v_thm"
 Translating union_dom
 Adding nsLookup representation thms for [cpProg_env_189]
 Saved theorem _______ "nsLookup_cpProg_env_190_pfun_eqs"
 Saved theorem _______ "union_dom_v_thm"
 Translating lookup_int
 Adding nsLookup representation thms for [cpProg_env_190]
 Saved theorem _______ "nsLookup_cpProg_env_191_pfun_eqs"
 Saved theorem _______ "lookup_int_v_thm"
 Translating insert_int
 Adding nsLookup representation thms for [cpProg_env_191]
 Saved theorem _______ "nsLookup_cpProg_env_192_pfun_eqs"
 Saved theorem _______ "insert_int_v_thm"
 Translating fast_compare
 Adding nsLookup representation thms for [cpProg_env_192]
 Saved theorem _______ "nsLookup_cpProg_env_193_pfun_eqs"
 Saved theorem _______ "fast_compare_v_thm"
 
 
 Cannot translate term:  fast_compare
 
 
 which has type:
 
 :mlstring -> mlstring -> ordering
 
 Failed translation: varc_compare
 error in quse /scratch/cakeml/regression3/cakeml-3558/examples/pseudo_bool/cp_encoding/array/cpProgScript.sml : UnableToTranslate ?
 error in load /scratch/cakeml/regression3/cakeml-3558/examples/pseudo_bool/cp_encoding/array/cpProgScript : UnableToTranslate ?
 Uncaught exception at /scratch/cakeml/regression3/cakeml-3558/translator/ml_translatorLib.sml:4629: UnableToTranslate ?
 Full log: /scratch/cakeml/regression3/cakeml-3558/examples/pseudo_bool/cp_encoding/array/.hol/logs/cpProgTheory