Job 2277

CakeML:bbe2c97e876259d08b32a544a8556820338d8314
  de-duplicate in wcnf_to_pb, better errors [Jan 20 17:32:08]
#978 (pb_output)
Merging into:e026a91d58aabda091e58bb8b4b8ca67b192f07c
  Fix mlvector given changes in HOL [Jan 17 02:43:46]
HOL:c833caa48ab90faf4bd20a55b58849e20d49f611
  Add a couple of sptree theorems [Jan 19 23:20:24]
Machine:pavlova

Jan 22 10:37:14 Claimed job
Jan 22 10:37:18 Reusing HOL
Jan 22 10:37:28 Starting developers
Jan 22 10:37:31 Finished developers                                               2s 227MB
Jan 22 10:37:32 Starting developers/bin
Jan 22 10:37:42 Finished developers/bin                                           9s   1GB
Jan 22 10:37:43 Starting compiler/proofs
Jan 22 12:21:41 Finished compiler/proofs                                    1h43m57s  38GB
Jan 22 12:21:42 Starting compiler/bootstrap/translation
Jan 22 20:34:35 Finished compiler/bootstrap/translation                     8h12m51s  65GB
Jan 22 20:34:36 Starting semantics/ffi
Jan 22 20:34:44 Finished semantics/ffi                                            7s 581MB
Jan 22 20:34:45 Starting semantics
Jan 22 20:34:46 Finished semantics                                                0s  67MB
Jan 22 20:34:47 Starting semantics/proofs
Jan 22 20:35:22 Finished semantics/proofs                                        34s   2GB
Jan 22 20:35:23 Starting semantics/alt_semantics
Jan 22 20:36:03 Finished semantics/alt_semantics                                 38s   1GB
Jan 22 20:36:04 Starting semantics/alt_semantics/proofs
Jan 22 20:47:10 Finished semantics/alt_semantics/proofs                       11m05s   6GB
Jan 22 20:47:11 Starting basis/pure
Jan 22 20:47:12 Finished basis/pure                                               0s  66MB
Jan 22 20:47:13 Starting translator
Jan 22 20:48:56 Finished translator                                            1m42s   3GB
Jan 22 20:48:57 Starting compiler/parsing
Jan 22 20:48:59 Finished compiler/parsing                                         0s  71MB
Jan 22 20:49:00 Starting characteristic
Jan 22 20:49:01 Finished characteristic                                           0s  93MB
Jan 22 20:49:02 Starting translator/monadic
Jan 22 20:49:03 Finished translator/monadic                                       0s  98MB
Jan 22 20:49:04 Starting basis
Jan 22 20:52:40 Finished basis                                                 3m35s   5GB
Jan 22 20:52:41 Starting compiler/inference
Jan 22 20:52:43 Finished compiler/inference                                       0s  85MB
Jan 22 20:52:44 Starting compiler/backend/reg_alloc
Jan 22 20:52:45 Finished compiler/backend/reg_alloc                               0s  66MB
Jan 22 20:52:46 Starting compiler/backend/gc
Jan 22 20:52:48 Finished compiler/backend/gc                                      0s 138MB
Jan 22 20:52:48 Starting compiler/backend
Jan 22 20:53:06 Finished compiler/backend                                        16s   1GB
Jan 22 20:53:07 Starting compiler/encoders/asm
Jan 22 20:53:08 Finished compiler/encoders/asm                                    0s  82MB
Jan 22 20:53:09 Starting compiler/encoders/x64
Jan 22 20:53:10 Finished compiler/encoders/x64                                    0s  94MB
Jan 22 20:53:11 Starting compiler/encoders/arm7
Jan 22 20:53:13 Finished compiler/encoders/arm7                                   0s  95MB
Jan 22 20:53:14 Starting compiler/encoders/arm8
Jan 22 20:53:15 Finished compiler/encoders/arm8                                   0s  90MB
Jan 22 20:53:16 Starting compiler/encoders/arm8_asl
Jan 22 23:00:28 Finished compiler/encoders/arm8_asl                         2h07m10s  46GB
Jan 22 23:00:29 Starting compiler/encoders/mips
Jan 22 23:00:30 Finished compiler/encoders/mips                                   0s  87MB
Jan 22 23:00:31 Starting compiler/encoders/riscv
Jan 22 23:00:32 Finished compiler/encoders/riscv                                  0s  88MB
Jan 22 23:00:33 Starting compiler/encoders/ag32
Jan 22 23:00:35 Finished compiler/encoders/ag32                                   0s  85MB
Jan 22 23:00:36 Starting compiler/backend/x64
Jan 22 23:00:37 Finished compiler/backend/x64                                     0s 129MB
Jan 22 23:00:38 Starting compiler/backend/arm7
Jan 22 23:00:40 Finished compiler/backend/arm7                                    0s 129MB
Jan 22 23:00:41 Starting compiler/backend/arm8
Jan 22 23:00:43 Finished compiler/backend/arm8                                    0s 129MB
Jan 22 23:00:43 Starting compiler/backend/mips
Jan 22 23:00:45 Finished compiler/backend/mips                                    0s 129MB
Jan 22 23:00:46 Starting compiler/backend/riscv
Jan 22 23:00:48 Finished compiler/backend/riscv                                   0s 129MB
Jan 22 23:00:49 Starting compiler/backend/ag32
Jan 22 23:02:06 Finished compiler/backend/ag32                                 1m16s   2GB
Jan 22 23:02:07 Starting compiler/parsing/proofs
Jan 22 23:02:08 Finished compiler/parsing/proofs                                  0s  75MB
Jan 22 23:02:09 Starting compiler/inference/proofs
Jan 22 23:02:10 Finished compiler/inference/proofs                                0s  89MB
Jan 22 23:02:11 Starting compiler/backend/semantics
Jan 22 23:03:37 Finished compiler/backend/semantics                            1m25s   3GB
Jan 22 23:03:38 Starting compiler/backend/reg_alloc/proofs
Jan 22 23:03:40 Finished compiler/backend/reg_alloc/proofs                        0s  91MB
Jan 22 23:03:41 Starting compiler/backend/proofs
Jan 22 23:04:45 Finished compiler/backend/proofs                               1m03s   3GB
Jan 22 23:04:46 Starting compiler/backend/serialiser
Jan 22 23:04:48 Finished compiler/backend/serialiser                              1s 188MB
Jan 22 23:04:49 Starting compiler/encoders/x64/proofs
Jan 22 23:14:09 Finished compiler/encoders/x64/proofs                          9m18s   5GB
Jan 22 23:14:09 Starting compiler/encoders/arm7/proofs
Jan 22 23:26:55 Finished compiler/encoders/arm7/proofs                        12m44s  10GB
Jan 22 23:26:56 Starting compiler/encoders/arm8/proofs
Jan 22 23:33:27 Finished compiler/encoders/arm8/proofs                         6m30s   5GB
Jan 22 23:33:28 Starting compiler/encoders/arm8_asl/proofs
Jan 23 00:20:47 Finished compiler/encoders/arm8_asl/proofs                    47m18s  10GB
Jan 23 00:20:48 Starting compiler/encoders/mips/proofs
Jan 23 00:30:43 Finished compiler/encoders/mips/proofs                         9m54s   7GB
Jan 23 00:30:44 Starting compiler/encoders/riscv/proofs
Jan 23 00:38:55 Finished compiler/encoders/riscv/proofs                        8m10s   3GB
Jan 23 00:38:56 Starting compiler/encoders/ag32/proofs
Jan 23 00:41:17 Finished compiler/encoders/ag32/proofs                         2m20s   2GB
Jan 23 00:41:18 Starting compiler/backend/x64/proofs
Jan 23 00:41:59 Finished compiler/backend/x64/proofs                             39s   3GB
Jan 23 00:42:00 Starting compiler/backend/arm7/proofs
Jan 23 00:42:41 Finished compiler/backend/arm7/proofs                            40s   2GB
Jan 23 00:42:42 Starting compiler/backend/arm8/proofs
Jan 23 00:43:21 Finished compiler/backend/arm8/proofs                            38s   3GB
Jan 23 00:43:21 Starting compiler/backend/arm8_asl
Jan 23 00:43:51 Finished compiler/backend/arm8_asl                               29s   2GB
Jan 23 00:43:52 Starting compiler/backend/mips/proofs
Jan 23 00:44:36 Finished compiler/backend/mips/proofs                            42s   3GB
Jan 23 00:44:37 Starting compiler/backend/riscv/proofs
Jan 23 00:45:27 Finished compiler/backend/riscv/proofs                           49s   3GB
Jan 23 00:45:28 Starting compiler/backend/ag32/proofs
Jan 23 00:58:55 Finished compiler/backend/ag32/proofs                         13m26s   4GB
Jan 23 00:58:56 Starting candle/set-theory
Jan 23 00:59:41 Finished candle/set-theory                                       43s   1GB
Jan 23 00:59:42 Starting candle/syntax-lib
Jan 23 00:59:43 Finished candle/syntax-lib                                        0s  67MB
Jan 23 00:59:44 Starting candle/standard/syntax
Jan 23 01:00:00 Finished candle/standard/syntax                                  15s   1GB
Jan 23 01:00:01 Starting candle/standard/semantics
Jan 23 01:02:20 Finished candle/standard/semantics                             2m18s   2GB
Jan 23 01:02:21 Starting candle/standard/monadic
Jan 23 01:02:23 Finished candle/standard/monadic                                  0s 104MB
Jan 23 01:02:23 Starting candle/standard/ml_kernel
Jan 23 01:04:13 Finished candle/standard/ml_kernel                             1m48s   5GB
Jan 23 01:04:14 Starting candle/overloading/syntax
Jan 23 01:07:38 Finished candle/overloading/syntax                             3m23s   2GB
Jan 23 01:07:39 Starting candle/overloading/semantics
Jan 23 01:19:00 Finished candle/overloading/semantics                         11m20s   6GB
Jan 23 01:19:01 Starting candle/overloading/monadic
Jan 23 01:21:34 Finished candle/overloading/monadic                            2m31s   3GB
Jan 23 01:21:35 Starting candle/overloading/ml_kernel
Jan 23 01:29:01 Finished candle/overloading/ml_kernel                          7m25s   6GB
Jan 23 01:29:02 Starting candle/overloading/ml_checker
Jan 23 01:31:33 Finished candle/overloading/ml_checker                         2m30s   7GB
Jan 23 01:31:34 Starting candle/prover
Jan 23 01:41:26 Finished candle/prover                                         9m51s   5GB
Jan 23 01:41:27 Starting pancake
Jan 23 01:42:27 Finished pancake                                                 59s   1GB
Jan 23 01:42:28 Starting pancake/ffi
Jan 23 01:42:29 Finished pancake/ffi                                              0s  20MB
Jan 23 01:42:30 Starting pancake/semantics
Jan 23 01:44:52 Finished pancake/semantics                                     2m21s   2GB
Jan 23 01:44:53 Starting pancake/parser
Jan 23 01:45:20 Finished pancake/parser                                          26s   2GB
Jan 23 01:45:21 Starting pancake/proofs
Jan 23 02:15:06 Finished pancake/proofs                                       29m43s   9GB
Jan 23 02:15:06 Starting characteristic/examples
Jan 23 02:16:41 Finished characteristic/examples                               1m34s   5GB
Jan 23 02:16:42 Starting tutorial/solutions
Jan 23 02:32:29 Finished tutorial/solutions                                   15m45s  17GB
Jan 23 02:32:29 Starting translator/monadic/examples
Jan 23 02:36:15 Finished translator/monadic/examples                           3m44s   5GB
Jan 23 02:36:16 Starting examples
Jan 23 02:50:36 Finished examples                                             14m18s   7GB
Jan 23 02:50:37 Starting examples/compilation/x64
Jan 23 04:46:22 Finished examples/compilation/x64                           1h55m44s  36GB
Jan 23 04:46:23 Starting examples/compilation/x64/proofs
Jan 23 04:50:07 Finished examples/compilation/x64/proofs                       3m43s   5GB
Jan 23 04:50:08 Starting examples/compilation/ag32
Jan 23 05:19:25 Finished examples/compilation/ag32                            29m16s  13GB
Jan 23 05:19:26 Starting examples/compilation/ag32/proofs
Jan 23 05:20:51 Finished examples/compilation/ag32/proofs                      1m24s   6GB
Jan 23 05:20:52 Starting examples/compilation/to_word
Jan 23 05:24:43 Finished examples/compilation/to_word                          3m50s  11GB
Jan 23 05:24:44 Starting examples/lpr_checker
Jan 23 05:26:01 Finished examples/lpr_checker                                  1m16s   2GB
Jan 23 05:26:02 Starting examples/lpr_checker/array
Jan 23 05:55:05 Finished examples/lpr_checker/array                           29m01s  12GB
Jan 23 05:55:06 Starting examples/lpr_checker/array/compilation
Jan 23 06:29:59 Finished examples/lpr_checker/array/compilation               34m51s  61GB
Jan 23 06:30:00 Starting examples/lpr_checker/array/compilation/proofs
Jan 23 06:31:56 Finished examples/lpr_checker/array/compilation/proofs         1m55s   9GB
Jan 23 06:31:57 Starting examples/lpr_checker/array/compilation/proofsARM8
Jan 23 06:56:14 Finished examples/lpr_checker/array/compilation/proofsARM8    24m16s  33GB
Jan 23 06:56:15 Starting examples/pseudo_bool
Jan 23 06:58:16 Finished examples/pseudo_bool                                  1m59s   2GB
Jan 23 06:58:17 Starting examples/pseudo_bool/cnf_encoding
Jan 23 06:58:53 Finished examples/pseudo_bool/cnf_encoding                       35s   1GB
Jan 23 06:58:54 Starting examples/pseudo_bool/graph_encoding
Jan 23 06:59:44 Finished examples/pseudo_bool/graph_encoding                     49s   2GB
Jan 23 06:59:45 Starting examples/pseudo_bool/array
Jan 23 07:52:50 Finished examples/pseudo_bool/array                           53m04s  15GB
Jan 23 07:52:51 Starting examples/pseudo_bool/array/compilation
Jan 23 09:56:52 Finished examples/pseudo_bool/array/compilation             2h04m00s 119GB
Jan 23 09:56:53 Starting examples/pseudo_bool/array/compilation/proofs
Jan 23 09:59:58 FAILED: examples/pseudo_bool/array/compilation/proofs
Scanning [1m$(HOLDIR)/src/sort[0m
Scanning [1m$(HOLDIR)/src/string[0m
Scanning [1m$(HOLDIR)/src/n-bit[0m
Scanning [1m$(HOLDIR)/src/res_quan/src[0m
Scanning [1m$(HOLDIR)/src/finite_maps[0m
Scanning [1m$(HOLDIR)/examples/algorithms[0m
Scanning [1m$(HOLDIR)/examples/machine-code/hoare-triple[0m
Scanning [1m$(HOLDIR)/src/ring/src[0m
Scanning [1m$(HOLDIR)/src/integer[0m
Scanning [1m$(HOLDIR)/examples/machine-code/multiword[0m
Scanning [1m$(HOLDIR)/examples/balanced_bst[0m
Scanning [1m$(HOLDIR)/examples/formal-languages[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/context-free[0m
Scanning [1m$(HOLDIR)/examples/formal-languages/regular[0m
Scanning [1m$(HOLDIR)/src/transfer[0m
Scanning [1m$(HOLDIR)/src/pred_set/src/more_theories[0m
Scanning [1m$(HOLDIR)/src/coalgebras[0m
Scanning [1m$(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
Scanning [1m$(CAKEMLDIR)/developers[0m
Scanning [1m$(CAKEMLDIR)/misc[0m
Scanning [1m$(CAKEMLDIR)/semantics/ffi[0m
Scanning [1m$(CAKEMLDIR)/semantics[0m
Scanning [1m$(CAKEMLDIR)/basis/pure[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/pattern_matching[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/unverified/reg_alloc[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc[0m
Scanning [1m$(HOLDIR)/src/hol88[0m
Scanning [1m$(HOLDIR)/src/real[0m
Scanning [1m$(HOLDIR)/src/floating-point[0m
Scanning [1m$(HOLDIR)/src/monad/more_monads[0m
Scanning [1m$(HOLDIR)/src/update[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/common[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/asm[0m
Scanning [1m$(CAKEMLDIR)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/gc[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/reg_alloc/proofs[0m
Scanning [1m$(CAKEMLDIR)/semantics/alt_semantics[0m
Scanning [1m$(CAKEMLDIR)/semantics/alt_semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/semantics[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/proofs[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/lib[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/model[0m
Scanning [1m$(HOLDIR)/examples/machine-code/decompiler[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/x64[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/x64/prog[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/x64/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/x64/proofs[0m
Scanning [1m$(CAKEMLDIR)/basis[0m
Scanning [1m$(HOLDIR)/examples/bootstrap[0m
Scanning [1m$(CAKEMLDIR)/examples[0m
Scanning [1m$(CAKEMLDIR)/examples/pseudo_bool[0m
Scanning [1m$(CAKEMLDIR)/examples/lpr_checker[0m
Scanning [1m$(CAKEMLDIR)/examples/pseudo_bool/cnf_encoding[0m
Scanning [1m$(CAKEMLDIR)/examples/pseudo_bool/graph_encoding[0m
Scanning [1m$(CAKEMLDIR)/examples/pseudo_bool/array[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/ag32[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/ag32[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm7[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm7[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/arm8/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/arm8[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/arm8[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/mips/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/mips[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/mips[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/model[0m
Scanning [1m$(HOLDIR)/examples/l3-machine-code/riscv/step[0m
Scanning [1m$(CAKEMLDIR)/compiler/encoders/riscv[0m
Scanning [1m$(CAKEMLDIR)/compiler/backend/riscv[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular[0m
Scanning [1m$(HOLDIR)/src/transfer/examples[0m
Scanning [1m$(HOLDIR)/examples/algorithms/unification/triangular/first-order[0m
Scanning [1m$(CAKEMLDIR)/compiler/inference[0m
Scanning [1m$(CAKEMLDIR)/pancake[0m
Scanning [1m$(CAKEMLDIR)/pancake/parser[0m
Scanning [1m$(CAKEMLDIR)/compiler[0m
Scanning [1m$(CAKEMLDIR)/examples/pseudo_bool/array/compilation[0m
Scanned 92 directories
Starting work on README.md
Starting work on cliqueProofTheory
Starting work on cnfProofTheory
Starting work on mccisProofTheory
README.md                                                           (0s)     OK
Starting work on mcisProofTheory
cliqueProofTheory                                                  (81s)     OK
Starting work on npbc_fullProofTheory
mcisProofTheory                                                    (82s)     OK
Starting work on subgraph_isoProofTheory
cnfProofTheory                                                     (88s)     OK
mccisProofTheory                                                   (91s)     OK
npbc_fullProofTheory                                               (79s)FAIL<1>
       out = concl_to_string concl  sem_concl (set fml) obj concl))
 
 failed.
 Failed to prove theorem machine_code_sound.
 
 Exception raised at Q.EXISTS_TAC:
 goal not an exists (THEN1 on line 96)
 error in quse /scratch/cakeml/regression/cakeml-2277/examples/pseudo_bool/array/compilation/proofs/npbc_fullProofScript.sml : HOL_ERR {message = "goal not an exists (THEN1 on line 96)", origin_function = "EXISTS_TAC", origin_structure = "Q"}
 error in load /scratch/cakeml/regression/cakeml-2277/examples/pseudo_bool/array/compilation/proofs/npbc_fullProofScript : HOL_ERR {message = "goal not an exists (THEN1 on line 96)", origin_function = "EXISTS_TAC", origin_structure = "Q"}
 Uncaught exception: HOL_ERR {message = "goal not an exists (THEN1 on line 96)", origin_function = "EXISTS_TAC", origin_structure = "Q"}
subgraph_isoProofTheory                                            (80s)MKILLED