Job 2548

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:37990a0757640901f13b89fb0114ac3aa2d5e064
  Fix issues simplifying and evaluating {NUM,INT}_{FLOOR,CEILING} [Aug 06 07:52:03]
Machine:lammmington

Aug 12 08:20:15 Claimed job
Aug 12 08:20:19 Reusing HOL
Aug 12 08:20:30 Starting developers
Aug 12 08:20:34 Finished developers                                               2s 243MB
Aug 12 08:20:35 Starting developers/bin
Aug 12 08:20:45 Finished developers/bin                                           9s   1GB
Aug 12 08:20:46 Starting compiler/proofs
Aug 12 10:14:39 Finished compiler/proofs                                    1h53m52s  43GB
Aug 12 10:14:40 Starting compiler/bootstrap/translation
Aug 12 19:00:27 Finished compiler/bootstrap/translation                     8h45m45s  58GB
Aug 12 19:00:28 Starting semantics/ffi
Aug 12 19:00:37 Finished semantics/ffi                                            7s 657MB
Aug 12 19:00:38 Starting semantics
Aug 12 19:00:39 Finished semantics                                                0s  65MB
Aug 12 19:00:40 Starting semantics/proofs
Aug 12 19:01:16 Finished semantics/proofs                                        35s   2GB
Aug 12 19:01:17 Starting semantics/alt_semantics
Aug 12 19:02:06 Finished semantics/alt_semantics                                 47s   1GB
Aug 12 19:02:07 Starting semantics/alt_semantics/proofs
Aug 12 19:13:18 Finished semantics/alt_semantics/proofs                       11m09s   5GB
Aug 12 19:13:19 Starting basis/pure
Aug 12 19:13:20 Finished basis/pure                                               0s  76MB
Aug 12 19:13:21 Starting translator
Aug 12 19:15:07 Finished translator                                            1m45s   3GB
Aug 12 19:15:08 Starting compiler/parsing
Aug 12 19:15:09 Finished compiler/parsing                                         0s  73MB
Aug 12 19:15:10 Starting characteristic
Aug 12 19:15:12 Finished characteristic                                           0s  90MB
Aug 12 19:15:13 Starting translator/monadic
Aug 12 19:15:14 Finished translator/monadic                                       0s 101MB
Aug 12 19:15:15 Starting basis
Aug 12 19:17:56 Finished basis                                                 2m39s  10GB
Aug 12 19:17:57 Starting compiler/inference
Aug 12 19:17:58 Finished compiler/inference                                       0s  94MB
Aug 12 19:17:59 Starting compiler/backend/reg_alloc
Aug 12 19:18:01 Finished compiler/backend/reg_alloc                               0s  69MB
Aug 12 19:18:01 Starting compiler/backend/gc
Aug 12 19:18:03 Finished compiler/backend/gc                                      0s 138MB
Aug 12 19:18:04 Starting compiler/backend
Aug 12 19:18:25 Finished compiler/backend                                        19s   1GB
Aug 12 19:18:26 Starting compiler/encoders/asm
Aug 12 19:18:27 Finished compiler/encoders/asm                                    0s  90MB
Aug 12 19:18:28 Starting compiler/encoders/x64
Aug 12 19:18:29 Finished compiler/encoders/x64                                    0s 103MB
Aug 12 19:18:30 Starting compiler/encoders/arm7
Aug 12 19:18:32 Finished compiler/encoders/arm7                                   0s 102MB
Aug 12 19:18:33 Starting compiler/encoders/arm8
Aug 12 19:18:34 Finished compiler/encoders/arm8                                   0s 102MB
Aug 12 19:18:35 Starting compiler/encoders/arm8_asl
Aug 12 19:20:48 Finished compiler/encoders/arm8_asl                            2m11s   1GB
Aug 12 19:20:48 Starting compiler/encoders/mips
Aug 12 19:20:50 Finished compiler/encoders/mips                                   0s 103MB
Aug 12 19:20:51 Starting compiler/encoders/riscv
Aug 12 19:20:52 Finished compiler/encoders/riscv                                  0s 102MB
Aug 12 19:20:53 Starting compiler/encoders/ag32
Aug 12 19:20:55 Finished compiler/encoders/ag32                                   0s  99MB
Aug 12 19:20:56 Starting compiler/backend/x64
Aug 12 19:20:57 Finished compiler/backend/x64                                     0s 143MB
Aug 12 19:20:58 Starting compiler/backend/arm7
Aug 12 19:21:00 Finished compiler/backend/arm7                                    0s 137MB
Aug 12 19:21:01 Starting compiler/backend/arm8
Aug 12 19:21:03 Finished compiler/backend/arm8                                    0s 137MB
Aug 12 19:21:04 Starting compiler/backend/mips
Aug 12 19:21:06 Finished compiler/backend/mips                                    0s 137MB
Aug 12 19:21:06 Starting compiler/backend/riscv
Aug 12 19:21:08 Finished compiler/backend/riscv                                   0s 137MB
Aug 12 19:21:09 Starting compiler/backend/ag32
Aug 12 19:22:29 Finished compiler/backend/ag32                                 1m19s   2GB
Aug 12 19:22:30 Starting compiler/parsing/proofs
Aug 12 19:22:31 Finished compiler/parsing/proofs                                  0s  78MB
Aug 12 19:22:32 Starting compiler/inference/proofs
Aug 12 19:22:34 Finished compiler/inference/proofs                                0s  95MB
Aug 12 19:22:35 Starting compiler/backend/semantics
Aug 12 19:26:27 Finished compiler/backend/semantics                            3m51s   3GB
Aug 12 19:26:28 Starting compiler/backend/reg_alloc/proofs
Aug 12 19:26:29 Finished compiler/backend/reg_alloc/proofs                        0s  97MB
Aug 12 19:26:30 Starting compiler/backend/proofs
Aug 12 19:27:35 Finished compiler/backend/proofs                               1m03s   3GB
Aug 12 19:27:36 Starting compiler/backend/serialiser
Aug 12 19:27:38 Finished compiler/backend/serialiser                              0s 146MB
Aug 12 19:27:39 Starting compiler/encoders/x64/proofs
Aug 12 19:37:06 Finished compiler/encoders/x64/proofs                          9m26s   5GB
Aug 12 19:37:06 Starting compiler/encoders/arm7/proofs
Aug 12 19:49:44 Finished compiler/encoders/arm7/proofs                        12m36s   8GB
Aug 12 19:49:45 Starting compiler/encoders/arm8/proofs
Aug 12 19:56:16 Finished compiler/encoders/arm8/proofs                         6m29s   6GB
Aug 12 19:56:17 Starting compiler/encoders/arm8_asl/proofs
Aug 12 20:10:34 Finished compiler/encoders/arm8_asl/proofs                    14m15s   4GB
Aug 12 20:10:34 Starting compiler/encoders/mips/proofs
Aug 12 20:20:34 Finished compiler/encoders/mips/proofs                         9m58s   7GB
Aug 12 20:20:35 Starting compiler/encoders/riscv/proofs
Aug 12 20:29:05 Finished compiler/encoders/riscv/proofs                        8m29s   5GB
Aug 12 20:29:06 Starting compiler/encoders/ag32/proofs
Aug 12 20:31:28 Finished compiler/encoders/ag32/proofs                         2m21s   2GB
Aug 12 20:31:29 Starting compiler/backend/x64/proofs
Aug 12 20:32:13 Finished compiler/backend/x64/proofs                             42s   3GB
Aug 12 20:32:14 Starting compiler/backend/arm7/proofs
Aug 12 20:32:58 Finished compiler/backend/arm7/proofs                            43s   2GB
Aug 12 20:32:59 Starting compiler/backend/arm8/proofs
Aug 12 20:33:43 Finished compiler/backend/arm8/proofs                            43s   3GB
Aug 12 20:33:44 Starting compiler/backend/arm8_asl
Aug 12 20:34:14 Finished compiler/backend/arm8_asl                               29s   2GB
Aug 12 20:34:15 Starting compiler/backend/mips/proofs
Aug 12 20:35:02 Finished compiler/backend/mips/proofs                            45s   3GB
Aug 12 20:35:02 Starting compiler/backend/riscv/proofs
Aug 12 20:35:55 Finished compiler/backend/riscv/proofs                           51s   4GB
Aug 12 20:35:56 Starting compiler/backend/ag32/proofs
Aug 12 20:50:20 Finished compiler/backend/ag32/proofs                         14m23s   7GB
Aug 12 20:50:21 Starting compiler/backend/cv_compute
Aug 12 20:52:07 Finished compiler/backend/cv_compute                           1m44s   3GB
Aug 12 20:52:07 Starting cv_translator
Aug 12 21:11:29 Finished cv_translator                                        19m20s  10GB
Aug 12 21:11:30 Starting candle/set-theory
Aug 12 21:12:18 Finished candle/set-theory                                       47s   1GB
Aug 12 21:12:19 Starting candle/syntax-lib
Aug 12 21:12:20 Finished candle/syntax-lib                                        0s  75MB
Aug 12 21:12:21 Starting candle/standard/syntax
Aug 12 21:12:40 Finished candle/standard/syntax                                  18s   1GB
Aug 12 21:12:41 Starting candle/standard/semantics
Aug 12 21:15:23 Finished candle/standard/semantics                             2m40s   3GB
Aug 12 21:15:23 Starting candle/standard/monadic
Aug 12 21:15:25 Finished candle/standard/monadic                                  0s  99MB
Aug 12 21:15:26 Starting candle/standard/ml_kernel
Aug 12 21:17:28 Finished candle/standard/ml_kernel                             2m01s   5GB
Aug 12 21:17:29 Starting candle/overloading/syntax
Aug 12 21:21:08 Finished candle/overloading/syntax                             3m37s   2GB
Aug 12 21:21:09 Starting candle/overloading/semantics
Aug 12 21:32:39 Finished candle/overloading/semantics                         11m29s   5GB
Aug 12 21:32:40 Starting candle/overloading/monadic
Aug 12 21:35:16 Finished candle/overloading/monadic                            2m34s   2GB
Aug 12 21:35:17 Starting candle/overloading/ml_kernel
Aug 12 21:43:11 Finished candle/overloading/ml_kernel                          7m53s   6GB
Aug 12 21:43:12 Starting candle/overloading/ml_checker
Aug 12 21:45:53 Finished candle/overloading/ml_checker                         2m39s   7GB
Aug 12 21:45:54 Starting candle/prover
Aug 12 21:56:16 Finished candle/prover                                        10m20s   5GB
Aug 12 21:56:16 Starting pancake
Aug 12 21:57:23 Finished pancake                                               1m06s   1GB
Aug 12 21:57:24 Starting pancake/ffi
Aug 12 21:57:25 Finished pancake/ffi                                              0s  22MB
Aug 12 21:57:26 Starting pancake/semantics
Aug 12 22:00:09 Finished pancake/semantics                                     2m42s   3GB
Aug 12 22:00:10 Starting pancake/parser
Aug 12 22:00:46 Finished pancake/parser                                          35s   2GB
Aug 12 22:00:47 Starting pancake/proofs
Aug 12 22:16:43 Finished pancake/proofs                                       15m55s   8GB
Aug 12 22:16:44 Starting characteristic/examples
Aug 12 22:18:23 Finished characteristic/examples                               1m37s   6GB
Aug 12 22:18:24 Starting tutorial/solutions
Aug 12 22:21:08 Finished tutorial/solutions                                    2m43s   5GB
Aug 12 22:21:08 Starting translator/monadic/examples
Aug 12 22:25:07 Finished translator/monadic/examples                           3m57s   5GB
Aug 12 22:25:08 Starting examples
Aug 12 22:39:45 Finished examples                                             14m36s   8GB
Aug 12 22:39:46 Starting examples/compilation/x64
Aug 12 22:49:22 Finished examples/compilation/x64                              9m34s   8GB
Aug 12 22:49:23 Starting examples/compilation/x64/proofs
Aug 12 22:54:04 Finished examples/compilation/x64/proofs                       4m40s   9GB
Aug 12 22:54:05 Starting examples/compilation/ag32
Aug 12 22:56:48 Finished examples/compilation/ag32                             2m41s   5GB
Aug 12 22:56:48 Starting examples/compilation/ag32/proofs
Aug 12 22:58:31 Finished examples/compilation/ag32/proofs                      1m41s  10GB
Aug 12 22:58:32 Starting examples/compilation/to_word
Aug 12 23:02:29 Finished examples/compilation/to_word                          3m56s  13GB
Aug 12 23:02:30 Starting examples/lpr_checker
Aug 12 23:03:49 Finished examples/lpr_checker                                  1m18s   2GB
Aug 12 23:03:50 Starting examples/lpr_checker/array
Aug 12 23:32:45 Finished examples/lpr_checker/array                           28m54s  11GB
Aug 12 23:32:46 Starting examples/lpr_checker/array/compilation
Aug 12 23:35:18 Finished examples/lpr_checker/array/compilation                2m30s  10GB
Aug 12 23:35:19 Starting examples/lpr_checker/array/compilation/proofs
Aug 12 23:37:20 Finished examples/lpr_checker/array/compilation/proofs         2m00s   8GB
Aug 12 23:37:21 Starting examples/lpr_checker/array/compilation/proofsARM8
Aug 12 23:39:07 Finished examples/lpr_checker/array/compilation/proofsARM8     1m45s   8GB
Aug 12 23:39:08 Starting examples/xlrup_checker
Aug 12 23:40:22 Finished examples/xlrup_checker                                1m12s   2GB
Aug 12 23:40:23 Starting examples/xlrup_checker/array
Aug 12 23:55:42 Finished examples/xlrup_checker/array                         15m18s   9GB
Aug 12 23:55:43 Starting examples/xlrup_checker/array/compilation
Aug 12 23:57:07 Finished examples/xlrup_checker/array/compilation              1m23s   6GB
Aug 12 23:57:08 Starting examples/xlrup_checker/array/compilation/proofs
Aug 12 23:58:48 Finished examples/xlrup_checker/array/compilation/proofs       1m39s   7GB
Aug 12 23:58:49 Starting examples/pseudo_bool
Aug 13 00:00:59 Finished examples/pseudo_bool                                  2m09s   2GB
Aug 13 00:01:01 Starting examples/pseudo_bool/cnf_encoding
Aug 13 00:01:40 Finished examples/pseudo_bool/cnf_encoding                       38s   1GB
Aug 13 00:01:41 Starting examples/pseudo_bool/graph_encoding
Aug 13 00:02:38 Finished examples/pseudo_bool/graph_encoding                     55s   1GB
Aug 13 00:02:39 Starting examples/pseudo_bool/array
Aug 13 01:10:01 Finished examples/pseudo_bool/array                         1h07m20s  42GB
Aug 13 01:10:01 Starting examples/pseudo_bool/array/compilation
Aug 13 01:23:16 Finished examples/pseudo_bool/array/compilation               13m13s  28GB
Aug 13 01:23:16 Starting examples/pseudo_bool/array/compilation/proofs
Aug 13 01:27:20 Finished examples/pseudo_bool/array/compilation/proofs         4m03s   9GB
Aug 13 01:27:21 Starting examples/pseudo_bool/array/compilation/proofsARM8
Aug 13 01:29:12 Finished examples/pseudo_bool/array/compilation/proofsARM8     1m49s   9GB
Aug 13 01:29:13 Starting examples/opentheory
Aug 13 01:37:25 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                                                       (27s)     OK
Starting work on readerTheory
readerTheory                                                       (62s)     OK
Starting work on reader_initTheory
reader_initTheory                                                  (34s)     OK
Starting work on readerProofTheory
readerProofTheory                                                  (73s)     OK
Starting work on reader_commonProgTheory
Starting work on readerSoundnessTheory
readerSoundnessTheory                                              (29s)     OK
reader_commonProgTheory                                           (267s)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/regression2/cakeml-2548/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/regression2/cakeml-2548/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"}