Job 2327

CakeML:5cf901913bf1a85f71c529da5c01593bbf7d1955
  ARM8 proof [Mar 06 09:08:24]
#984 (compression)
Merging into:865f0382dcffc38919b6d1ae355d103e3f570dc5
  Merge pull request #982 from CakeML/contexts [Mar 03 14:31:28]
HOL:772a64a23fab01445886a113b810bd3c02930e63
  Tweak tailrecLib to allow function terms that are composite [Mar 04 00:41:36]
Machine:pavlova

Mar 06 23:43:47 Claimed job
Mar 06 23:43:52 Building HOL
Mar 06 23:57:45 Starting developers
Mar 06 23:57:48 Finished developers                                               2s 126MB
Mar 06 23:57:49 Starting developers/bin
Mar 06 23:58:01 Finished developers/bin                                          10s   1GB
Mar 06 23:58:02 Starting compiler/proofs
Mar 07 01:44:13 Finished compiler/proofs                                    1h46m10s  29GB
Mar 07 01:44:14 Starting compiler/bootstrap/translation
Mar 07 09:44:21 Finished compiler/bootstrap/translation                     8h00m06s  82GB
Mar 07 09:44:22 Starting semantics/ffi
Mar 07 09:44:31 Finished semantics/ffi                                            7s 683MB
Mar 07 09:44:32 Starting semantics
Mar 07 09:44:33 Finished semantics                                                0s  66MB
Mar 07 09:44:34 Starting semantics/proofs
Mar 07 09:45:09 Finished semantics/proofs                                        34s   2GB
Mar 07 09:45:10 Starting semantics/alt_semantics
Mar 07 09:45:49 Finished semantics/alt_semantics                                 37s   1GB
Mar 07 09:45:50 Starting semantics/alt_semantics/proofs
Mar 07 09:56:48 Finished semantics/alt_semantics/proofs                       10m57s   5GB
Mar 07 09:56:49 Starting basis/pure
Mar 07 09:56:50 Finished basis/pure                                               0s  68MB
Mar 07 09:56:51 Starting translator
Mar 07 09:58:34 Finished translator                                            1m41s   4GB
Mar 07 09:58:35 Starting compiler/parsing
Mar 07 09:58:36 Finished compiler/parsing                                         0s  67MB
Mar 07 09:58:37 Starting characteristic
Mar 07 09:58:38 Finished characteristic                                           0s  89MB
Mar 07 09:58:39 Starting translator/monadic
Mar 07 09:58:41 Finished translator/monadic                                       0s  90MB
Mar 07 09:58:42 Starting basis
Mar 07 10:02:18 Finished basis                                                 3m35s   5GB
Mar 07 10:02:19 Starting compiler/inference
Mar 07 10:02:20 Finished compiler/inference                                       0s  80MB
Mar 07 10:02:21 Starting compiler/backend/reg_alloc
Mar 07 10:02:22 Finished compiler/backend/reg_alloc                               0s  67MB
Mar 07 10:02:23 Starting compiler/backend/gc
Mar 07 10:02:25 Finished compiler/backend/gc                                      0s 130MB
Mar 07 10:02:26 Starting compiler/backend
Mar 07 10:02:44 Finished compiler/backend                                        16s   1GB
Mar 07 10:02:44 Starting compiler/encoders/asm
Mar 07 10:02:46 Finished compiler/encoders/asm                                    0s  95MB
Mar 07 10:02:47 Starting compiler/encoders/x64
Mar 07 10:02:48 Finished compiler/encoders/x64                                    0s  96MB
Mar 07 10:02:49 Starting compiler/encoders/arm7
Mar 07 10:02:51 Finished compiler/encoders/arm7                                   0s  93MB
Mar 07 10:02:52 Starting compiler/encoders/arm8
Mar 07 10:02:53 Finished compiler/encoders/arm8                                   0s  94MB
Mar 07 10:02:54 Starting compiler/encoders/arm8_asl
Mar 07 12:24:22 Finished compiler/encoders/arm8_asl                         2h21m26s  47GB
Mar 07 12:24:23 Starting compiler/encoders/mips
Mar 07 12:24:24 Finished compiler/encoders/mips                                   0s  94MB
Mar 07 12:24:25 Starting compiler/encoders/riscv
Mar 07 12:24:27 Finished compiler/encoders/riscv                                  0s  93MB
Mar 07 12:24:28 Starting compiler/encoders/ag32
Mar 07 12:24:29 Finished compiler/encoders/ag32                                   0s  94MB
Mar 07 12:24:30 Starting compiler/backend/x64
Mar 07 12:24:32 Finished compiler/backend/x64                                     0s 133MB
Mar 07 12:24:33 Starting compiler/backend/arm7
Mar 07 12:24:34 Finished compiler/backend/arm7                                    0s 133MB
Mar 07 12:24:35 Starting compiler/backend/arm8
Mar 07 12:24:37 Finished compiler/backend/arm8                                    0s 133MB
Mar 07 12:24:38 Starting compiler/backend/mips
Mar 07 12:24:40 Finished compiler/backend/mips                                    0s 133MB
Mar 07 12:24:41 Starting compiler/backend/riscv
Mar 07 12:24:42 Finished compiler/backend/riscv                                   0s 133MB
Mar 07 12:24:43 Starting compiler/backend/ag32
Mar 07 12:26:03 Finished compiler/backend/ag32                                 1m18s   3GB
Mar 07 12:26:04 Starting compiler/parsing/proofs
Mar 07 12:26:05 Finished compiler/parsing/proofs                                  0s  78MB
Mar 07 12:26:06 Starting compiler/inference/proofs
Mar 07 12:26:08 Finished compiler/inference/proofs                                0s  89MB
Mar 07 12:26:08 Starting compiler/backend/semantics
Mar 07 12:27:34 Finished compiler/backend/semantics                            1m24s   2GB
Mar 07 12:27:35 Starting compiler/backend/reg_alloc/proofs
Mar 07 12:27:37 Finished compiler/backend/reg_alloc/proofs                        0s  90MB
Mar 07 12:27:38 Starting compiler/backend/proofs
Mar 07 12:28:39 Finished compiler/backend/proofs                               1m00s   3GB
Mar 07 12:28:40 Starting compiler/backend/serialiser
Mar 07 12:28:42 Finished compiler/backend/serialiser                              1s 188MB
Mar 07 12:28:43 Starting compiler/encoders/x64/proofs
Mar 07 12:38:11 Finished compiler/encoders/x64/proofs                          9m27s   5GB
Mar 07 12:38:12 Starting compiler/encoders/arm7/proofs
Mar 07 12:50:57 Finished compiler/encoders/arm7/proofs                        12m43s   9GB
Mar 07 12:50:58 Starting compiler/encoders/arm8/proofs
Mar 07 12:57:17 Finished compiler/encoders/arm8/proofs                         6m18s   7GB
Mar 07 12:57:18 Starting compiler/encoders/arm8_asl/proofs
Mar 07 13:44:53 Finished compiler/encoders/arm8_asl/proofs                    47m34s  11GB
Mar 07 13:44:54 Starting compiler/encoders/mips/proofs
Mar 07 13:54:52 Finished compiler/encoders/mips/proofs                         9m57s   5GB
Mar 07 13:54:53 Starting compiler/encoders/riscv/proofs
Mar 07 14:02:53 Finished compiler/encoders/riscv/proofs                        7m59s   3GB
Mar 07 14:02:54 Starting compiler/encoders/ag32/proofs
Mar 07 14:05:14 Finished compiler/encoders/ag32/proofs                         2m18s   2GB
Mar 07 14:05:15 Starting compiler/backend/x64/proofs
Mar 07 14:05:56 Finished compiler/backend/x64/proofs                             39s   3GB
Mar 07 14:05:57 Starting compiler/backend/arm7/proofs
Mar 07 14:06:39 Finished compiler/backend/arm7/proofs                            41s   2GB
Mar 07 14:06:40 Starting compiler/backend/arm8/proofs
Mar 07 14:07:18 Finished compiler/backend/arm8/proofs                            37s   3GB
Mar 07 14:07:19 Starting compiler/backend/arm8_asl
Mar 07 14:07:47 Finished compiler/backend/arm8_asl                               27s   2GB
Mar 07 14:07:48 Starting compiler/backend/mips/proofs
Mar 07 14:08:32 Finished compiler/backend/mips/proofs                            43s   3GB
Mar 07 14:08:33 Starting compiler/backend/riscv/proofs
Mar 07 14:09:21 Finished compiler/backend/riscv/proofs                           47s   4GB
Mar 07 14:09:22 Starting compiler/backend/ag32/proofs
Mar 07 14:22:32 Finished compiler/backend/ag32/proofs                         13m09s   6GB
Mar 07 14:22:33 Starting candle/set-theory
Mar 07 14:23:17 Finished candle/set-theory                                       43s   1GB
Mar 07 14:23:18 Starting candle/syntax-lib
Mar 07 14:23:19 Finished candle/syntax-lib                                        0s  69MB
Mar 07 14:23:20 Starting candle/standard/syntax
Mar 07 14:23:36 Finished candle/standard/syntax                                  14s   1GB
Mar 07 14:23:37 Starting candle/standard/semantics
Mar 07 14:26:03 Finished candle/standard/semantics                             2m25s   3GB
Mar 07 14:26:04 Starting candle/standard/monadic
Mar 07 14:26:05 Finished candle/standard/monadic                                  0s  97MB
Mar 07 14:26:06 Starting candle/standard/ml_kernel
Mar 07 14:27:56 Finished candle/standard/ml_kernel                             1m48s   5GB
Mar 07 14:27:57 Starting candle/overloading/syntax
Mar 07 14:31:24 Finished candle/overloading/syntax                             3m26s   2GB
Mar 07 14:31:25 Starting candle/overloading/semantics
Mar 07 14:42:46 Finished candle/overloading/semantics                         11m19s   5GB
Mar 07 14:42:46 Starting candle/overloading/monadic
Mar 07 14:45:18 Finished candle/overloading/monadic                            2m30s   3GB
Mar 07 14:45:19 Starting candle/overloading/ml_kernel
Mar 07 14:52:54 Finished candle/overloading/ml_kernel                          7m33s   7GB
Mar 07 14:52:55 Starting candle/overloading/ml_checker
Mar 07 14:55:23 Finished candle/overloading/ml_checker                         2m27s   6GB
Mar 07 14:55:24 Starting candle/prover
Mar 07 15:05:10 Finished candle/prover                                         9m45s   5GB
Mar 07 15:05:11 Starting pancake
Mar 07 15:06:12 Finished pancake                                                 59s   1GB
Mar 07 15:06:12 Starting pancake/ffi
Mar 07 15:06:13 Finished pancake/ffi                                              0s  21MB
Mar 07 15:06:14 Starting pancake/semantics
Mar 07 15:08:34 Finished pancake/semantics                                     2m19s   2GB
Mar 07 15:08:35 Starting pancake/parser
Mar 07 15:09:02 Finished pancake/parser                                          25s   2GB
Mar 07 15:09:03 Starting pancake/proofs
Mar 07 15:38:33 Finished pancake/proofs                                       29m29s   8GB
Mar 07 15:38:34 Starting characteristic/examples
Mar 07 15:40:10 Finished characteristic/examples                               1m35s   5GB
Mar 07 15:40:11 Starting tutorial/solutions
Mar 07 15:56:09 Finished tutorial/solutions                                   15m56s  30GB
Mar 07 15:56:10 Starting translator/monadic/examples
Mar 07 15:59:53 Finished translator/monadic/examples                           3m42s   5GB
Mar 07 15:59:53 Starting examples
Mar 07 16:14:27 Finished examples                                             14m33s   7GB
Mar 07 16:14:28 Starting examples/compilation/x64
Mar 07 18:11:03 Finished examples/compilation/x64                           1h56m33s  36GB
Mar 07 18:11:04 Starting examples/compilation/x64/proofs
Mar 07 18:14:56 Finished examples/compilation/x64/proofs                       3m51s   5GB
Mar 07 18:14:57 Starting examples/compilation/ag32
Mar 07 18:44:14 Finished examples/compilation/ag32                            29m15s  10GB
Mar 07 18:44:15 Starting examples/compilation/ag32/proofs
Mar 07 18:45:42 Finished examples/compilation/ag32/proofs                      1m26s   7GB
Mar 07 18:45:43 Starting examples/compilation/to_word
Mar 07 18:49:42 Finished examples/compilation/to_word                          3m58s  12GB
Mar 07 18:49:43 Starting examples/lpr_checker
Mar 07 18:50:59 Finished examples/lpr_checker                                  1m15s   2GB
Mar 07 18:51:00 Starting examples/lpr_checker/array
Mar 07 19:20:54 Finished examples/lpr_checker/array                           29m53s  11GB
Mar 07 19:20:55 Starting examples/lpr_checker/array/compilation
Mar 07 19:57:28 Finished examples/lpr_checker/array/compilation               36m31s  71GB
Mar 07 19:57:29 Starting examples/lpr_checker/array/compilation/proofs
Mar 07 19:59:28 Finished examples/lpr_checker/array/compilation/proofs         1m58s   7GB
Mar 07 19:59:29 Starting examples/lpr_checker/array/compilation/proofsARM8
Mar 07 20:23:59 Finished examples/lpr_checker/array/compilation/proofsARM8    24m29s  36GB
Mar 07 20:24:00 Starting examples/xlrup_checker
Mar 07 20:25:10 Finished examples/xlrup_checker                                1m08s   1GB
Mar 07 20:25:11 Starting examples/xlrup_checker/array
Mar 07 20:41:31 Finished examples/xlrup_checker/array                         16m19s   8GB
Mar 07 20:41:32 Starting examples/xlrup_checker/array/compilation
Mar 07 21:02:30 Finished examples/xlrup_checker/array/compilation             20m56s  23GB
Mar 07 21:02:30 Starting examples/xlrup_checker/array/compilation/proofs
Mar 07 21:03:56 Finished examples/xlrup_checker/array/compilation/proofs       1m24s   6GB
Mar 07 21:03:57 Starting examples/pseudo_bool
Mar 07 21:05:59 Finished examples/pseudo_bool                                  2m01s   2GB
Mar 07 21:06:00 Starting examples/pseudo_bool/cnf_encoding
Mar 07 21:06:36 Finished examples/pseudo_bool/cnf_encoding                       35s   1GB
Mar 07 21:06:37 Starting examples/pseudo_bool/graph_encoding
Mar 07 21:07:26 Finished examples/pseudo_bool/graph_encoding                     47s   1GB
Mar 07 21:07:27 Starting examples/pseudo_bool/array
Mar 07 22:10:19 Finished examples/pseudo_bool/array                         1h02m51s  21GB
Mar 07 22:10:20 Starting examples/pseudo_bool/array/compilation
Mar 08 05:36:42 Finished examples/pseudo_bool/array/compilation             7h26m20s 106GB
Mar 08 05:36:43 Starting examples/pseudo_bool/array/compilation/proofs
Mar 08 05:40:04 Finished examples/pseudo_bool/array/compilation/proofs         3m20s   7GB
Mar 08 05:40:05 Starting examples/opentheory
Mar 08 05:50:41 Finished examples/opentheory                                  10m34s   7GB
Mar 08 05:50:41 Starting examples/opentheory
Mar 08 05:50:43 Finished examples/opentheory                                      0s 133MB
Mar 08 05:50:44 Starting examples/opentheory/compilation
Mar 08 06:27:15 Finished examples/opentheory/compilation                      36m30s  67GB
Mar 08 06:27:16 Starting examples/opentheory/compilation/proofs
Mar 08 06:28:48 Finished examples/opentheory/compilation/proofs                1m31s   6GB
Mar 08 06:28:49 Starting examples/opentheory/compilation/ag32
Mar 08 07:00:31 Finished examples/opentheory/compilation/ag32                 31m41s  46GB
Mar 08 07:00:32 Starting examples/opentheory/compilation/ag32/proofs
Mar 08 07:02:53 Finished examples/opentheory/compilation/ag32/proofs           2m20s  13GB
Mar 08 07:02:54 Starting examples/sat_encodings
Mar 08 07:05:34 Finished examples/sat_encodings                                2m38s   1GB
Mar 08 07:05:35 Starting examples/sat_encodings/case_studies
Mar 08 07:07:31 Finished examples/sat_encodings/case_studies                   1m55s   2GB
Mar 08 07:07:32 Starting examples/sat_encodings/translation
Mar 08 07:13:40 Finished examples/sat_encodings/translation                    6m07s   7GB
Mar 08 07:13:41 Starting examples/sat_encodings/translation/compilation
Mar 08 07:48:24 Finished examples/sat_encodings/translation/compilation       34m42s  44GB
Mar 08 07:48:25 Starting examples/deflate
Mar 08 07:49:41 Finished examples/deflate                                      1m14s   1GB
Mar 08 07:49:41 Starting examples/deflate/translation
Mar 08 07:51:20 Finished examples/deflate/translation                          1m37s   7GB
Mar 08 07:51:21 Starting examples/deflate/translation/compilation
Mar 08 08:08:08 Finished examples/deflate/translation/compilation             16m46s  22GB
Mar 08 08:08:09 Starting examples/vipr
Mar 08 08:11:22 FAILED: examples/vipr
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 28 directories
Starting work on README.md
Starting work on sptree_unionWithTheory
Starting work on real_plusTheory
README.md                                                           (0s)     OK
sptree_unionWithTheory                                             (12s)     OK
Starting work on milpTheory
real_plusTheory                                                    (13s)     OK
milpTheory                                                         (31s)     OK
Starting work on vipr_checkerTheory
vipr_checkerTheory                                                 (29s)     OK
Starting work on viprProgTheory
viprProgTheory                                                    (103s)FAIL<1>
      COMMANDLINE cl)
 
 failed.
 Failed to prove theorem main_spec_stdin.
 
 Exception raised at Tactical.FIRST_ASSUM:
  (THEN1 on line 177)
 error in quse /scratch/cakeml/regression/cakeml-2327/examples/vipr/viprProgScript.sml : HOL_ERR {message = " (THEN1 on line 177)", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}
 error in load /scratch/cakeml/regression/cakeml-2327/examples/vipr/viprProgScript : HOL_ERR {message = " (THEN1 on line 177)", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}
 Uncaught exception: HOL_ERR {message = " (THEN1 on line 177)", origin_function = "FIRST_ASSUM", origin_structure = "Tactical"}