Job 3566

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

Oct 01 07:15:37 Claimed job
Oct 01 07:15:41 Reusing HOL
Oct 01 07:15:50 Starting developers
Oct 01 07:16:41 Finished developers                                              50s   1GB
Oct 01 07:16:42 Starting developers/bin
Oct 01 07:16:52 Finished developers/bin                                           8s   1GB
Oct 01 07:16:53 Starting misc
Oct 01 07:17:39 Finished misc                                                    45s   1GB
Oct 01 07:17:40 Starting compiler/proofs
Oct 01 08:39:44 Finished compiler/proofs                                    1h22m01s  10GB
Oct 01 08:39:45 Starting compiler/bootstrap/compilation/x64/64/proofs
Oct 01 15:58:15 Finished compiler/bootstrap/compilation/x64/64/proofs       7h18m28s  83GB
Oct 01 15:58:16 Starting semantics/ffi
Oct 01 15:58:39 Finished semantics/ffi                                           22s   1GB
Oct 01 15:58:40 Starting semantics
Oct 01 15:58:47 Finished semantics                                                6s   1GB
Oct 01 15:58:48 Starting semantics/proofs
Oct 01 15:59:19 Finished semantics/proofs                                        29s   1GB
Oct 01 15:59:20 Starting semantics/alt_semantics
Oct 01 15:59:43 Finished semantics/alt_semantics                                 22s   1GB
Oct 01 15:59:44 Starting semantics/alt_semantics/proofs
Oct 01 16:03:54 Finished semantics/alt_semantics/proofs                        4m09s   1GB
Oct 01 16:03:55 Starting basis/pure
Oct 01 16:04:03 Finished basis/pure                                               6s   1GB
Oct 01 16:04:04 Starting translator
Oct 01 16:05:23 Finished translator                                            1m18s   2GB
Oct 01 16:05:24 Starting compiler/parsing
Oct 01 16:06:18 Finished compiler/parsing                                        53s   2GB
Oct 01 16:06:19 Starting characteristic
Oct 01 16:06:26 Finished characteristic                                           6s   1GB
Oct 01 16:06:27 Starting translator/monadic
Oct 01 16:06:35 Finished translator/monadic                                       6s   1GB
Oct 01 16:06:36 Starting translator/monadic/monad_base
Oct 01 16:06:42 Finished translator/monadic/monad_base                            5s   1GB
Oct 01 16:06:43 Starting profiler
Oct 01 16:07:21 Finished profiler                                                36s   1GB
Oct 01 16:07:22 Starting basis
Oct 01 16:09:17 Finished basis                                                 1m54s   4GB
Oct 01 16:09:18 Starting compiler
Oct 01 16:09:25 Finished compiler                                                 5s   1GB
Oct 01 16:09:26 Starting compiler/inference
Oct 01 16:09:33 Finished compiler/inference                                       5s   1GB
Oct 01 16:09:34 Starting compiler/backend/reg_alloc
Oct 01 16:09:41 Finished compiler/backend/reg_alloc                               5s   1GB
Oct 01 16:09:42 Starting compiler/backend/gc
Oct 01 16:09:49 Finished compiler/backend/gc                                      6s   1GB
Oct 01 16:09:50 Starting compiler/backend
Oct 01 16:10:00 Finished compiler/backend                                         9s   1GB
Oct 01 16:10:01 Starting compiler/encoders/asm
Oct 01 16:10:08 Finished compiler/encoders/asm                                    5s   1GB
Oct 01 16:10:09 Starting compiler/encoders/x64
Oct 01 16:10:16 Finished compiler/encoders/x64                                    5s   1GB
Oct 01 16:10:17 Starting compiler/encoders/arm7
Oct 01 16:10:23 Finished compiler/encoders/arm7                                   5s   1GB
Oct 01 16:10:24 Starting compiler/encoders/arm8
Oct 01 16:10:31 Finished compiler/encoders/arm8                                   5s   1GB
Oct 01 16:10:32 Starting compiler/encoders/arm8_asl
Oct 01 16:10:54 Finished compiler/encoders/arm8_asl                              21s   1GB
Oct 01 16:10:55 Starting compiler/encoders/mips
Oct 01 16:11:02 Finished compiler/encoders/mips                                   6s   1GB
Oct 01 16:11:03 Starting compiler/encoders/riscv
Oct 01 16:11:10 Finished compiler/encoders/riscv                                  5s   1GB
Oct 01 16:11:11 Starting compiler/encoders/ag32
Oct 01 16:11:18 Finished compiler/encoders/ag32                                   5s   1GB
Oct 01 16:11:19 Starting compiler/encoders/tests
Oct 01 16:11:26 Finished compiler/encoders/tests                                  6s   1GB
Oct 01 16:11:27 Starting compiler/encoders/monadic_enc
Oct 01 16:11:54 Finished compiler/encoders/monadic_enc                           26s   1GB
Oct 01 16:11:55 Starting compiler/backend/x64
Oct 01 16:12:02 Finished compiler/backend/x64                                     5s   1GB
Oct 01 16:12:03 Starting compiler/backend/arm7
Oct 01 16:12:10 Finished compiler/backend/arm7                                    5s   1GB
Oct 01 16:12:11 Starting compiler/backend/arm8
Oct 01 16:12:18 Finished compiler/backend/arm8                                    5s   1GB
Oct 01 16:12:19 Starting compiler/backend/mips
Oct 01 16:12:26 Finished compiler/backend/mips                                    5s   1GB
Oct 01 16:12:27 Starting compiler/backend/riscv
Oct 01 16:12:34 Finished compiler/backend/riscv                                   5s   1GB
Oct 01 16:12:35 Starting compiler/backend/ag32
Oct 01 16:13:45 Finished compiler/backend/ag32                                 1m09s   1GB
Oct 01 16:13:46 Starting compiler/backend/pattern_matching
Oct 01 16:14:08 Finished compiler/backend/pattern_matching                       20s   1GB
Oct 01 16:14:09 Starting compiler/parsing/ocaml
Oct 01 16:16:40 Finished compiler/parsing/ocaml                                2m29s   1GB
Oct 01 16:16:41 Starting compiler/printing
Oct 01 16:17:42 Finished compiler/printing                                     1m00s   1GB
Oct 01 16:17:43 Starting compiler/parsing/proofs
Oct 01 16:17:50 Finished compiler/parsing/proofs                                  6s   1GB
Oct 01 16:17:51 Starting compiler/inference/proofs
Oct 01 16:17:58 Finished compiler/inference/proofs                                5s   1GB
Oct 01 16:17:59 Starting compiler/backend/semantics
Oct 01 16:21:22 Finished compiler/backend/semantics                            3m21s   3GB
Oct 01 16:21:23 Starting compiler/backend/reg_alloc/proofs
Oct 01 16:21:30 Finished compiler/backend/reg_alloc/proofs                        6s   1GB
Oct 01 16:21:31 Starting compiler/backend/proofs
Oct 01 16:22:23 Finished compiler/backend/proofs                                 51s   2GB
Oct 01 16:22:24 Starting compiler/backend/serialiser
Oct 01 16:22:31 Finished compiler/backend/serialiser                              6s   1GB
Oct 01 16:22:32 Starting compiler/encoders/x64/proofs
Oct 01 16:22:39 Finished compiler/encoders/x64/proofs                             5s   1GB
Oct 01 16:22:40 Starting compiler/encoders/arm7/proofs
Oct 01 16:35:20 Finished compiler/encoders/arm7/proofs                        12m38s   5GB
Oct 01 16:35:21 Starting compiler/encoders/arm8/proofs
Oct 01 16:44:02 Finished compiler/encoders/arm8/proofs                         8m40s   3GB
Oct 01 16:44:03 Starting compiler/encoders/arm8_asl/proofs
Oct 01 17:02:05 Finished compiler/encoders/arm8_asl/proofs                    18m01s   3GB
Oct 01 17:02:06 Starting compiler/encoders/mips/proofs
Oct 01 17:13:12 Finished compiler/encoders/mips/proofs                        11m05s   8GB
Oct 01 17:13:13 Starting compiler/encoders/riscv/proofs
Oct 01 17:23:35 Finished compiler/encoders/riscv/proofs                       10m20s   4GB
Oct 01 17:23:36 Starting compiler/encoders/ag32/proofs
Oct 01 17:27:04 Finished compiler/encoders/ag32/proofs                         3m26s   1GB
Oct 01 17:27:05 Starting compiler/backend/x64/proofs
Oct 01 17:27:12 Finished compiler/backend/x64/proofs                              6s   1GB
Oct 01 17:27:13 Starting compiler/backend/arm7/proofs
Oct 01 17:28:02 Finished compiler/backend/arm7/proofs                            48s   2GB
Oct 01 17:28:03 Starting compiler/backend/arm8/proofs
Oct 01 17:28:51 Finished compiler/backend/arm8/proofs                            46s   2GB
Oct 01 17:28:52 Starting compiler/backend/arm8_asl
Oct 01 17:29:38 Finished compiler/backend/arm8_asl                               45s   2GB
Oct 01 17:29:39 Starting compiler/backend/mips/proofs
Oct 01 17:30:27 Finished compiler/backend/mips/proofs                            47s   2GB
Oct 01 17:30:28 Starting compiler/backend/riscv/proofs
Oct 01 17:31:15 Finished compiler/backend/riscv/proofs                           46s   2GB
Oct 01 17:31:16 Starting compiler/backend/ag32/proofs
Oct 01 17:41:08 Finished compiler/backend/ag32/proofs                          9m51s   4GB
Oct 01 17:41:09 Starting compiler/backend/cv_compute
Oct 01 17:41:46 Finished compiler/backend/cv_compute                             35s   1GB
Oct 01 17:41:47 Starting cv_translator
Oct 01 17:47:12 Finished cv_translator                                         5m24s   3GB
Oct 01 17:47:13 Starting candle
Oct 01 17:47:20 Finished candle                                                   6s   1GB
Oct 01 17:47:21 Starting candle/set-theory
Oct 01 17:47:44 Finished candle/set-theory                                       21s   1GB
Oct 01 17:47:45 Starting candle/syntax-lib
Oct 01 17:47:52 Finished candle/syntax-lib                                        6s   1GB
Oct 01 17:47:53 Starting candle/standard
Oct 01 17:48:00 Finished candle/standard                                          6s   1GB
Oct 01 17:48:01 Starting candle/standard/syntax
Oct 01 17:48:22 Finished candle/standard/syntax                                  19s   1GB
Oct 01 17:48:23 Starting candle/standard/syntax/little_theories
Oct 01 17:49:46 Finished candle/standard/syntax/little_theories                1m22s   1GB
Oct 01 17:49:47 Starting candle/standard/semantics
Oct 01 17:49:54 Finished candle/standard/semantics                                6s   1GB
Oct 01 17:49:55 Starting candle/standard/monadic
Oct 01 17:50:02 Finished candle/standard/monadic                                  6s   1GB
Oct 01 17:50:03 Starting candle/standard/ml_kernel
Oct 01 17:52:24 Finished candle/standard/ml_kernel                             2m19s   5GB
Oct 01 17:52:25 Starting candle/overloading
Oct 01 17:52:32 Finished candle/overloading                                       6s   1GB
Oct 01 17:52:33 Starting candle/overloading/syntax
Oct 01 17:55:47 Finished candle/overloading/syntax                             3m13s   2GB
Oct 01 17:55:48 Starting candle/overloading/semantics
Oct 01 18:05:40 Finished candle/overloading/semantics                          9m50s   7GB
Oct 01 18:05:40 Starting candle/overloading/monadic
Oct 01 18:07:55 Finished candle/overloading/monadic                            2m13s   1GB
Oct 01 18:07:56 Starting candle/overloading/ml_kernel
Oct 01 18:15:28 Finished candle/overloading/ml_kernel                          7m31s   6GB
Oct 01 18:15:29 Starting candle/overloading/ml_checker
Oct 01 18:18:31 Finished candle/overloading/ml_checker                         3m00s   6GB
Oct 01 18:18:32 Starting candle/prover
Oct 01 18:18:39 Finished candle/prover                                            6s   1GB
Oct 01 18:18:40 Starting candle/prover/compute
Oct 01 18:18:47 Finished candle/prover/compute                                    6s   1GB
Oct 01 18:18:48 Starting pancake
Oct 01 18:18:55 Finished pancake                                                  6s   1GB
Oct 01 18:18:56 Starting pancake/semantics
Oct 01 18:22:21 Finished pancake/semantics                                     3m23s   2GB
Oct 01 18:22:22 Starting pancake/parser
Oct 01 18:23:11 Finished pancake/parser                                          48s   1GB
Oct 01 18:23:12 Starting pancake/static_checker
Oct 01 18:25:57 Finished pancake/static_checker                                2m44s   1GB
Oct 01 18:25:58 Starting pancake/proofs
Oct 01 18:43:00 Finished pancake/proofs                                       17m00s   6GB
Oct 01 18:43:01 Starting compiler/dafny
Oct 01 18:43:30 Finished compiler/dafny                                          28s   1GB
Oct 01 18:43:31 Starting compiler/dafny/translation
Oct 01 18:54:47 Finished compiler/dafny/translation                           11m14s   6GB
Oct 01 18:54:48 Starting compiler/dafny/compilation
Oct 01 18:57:10 Finished compiler/dafny/compilation                            2m20s   6GB
Oct 01 18:57:11 Starting compiler/dafny/semantics
Oct 01 18:57:55 Finished compiler/dafny/semantics                                43s   1GB
Oct 01 18:57:56 Starting compiler/dafny/proofs
Oct 01 18:59:42 Finished compiler/dafny/proofs                                 1m45s   1GB
Oct 01 18:59:43 Starting compiler/dafny/vcg
Oct 01 18:59:51 Finished compiler/dafny/vcg                                       6s   1GB
Oct 01 18:59:52 Starting compiler/dafny/vcg/examples
Oct 01 19:00:28 Finished compiler/dafny/vcg/examples                             35s   2GB
Oct 01 19:00:29 Starting compiler/scheme
Oct 01 19:01:02 Finished compiler/scheme                                         31s   1GB
Oct 01 19:01:03 Starting compiler/scheme/translation
Oct 01 19:08:17 Finished compiler/scheme/translation                           7m13s   7GB
Oct 01 19:08:18 Starting compiler/scheme/compilation
Oct 01 19:10:06 Finished compiler/scheme/compilation                           1m47s   5GB
Oct 01 19:10:07 Starting compiler/scheme/proofs
Oct 01 19:17:18 Finished compiler/scheme/proofs                                7m09s   2GB
Oct 01 19:17:18 Starting characteristic/examples
Oct 01 19:19:01 Finished characteristic/examples                               1m41s   5GB
Oct 01 19:19:02 Starting tutorial
Oct 01 19:19:09 Finished tutorial                                                 6s   1GB
Oct 01 19:19:10 Starting tutorial/solutions
Oct 01 19:22:08 Finished tutorial/solutions                                    2m57s   3GB
Oct 01 19:22:09 Starting translator/monadic/examples
Oct 01 19:25:30 Finished translator/monadic/examples                           3m20s   4GB
Oct 01 19:25:31 Starting examples
Oct 01 19:29:59 Finished examples                                              4m26s   5GB
Oct 01 19:30:00 Starting examples/compilation
Oct 01 19:30:08 Finished examples/compilation                                     6s   1GB
Oct 01 19:30:09 Starting examples/compilation/x64
Oct 01 19:39:33 Finished examples/compilation/x64                              9m23s   4GB
Oct 01 19:39:34 Starting examples/compilation/x64/proofs
Oct 01 19:43:30 Finished examples/compilation/x64/proofs                       3m54s   4GB
Oct 01 19:43:31 Starting examples/compilation/ag32
Oct 01 19:46:20 Finished examples/compilation/ag32                             2m47s   3GB
Oct 01 19:46:21 Starting examples/compilation/ag32/proofs
Oct 01 19:47:51 Finished examples/compilation/ag32/proofs                      1m29s   5GB
Oct 01 19:47:52 Starting examples/lpr_checker
Oct 01 19:48:37 Finished examples/lpr_checker                                    43s   1GB
Oct 01 19:48:38 Starting examples/lpr_checker/array
Oct 01 20:02:04 Finished examples/lpr_checker/array                           13m24s   6GB
Oct 01 20:02:05 Starting examples/lpr_checker/array/compilation
Oct 01 20:05:59 Finished examples/lpr_checker/array/compilation                3m53s   7GB
Oct 01 20:06:00 Starting examples/lpr_checker/array/compilation/proofs
Oct 01 20:07:48 Finished examples/lpr_checker/array/compilation/proofs         1m47s   6GB
Oct 01 20:07:49 Starting examples/lpr_checker/array/compilation/proofsARM8
Oct 01 20:09:49 Finished examples/lpr_checker/array/compilation/proofsARM8     1m58s   6GB
Oct 01 20:09:49 Starting .
Oct 01 20:09:57 Finished .                                                        6s   1GB
Oct 01 20:09:58 Starting examples/xlrup_checker
Oct 01 20:10:56 Finished examples/xlrup_checker                                  57s   1GB
Oct 01 20:10:57 Starting examples/xlrup_checker/array
Oct 01 20:20:47 Finished examples/xlrup_checker/array                          9m48s   2GB
Oct 01 20:20:48 Starting examples/xlrup_checker/array/compilation
Oct 01 20:22:29 Finished examples/xlrup_checker/array/compilation              1m39s   5GB
Oct 01 20:22:30 Starting examples/xlrup_checker/array/compilation/proofs
Oct 01 20:24:08 Finished examples/xlrup_checker/array/compilation/proofs       1m36s   5GB
Oct 01 20:24:09 Starting examples/cnf
Oct 01 20:24:43 Finished examples/cnf                                            33s   1GB
Oct 01 20:24:44 Starting examples/cnf/array
Oct 01 20:28:02 Finished examples/cnf/array                                    3m17s   2GB
Oct 01 20:28:03 Starting examples/cnf/dist
Oct 01 20:28:16 Finished examples/cnf/dist                                       10s   1GB
Oct 01 20:28:17 Starting examples/cnf/dist/array
Oct 01 20:32:54 Finished examples/cnf/dist/array                               4m35s   2GB
Oct 01 20:32:55 Starting examples/cnf/dist/array/compilation
Oct 01 20:34:00 Finished examples/cnf/dist/array/compilation                   1m04s   3GB
Oct 01 20:34:01 Starting examples/cnf/dist/array/compilation/proofs
Oct 01 20:35:30 Finished examples/cnf/dist/array/compilation/proofs            1m25s   3GB
Oct 01 20:35:31 Starting examples/cnf/lrup
Oct 01 20:35:44 Finished examples/cnf/lrup                                       11s   1GB
Oct 01 20:35:45 Starting examples/cnf/lrup/array
Oct 01 20:39:02 Finished examples/cnf/lrup/array                               3m16s   1GB
Oct 01 20:39:03 Starting examples/cnf/lrup/array/compilation
Oct 01 20:40:28 Finished examples/cnf/lrup/array/compilation                   1m24s   4GB
Oct 01 20:40:29 Starting examples/cnf/lrup/array/compilation/proofs
Oct 01 20:42:01 Finished examples/cnf/lrup/array/compilation/proofs            1m30s   4GB
Oct 01 20:42:02 Starting examples/cnf/xlrup
Oct 01 20:42:45 Finished examples/cnf/xlrup                                      42s   1GB
Oct 01 20:42:46 Starting examples/cnf/xlrup/array
Oct 01 20:50:40 Finished examples/cnf/xlrup/array                              7m53s   3GB
Oct 01 20:50:41 Starting examples/cnf/xlrup/array/compilation
Oct 01 20:52:18 Finished examples/cnf/xlrup/array/compilation                  1m35s   5GB
Oct 01 20:52:19 Starting examples/cnf/xlrup/array/compilation/proofs
Oct 01 20:53:53 Finished examples/cnf/xlrup/array/compilation/proofs           1m33s   4GB
Oct 01 20:53:54 Starting examples/scpog_checker
Oct 01 20:54:50 Finished examples/scpog_checker                                  55s   1GB
Oct 01 20:54:51 Starting examples/scpog_checker/array
Oct 01 21:01:01 Finished examples/scpog_checker/array                          6m09s   2GB
Oct 01 21:01:02 Starting examples/scpog_checker/array/compilation
Oct 01 21:03:58 Finished examples/scpog_checker/array/compilation              2m54s   8GB
Oct 01 21:03:59 Starting examples/scpog_checker/array/compilation/proofs
Oct 01 21:05:50 Finished examples/scpog_checker/array/compilation/proofs       1m50s   6GB
Oct 01 21:05:51 Starting examples/pseudo_bool
Oct 01 21:08:26 Finished examples/pseudo_bool                                  2m33s   1GB
Oct 01 21:08:27 Starting examples/pseudo_bool/cnf_encoding
Oct 01 21:09:06 Finished examples/pseudo_bool/cnf_encoding                       37s   1GB
Oct 01 21:09:07 Starting examples/pseudo_bool/graph_encoding
Oct 01 21:09:59 Finished examples/pseudo_bool/graph_encoding                     51s   1GB
Oct 01 21:10:00 Starting examples/pseudo_bool/array
Oct 01 21:52:39 Finished examples/pseudo_bool/array                           42m38s  17GB
Oct 01 21:52:40 Starting examples/pseudo_bool/array/compilation
Oct 01 22:01:11 Finished examples/pseudo_bool/array/compilation                8m30s  20GB
Oct 01 22:01:12 Starting examples/pseudo_bool/array/compilation/proofs
Oct 01 22:04:06 Finished examples/pseudo_bool/array/compilation/proofs         2m53s   7GB
Oct 01 22:04:07 Starting examples/pseudo_bool/array/compilation/proofsARM8
Oct 01 22:07:10 Finished examples/pseudo_bool/array/compilation/proofsARM8     3m01s   7GB
Oct 01 22:07:11 Starting examples/pseudo_bool/cnf_encoding/array
Oct 01 22:09:43 Finished examples/pseudo_bool/cnf_encoding/array               2m31s   3GB
Oct 01 22:09:44 Starting examples/pseudo_bool/cnf_encoding/array/compilation
Oct 01 22:18:17 Finished examples/pseudo_bool/cnf_encoding/array/compilation     8m31s  21GB
Oct 01 22:18:18 Starting examples/pseudo_bool/cnf_encoding/array/compilation/proofs
Oct 01 22:21:10 Finished examples/pseudo_bool/cnf_encoding/array/compilation/proofs     2m51s   8GB
Oct 01 22:21:11 Starting examples/pseudo_bool/graph_encoding/array
Oct 01 22:26:01 Finished examples/pseudo_bool/graph_encoding/array             4m48s   3GB
Oct 01 22:26:01 Starting examples/pseudo_bool/graph_encoding/array/compilation
Oct 01 22:43:00 Finished examples/pseudo_bool/graph_encoding/array/compilation    16m57s  23GB
Oct 01 22:43:01 Starting examples/pseudo_bool/graph_encoding/array/compilation/proofs
Oct 01 22:48:38 Finished examples/pseudo_bool/graph_encoding/array/compilation/proofs     5m35s   9GB
Oct 01 22:48:39 Starting examples/pseudo_bool/cp_encoding
Oct 01 22:51:59 Finished examples/pseudo_bool/cp_encoding                      3m18s   1GB
Oct 01 22:52:00 Starting examples/pseudo_bool/cp_encoding/array
Oct 01 22:54:58 FAILED: examples/pseudo_bool/cp_encoding/array
  HOLORIG=/scratch/cakeml/regression3/cakeml-3566/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                                              (162s)        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-3566/examples/pseudo_bool/cp_encoding/array/cpProgScript.sml : UnableToTranslate ?
 error in load /scratch/cakeml/regression3/cakeml-3566/examples/pseudo_bool/cp_encoding/array/cpProgScript : UnableToTranslate ?
 Uncaught exception at /scratch/cakeml/regression3/cakeml-3566/translator/ml_translatorLib.sml:4629: UnableToTranslate ?
 Full log: /scratch/cakeml/regression3/cakeml-3566/examples/pseudo_bool/cp_encoding/array/.hol/logs/cpProgTheory