Job 2554

CakeML:8620f3df78d7960734a2f98b4264564047077b81
  Update cc calls in makefiles [Aug 10 13:40:56]
#1032 (new-double-ffi)
Merging into:a61f2812e286bddf33d858448ec9dd5d671bbfcb
  Merge pull request #1025 from talsewell/word_simp_separated_if [Aug 12 08:13:37]
HOL:201b9451bbb6cc11025a8c71b859f6249529084a
  Change addUDEdge to take set of nodes as edge argument [Aug 14 10:39:41]
Machine:pavlova

Aug 15 03:41:14 Claimed job
Aug 15 03:41:26 Building HOL
Aug 15 03:55:43 Starting developers
Aug 15 03:55:46 Finished developers                                               2s 186MB
Aug 15 03:55:47 Starting developers/bin
Aug 15 03:56:01 Finished developers/bin                                          12s   1GB
Aug 15 03:56:02 Starting compiler/proofs
Aug 15 05:53:58 Finished compiler/proofs                                    1h57m55s  38GB
Aug 15 05:53:59 Starting compiler/bootstrap/translation
Aug 15 14:39:35 Finished compiler/bootstrap/translation                     8h45m35s  60GB
Aug 15 14:39:36 Starting semantics/ffi
Aug 15 14:39:44 Finished semantics/ffi                                            7s 631MB
Aug 15 14:39:45 Starting semantics
Aug 15 14:39:46 Finished semantics                                                0s  62MB
Aug 15 14:39:47 Starting semantics/proofs
Aug 15 14:40:26 Finished semantics/proofs                                        38s   2GB
Aug 15 14:40:27 Starting semantics/alt_semantics
Aug 15 14:41:17 Finished semantics/alt_semantics                                 48s   1GB
Aug 15 14:41:18 Starting semantics/alt_semantics/proofs
Aug 15 14:52:37 Finished semantics/alt_semantics/proofs                       11m18s   6GB
Aug 15 14:52:38 Starting basis/pure
Aug 15 14:52:39 Finished basis/pure                                               0s  71MB
Aug 15 14:52:40 Starting translator
Aug 15 14:54:28 Finished translator                                            1m47s   4GB
Aug 15 14:54:29 Starting compiler/parsing
Aug 15 14:54:31 Finished compiler/parsing                                         0s  73MB
Aug 15 14:54:32 Starting characteristic
Aug 15 14:54:33 Finished characteristic                                           0s  90MB
Aug 15 14:54:34 Starting translator/monadic
Aug 15 14:54:36 Finished translator/monadic                                       0s 102MB
Aug 15 14:54:36 Starting basis
Aug 15 14:57:10 Finished basis                                                 2m32s   5GB
Aug 15 14:57:11 Starting compiler/inference
Aug 15 14:57:12 Finished compiler/inference                                       0s  94MB
Aug 15 14:57:13 Starting compiler/backend/reg_alloc
Aug 15 14:57:15 Finished compiler/backend/reg_alloc                               0s  69MB
Aug 15 14:57:15 Starting compiler/backend/gc
Aug 15 14:57:17 Finished compiler/backend/gc                                      0s 147MB
Aug 15 14:57:18 Starting compiler/backend
Aug 15 14:57:39 Finished compiler/backend                                        19s   1GB
Aug 15 14:57:39 Starting compiler/encoders/asm
Aug 15 14:57:41 Finished compiler/encoders/asm                                    0s  91MB
Aug 15 14:57:42 Starting compiler/encoders/x64
Aug 15 14:57:43 Finished compiler/encoders/x64                                    0s 104MB
Aug 15 14:57:44 Starting compiler/encoders/arm7
Aug 15 14:57:46 Finished compiler/encoders/arm7                                   0s 103MB
Aug 15 14:57:47 Starting compiler/encoders/arm8
Aug 15 14:57:48 Finished compiler/encoders/arm8                                   0s 104MB
Aug 15 14:57:49 Starting compiler/encoders/arm8_asl
Aug 15 17:16:52 Finished compiler/encoders/arm8_asl                         2h19m02s  43GB
Aug 15 17:16:53 Starting compiler/encoders/mips
Aug 15 17:16:54 Finished compiler/encoders/mips                                   0s 104MB
Aug 15 17:16:55 Starting compiler/encoders/riscv
Aug 15 17:16:57 Finished compiler/encoders/riscv                                  0s 104MB
Aug 15 17:16:58 Starting compiler/encoders/ag32
Aug 15 17:16:59 Finished compiler/encoders/ag32                                   0s  92MB
Aug 15 17:17:00 Starting compiler/backend/x64
Aug 15 17:17:02 Finished compiler/backend/x64                                     0s 139MB
Aug 15 17:17:03 Starting compiler/backend/arm7
Aug 15 17:17:05 Finished compiler/backend/arm7                                    0s 139MB
Aug 15 17:17:05 Starting compiler/backend/arm8
Aug 15 17:17:07 Finished compiler/backend/arm8                                    0s 139MB
Aug 15 17:17:08 Starting compiler/backend/mips
Aug 15 17:17:10 Finished compiler/backend/mips                                    0s 138MB
Aug 15 17:17:11 Starting compiler/backend/riscv
Aug 15 17:17:13 Finished compiler/backend/riscv                                   0s 139MB
Aug 15 17:17:14 Starting compiler/backend/ag32
Aug 15 17:18:34 Finished compiler/backend/ag32                                 1m19s   2GB
Aug 15 17:18:35 Starting compiler/parsing/proofs
Aug 15 17:18:36 Finished compiler/parsing/proofs                                  0s  74MB
Aug 15 17:18:37 Starting compiler/inference/proofs
Aug 15 17:18:39 Finished compiler/inference/proofs                                0s  92MB
Aug 15 17:18:40 Starting compiler/backend/semantics
Aug 15 17:22:31 Finished compiler/backend/semantics                            3m50s   3GB
Aug 15 17:22:32 Starting compiler/backend/reg_alloc/proofs
Aug 15 17:22:34 Finished compiler/backend/reg_alloc/proofs                        0s  94MB
Aug 15 17:22:35 Starting compiler/backend/proofs
Aug 15 17:23:41 Finished compiler/backend/proofs                               1m05s   3GB
Aug 15 17:23:42 Starting compiler/backend/serialiser
Aug 15 17:23:44 Finished compiler/backend/serialiser                              0s 141MB
Aug 15 17:23:45 Starting compiler/encoders/x64/proofs
Aug 15 17:33:14 Finished compiler/encoders/x64/proofs                          9m28s   5GB
Aug 15 17:33:15 Starting compiler/encoders/arm7/proofs
Aug 15 17:46:05 Finished compiler/encoders/arm7/proofs                        12m49s  10GB
Aug 15 17:46:06 Starting compiler/encoders/arm8/proofs
Aug 15 17:52:42 Finished compiler/encoders/arm8/proofs                         6m35s   5GB
Aug 15 17:52:43 Starting compiler/encoders/arm8_asl/proofs
Aug 15 18:40:17 Finished compiler/encoders/arm8_asl/proofs                    47m33s  10GB
Aug 15 18:40:18 Starting compiler/encoders/mips/proofs
Aug 15 18:50:24 Finished compiler/encoders/mips/proofs                        10m04s   7GB
Aug 15 18:50:24 Starting compiler/encoders/riscv/proofs
Aug 15 18:58:59 Finished compiler/encoders/riscv/proofs                        8m33s   3GB
Aug 15 18:59:00 Starting compiler/encoders/ag32/proofs
Aug 15 19:01:24 Finished compiler/encoders/ag32/proofs                         2m23s   2GB
Aug 15 19:01:25 Starting compiler/backend/x64/proofs
Aug 15 19:02:08 Finished compiler/backend/x64/proofs                             42s   2GB
Aug 15 19:02:09 Starting compiler/backend/arm7/proofs
Aug 15 19:02:56 Finished compiler/backend/arm7/proofs                            46s   3GB
Aug 15 19:02:57 Starting compiler/backend/arm8/proofs
Aug 15 19:03:40 Finished compiler/backend/arm8/proofs                            41s   3GB
Aug 15 19:03:41 Starting compiler/backend/arm8_asl
Aug 15 19:04:11 Finished compiler/backend/arm8_asl                               28s   2GB
Aug 15 19:04:11 Starting compiler/backend/mips/proofs
Aug 15 19:04:58 Finished compiler/backend/mips/proofs                            45s   3GB
Aug 15 19:04:59 Starting compiler/backend/riscv/proofs
Aug 15 19:05:53 Finished compiler/backend/riscv/proofs                           53s   3GB
Aug 15 19:05:54 Starting compiler/backend/ag32/proofs
Aug 15 19:20:13 Finished compiler/backend/ag32/proofs                         14m17s   6GB
Aug 15 19:20:13 Starting compiler/backend/cv_compute
Aug 15 19:21:56 Finished compiler/backend/cv_compute                           1m41s   3GB
Aug 15 19:21:57 Starting cv_translator
Aug 15 19:41:18 Finished cv_translator                                        19m19s  12GB
Aug 15 19:41:19 Starting candle/set-theory
Aug 15 19:42:05 Finished candle/set-theory                                       45s   1GB
Aug 15 19:42:06 Starting candle/syntax-lib
Aug 15 19:42:07 Finished candle/syntax-lib                                        0s  76MB
Aug 15 19:42:08 Starting candle/standard/syntax
Aug 15 19:42:26 Finished candle/standard/syntax                                  17s   1GB
Aug 15 19:42:27 Starting candle/standard/semantics
Aug 15 19:45:07 Finished candle/standard/semantics                             2m38s   3GB
Aug 15 19:45:08 Starting candle/standard/monadic
Aug 15 19:45:09 Finished candle/standard/monadic                                  0s 108MB
Aug 15 19:45:10 Starting candle/standard/ml_kernel
Aug 15 19:47:09 Finished candle/standard/ml_kernel                             1m57s   5GB
Aug 15 19:47:09 Starting candle/overloading/syntax
Aug 15 19:50:38 Finished candle/overloading/syntax                             3m27s   2GB
Aug 15 19:50:39 Starting candle/overloading/semantics
Aug 15 20:02:07 Finished candle/overloading/semantics                         11m27s   4GB
Aug 15 20:02:08 Starting candle/overloading/monadic
Aug 15 20:04:42 Finished candle/overloading/monadic                            2m33s   2GB
Aug 15 20:04:43 Starting candle/overloading/ml_kernel
Aug 15 20:12:32 Finished candle/overloading/ml_kernel                          7m48s   6GB
Aug 15 20:12:33 Starting candle/overloading/ml_checker
Aug 15 20:15:12 Finished candle/overloading/ml_checker                         2m37s   7GB
Aug 15 20:15:13 Starting candle/prover
Aug 15 20:25:32 Finished candle/prover                                        10m17s   6GB
Aug 15 20:25:33 Starting pancake
Aug 15 20:26:41 Finished pancake                                               1m07s   1GB
Aug 15 20:26:42 Starting pancake/ffi
Aug 15 20:26:43 Finished pancake/ffi                                              0s  23MB
Aug 15 20:26:44 Starting pancake/semantics
Aug 15 20:29:31 Finished pancake/semantics                                     2m45s   2GB
Aug 15 20:29:31 Starting pancake/parser
Aug 15 20:30:07 Finished pancake/parser                                          34s   2GB
Aug 15 20:30:08 Starting pancake/proofs
Aug 15 20:46:11 Finished pancake/proofs                                       16m02s   6GB
Aug 15 20:46:12 Starting characteristic/examples
Aug 15 20:47:51 Finished characteristic/examples                               1m38s   6GB
Aug 15 20:47:52 Starting tutorial/solutions
Aug 15 20:50:38 Finished tutorial/solutions                                    2m44s   5GB
Aug 15 20:50:39 Starting translator/monadic/examples
Aug 15 20:54:40 Finished translator/monadic/examples                           4m00s   5GB
Aug 15 20:54:41 Starting examples
Aug 15 21:09:53 Finished examples                                             15m11s   9GB
Aug 15 21:09:54 Starting examples/compilation/x64
Aug 15 21:19:24 Finished examples/compilation/x64                              9m29s   8GB
Aug 15 21:19:25 Starting examples/compilation/x64/proofs
Aug 15 21:23:56 Finished examples/compilation/x64/proofs                       4m29s   7GB
Aug 15 21:23:57 Starting examples/compilation/ag32
Aug 15 21:26:40 Finished examples/compilation/ag32                             2m42s   5GB
Aug 15 21:26:40 Starting examples/compilation/ag32/proofs
Aug 15 21:28:30 Finished examples/compilation/ag32/proofs                      1m48s   8GB
Aug 15 21:28:31 Starting examples/compilation/to_word
Aug 15 21:32:39 Finished examples/compilation/to_word                          4m07s  14GB
Aug 15 21:32:40 Starting examples/lpr_checker
Aug 15 21:34:00 Finished examples/lpr_checker                                  1m18s   2GB
Aug 15 21:34:00 Starting examples/lpr_checker/array
Aug 15 22:03:22 Finished examples/lpr_checker/array                           29m20s  27GB
Aug 15 22:03:23 Starting examples/lpr_checker/array/compilation
Aug 15 22:05:57 Finished examples/lpr_checker/array/compilation                2m33s   9GB
Aug 15 22:05:58 Starting examples/lpr_checker/array/compilation/proofs
Aug 15 22:07:49 Finished examples/lpr_checker/array/compilation/proofs         1m50s   9GB
Aug 15 22:07:50 Starting examples/lpr_checker/array/compilation/proofsARM8
Aug 15 22:09:43 Finished examples/lpr_checker/array/compilation/proofsARM8     1m51s   9GB
Aug 15 22:09:44 Starting examples/xlrup_checker
Aug 15 22:10:59 Finished examples/xlrup_checker                                1m14s   2GB
Aug 15 22:11:00 Starting examples/xlrup_checker/array
Aug 15 22:26:18 Finished examples/xlrup_checker/array                         15m17s   9GB
Aug 15 22:26:19 Starting examples/xlrup_checker/array/compilation
Aug 15 22:27:45 Finished examples/xlrup_checker/array/compilation              1m24s   6GB
Aug 15 22:27:46 Starting examples/xlrup_checker/array/compilation/proofs
Aug 15 22:29:25 Finished examples/xlrup_checker/array/compilation/proofs       1m38s   8GB
Aug 15 22:29:26 Starting examples/pseudo_bool
Aug 15 22:31:39 Finished examples/pseudo_bool                                  2m11s   2GB
Aug 15 22:31:39 Starting examples/pseudo_bool/cnf_encoding
Aug 15 22:32:19 Finished examples/pseudo_bool/cnf_encoding                       38s   1GB
Aug 15 22:32:20 Starting examples/pseudo_bool/graph_encoding
Aug 15 22:33:13 Finished examples/pseudo_bool/graph_encoding                     52s   1GB
Aug 15 22:33:14 Starting examples/pseudo_bool/array
Aug 15 23:40:27 Finished examples/pseudo_bool/array                         1h07m12s  41GB
Aug 15 23:40:28 Starting examples/pseudo_bool/array/compilation
Aug 15 23:53:39 Finished examples/pseudo_bool/array/compilation               13m09s  28GB
Aug 15 23:53:40 Starting examples/pseudo_bool/array/compilation/proofs
Aug 15 23:57:45 Finished examples/pseudo_bool/array/compilation/proofs         4m04s  10GB
Aug 15 23:57:46 Starting examples/pseudo_bool/array/compilation/proofsARM8
Aug 16 00:00:43 Finished examples/pseudo_bool/array/compilation/proofsARM8     2m56s   9GB
Aug 16 00:00:44 Starting examples/opentheory
Aug 16 00:08:47 FAILED: examples/opentheory
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)/examples/balanced_bst
Scanning $(HOLDIR)/examples/formal-languages
Scanning $(HOLDIR)/examples/formal-languages/context-free
Scanning $(HOLDIR)/examples/formal-languages/regular
Scanning $(HOLDIR)/src/transfer
Scanning $(HOLDIR)/src/pred_set/src/more_theories
Scanning $(HOLDIR)/src/coalgebras
Scanning $(HOLDIR)/examples/fun-op-sem/lprefix_lub
Scanning $(HOLDIR)/examples/machine-code/hoare-triple
Scanning $(CAKEMLDIR)/developers
Scanning $(CAKEMLDIR)/misc
Scanning $(CAKEMLDIR)/semantics/ffi
Scanning $(CAKEMLDIR)/semantics
Scanning $(CAKEMLDIR)/basis/pure
Scanning $(CAKEMLDIR)/semantics/proofs
Scanning $(CAKEMLDIR)/compiler/parsing
Scanning $(CAKEMLDIR)/translator
Scanning $(CAKEMLDIR)/characteristic
Scanning $(CAKEMLDIR)/translator/monadic/monad_base
Scanning $(CAKEMLDIR)/translator/monadic
Scanning $(CAKEMLDIR)/basis
Scanning $(CAKEMLDIR)/candle/standard/ml_kernel/lisp
Scanning $(CAKEMLDIR)/candle/syntax-lib
Scanning $(CAKEMLDIR)/candle/standard/syntax
Scanning $(CAKEMLDIR)/candle/standard/monadic
Scanning $(CAKEMLDIR)/candle/standard/ml_kernel
Scanning $(CAKEMLDIR)/candle/set-theory
Scanning $(CAKEMLDIR)/candle/standard/semantics
Scanned 36 directories
Starting work on README.md
Starting work on prettyTheory
README.md                                                           (0s)     OK
prettyTheory                                                       (25s)     OK
Starting work on readerTheory
readerTheory                                                       (58s)     OK
Starting work on reader_initTheory
reader_initTheory                                                  (35s)     OK
Starting work on readerProofTheory
readerProofTheory                                                  (73s)     OK
Starting work on reader_commonProgTheory
Starting work on readerSoundnessTheory
readerSoundnessTheory                                              (30s)     OK
reader_commonProgTheory                                           (263s)FAIL<1>
      (Refv init_context_v)}
 
 failed.
 Failed to prove theorem HOL_STORE_init_precond.
 
 Exception raised at Q.MATCH_GOALSUB_ABBREV_TAC:
 No matching sub-term found (THEN1 on line 268)
 error in quse /scratch/cakeml/regression/cakeml-2554/examples/opentheory/reader_commonProgScript.sml : HOL_ERR {message = "No matching sub-term found (THEN1 on line 268)", origin_function = "MATCH_GOALSUB_ABBREV_TAC", origin_structure = "Q"}
 error in load /scratch/cakeml/regression/cakeml-2554/examples/opentheory/reader_commonProgScript : HOL_ERR {message = "No matching sub-term found (THEN1 on line 268)", origin_function = "MATCH_GOALSUB_ABBREV_TAC", origin_structure = "Q"}
 Uncaught exception: HOL_ERR {message = "No matching sub-term found (THEN1 on line 268)", origin_function = "MATCH_GOALSUB_ABBREV_TAC", origin_structure = "Q"}