Job 3628

CakeML:1568ac3d52f076d85369e4b0ece8fd3e0fc6d2c8
  Fix for new dom in grammar [Oct 19 12:34:28]
#1551 (index-arith)
Merging into:8df351c7c49bea09861851370b39f79c903ce80e
  Simplify the AST's S-expression representation/parsing (#1550) [Oct 18 13:48:49]
HOL:652d1f0aad5cd537ed1e5d470ba3444e70ba470e
  Merge remote-tracking branch 'origin/master' into develop [Sep 27 02:14:15]
Machine:fairybread

Oct 19 13:02:48 Claimed job
Oct 19 13:02:54 Reusing HOL
Oct 19 13:03:03 Starting developers
Oct 19 13:04:01 Finished developers                                              57s   1GB
Oct 19 13:04:02 Starting developers/bin
Oct 19 13:04:12 Finished developers/bin                                           8s   1GB
Oct 19 13:04:13 Starting misc
Oct 19 13:04:59 Finished misc                                                    45s   1GB
Oct 19 13:05:00 Starting compiler/proofs
Oct 19 14:34:58 Finished compiler/proofs                                    1h29m56s  12GB
Oct 19 14:34:59 Starting compiler/bootstrap/compilation/x64/64/proofs
Oct 19 20:43:56 Finished compiler/bootstrap/compilation/x64/64/proofs       6h08m56s 109GB
Oct 19 20:43:57 Starting semantics/ffi
Oct 19 20:44:21 Finished semantics/ffi                                           22s   1GB
Oct 19 20:44:22 Starting semantics
Oct 19 20:44:30 Finished semantics                                                6s   1GB
Oct 19 20:44:30 Starting semantics/proofs
Oct 19 20:45:03 Finished semantics/proofs                                        31s   1GB
Oct 19 20:45:04 Starting semantics/alt_semantics
Oct 19 20:45:27 Finished semantics/alt_semantics                                 22s   1GB
Oct 19 20:45:28 Starting semantics/alt_semantics/proofs
Oct 19 20:49:54 Finished semantics/alt_semantics/proofs                        4m24s   2GB
Oct 19 20:49:55 Starting basis/pure
Oct 19 20:50:03 Finished basis/pure                                               7s   1GB
Oct 19 20:50:04 Starting translator
Oct 19 20:51:24 Finished translator                                            1m18s   2GB
Oct 19 20:51:25 Starting compiler/parsing
Oct 19 20:52:18 Finished compiler/parsing                                        52s   2GB
Oct 19 20:52:19 Starting characteristic
Oct 19 20:52:26 Finished characteristic                                           6s   1GB
Oct 19 20:52:27 Starting translator/monadic
Oct 19 20:52:35 Finished translator/monadic                                       6s   1GB
Oct 19 20:52:36 Starting translator/monadic/monad_base
Oct 19 20:52:43 Finished translator/monadic/monad_base                            6s   1GB
Oct 19 20:52:44 Starting profiler
Oct 19 20:53:23 Finished profiler                                                38s   1GB
Oct 19 20:53:24 Starting basis
Oct 19 20:55:51 Finished basis                                                 2m25s   5GB
Oct 19 20:55:52 Starting compiler
Oct 19 20:56:00 Finished compiler                                                 6s   1GB
Oct 19 20:56:01 Starting compiler/inference
Oct 19 20:56:08 Finished compiler/inference                                       6s   1GB
Oct 19 20:56:09 Starting compiler/backend/reg_alloc
Oct 19 20:56:17 Finished compiler/backend/reg_alloc                               6s   1GB
Oct 19 20:56:18 Starting compiler/backend/gc
Oct 19 20:56:25 Finished compiler/backend/gc                                      6s   1GB
Oct 19 20:56:26 Starting compiler/backend
Oct 19 20:56:38 Finished compiler/backend                                        10s   1GB
Oct 19 20:56:39 Starting compiler/backend/tests
Oct 19 20:57:15 Finished compiler/backend/tests                                  35s   1GB
Oct 19 20:57:16 Starting compiler/encoders/asm
Oct 19 20:57:24 Finished compiler/encoders/asm                                    6s   1GB
Oct 19 20:57:25 Starting compiler/encoders/x64
Oct 19 20:57:33 Finished compiler/encoders/x64                                    6s   1GB
Oct 19 20:57:34 Starting compiler/encoders/arm7
Oct 19 20:57:41 Finished compiler/encoders/arm7                                   6s   1GB
Oct 19 20:57:42 Starting compiler/encoders/arm8
Oct 19 20:57:50 Finished compiler/encoders/arm8                                   6s   1GB
Oct 19 20:57:51 Starting compiler/encoders/arm8_asl
Oct 19 20:58:14 Finished compiler/encoders/arm8_asl                              22s   1GB
Oct 19 20:58:15 Starting compiler/encoders/mips
Oct 19 20:58:23 Finished compiler/encoders/mips                                   6s   1GB
Oct 19 20:58:24 Starting compiler/encoders/riscv
Oct 19 20:58:31 Finished compiler/encoders/riscv                                  6s   1GB
Oct 19 20:58:32 Starting compiler/encoders/ag32
Oct 19 20:58:40 Finished compiler/encoders/ag32                                   6s   1GB
Oct 19 20:58:41 Starting compiler/encoders/tests
Oct 19 20:59:25 Finished compiler/encoders/tests                                 43s   1GB
Oct 19 20:59:26 Starting compiler/encoders/monadic_enc
Oct 19 20:59:53 Finished compiler/encoders/monadic_enc                           25s   1GB
Oct 19 20:59:54 Starting compiler/backend/x64
Oct 19 21:00:01 Finished compiler/backend/x64                                     6s   1GB
Oct 19 21:00:02 Starting compiler/backend/arm7
Oct 19 21:00:10 Finished compiler/backend/arm7                                    6s   1GB
Oct 19 21:00:11 Starting compiler/backend/arm8
Oct 19 21:00:18 Finished compiler/backend/arm8                                    6s   1GB
Oct 19 21:00:19 Starting compiler/backend/mips
Oct 19 21:00:27 Finished compiler/backend/mips                                    6s   1GB
Oct 19 21:00:28 Starting compiler/backend/riscv
Oct 19 21:00:35 Finished compiler/backend/riscv                                   6s   1GB
Oct 19 21:00:36 Starting compiler/backend/ag32
Oct 19 21:01:47 Finished compiler/backend/ag32                                 1m09s   1GB
Oct 19 21:01:48 Starting compiler/backend/pattern_matching
Oct 19 21:02:10 Finished compiler/backend/pattern_matching                       21s   1GB
Oct 19 21:02:11 Starting compiler/printing
Oct 19 21:03:10 Finished compiler/printing                                       57s   1GB
Oct 19 21:03:11 Starting compiler/parsing/proofs
Oct 19 21:03:18 Finished compiler/parsing/proofs                                  6s   1GB
Oct 19 21:03:19 Starting compiler/inference/proofs
Oct 19 21:03:27 Finished compiler/inference/proofs                                6s   1GB
Oct 19 21:03:28 Starting compiler/backend/semantics
Oct 19 21:06:10 Finished compiler/backend/semantics                            2m41s   1GB
Oct 19 21:06:11 Starting compiler/backend/reg_alloc/proofs
Oct 19 21:06:19 Finished compiler/backend/reg_alloc/proofs                        6s   1GB
Oct 19 21:06:20 Starting compiler/backend/proofs
Oct 19 21:07:13 Finished compiler/backend/proofs                                 52s   2GB
Oct 19 21:07:14 Starting compiler/backend/serialiser
Oct 19 21:07:22 Finished compiler/backend/serialiser                              6s   1GB
Oct 19 21:07:23 Starting compiler/encoders/x64/proofs
Oct 19 21:07:30 Finished compiler/encoders/x64/proofs                             6s   1GB
Oct 19 21:07:31 Starting compiler/encoders/arm7/proofs
Oct 19 21:20:58 Finished compiler/encoders/arm7/proofs                        13m25s   9GB
Oct 19 21:20:59 Starting compiler/encoders/arm8/proofs
Oct 19 21:33:37 Finished compiler/encoders/arm8/proofs                        12m37s  15GB
Oct 19 21:33:38 Starting compiler/encoders/arm8_asl/proofs
Oct 19 22:02:22 Finished compiler/encoders/arm8_asl/proofs                    28m42s  34GB
Oct 19 22:02:23 Starting compiler/encoders/mips/proofs
Oct 19 22:14:18 Finished compiler/encoders/mips/proofs                        11m54s   5GB
Oct 19 22:14:19 Starting compiler/encoders/riscv/proofs
Oct 19 22:24:27 Finished compiler/encoders/riscv/proofs                       10m07s   4GB
Oct 19 22:24:28 Starting compiler/encoders/ag32/proofs
Oct 19 22:27:59 Finished compiler/encoders/ag32/proofs                         3m29s   2GB
Oct 19 22:28:00 Starting compiler/backend/x64/proofs
Oct 19 22:28:07 Finished compiler/backend/x64/proofs                              6s   1GB
Oct 19 22:28:08 Starting compiler/backend/arm7/proofs
Oct 19 22:28:59 Finished compiler/backend/arm7/proofs                            49s   2GB
Oct 19 22:29:00 Starting compiler/backend/arm8/proofs
Oct 19 22:29:49 Finished compiler/backend/arm8/proofs                            48s   2GB
Oct 19 22:29:50 Starting compiler/backend/arm8_asl
Oct 19 22:30:36 Finished compiler/backend/arm8_asl                               45s   2GB
Oct 19 22:30:37 Starting compiler/backend/mips/proofs
Oct 19 22:31:26 Finished compiler/backend/mips/proofs                            48s   2GB
Oct 19 22:31:27 Starting compiler/backend/riscv/proofs
Oct 19 22:32:13 Finished compiler/backend/riscv/proofs                           45s   2GB
Oct 19 22:32:14 Starting compiler/backend/San
Oct 19 22:33:29 Finished compiler/backend/San                                  1m13s   4GB
Oct 19 22:33:30 Starting compiler/backend/ag32/proofs
Oct 19 22:43:29 Finished compiler/backend/ag32/proofs                          9m58s   5GB
Oct 19 22:43:30 Starting compiler/backend/cv_compute
Oct 19 22:44:08 Finished compiler/backend/cv_compute                             36s   1GB
Oct 19 22:44:09 Starting cv_translator
Oct 19 22:47:15 Finished cv_translator                                         3m04s   3GB
Oct 19 22:47:16 Starting candle
Oct 19 22:47:24 Finished candle                                                   7s   1GB
Oct 19 22:47:25 Starting candle/set-theory
Oct 19 22:47:48 Finished candle/set-theory                                       22s   1GB
Oct 19 22:47:49 Starting candle/syntax-lib
Oct 19 22:47:57 Finished candle/syntax-lib                                        6s   1GB
Oct 19 22:47:58 Starting candle/standard
Oct 19 22:48:06 Finished candle/standard                                          6s   1GB
Oct 19 22:48:07 Starting candle/standard/syntax
Oct 19 22:48:28 Finished candle/standard/syntax                                  19s   1GB
Oct 19 22:48:29 Starting candle/standard/syntax/little_theories
Oct 19 22:50:36 Finished candle/standard/syntax/little_theories                2m06s   1GB
Oct 19 22:50:36 Starting candle/standard/semantics
Oct 19 22:50:44 Finished candle/standard/semantics                                6s   1GB
Oct 19 22:50:45 Starting candle/standard/monadic
Oct 19 22:50:53 Finished candle/standard/monadic                                  6s   1GB
Oct 19 22:50:54 Starting candle/standard/ml_kernel
Oct 19 22:53:43 Finished candle/standard/ml_kernel                             2m48s   6GB
Oct 19 22:53:44 Starting candle/overloading
Oct 19 22:53:52 Finished candle/overloading                                       6s   1GB
Oct 19 22:53:53 Starting candle/overloading/syntax
Oct 19 22:57:16 Finished candle/overloading/syntax                             3m22s   1GB
Oct 19 22:57:17 Starting candle/overloading/semantics
Oct 19 23:05:55 Finished candle/overloading/semantics                          8m37s   5GB
Oct 19 23:05:56 Starting candle/overloading/monadic
Oct 19 23:08:06 Finished candle/overloading/monadic                            2m08s   1GB
Oct 19 23:08:07 Starting candle/overloading/ml_kernel
Oct 19 23:16:10 Finished candle/overloading/ml_kernel                          8m02s   8GB
Oct 19 23:16:11 Starting candle/overloading/ml_checker
Oct 19 23:18:42 Finished candle/overloading/ml_checker                         2m29s   8GB
Oct 19 23:18:43 Starting candle/prover
Oct 19 23:18:50 Finished candle/prover                                            6s   1GB
Oct 19 23:18:51 Starting candle/prover/compute
Oct 19 23:18:59 Finished candle/prover/compute                                    6s   1GB
Oct 19 23:19:00 Starting candle/parser
Oct 19 23:19:08 Finished candle/parser                                            7s   1GB
Oct 19 23:19:09 Starting pancake
Oct 19 23:19:17 Finished pancake                                                  7s   1GB
Oct 19 23:19:18 Starting pancake/semantics
Oct 19 23:22:52 Finished pancake/semantics                                     3m33s   2GB
Oct 19 23:22:53 Starting pancake/parser
Oct 19 23:23:43 Finished pancake/parser                                          48s   1GB
Oct 19 23:23:44 Starting pancake/static_checker
Oct 19 23:26:29 Finished pancake/static_checker                                2m44s   1GB
Oct 19 23:26:30 Starting pancake/proofs
Oct 19 23:44:20 Finished pancake/proofs                                       17m49s   5GB
Oct 19 23:44:21 Starting pancake/decompiler
Oct 19 23:45:18 Finished pancake/decompiler                                      55s   2GB
Oct 19 23:45:19 Starting pancake/decompiler/examples
Oct 19 23:46:13 Finished pancake/decompiler/examples                             53s   3GB
Oct 19 23:46:14 Starting compiler/dafny
Oct 19 23:46:43 Finished compiler/dafny                                          28s   1GB
Oct 19 23:46:44 Starting compiler/dafny/translation
Oct 19 23:56:33 Finished compiler/dafny/translation                            9m47s   7GB
Oct 19 23:56:34 Starting compiler/dafny/compilation
Oct 19 23:58:51 Finished compiler/dafny/compilation                            2m16s   8GB
Oct 19 23:58:52 Starting compiler/dafny/semantics
Oct 19 23:59:36 Finished compiler/dafny/semantics                                43s   1GB
Oct 19 23:59:37 Starting compiler/dafny/proofs
Oct 20 00:01:28 Finished compiler/dafny/proofs                                 1m49s   2GB
Oct 20 00:01:28 Starting compiler/dafny/vcg
Oct 20 00:01:38 Finished compiler/dafny/vcg                                       7s   1GB
Oct 20 00:01:38 Starting compiler/dafny/vcg/examples
Oct 20 00:02:14 Finished compiler/dafny/vcg/examples                             34s   1GB
Oct 20 00:02:15 Starting compiler/scheme
Oct 20 00:02:49 Finished compiler/scheme                                         33s   1GB
Oct 20 00:02:50 Starting compiler/scheme/translation
Oct 20 00:07:27 Finished compiler/scheme/translation                           4m36s   7GB
Oct 20 00:07:28 Starting compiler/scheme/compilation
Oct 20 00:09:27 Finished compiler/scheme/compilation                           1m58s   6GB
Oct 20 00:09:28 Starting compiler/scheme/proofs
Oct 20 00:16:37 Finished compiler/scheme/proofs                                7m07s   3GB
Oct 20 00:16:38 Starting characteristic/examples
Oct 20 00:18:21 Finished characteristic/examples                               1m42s   6GB
Oct 20 00:18:22 Starting tutorial
Oct 20 00:18:30 Finished tutorial                                                 6s   1GB
Oct 20 00:18:31 Starting tutorial/solutions
Oct 20 00:21:59 Finished tutorial/solutions                                    3m26s   6GB
Oct 20 00:22:00 Starting translator/monadic/examples
Oct 20 00:25:23 Finished translator/monadic/examples                           3m22s   5GB
Oct 20 00:25:24 Starting examples
Oct 20 00:30:20 Finished examples                                              4m55s   5GB
Oct 20 00:30:21 Starting examples/compilation
Oct 20 00:30:29 Finished examples/compilation                                     7s   1GB
Oct 20 00:30:30 Starting examples/compilation/x64
Oct 20 00:44:08 Finished examples/compilation/x64                             13m36s   6GB
Oct 20 00:44:09 Starting examples/compilation/x64/proofs
Oct 20 00:48:36 Finished examples/compilation/x64/proofs                       4m26s   5GB
Oct 20 00:48:37 Starting examples/compilation/ag32
Oct 20 00:51:49 Finished examples/compilation/ag32                             3m10s   4GB
Oct 20 00:51:50 Starting examples/compilation/ag32/proofs
Oct 20 00:53:34 Finished examples/compilation/ag32/proofs                      1m43s   6GB
Oct 20 00:53:35 Starting examples/lpr_checker
Oct 20 00:54:21 Finished examples/lpr_checker                                    45s   1GB
Oct 20 00:54:22 Starting examples/lpr_checker/array
Oct 20 01:05:52 Finished examples/lpr_checker/array                           11m29s   7GB
Oct 20 01:05:53 Starting examples/lpr_checker/array/compilation
Oct 20 01:11:02 Finished examples/lpr_checker/array/compilation                5m07s   8GB
Oct 20 01:11:03 Starting examples/lpr_checker/array/compilation/proofs
Oct 20 01:13:00 Finished examples/lpr_checker/array/compilation/proofs         1m56s   7GB
Oct 20 01:13:01 Starting examples/lpr_checker/array/compilation/proofsARM8
Oct 20 01:15:16 Finished examples/lpr_checker/array/compilation/proofsARM8     2m13s   7GB
Oct 20 01:15:17 Starting .
Oct 20 01:15:24 Finished .                                                        6s   1GB
Oct 20 01:15:25 Starting examples/xlrup_checker
Oct 20 01:16:22 Finished examples/xlrup_checker                                  56s   1GB
Oct 20 01:16:23 Starting examples/xlrup_checker/array
Oct 20 01:24:44 Finished examples/xlrup_checker/array                          8m19s   4GB
Oct 20 01:24:45 Starting examples/xlrup_checker/array/compilation
Oct 20 01:26:39 Finished examples/xlrup_checker/array/compilation              1m53s   5GB
Oct 20 01:26:40 Starting examples/xlrup_checker/array/compilation/proofs
Oct 20 01:28:30 Finished examples/xlrup_checker/array/compilation/proofs       1m48s   6GB
Oct 20 01:28:31 Starting examples/cnf
Oct 20 01:29:06 Finished examples/cnf                                            34s   1GB
Oct 20 01:29:07 Starting examples/cnf/array
Oct 20 01:31:58 Finished examples/cnf/array                                    2m49s   2GB
Oct 20 01:31:59 Starting examples/cnf/dist
Oct 20 01:32:11 Finished examples/cnf/dist                                       11s   1GB
Oct 20 01:32:12 Starting examples/cnf/dist/array
Oct 20 01:37:21 Finished examples/cnf/dist/array                               5m08s   5GB
Oct 20 01:37:22 Starting examples/cnf/dist/array/compilation
Oct 20 01:38:41 Finished examples/cnf/dist/array/compilation                   1m18s   4GB
Oct 20 01:38:42 Starting examples/cnf/dist/array/compilation/proofs
Oct 20 01:40:24 Finished examples/cnf/dist/array/compilation/proofs            1m41s   5GB
Oct 20 01:40:25 Starting examples/cnf/lrup
Oct 20 01:40:38 Finished examples/cnf/lrup                                       12s   1GB
Oct 20 01:40:39 Starting examples/cnf/lrup/array
Oct 20 01:43:46 Finished examples/cnf/lrup/array                               3m05s   2GB
Oct 20 01:43:47 Starting examples/cnf/lrup/array/compilation
Oct 20 01:45:20 Finished examples/cnf/lrup/array/compilation                   1m31s   4GB
Oct 20 01:45:21 Starting examples/cnf/lrup/array/compilation/proofs
Oct 20 01:46:59 Finished examples/cnf/lrup/array/compilation/proofs            1m37s   5GB
Oct 20 01:47:00 Starting examples/cnf/xlrup
Oct 20 01:47:43 Finished examples/cnf/xlrup                                      41s   1GB
Oct 20 01:47:44 Starting examples/cnf/xlrup/array
Oct 20 01:54:06 Finished examples/cnf/xlrup/array                              6m21s   2GB
Oct 20 01:54:07 Starting examples/cnf/xlrup/array/compilation
Oct 20 01:55:50 Finished examples/cnf/xlrup/array/compilation                  1m42s   5GB
Oct 20 01:55:51 Starting examples/cnf/xlrup/array/compilation/proofs
Oct 20 01:57:35 Finished examples/cnf/xlrup/array/compilation/proofs           1m42s   5GB
Oct 20 01:57:36 Starting examples/scpog_checker
Oct 20 01:58:29 Finished examples/scpog_checker                                  52s   1GB
Oct 20 01:58:30 Starting examples/scpog_checker/array
Oct 20 02:03:57 Finished examples/scpog_checker/array                          5m26s   2GB
Oct 20 02:03:58 Starting examples/scpog_checker/array/compilation
Oct 20 02:07:11 Finished examples/scpog_checker/array/compilation              3m11s   8GB
Oct 20 02:07:12 Starting examples/scpog_checker/array/compilation/proofs
Oct 20 02:09:09 Finished examples/scpog_checker/array/compilation/proofs       1m56s   7GB
Oct 20 02:09:10 Starting examples/pseudo_bool
Oct 20 02:11:45 Finished examples/pseudo_bool                                  2m34s   2GB
Oct 20 02:11:46 Starting examples/pseudo_bool/cnf_encoding
Oct 20 02:12:26 Finished examples/pseudo_bool/cnf_encoding                       39s   1GB
Oct 20 02:12:27 Starting examples/pseudo_bool/graph_encoding
Oct 20 02:13:21 Finished examples/pseudo_bool/graph_encoding                     52s   1GB
Oct 20 02:13:22 Starting examples/pseudo_bool/array
Oct 20 03:00:40 Finished examples/pseudo_bool/array                           47m16s  31GB
Oct 20 03:00:41 Starting examples/pseudo_bool/array/compilation
Oct 20 03:09:19 Finished examples/pseudo_bool/array/compilation                8m36s  21GB
Oct 20 03:09:19 Starting examples/pseudo_bool/array/compilation/proofs
Oct 20 03:12:30 Finished examples/pseudo_bool/array/compilation/proofs         3m09s  10GB
Oct 20 03:12:30 Starting examples/pseudo_bool/array/compilation/proofsARM8
Oct 20 03:15:52 Finished examples/pseudo_bool/array/compilation/proofsARM8     3m20s  10GB
Oct 20 03:15:52 Starting examples/pseudo_bool/cnf_encoding/array
Oct 20 03:18:21 Finished examples/pseudo_bool/cnf_encoding/array               2m27s   3GB
Oct 20 03:18:22 Starting examples/pseudo_bool/cnf_encoding/array/compilation
Oct 20 03:27:07 Finished examples/pseudo_bool/cnf_encoding/array/compilation     8m44s  24GB
Oct 20 03:27:08 Starting examples/pseudo_bool/cnf_encoding/array/compilation/proofs
Oct 20 03:30:34 Finished examples/pseudo_bool/cnf_encoding/array/compilation/proofs     3m25s  10GB
Oct 20 03:30:35 Starting examples/pseudo_bool/graph_encoding/array
Oct 20 03:35:45 Finished examples/pseudo_bool/graph_encoding/array             5m08s   3GB
Oct 20 03:35:46 Starting examples/pseudo_bool/graph_encoding/array/compilation
Oct 20 03:53:26 Finished examples/pseudo_bool/graph_encoding/array/compilation    17m37s  24GB
Oct 20 03:53:27 Starting examples/pseudo_bool/graph_encoding/array/compilation/proofs
Oct 20 04:00:00 Finished examples/pseudo_bool/graph_encoding/array/compilation/proofs     6m31s  10GB
Oct 20 04:00:01 Starting examples/pseudo_bool/cp_encoding
Oct 20 04:02:17 FAILED: examples/pseudo_bool/cp_encoding
  HOLORIG=/scratch/regbox/regression2/cakeml-3628/examples/pseudo_bool/cp_encoding [ -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/parser
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/reg_alloc
Scanning $(CAKEMLDIR)/compiler/backend/semantics
Scanning $(CAKEMLDIR)/compiler/encoders/asm
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)/misc
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/backend/San
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/proofs
Scanning $(CAKEMLDIR)/compiler/backend/riscv
Scanning $(CAKEMLDIR)/compiler/backend/riscv/proofs
Scanning $(CAKEMLDIR)/compiler/backend/serialiser
Scanning $(CAKEMLDIR)/compiler/backend/tests
Scanning $(CAKEMLDIR)/compiler/backend/x64
Scanning $(CAKEMLDIR)/compiler/backend/x64/proofs
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/export/x64/64
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)/unverified/sexpr-bootstrap/export/32
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/export/arm8/64
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 $(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 $(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/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)/pancake
Scanning $(CAKEMLDIR)/pancake/parser
Scanning $(CAKEMLDIR)/pancake/semantics
Scanning $(CAKEMLDIR)/pancake/decompiler
Scanning $(CAKEMLDIR)/pancake/decompiler/examples
Scanning $(CAKEMLDIR)/pancake/proofs
Scanning $(CAKEMLDIR)/pancake/static_checker
Scanning $(CAKEMLDIR)/pancake/temp
Scanning $(CAKEMLDIR)/profiler
Scanning $(CAKEMLDIR)/semantics/alt_semantics
Scanning $(CAKEMLDIR)/semantics/alt_semantics/proofs
Scanning $(CAKEMLDIR)/semantics/ffi
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/export
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/export/arm8
Scanning $(CAKEMLDIR)/unverified/sexpr-bootstrap/export/x64
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 312 directories
Building 19 theory files
Starting work on README.md
Starting work on cpTheory
Starting work on int_bitwiseExtraTheory
README.md                                                   (0s)             OK
int_bitwiseExtraTheory                                     (11s)  [1/19]     OK
cpTheory                                                   (26s)  [2/19]     OK
Starting work on ilpTheory
Starting work on cp_parseTheory
ilpTheory                                                  (14s)  [3/19]     OK
Starting work on cp_to_ilpTheory
Starting work on ilp_to_pbTheory
cp_parseTheory                                             (28s)  [4/19]     OK
ilp_to_pbTheory                                            (12s)  [5/19]     OK
cp_to_ilpTheory                                            (29s)  [6/19]     OK
Starting work on cp_to_ilp_arrayTheory
Starting work on cp_to_ilp_channelingTheory
Starting work on cp_to_ilp_countingTheory
Starting work on cp_to_ilp_extensionalTheory
cp_to_ilp_channelingTheory                                 (14s)  [7/19]     OK
Starting work on cp_to_ilp_lexicographicalTheory
cp_to_ilp_arrayTheory                                      (15s)  [8/19]     OK
Starting work on cp_to_ilp_linearTheory
cp_to_ilp_extensionalTheory                                (19s)  [9/19]     OK
Starting work on cp_to_ilp_logicalTheory
cp_to_ilp_countingTheory                                   (22s) [10/19]     OK
Starting work on cp_to_ilp_primTheory
cp_to_ilp_linearTheory                                     (16s) [11/19]     OK
Starting work on cp_to_ilp_miscTheory
cp_to_ilp_lexicographicalTheory                            (21s) [12/19]     OK
cp_to_ilp_logicalTheory                                    (15s) [13/19]     OK
Starting work on cp_to_ilp_schedulingTheory
Starting work on cp_to_ilp_sortingTheory
cp_to_ilp_miscTheory                                       (11s)        FAIL<1>
cp_to_ilp_primTheory                                       (22s)         killed
cp_to_ilp_schedulingTheory                                  (7s)         killed
cp_to_ilp_sortingTheory                                     (7s)         killed
*** Holmake aborted - 1 target failed:
*** cp_to_ilp_miscTheory (status 1)
 <<HOL message: Created theory "cp_to_ilp_misc">>
 <<HOL warning: Context.snapshot: ambient context read while a proof was running (in cp_to_ilp_misc)>>
 Saved theorem _______ "PLUS_MOD_NEQ"
 Saved theorem _______ "ADD_1_MOD_EQ"
 Saved theorem _______ "FINITE_INJ_IMP_SURJ"
 Saved theorem _______ "FUNPOW_step_INJ"
 Proof of 
 
 circuit_sem Xs w 
 EVERY (X. 0  varc w X  Num (varc w X) < LENGTH Xs) Xs 
 ALL_DISTINCT (MAP (varc w) Xs) 
 pos.
   pos 0 = 0  (i. i < LENGTH Xs  pos i < LENGTH Xs) 
   i. i < LENGTH Xs  pos (Num (varc w Xsi)) = (pos i + 1) MOD LENGTH Xs
 
 failed.
 Tactic failure proving "circuit_sem_alt"; heap saved to cp_to_ilp_misc.circuit_sem_alt.dumpedheap.
 Resume with: bin/hol --holstate=cp_to_ilp_misc.circuit_sem_alt.dumpedheap
 Full log: /scratch/regbox/regression2/cakeml-3628/examples/pseudo_bool/cp_encoding/.hol/logs/cp_to_ilp_miscTheory