Job 2404

CakeML:dd0a848ec6f2a6564b26af03a443cb099ed625c9
  swap order of scripts [Jun 03 13:25:00]
#997 (pb-err)
Merging into:02337571365840ea3f5e1545b7ed3cda41684a8d
  Merge pull request #985 from CakeML/cvunify [Jun 03 08:35:49]
HOL:a1037385a92acdb9b8bb1f0c243fe6f1f6120eaf
  Fix examples/vector given changes in 562bb668f092d [Jun 03 00:48:36]
Machine:lammmington

Jun 05 06:31:25 Claimed job
Jun 05 06:31:34 Building HOL
Jun 05 06:47:12 Starting developers
Jun 05 06:47:16 Finished developers                                               2s 210MB
Jun 05 06:47:17 Starting developers/bin
Jun 05 06:47:33 Finished developers/bin                                          15s   1GB
Jun 05 06:47:34 Starting compiler/proofs
Jun 05 08:41:39 Finished compiler/proofs                                    1h54m03s  32GB
Jun 05 08:41:40 Starting compiler/bootstrap/translation
Jun 05 16:49:47 Finished compiler/bootstrap/translation                     8h08m06s  66GB
Jun 05 16:49:48 Starting semantics/ffi
Jun 05 16:49:57 Finished semantics/ffi                                            7s 738MB
Jun 05 16:49:58 Starting semantics
Jun 05 16:49:59 Finished semantics                                                0s  69MB
Jun 05 16:50:00 Starting semantics/proofs
Jun 05 16:50:37 Finished semantics/proofs                                        36s   2GB
Jun 05 16:50:38 Starting semantics/alt_semantics
Jun 05 16:51:19 Finished semantics/alt_semantics                                 39s   1GB
Jun 05 16:51:20 Starting semantics/alt_semantics/proofs
Jun 05 17:02:25 Finished semantics/alt_semantics/proofs                       11m04s   3GB
Jun 05 17:02:26 Starting basis/pure
Jun 05 17:02:28 Finished basis/pure                                               0s  70MB
Jun 05 17:02:28 Starting translator
Jun 05 17:04:19 Finished translator                                            1m49s   4GB
Jun 05 17:04:20 Starting compiler/parsing
Jun 05 17:04:21 Finished compiler/parsing                                         0s  70MB
Jun 05 17:04:22 Starting characteristic
Jun 05 17:04:23 Finished characteristic                                           0s  88MB
Jun 05 17:04:24 Starting translator/monadic
Jun 05 17:04:26 Finished translator/monadic                                       0s  96MB
Jun 05 17:04:27 Starting basis
Jun 05 17:08:01 Finished basis                                                 3m33s   5GB
Jun 05 17:08:02 Starting compiler/inference
Jun 05 17:08:04 Finished compiler/inference                                       1s 182MB
Jun 05 17:08:05 Starting compiler/backend/reg_alloc
Jun 05 17:08:06 Finished compiler/backend/reg_alloc                               0s  69MB
Jun 05 17:08:07 Starting compiler/backend/gc
Jun 05 17:08:09 Finished compiler/backend/gc                                      0s 138MB
Jun 05 17:08:10 Starting compiler/backend
Jun 05 17:08:30 Finished compiler/backend                                        19s   1GB
Jun 05 17:08:31 Starting compiler/encoders/asm
Jun 05 17:08:33 Finished compiler/encoders/asm                                    0s  89MB
Jun 05 17:08:34 Starting compiler/encoders/x64
Jun 05 17:08:35 Finished compiler/encoders/x64                                    0s 100MB
Jun 05 17:08:36 Starting compiler/encoders/arm7
Jun 05 17:08:38 Finished compiler/encoders/arm7                                   0s 101MB
Jun 05 17:08:39 Starting compiler/encoders/arm8
Jun 05 17:08:40 Finished compiler/encoders/arm8                                   0s 101MB
Jun 05 17:08:41 Starting compiler/encoders/arm8_asl
Jun 05 19:19:20 Finished compiler/encoders/arm8_asl                         2h10m37s  39GB
Jun 05 19:19:20 Starting compiler/encoders/mips
Jun 05 19:19:22 Finished compiler/encoders/mips                                   0s 103MB
Jun 05 19:19:23 Starting compiler/encoders/riscv
Jun 05 19:19:24 Finished compiler/encoders/riscv                                  0s  93MB
Jun 05 19:19:25 Starting compiler/encoders/ag32
Jun 05 19:19:27 Finished compiler/encoders/ag32                                   0s  96MB
Jun 05 19:19:28 Starting compiler/backend/x64
Jun 05 19:19:30 Finished compiler/backend/x64                                     0s 135MB
Jun 05 19:19:30 Starting compiler/backend/arm7
Jun 05 19:19:32 Finished compiler/backend/arm7                                    0s 135MB
Jun 05 19:19:33 Starting compiler/backend/arm8
Jun 05 19:19:35 Finished compiler/backend/arm8                                    0s 135MB
Jun 05 19:19:36 Starting compiler/backend/mips
Jun 05 19:19:38 Finished compiler/backend/mips                                    0s 135MB
Jun 05 19:19:39 Starting compiler/backend/riscv
Jun 05 19:19:40 Finished compiler/backend/riscv                                   0s 135MB
Jun 05 19:19:41 Starting compiler/backend/ag32
Jun 05 19:21:01 Finished compiler/backend/ag32                                 1m18s   2GB
Jun 05 19:21:02 Starting compiler/parsing/proofs
Jun 05 19:21:04 Finished compiler/parsing/proofs                                  0s  73MB
Jun 05 19:21:05 Starting compiler/inference/proofs
Jun 05 19:21:07 Finished compiler/inference/proofs                                1s 183MB
Jun 05 19:21:08 Starting compiler/backend/semantics
Jun 05 19:24:56 Finished compiler/backend/semantics                            3m47s   3GB
Jun 05 19:24:57 Starting compiler/backend/reg_alloc/proofs
Jun 05 19:24:59 Finished compiler/backend/reg_alloc/proofs                        0s  91MB
Jun 05 19:24:59 Starting compiler/backend/proofs
Jun 05 19:26:05 Finished compiler/backend/proofs                               1m04s   3GB
Jun 05 19:26:06 Starting compiler/backend/serialiser
Jun 05 19:26:08 Finished compiler/backend/serialiser                              0s 138MB
Jun 05 19:26:09 Starting compiler/encoders/x64/proofs
Jun 05 19:35:19 Finished compiler/encoders/x64/proofs                          9m09s   6GB
Jun 05 19:35:20 Starting compiler/encoders/arm7/proofs
Jun 05 19:48:05 Finished compiler/encoders/arm7/proofs                        12m43s   8GB
Jun 05 19:48:06 Starting compiler/encoders/arm8/proofs
Jun 05 19:54:37 Finished compiler/encoders/arm8/proofs                         6m30s   5GB
Jun 05 19:54:38 Starting compiler/encoders/arm8_asl/proofs
Jun 05 20:42:03 Finished compiler/encoders/arm8_asl/proofs                    47m23s  11GB
Jun 05 20:42:03 Starting compiler/encoders/mips/proofs
Jun 05 20:52:00 Finished compiler/encoders/mips/proofs                         9m55s   8GB
Jun 05 20:52:01 Starting compiler/encoders/riscv/proofs
Jun 05 21:00:40 Finished compiler/encoders/riscv/proofs                        8m38s   4GB
Jun 05 21:00:41 Starting compiler/encoders/ag32/proofs
Jun 05 21:03:06 Finished compiler/encoders/ag32/proofs                         2m24s   2GB
Jun 05 21:03:07 Starting compiler/backend/x64/proofs
Jun 05 21:03:51 Finished compiler/backend/x64/proofs                             43s   3GB
Jun 05 21:03:52 Starting compiler/backend/arm7/proofs
Jun 05 21:04:39 Finished compiler/backend/arm7/proofs                            45s   2GB
Jun 05 21:04:40 Starting compiler/backend/arm8/proofs
Jun 05 21:05:22 Finished compiler/backend/arm8/proofs                            41s   3GB
Jun 05 21:05:23 Starting compiler/backend/arm8_asl
Jun 05 21:05:52 Finished compiler/backend/arm8_asl                               27s   2GB
Jun 05 21:05:53 Starting compiler/backend/mips/proofs
Jun 05 21:06:39 Finished compiler/backend/mips/proofs                            45s   3GB
Jun 05 21:06:40 Starting compiler/backend/riscv/proofs
Jun 05 21:07:35 Finished compiler/backend/riscv/proofs                           53s   4GB
Jun 05 21:07:36 Starting compiler/backend/ag32/proofs
Jun 05 21:22:16 Finished compiler/backend/ag32/proofs                         14m38s   6GB
Jun 05 21:22:17 Starting compiler/backend/cv_compute
Jun 05 21:24:04 Finished compiler/backend/cv_compute                           1m46s   3GB
Jun 05 21:24:05 Starting cv_translator
Jun 05 21:33:35 Finished cv_translator                                         9m29s   9GB
Jun 05 21:33:36 Starting candle/set-theory
Jun 05 21:34:25 Finished candle/set-theory                                       48s   1GB
Jun 05 21:34:26 Starting candle/syntax-lib
Jun 05 21:34:27 Finished candle/syntax-lib                                        0s  72MB
Jun 05 21:34:28 Starting candle/standard/syntax
Jun 05 21:34:47 Finished candle/standard/syntax                                  18s   1GB
Jun 05 21:34:48 Starting candle/standard/semantics
Jun 05 21:37:29 Finished candle/standard/semantics                             2m40s   3GB
Jun 05 21:37:30 Starting candle/standard/monadic
Jun 05 21:37:32 Finished candle/standard/monadic                                  0s 107MB
Jun 05 21:37:32 Starting candle/standard/ml_kernel
Jun 05 21:39:27 Finished candle/standard/ml_kernel                             1m53s   5GB
Jun 05 21:39:28 Starting candle/overloading/syntax
Jun 05 21:43:07 Finished candle/overloading/syntax                             3m38s   2GB
Jun 05 21:43:08 Starting candle/overloading/semantics
Jun 05 21:54:42 Finished candle/overloading/semantics                         11m33s   7GB
Jun 05 21:54:43 Starting candle/overloading/monadic
Jun 05 21:57:18 Finished candle/overloading/monadic                            2m33s   3GB
Jun 05 21:57:19 Starting candle/overloading/ml_kernel
Jun 05 22:05:01 Finished candle/overloading/ml_kernel                          7m40s   7GB
Jun 05 22:05:02 Starting candle/overloading/ml_checker
Jun 05 22:07:36 Finished candle/overloading/ml_checker                         2m33s   7GB
Jun 05 22:07:37 Starting candle/prover
Jun 05 22:17:42 Finished candle/prover                                        10m03s   5GB
Jun 05 22:17:42 Starting pancake
Jun 05 22:18:49 Finished pancake                                               1m05s   1GB
Jun 05 22:18:50 Starting pancake/ffi
Jun 05 22:18:50 Finished pancake/ffi                                              0s  24MB
Jun 05 22:18:51 Starting pancake/semantics
Jun 05 22:21:37 Finished pancake/semantics                                     2m44s   2GB
Jun 05 22:21:38 Starting pancake/parser
Jun 05 22:22:10 Finished pancake/parser                                          31s   2GB
Jun 05 22:22:11 Starting pancake/proofs
Jun 05 22:53:14 Finished pancake/proofs                                       31m01s   9GB
Jun 05 22:53:15 Starting characteristic/examples
Jun 05 22:54:52 Finished characteristic/examples                               1m36s   6GB
Jun 05 22:54:53 Starting tutorial/solutions
Jun 05 23:10:17 Finished tutorial/solutions                                   15m23s  15GB
Jun 05 23:10:18 Starting translator/monadic/examples
Jun 05 23:14:14 Finished translator/monadic/examples                           3m54s   5GB
Jun 05 23:14:15 Starting examples
Jun 05 23:28:39 Finished examples                                             14m23s   8GB
Jun 05 23:28:40 Starting examples/compilation/x64
Jun 06 01:26:40 Finished examples/compilation/x64                           1h57m59s  23GB
Jun 06 01:26:41 Starting examples/compilation/x64/proofs
Jun 06 01:30:39 Finished examples/compilation/x64/proofs                       3m57s   6GB
Jun 06 01:30:40 Starting examples/compilation/ag32
Jun 06 02:00:35 Finished examples/compilation/ag32                            29m53s  13GB
Jun 06 02:00:35 Starting examples/compilation/ag32/proofs
Jun 06 02:02:06 Finished examples/compilation/ag32/proofs                      1m29s   7GB
Jun 06 02:02:07 Starting examples/compilation/to_word
Jun 06 02:06:01 Finished examples/compilation/to_word                          3m53s  12GB
Jun 06 02:06:03 Starting examples/lpr_checker
Jun 06 02:07:27 Finished examples/lpr_checker                                  1m23s   2GB
Jun 06 02:07:28 Starting examples/lpr_checker/array
Jun 06 02:36:25 Finished examples/lpr_checker/array                           28m56s  10GB
Jun 06 02:36:26 Starting examples/lpr_checker/array/compilation
Jun 06 03:14:57 Finished examples/lpr_checker/array/compilation               38m29s  64GB
Jun 06 03:14:58 Starting examples/lpr_checker/array/compilation/proofs
Jun 06 03:16:39 Finished examples/lpr_checker/array/compilation/proofs         1m40s   7GB
Jun 06 03:16:40 Starting examples/lpr_checker/array/compilation/proofsARM8
Jun 06 03:27:26 Finished examples/lpr_checker/array/compilation/proofsARM8    10m45s  35GB
Jun 06 03:27:27 Starting examples/xlrup_checker
Jun 06 03:28:43 Finished examples/xlrup_checker                                1m14s   2GB
Jun 06 03:28:44 Starting examples/xlrup_checker/array
Jun 06 03:43:51 Finished examples/xlrup_checker/array                         15m06s   5GB
Jun 06 03:43:52 Starting examples/xlrup_checker/array/compilation
Jun 06 04:04:59 Finished examples/xlrup_checker/array/compilation             21m06s  30GB
Jun 06 04:05:00 Starting examples/xlrup_checker/array/compilation/proofs
Jun 06 04:06:31 Finished examples/xlrup_checker/array/compilation/proofs       1m29s   7GB
Jun 06 04:06:32 Starting examples/pseudo_bool
Jun 06 04:08:42 Finished examples/pseudo_bool                                  2m09s   2GB
Jun 06 04:08:43 Starting examples/pseudo_bool/cnf_encoding
Jun 06 04:09:24 Finished examples/pseudo_bool/cnf_encoding                       39s   1GB
Jun 06 04:09:25 Starting examples/pseudo_bool/graph_encoding
Jun 06 04:10:21 Finished examples/pseudo_bool/graph_encoding                     55s   2GB
Jun 06 04:10:22 Starting examples/pseudo_bool/array
Jun 06 05:15:55 Finished examples/pseudo_bool/array                         1h05m31s  45GB
Jun 06 05:15:56 Starting examples/pseudo_bool/array/compilation
Jun 06 10:13:25 Finished examples/pseudo_bool/array/compilation             4h57m27s 142GB
Jun 06 10:13:26 Starting examples/pseudo_bool/array/compilation/proofs
Jun 06 10:17:02 Finished examples/pseudo_bool/array/compilation/proofs         3m35s   9GB
Jun 06 10:17:03 Starting examples/pseudo_bool/array/compilation/proofsARM8
Jun 06 10:33:12 Finished examples/pseudo_bool/array/compilation/proofsARM8    16m07s  45GB
Jun 06 10:33:13 Starting examples/opentheory
Jun 06 10:44:09 Finished examples/opentheory                                  10m55s   7GB
Jun 06 10:44:10 Starting examples/opentheory
Jun 06 10:44:12 Finished examples/opentheory                                      0s 133MB
Jun 06 10:44:13 Starting examples/opentheory/compilation
Jun 06 11:20:54 Finished examples/opentheory/compilation                      36m39s  51GB
Jun 06 11:20:55 Starting examples/opentheory/compilation/proofs
Jun 06 11:22:27 Finished examples/opentheory/compilation/proofs                1m31s   6GB
Jun 06 11:22:28 Starting examples/opentheory/compilation/ag32
Jun 06 11:56:01 Finished examples/opentheory/compilation/ag32                 33m32s  64GB
Jun 06 11:56:02 Starting examples/opentheory/compilation/ag32/proofs
Jun 06 11:58:25 Finished examples/opentheory/compilation/ag32/proofs           2m21s  11GB
Jun 06 11:58:26 Starting examples/sat_encodings
Jun 06 12:01:24 Finished examples/sat_encodings                                2m56s   1GB
Jun 06 12:01:25 Starting examples/sat_encodings/case_studies
Jun 06 12:03:36 Finished examples/sat_encodings/case_studies                   2m09s   2GB
Jun 06 12:03:37 Starting examples/sat_encodings/translation
Jun 06 12:10:08 Finished examples/sat_encodings/translation                    6m30s   7GB
Jun 06 12:10:09 Starting examples/sat_encodings/translation/compilation
Jun 06 12:45:20 Finished examples/sat_encodings/translation/compilation       35m10s  27GB
Jun 06 12:45:21 Starting examples/deflate
Jun 06 12:46:44 Finished examples/deflate                                      1m21s   1GB
Jun 06 12:46:45 Starting examples/deflate/translation
Jun 06 12:48:26 Finished examples/deflate/translation                          1m40s   7GB
Jun 06 12:48:27 Starting examples/deflate/translation/compilation
Jun 06 13:05:23 Finished examples/deflate/translation/compilation             16m55s  23GB
Jun 06 13:05:24 Starting examples/vipr
Jun 06 13:06:13 FAILED: examples/vipr
Scanning [1m$(HOLDIR)/src/bag[0m
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/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$(HOLDIR)/examples/machine-code/hoare-triple[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)/semantics/proofs[0m
Scanning [1m$(CAKEMLDIR)/compiler/parsing[0m
Scanning [1m$(CAKEMLDIR)/translator[0m
Scanning [1m$(CAKEMLDIR)/characteristic[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic/monad_base[0m
Scanning [1m$(CAKEMLDIR)/translator/monadic[0m
Scanning [1m$(CAKEMLDIR)/basis[0m
Scanned 29 directories
Starting work on README.md
Starting work on sptree_unionWithTheory
Starting work on real_plusTheory
README.md                                                           (0s)     OK
sptree_unionWithTheory                                             (14s)     OK
Starting work on milpTheory
real_plusTheory                                                    (16s)     OK
milpTheory                                                         (26s)FAIL<1>
      "eval_lhs_cmul",
      [
         QUOTE
         " (*#loc 350 23*)\n  eval_lhs w (cmul r lhs) =\n  r * eval_lhs w lhs"
         ],
      (fn ... => ...)
      )
 error in quse /scratch/cakeml/regression2/cakeml-2404/examples/vipr/milpScript.sml : Fail "Static Errors"
 error in load /scratch/cakeml/regression2/cakeml-2404/examples/vipr/milpScript : Fail "Static Errors"
 Uncaught exception: Fail "Static Errors"