Job 2275

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:4103c90e68aea21ac033b5e9205a8521e7a51b71
  FTBFS HolBdd and temporal_deep examples [Jan 17 23:33:26]
Machine:pavlova

Jan 20 18:22:28 Claimed job
Jan 20 18:22:33 Reusing HOL
Jan 20 18:22:43 Starting developers
Jan 20 18:22:47 Finished developers                                               2s 211MB
Jan 20 18:22:47 Starting developers/bin
Jan 20 18:22:58 Finished developers/bin                                           9s   1GB
Jan 20 18:22:59 Starting compiler/proofs
Jan 20 20:08:16 Finished compiler/proofs                                    1h45m15s  31GB
Jan 20 20:08:17 Starting compiler/bootstrap/translation
Jan 21 04:15:12 Finished compiler/bootstrap/translation                     8h06m54s  78GB
Jan 21 04:15:13 Starting semantics/ffi
Jan 21 04:15:21 Finished semantics/ffi                                            7s 582MB
Jan 21 04:15:22 Starting semantics
Jan 21 04:15:24 Finished semantics                                                0s  67MB
Jan 21 04:15:24 Starting semantics/proofs
Jan 21 04:16:00 Finished semantics/proofs                                        34s   2GB
Jan 21 04:16:01 Starting semantics/alt_semantics
Jan 21 04:16:41 Finished semantics/alt_semantics                                 38s   1GB
Jan 21 04:16:41 Starting semantics/alt_semantics/proofs
Jan 21 04:27:44 Finished semantics/alt_semantics/proofs                       11m01s   4GB
Jan 21 04:27:44 Starting basis/pure
Jan 21 04:27:46 Finished basis/pure                                               0s  66MB
Jan 21 04:27:47 Starting translator
Jan 21 04:29:28 Finished translator                                            1m40s   3GB
Jan 21 04:29:29 Starting compiler/parsing
Jan 21 04:29:30 Finished compiler/parsing                                         0s  73MB
Jan 21 04:29:31 Starting characteristic
Jan 21 04:29:33 Finished characteristic                                           0s  90MB
Jan 21 04:29:33 Starting translator/monadic
Jan 21 04:29:35 Finished translator/monadic                                       0s  99MB
Jan 21 04:29:36 Starting basis
Jan 21 04:33:18 Finished basis                                                 3m41s   6GB
Jan 21 04:33:19 Starting compiler/inference
Jan 21 04:33:20 Finished compiler/inference                                       0s  85MB
Jan 21 04:33:21 Starting compiler/backend/reg_alloc
Jan 21 04:33:22 Finished compiler/backend/reg_alloc                               0s  66MB
Jan 21 04:33:23 Starting compiler/backend/gc
Jan 21 04:33:25 Finished compiler/backend/gc                                      0s 138MB
Jan 21 04:33:26 Starting compiler/backend
Jan 21 04:33:44 Finished compiler/backend                                        17s   1GB
Jan 21 04:33:44 Starting compiler/encoders/asm
Jan 21 04:33:46 Finished compiler/encoders/asm                                    0s  91MB
Jan 21 04:33:47 Starting compiler/encoders/x64
Jan 21 04:33:48 Finished compiler/encoders/x64                                    0s  95MB
Jan 21 04:33:49 Starting compiler/encoders/arm7
Jan 21 04:33:50 Finished compiler/encoders/arm7                                   0s  95MB
Jan 21 04:33:51 Starting compiler/encoders/arm8
Jan 21 04:33:53 Finished compiler/encoders/arm8                                   0s  91MB
Jan 21 04:33:54 Starting compiler/encoders/arm8_asl
Jan 21 06:55:41 Finished compiler/encoders/arm8_asl                         2h21m46s  40GB
Jan 21 06:55:42 Starting compiler/encoders/mips
Jan 21 06:55:43 Finished compiler/encoders/mips                                   0s  87MB
Jan 21 06:55:44 Starting compiler/encoders/riscv
Jan 21 06:55:46 Finished compiler/encoders/riscv                                  0s  91MB
Jan 21 06:55:46 Starting compiler/encoders/ag32
Jan 21 06:55:48 Finished compiler/encoders/ag32                                   0s  85MB
Jan 21 06:55:49 Starting compiler/backend/x64
Jan 21 06:55:50 Finished compiler/backend/x64                                     0s 129MB
Jan 21 06:55:51 Starting compiler/backend/arm7
Jan 21 06:55:53 Finished compiler/backend/arm7                                    0s 129MB
Jan 21 06:55:54 Starting compiler/backend/arm8
Jan 21 06:55:56 Finished compiler/backend/arm8                                    0s 129MB
Jan 21 06:55:56 Starting compiler/backend/mips
Jan 21 06:55:58 Finished compiler/backend/mips                                    0s 129MB
Jan 21 06:55:59 Starting compiler/backend/riscv
Jan 21 06:56:01 Finished compiler/backend/riscv                                   0s 129MB
Jan 21 06:56:02 Starting compiler/backend/ag32
Jan 21 06:57:20 Finished compiler/backend/ag32                                 1m17s   2GB
Jan 21 06:57:20 Starting compiler/parsing/proofs
Jan 21 06:57:22 Finished compiler/parsing/proofs                                  0s  75MB
Jan 21 06:57:23 Starting compiler/inference/proofs
Jan 21 06:57:24 Finished compiler/inference/proofs                                0s  86MB
Jan 21 06:57:25 Starting compiler/backend/semantics
Jan 21 06:58:52 Finished compiler/backend/semantics                            1m25s   2GB
Jan 21 06:58:52 Starting compiler/backend/reg_alloc/proofs
Jan 21 06:58:54 Finished compiler/backend/reg_alloc/proofs                        0s  90MB
Jan 21 06:58:55 Starting compiler/backend/proofs
Jan 21 06:59:57 Finished compiler/backend/proofs                               1m00s   3GB
Jan 21 06:59:57 Starting compiler/backend/serialiser
Jan 21 07:00:00 Finished compiler/backend/serialiser                              1s 187MB
Jan 21 07:00:00 Starting compiler/encoders/x64/proofs
Jan 21 07:09:27 Finished compiler/encoders/x64/proofs                          9m25s   5GB
Jan 21 07:09:27 Starting compiler/encoders/arm7/proofs
Jan 21 07:22:07 Finished compiler/encoders/arm7/proofs                        12m38s   5GB
Jan 21 07:22:07 Starting compiler/encoders/arm8/proofs
Jan 21 07:28:50 Finished compiler/encoders/arm8/proofs                         6m41s   4GB
Jan 21 07:28:50 Starting compiler/encoders/arm8_asl/proofs
Jan 21 08:16:37 Finished compiler/encoders/arm8_asl/proofs                    47m45s  10GB
Jan 21 08:16:38 Starting compiler/encoders/mips/proofs
Jan 21 08:26:48 Finished compiler/encoders/mips/proofs                        10m08s   5GB
Jan 21 08:26:49 Starting compiler/encoders/riscv/proofs
Jan 21 08:35:17 Finished compiler/encoders/riscv/proofs                        8m28s   5GB
Jan 21 08:35:18 Starting compiler/encoders/ag32/proofs
Jan 21 08:37:40 Finished compiler/encoders/ag32/proofs                         2m20s   2GB
Jan 21 08:37:40 Starting compiler/backend/x64/proofs
Jan 21 08:38:22 Finished compiler/backend/x64/proofs                             40s   3GB
Jan 21 08:38:23 Starting compiler/backend/arm7/proofs
Jan 21 08:39:08 Finished compiler/backend/arm7/proofs                            44s   2GB
Jan 21 08:39:09 Starting compiler/backend/arm8/proofs
Jan 21 08:39:48 Finished compiler/backend/arm8/proofs                            38s   3GB
Jan 21 08:39:49 Starting compiler/backend/arm8_asl
Jan 21 08:40:18 Finished compiler/backend/arm8_asl                               28s   2GB
Jan 21 08:40:19 Starting compiler/backend/mips/proofs
Jan 21 08:41:04 Finished compiler/backend/mips/proofs                            44s   3GB
Jan 21 08:41:05 Starting compiler/backend/riscv/proofs
Jan 21 08:41:55 Finished compiler/backend/riscv/proofs                           49s   4GB
Jan 21 08:41:56 Starting compiler/backend/ag32/proofs
Jan 21 08:55:31 Finished compiler/backend/ag32/proofs                         13m33s   5GB
Jan 21 08:55:32 Starting candle/set-theory
Jan 21 08:56:15 Finished candle/set-theory                                       42s   1GB
Jan 21 08:56:16 Starting candle/syntax-lib
Jan 21 08:56:17 Finished candle/syntax-lib                                        0s  67MB
Jan 21 08:56:18 Starting candle/standard/syntax
Jan 21 08:56:34 Finished candle/standard/syntax                                  14s   1GB
Jan 21 08:56:34 Starting candle/standard/semantics
Jan 21 08:58:55 Finished candle/standard/semantics                             2m19s   2GB
Jan 21 08:58:56 Starting candle/standard/monadic
Jan 21 08:58:58 Finished candle/standard/monadic                                  0s 104MB
Jan 21 08:58:59 Starting candle/standard/ml_kernel
Jan 21 09:00:49 Finished candle/standard/ml_kernel                             1m48s   4GB
Jan 21 09:00:49 Starting candle/overloading/syntax
Jan 21 09:04:14 Finished candle/overloading/syntax                             3m23s   2GB
Jan 21 09:04:15 Starting candle/overloading/semantics
Jan 21 09:15:35 Finished candle/overloading/semantics                         11m19s   5GB
Jan 21 09:15:36 Starting candle/overloading/monadic
Jan 21 09:18:11 Finished candle/overloading/monadic                            2m32s   3GB
Jan 21 09:18:12 Starting candle/overloading/ml_kernel
Jan 21 09:25:41 Finished candle/overloading/ml_kernel                          7m28s   6GB
Jan 21 09:25:42 Starting candle/overloading/ml_checker
Jan 21 09:28:15 Finished candle/overloading/ml_checker                         2m31s   7GB
Jan 21 09:28:16 Starting candle/prover
Jan 21 09:38:04 Finished candle/prover                                         9m47s   5GB
Jan 21 09:38:05 Starting pancake
Jan 21 09:39:05 Finished pancake                                                 59s   1GB
Jan 21 09:39:06 Starting pancake/ffi
Jan 21 09:39:07 Finished pancake/ffi                                              0s  20MB
Jan 21 09:39:08 Starting pancake/semantics
Jan 21 09:41:28 Finished pancake/semantics                                     2m19s   2GB
Jan 21 09:41:29 Starting pancake/parser
Jan 21 09:41:55 Finished pancake/parser                                          25s   1GB
Jan 21 09:41:56 Starting pancake/proofs
Jan 21 10:11:51 Finished pancake/proofs                                       29m54s   8GB
Jan 21 10:11:52 Starting characteristic/examples
Jan 21 10:13:27 Finished characteristic/examples                               1m34s   5GB
Jan 21 10:13:28 Starting tutorial/solutions
Jan 21 10:28:48 Finished tutorial/solutions                                   15m19s  11GB
Jan 21 10:28:49 Starting translator/monadic/examples
Jan 21 10:32:36 Finished translator/monadic/examples                           3m46s   5GB
Jan 21 10:32:37 Starting examples
Jan 21 10:47:06 Finished examples                                             14m28s   7GB
Jan 21 10:47:07 Starting examples/compilation/x64
Jan 21 12:44:07 Finished examples/compilation/x64                           1h56m58s  26GB
Jan 21 12:44:08 Starting examples/compilation/x64/proofs
Jan 21 12:47:56 Finished examples/compilation/x64/proofs                       3m46s   6GB
Jan 21 12:47:57 Starting examples/compilation/ag32
Jan 21 13:17:34 Finished examples/compilation/ag32                            29m36s  11GB
Jan 21 13:17:35 Starting examples/compilation/ag32/proofs
Jan 21 13:19:04 Finished examples/compilation/ag32/proofs                      1m28s   6GB
Jan 21 13:19:05 Starting examples/compilation/to_word
Jan 21 13:22:55 Finished examples/compilation/to_word                          3m49s  12GB
Jan 21 13:22:56 Starting examples/lpr_checker
Jan 21 13:24:14 Finished examples/lpr_checker                                  1m16s   2GB
Jan 21 13:24:14 Starting examples/lpr_checker/array
Jan 21 13:53:10 Finished examples/lpr_checker/array                           28m54s   8GB
Jan 21 13:53:11 Starting examples/lpr_checker/array/compilation
Jan 21 14:29:52 Finished examples/lpr_checker/array/compilation               36m39s  70GB
Jan 21 14:29:53 Starting examples/lpr_checker/array/compilation/proofs
Jan 21 14:31:45 Finished examples/lpr_checker/array/compilation/proofs         1m52s   9GB
Jan 21 14:31:46 Starting examples/lpr_checker/array/compilation/proofsARM8
Jan 21 14:53:20 Finished examples/lpr_checker/array/compilation/proofsARM8    21m32s  44GB
Jan 21 14:53:21 Starting examples/pseudo_bool
Jan 21 14:55:22 Finished examples/pseudo_bool                                  2m00s   2GB
Jan 21 14:55:23 Starting examples/pseudo_bool/cnf_encoding
Jan 21 14:56:00 Finished examples/pseudo_bool/cnf_encoding                       36s   1GB
Jan 21 14:56:01 Starting examples/pseudo_bool/graph_encoding
Jan 21 14:56:49 Finished examples/pseudo_bool/graph_encoding                     46s   1GB
Jan 21 14:56:49 Starting examples/pseudo_bool/array
Jan 21 15:50:36 Finished examples/pseudo_bool/array                           53m45s  10GB
Jan 21 15:50:37 Starting examples/pseudo_bool/array/compilation
Jan 21 17:57:29 Finished examples/pseudo_bool/array/compilation             2h06m50s 146GB
Jan 21 17:57:30 Starting examples/pseudo_bool/array/compilation/proofs
Jan 21 18:00:35 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                                                  (83s)     OK
Starting work on npbc_fullProofTheory
mcisProofTheory                                                    (86s)     OK
Starting work on subgraph_isoProofTheory
cnfProofTheory                                                     (86s)     OK
mccisProofTheory                                                   (89s)     OK
npbc_fullProofTheory                                               (80s)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-2275/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-2275/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                                            (76s)MKILLED