Job 3627

CakeML:09ad416dff52f8d967cae8df80f4350d96648ac2
  Repair REPL and Dafny proofs for index witnesses (#1485) [Oct 18 21:34:51]
#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:spagbol

Oct 18 22:01:15 Claimed job
Oct 18 22:01:20 Reusing HOL
Oct 18 22:01:29 Starting developers
Oct 18 22:02:28 Finished developers                                              57s   1GB
Oct 18 22:02:29 Starting developers/bin
Oct 18 22:02:38 Finished developers/bin                                           8s   1GB
Oct 18 22:02:39 Starting misc
Oct 18 22:03:28 Finished misc                                                    47s   1GB
Oct 18 22:03:29 Starting compiler/proofs
Oct 18 23:33:09 Finished compiler/proofs                                    1h29m38s  10GB
Oct 18 23:33:10 Starting compiler/bootstrap/compilation/x64/64/proofs
Oct 19 05:58:17 Finished compiler/bootstrap/compilation/x64/64/proofs       6h25m06s 122GB
Oct 19 05:58:18 Starting semantics/ffi
Oct 19 05:58:40 Finished semantics/ffi                                           21s   1GB
Oct 19 05:58:41 Starting semantics
Oct 19 05:58:49 Finished semantics                                                6s   1GB
Oct 19 05:58:50 Starting semantics/proofs
Oct 19 05:59:20 Finished semantics/proofs                                        29s   1GB
Oct 19 05:59:21 Starting semantics/alt_semantics
Oct 19 05:59:45 Finished semantics/alt_semantics                                 22s   1GB
Oct 19 05:59:46 Starting semantics/alt_semantics/proofs
Oct 19 06:04:13 Finished semantics/alt_semantics/proofs                        4m26s   2GB
Oct 19 06:04:14 Starting basis/pure
Oct 19 06:04:22 Finished basis/pure                                               6s   1GB
Oct 19 06:04:23 Starting translator
Oct 19 06:05:44 Finished translator                                            1m19s   2GB
Oct 19 06:05:45 Starting compiler/parsing
Oct 19 06:06:40 Finished compiler/parsing                                        54s   2GB
Oct 19 06:06:41 Starting characteristic
Oct 19 06:06:48 Finished characteristic                                           6s   1GB
Oct 19 06:06:49 Starting translator/monadic
Oct 19 06:06:56 Finished translator/monadic                                       6s   1GB
Oct 19 06:06:57 Starting translator/monadic/monad_base
Oct 19 06:07:05 Finished translator/monadic/monad_base                            6s   1GB
Oct 19 06:07:05 Starting profiler
Oct 19 06:07:42 Finished profiler                                                35s   2GB
Oct 19 06:07:43 Starting basis
Oct 19 06:10:11 Finished basis                                                 2m27s   5GB
Oct 19 06:10:12 Starting compiler
Oct 19 06:10:20 Finished compiler                                                 6s   1GB
Oct 19 06:10:21 Starting compiler/inference
Oct 19 06:10:28 Finished compiler/inference                                       6s   1GB
Oct 19 06:10:29 Starting compiler/backend/reg_alloc
Oct 19 06:10:37 Finished compiler/backend/reg_alloc                               6s   1GB
Oct 19 06:10:38 Starting compiler/backend/gc
Oct 19 06:10:45 Finished compiler/backend/gc                                      6s   1GB
Oct 19 06:10:46 Starting compiler/backend
Oct 19 06:10:57 Finished compiler/backend                                        10s   1GB
Oct 19 06:10:58 Starting compiler/backend/tests
Oct 19 06:11:34 Finished compiler/backend/tests                                  35s   1GB
Oct 19 06:11:35 Starting compiler/encoders/asm
Oct 19 06:11:43 Finished compiler/encoders/asm                                    6s   1GB
Oct 19 06:11:43 Starting compiler/encoders/x64
Oct 19 06:11:51 Finished compiler/encoders/x64                                    6s   1GB
Oct 19 06:11:52 Starting compiler/encoders/arm7
Oct 19 06:11:59 Finished compiler/encoders/arm7                                   6s   1GB
Oct 19 06:12:00 Starting compiler/encoders/arm8
Oct 19 06:12:07 Finished compiler/encoders/arm8                                   6s   1GB
Oct 19 06:12:08 Starting compiler/encoders/arm8_asl
Oct 19 06:12:32 Finished compiler/encoders/arm8_asl                              22s   1GB
Oct 19 06:12:33 Starting compiler/encoders/mips
Oct 19 06:12:40 Finished compiler/encoders/mips                                   6s   1GB
Oct 19 06:12:41 Starting compiler/encoders/riscv
Oct 19 06:12:48 Finished compiler/encoders/riscv                                  6s   1GB
Oct 19 06:12:49 Starting compiler/encoders/ag32
Oct 19 06:12:56 Finished compiler/encoders/ag32                                   6s   1GB
Oct 19 06:12:57 Starting compiler/encoders/tests
Oct 19 06:13:42 Finished compiler/encoders/tests                                 43s   1GB
Oct 19 06:13:43 Starting compiler/encoders/monadic_enc
Oct 19 06:14:10 Finished compiler/encoders/monadic_enc                           26s   1GB
Oct 19 06:14:11 Starting compiler/backend/x64
Oct 19 06:14:18 Finished compiler/backend/x64                                     6s   1GB
Oct 19 06:14:19 Starting compiler/backend/arm7
Oct 19 06:14:27 Finished compiler/backend/arm7                                    6s   1GB
Oct 19 06:14:27 Starting compiler/backend/arm8
Oct 19 06:14:35 Finished compiler/backend/arm8                                    6s   1GB
Oct 19 06:14:36 Starting compiler/backend/mips
Oct 19 06:14:44 Finished compiler/backend/mips                                    6s   1GB
Oct 19 06:14:44 Starting compiler/backend/riscv
Oct 19 06:14:52 Finished compiler/backend/riscv                                   6s   1GB
Oct 19 06:14:53 Starting compiler/backend/ag32
Oct 19 06:16:05 Finished compiler/backend/ag32                                 1m11s   1GB
Oct 19 06:16:06 Starting compiler/backend/pattern_matching
Oct 19 06:16:28 Finished compiler/backend/pattern_matching                       21s   1GB
Oct 19 06:16:29 Starting compiler/printing
Oct 19 06:17:25 Finished compiler/printing                                       54s   1GB
Oct 19 06:17:26 Starting compiler/parsing/proofs
Oct 19 06:17:33 Finished compiler/parsing/proofs                                  6s   1GB
Oct 19 06:17:34 Starting compiler/inference/proofs
Oct 19 06:17:42 Finished compiler/inference/proofs                                6s   1GB
Oct 19 06:17:43 Starting compiler/backend/semantics
Oct 19 06:20:25 Finished compiler/backend/semantics                            2m41s   1GB
Oct 19 06:20:26 Starting compiler/backend/reg_alloc/proofs
Oct 19 06:20:33 Finished compiler/backend/reg_alloc/proofs                        6s   1GB
Oct 19 06:20:34 Starting compiler/backend/proofs
Oct 19 06:21:29 Finished compiler/backend/proofs                                 53s   2GB
Oct 19 06:21:30 Starting compiler/backend/serialiser
Oct 19 06:21:38 Finished compiler/backend/serialiser                              6s   1GB
Oct 19 06:21:38 Starting compiler/encoders/x64/proofs
Oct 19 06:21:46 Finished compiler/encoders/x64/proofs                             6s   1GB
Oct 19 06:21:47 Starting compiler/encoders/arm7/proofs
Oct 19 06:34:52 Finished compiler/encoders/arm7/proofs                        13m04s  10GB
Oct 19 06:34:53 Starting compiler/encoders/arm8/proofs
Oct 19 06:47:09 Finished compiler/encoders/arm8/proofs                        12m14s  14GB
Oct 19 06:47:10 Starting compiler/encoders/arm8_asl/proofs
Oct 19 07:15:03 Finished compiler/encoders/arm8_asl/proofs                    27m51s  23GB
Oct 19 07:15:04 Starting compiler/encoders/mips/proofs
Oct 19 07:27:07 Finished compiler/encoders/mips/proofs                        12m02s   8GB
Oct 19 07:27:08 Starting compiler/encoders/riscv/proofs
Oct 19 07:37:24 Finished compiler/encoders/riscv/proofs                       10m15s   3GB
Oct 19 07:37:25 Starting compiler/encoders/ag32/proofs
Oct 19 07:40:52 Finished compiler/encoders/ag32/proofs                         3m25s   1GB
Oct 19 07:40:53 Starting compiler/backend/x64/proofs
Oct 19 07:41:01 Finished compiler/backend/x64/proofs                              6s   1GB
Oct 19 07:41:02 Starting compiler/backend/arm7/proofs
Oct 19 07:41:45 Finished compiler/backend/arm7/proofs                            42s   2GB
Oct 19 07:41:46 Starting compiler/backend/arm8/proofs
Oct 19 07:42:34 Finished compiler/backend/arm8/proofs                            47s   2GB
Oct 19 07:42:35 Starting compiler/backend/arm8_asl
Oct 19 07:43:18 Finished compiler/backend/arm8_asl                               42s   2GB
Oct 19 07:43:19 Starting compiler/backend/mips/proofs
Oct 19 07:44:05 Finished compiler/backend/mips/proofs                            45s   2GB
Oct 19 07:44:06 Starting compiler/backend/riscv/proofs
Oct 19 07:44:52 Finished compiler/backend/riscv/proofs                           45s   2GB
Oct 19 07:44:53 Starting compiler/backend/San
Oct 19 07:46:03 Finished compiler/backend/San                                  1m09s   3GB
Oct 19 07:46:04 Starting compiler/backend/ag32/proofs
Oct 19 07:55:46 Finished compiler/backend/ag32/proofs                          9m40s   4GB
Oct 19 07:55:47 Starting compiler/backend/cv_compute
Oct 19 07:56:25 Finished compiler/backend/cv_compute                             36s   1GB
Oct 19 07:56:26 Starting cv_translator
Oct 19 07:59:27 Finished cv_translator                                         3m00s   4GB
Oct 19 07:59:28 Starting candle
Oct 19 07:59:36 Finished candle                                                   6s   1GB
Oct 19 07:59:37 Starting candle/set-theory
Oct 19 08:00:00 Finished candle/set-theory                                       22s   1GB
Oct 19 08:00:01 Starting candle/syntax-lib
Oct 19 08:00:09 Finished candle/syntax-lib                                        6s   1GB
Oct 19 08:00:10 Starting candle/standard
Oct 19 08:00:17 Finished candle/standard                                          6s   1GB
Oct 19 08:00:18 Starting candle/standard/syntax
Oct 19 08:00:38 Finished candle/standard/syntax                                  18s   1GB
Oct 19 08:00:39 Starting candle/standard/syntax/little_theories
Oct 19 08:02:41 Finished candle/standard/syntax/little_theories                2m01s   1GB
Oct 19 08:02:42 Starting candle/standard/semantics
Oct 19 08:02:50 Finished candle/standard/semantics                                6s   1GB
Oct 19 08:02:51 Starting candle/standard/monadic
Oct 19 08:02:58 Finished candle/standard/monadic                                  6s   1GB
Oct 19 08:02:59 Starting candle/standard/ml_kernel
Oct 19 08:05:38 Finished candle/standard/ml_kernel                             2m37s   6GB
Oct 19 08:05:38 Starting candle/overloading
Oct 19 08:05:46 Finished candle/overloading                                       6s   1GB
Oct 19 08:05:47 Starting candle/overloading/syntax
Oct 19 08:09:07 Finished candle/overloading/syntax                             3m18s   2GB
Oct 19 08:09:08 Starting candle/overloading/semantics
Oct 19 08:17:56 Finished candle/overloading/semantics                          8m47s   4GB
Oct 19 08:17:57 Starting candle/overloading/monadic
Oct 19 08:20:08 Finished candle/overloading/monadic                            2m10s   1GB
Oct 19 08:20:09 Starting candle/overloading/ml_kernel
Oct 19 08:28:06 Finished candle/overloading/ml_kernel                          7m55s   8GB
Oct 19 08:28:07 Starting candle/overloading/ml_checker
Oct 19 08:30:35 Finished candle/overloading/ml_checker                         2m27s   7GB
Oct 19 08:30:36 Starting candle/prover
Oct 19 08:30:44 Finished candle/prover                                            6s   1GB
Oct 19 08:30:45 Starting candle/prover/compute
Oct 19 08:30:52 Finished candle/prover/compute                                    6s   1GB
Oct 19 08:30:53 Starting candle/parser
Oct 19 08:31:00 Finished candle/parser                                            6s   1GB
Oct 19 08:31:01 Starting pancake
Oct 19 08:31:09 Finished pancake                                                  6s   1GB
Oct 19 08:31:10 Starting pancake/semantics
Oct 19 08:34:41 Finished pancake/semantics                                     3m30s   2GB
Oct 19 08:34:42 Starting pancake/parser
Oct 19 08:35:32 Finished pancake/parser                                          48s   1GB
Oct 19 08:35:33 Starting pancake/static_checker
Oct 19 08:38:18 Finished pancake/static_checker                                2m43s   1GB
Oct 19 08:38:19 Starting pancake/proofs
Oct 19 08:56:03 Finished pancake/proofs                                       17m43s   6GB
Oct 19 08:56:04 Starting pancake/decompiler
Oct 19 08:57:05 Finished pancake/decompiler                                      59s   2GB
Oct 19 08:57:06 Starting pancake/decompiler/examples
Oct 19 08:57:57 Finished pancake/decompiler/examples                             49s   2GB
Oct 19 08:57:58 Starting compiler/dafny
Oct 19 08:58:29 Finished compiler/dafny                                          29s   1GB
Oct 19 08:58:30 Starting compiler/dafny/translation
Oct 19 09:08:06 Finished compiler/dafny/translation                            9m35s   7GB
Oct 19 09:08:07 Starting compiler/dafny/compilation
Oct 19 09:10:24 Finished compiler/dafny/compilation                            2m16s   5GB
Oct 19 09:10:25 Starting compiler/dafny/semantics
Oct 19 09:11:09 Finished compiler/dafny/semantics                                42s   1GB
Oct 19 09:11:10 Starting compiler/dafny/proofs
Oct 19 09:13:00 Finished compiler/dafny/proofs                                 1m48s   1GB
Oct 19 09:13:01 Starting compiler/dafny/vcg
Oct 19 09:13:08 Finished compiler/dafny/vcg                                       6s   1GB
Oct 19 09:13:09 Starting compiler/dafny/vcg/examples
Oct 19 09:13:46 Finished compiler/dafny/vcg/examples                             35s   1GB
Oct 19 09:13:47 Starting compiler/scheme
Oct 19 09:14:17 Finished compiler/scheme                                         29s   1GB
Oct 19 09:14:18 Starting compiler/scheme/translation
Oct 19 09:18:57 Finished compiler/scheme/translation                           4m38s   6GB
Oct 19 09:18:58 Starting compiler/scheme/compilation
Oct 19 09:20:49 Finished compiler/scheme/compilation                           1m50s   5GB
Oct 19 09:20:50 Starting compiler/scheme/proofs
Oct 19 09:27:55 Finished compiler/scheme/proofs                                7m04s   2GB
Oct 19 09:27:56 Starting characteristic/examples
Oct 19 09:29:40 Finished characteristic/examples                               1m43s   6GB
Oct 19 09:29:41 Starting tutorial
Oct 19 09:29:48 Finished tutorial                                                 6s   1GB
Oct 19 09:29:49 Starting tutorial/solutions
Oct 19 09:33:23 Finished tutorial/solutions                                    3m32s   5GB
Oct 19 09:33:24 Starting translator/monadic/examples
Oct 19 09:36:46 Finished translator/monadic/examples                           3m21s   5GB
Oct 19 09:36:47 Starting examples
Oct 19 09:41:46 Finished examples                                              4m58s   5GB
Oct 19 09:41:47 Starting examples/compilation
Oct 19 09:41:55 Finished examples/compilation                                     7s   1GB
Oct 19 09:41:56 Starting examples/compilation/x64
Oct 19 09:54:55 Finished examples/compilation/x64                             12m58s   4GB
Oct 19 09:54:56 Starting examples/compilation/x64/proofs
Oct 19 09:59:03 Finished examples/compilation/x64/proofs                       4m06s   5GB
Oct 19 09:59:04 Starting examples/compilation/ag32
Oct 19 10:02:08 Finished examples/compilation/ag32                             3m02s   4GB
Oct 19 10:02:09 Starting examples/compilation/ag32/proofs
Oct 19 10:03:46 Finished examples/compilation/ag32/proofs                      1m36s   5GB
Oct 19 10:03:47 Starting examples/lpr_checker
Oct 19 10:04:30 Finished examples/lpr_checker                                    42s   1GB
Oct 19 10:04:31 Starting examples/lpr_checker/array
Oct 19 10:16:23 Finished examples/lpr_checker/array                           11m50s   6GB
Oct 19 10:16:24 Starting examples/lpr_checker/array/compilation
Oct 19 10:21:19 Finished examples/lpr_checker/array/compilation                4m54s   7GB
Oct 19 10:21:20 Starting examples/lpr_checker/array/compilation/proofs
Oct 19 10:23:14 Finished examples/lpr_checker/array/compilation/proofs         1m52s   7GB
Oct 19 10:23:15 Starting examples/lpr_checker/array/compilation/proofsARM8
Oct 19 10:25:22 Finished examples/lpr_checker/array/compilation/proofsARM8     2m06s   8GB
Oct 19 10:25:23 Starting .
Oct 19 10:25:31 Finished .                                                        6s   1GB
Oct 19 10:25:32 Starting examples/xlrup_checker
Oct 19 10:26:30 Finished examples/xlrup_checker                                  57s   1GB
Oct 19 10:26:30 Starting examples/xlrup_checker/array
Oct 19 10:35:06 Finished examples/xlrup_checker/array                          8m34s   4GB
Oct 19 10:35:07 Starting examples/xlrup_checker/array/compilation
Oct 19 10:37:08 Finished examples/xlrup_checker/array/compilation              2m00s   6GB
Oct 19 10:37:09 Starting examples/xlrup_checker/array/compilation/proofs
Oct 19 10:38:57 Finished examples/xlrup_checker/array/compilation/proofs       1m46s   6GB
Oct 19 10:38:58 Starting examples/cnf
Oct 19 10:39:33 Finished examples/cnf                                            33s   1GB
Oct 19 10:39:34 Starting examples/cnf/array
Oct 19 10:42:19 Finished examples/cnf/array                                    2m43s   1GB
Oct 19 10:42:20 Starting examples/cnf/dist
Oct 19 10:42:32 Finished examples/cnf/dist                                       10s   1GB
Oct 19 10:42:32 Starting examples/cnf/dist/array
Oct 19 10:47:40 Finished examples/cnf/dist/array                               5m06s   3GB
Oct 19 10:47:41 Starting examples/cnf/dist/array/compilation
Oct 19 10:49:03 Finished examples/cnf/dist/array/compilation                   1m21s   4GB
Oct 19 10:49:04 Starting examples/cnf/dist/array/compilation/proofs
Oct 19 10:50:31 Finished examples/cnf/dist/array/compilation/proofs            1m25s   5GB
Oct 19 10:50:32 Starting examples/cnf/lrup
Oct 19 10:50:45 Finished examples/cnf/lrup                                       11s   1GB
Oct 19 10:50:46 Starting examples/cnf/lrup/array
Oct 19 10:53:50 Finished examples/cnf/lrup/array                               3m03s   2GB
Oct 19 10:53:51 Starting examples/cnf/lrup/array/compilation
Oct 19 10:55:23 Finished examples/cnf/lrup/array/compilation                   1m31s   4GB
Oct 19 10:55:24 Starting examples/cnf/lrup/array/compilation/proofs
Oct 19 10:57:07 Finished examples/cnf/lrup/array/compilation/proofs            1m41s   5GB
Oct 19 10:57:08 Starting examples/cnf/xlrup
Oct 19 10:57:50 Finished examples/cnf/xlrup                                      41s   1GB
Oct 19 10:57:51 Starting examples/cnf/xlrup/array
Oct 19 11:04:19 Finished examples/cnf/xlrup/array                              6m26s   2GB
Oct 19 11:04:20 Starting examples/cnf/xlrup/array/compilation
Oct 19 11:06:04 Finished examples/cnf/xlrup/array/compilation                  1m43s   4GB
Oct 19 11:06:05 Starting examples/cnf/xlrup/array/compilation/proofs
Oct 19 11:07:45 Finished examples/cnf/xlrup/array/compilation/proofs           1m38s   5GB
Oct 19 11:07:46 Starting examples/scpog_checker
Oct 19 11:08:39 Finished examples/scpog_checker                                  52s   1GB
Oct 19 11:08:40 Starting examples/scpog_checker/array
Oct 19 11:14:16 Finished examples/scpog_checker/array                          5m34s   2GB
Oct 19 11:14:17 Starting examples/scpog_checker/array/compilation
Oct 19 11:17:21 Finished examples/scpog_checker/array/compilation              3m03s   9GB
Oct 19 11:17:22 Starting examples/scpog_checker/array/compilation/proofs
Oct 19 11:19:17 Finished examples/scpog_checker/array/compilation/proofs       1m54s   7GB
Oct 19 11:19:18 Starting examples/pseudo_bool
Oct 19 11:21:53 Finished examples/pseudo_bool                                  2m34s   1GB
Oct 19 11:21:54 Starting examples/pseudo_bool/cnf_encoding
Oct 19 11:22:32 Finished examples/pseudo_bool/cnf_encoding                       37s   1GB
Oct 19 11:22:33 Starting examples/pseudo_bool/graph_encoding
Oct 19 11:23:16 FAILED: examples/pseudo_bool/graph_encoding
  HOLORIG=/scratch/regbox/regression/cakeml-3627/examples/pseudo_bool/graph_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 5 theory files
Starting work on README.md
Starting work on graph_basicTheory
README.md                                                   (0s)             OK
graph_basicTheory                                          (15s)   [1/5]     OK
Starting work on cliqueTheory
Starting work on colourTheory
Starting work on mcisTheory
Starting work on subgraph_isoTheory
subgraph_isoTheory                                         (13s)   [2/5]     OK
cliqueTheory                                               (14s)   [3/5]     OK
mcisTheory                                                 (15s)        FAIL<1>
colourTheory                                               (15s)         killed
*** Holmake aborted - 1 target failed:
*** mcisTheory (status 1)
 Saved theorem _______ "enc_11"
 Saved theorem _______ "enc_distinct"
 Saved theorem _______ "enc_nchotomy"
 Saved theorem _______ "enc_Axiom"
 Saved theorem _______ "enc_induction"
 Saved theorem _______ "enc_case_cong"
 Saved theorem _______ "enc_case_eq"
 <<HOL message: Defined type: "enc">>
 Saved definition ____ "has_mapping_al1_def"
 Saved definition ____ "has_mapping_am1_def"
 Saved definition ____ "all_has_mapping_def"
 Saved definition ____ "one_one_def"
 Saved definition ____ "all_one_one_def"
 Saved definition ____ "edge_map_def"
 Saved definition ____ "not_edge_map_def"
 Saved definition ____ "all_full_edge_map_def"
 Saved definition ____ "unmapped_obj_def"
 Saved definition ____ "encode_base_def"
 Saved theorem _______ "b2i_geq_1"
 Saved theorem _______ "b2i_eq_1"
 Saved theorem _______ "b2i_eq_0"
 Saved theorem _______ "neg_b2i_eq_1"
 Saved theorem _______ "b2i_geq_zero"
 Saved theorem _______ "b2i_add_one_geq_one"
 <<HOL warning: Context.snapshot: ambient context read while a proof was running (in mcis)>>
 Saved theorem _______ "iSUM_ge_zero"
 Saved theorem _______ "b2i_iSUM_eq_0"
 Saved theorem _______ "iSUM_geq_1"
 Saved theorem _______ "iSUM_eq_1"
 Saved theorem _______ "iSUM_sub_b2i_geq_0'"
 Saved theorem _______ "iSUM_sub_b2i_geq_0"
 Saved theorem _______ "iSUM_sub_b2i_geq"
 Saved theorem _______ "iSUM_GENLIST_const"
 Saved theorem _______ "iSUM_SNOC"
 Saved theorem _______ "iSUM_GENLIST_eq_k"
 Saved theorem _______ "MEM_if"
 Saved theorem _______ "iSUM_MAP_b2i_ge_0"
 Saved theorem _______ "iSUM_MAP_b2i_ge_1"
 Saved theorem _______ "one_iSUM_MAP_b2i"
 Proof of 
 
 good_graph (vp,ep)  good_graph (vt,et) 
 encode_base (vp,ep) (vt,et) = constraints 
 ((f vs. injective_partial_map f vs (vp,ep) (vt,et)  CARD vs = k) 
  w. satisfies w (set (MAP SND constraints)) 
      eval_obj (unmapped_obj vp) w = &vp  &k)
 
 failed.
 Tactic failure proving "encode_base_correct"; heap saved to mcis.encode_base_correct.dumpedheap.
 Resume with: bin/hol --holstate=mcis.encode_base_correct.dumpedheap
 Full log: /scratch/regbox/regression/cakeml-3627/examples/pseudo_bool/graph_encoding/.hol/logs/mcisTheory