Job 2308

CakeML:078b5dabc339348758411ad4d46b392ba6ff8890
  remove _ from sexp op names [Feb 19 14:46:17]
#983 (fromsexpfix)
Merging into:7b2d2fceaca11d0a04487744c515e8b9fcc712cd
  fix cnf_xor infinite loop [Feb 27 04:31:21]
HOL:525694a1f1c7016dea954894bea6e6e396f7d6b3
  HolSmt: add unit tests for circular definitions [Feb 21 23:04:33]
Machine:pavlova

Feb 27 04:51:53 Claimed job
Feb 27 04:52:03 Building HOL
Feb 27 05:06:10 Starting developers
Feb 27 05:06:14 Finished developers                                               2s 182MB
Feb 27 05:06:15 Starting developers/bin
Feb 27 05:06:26 Finished developers/bin                                          10s   1GB
Feb 27 05:06:27 Starting compiler/proofs
Feb 27 06:52:26 Finished compiler/proofs                                    1h45m57s  42GB
Feb 27 06:52:27 Starting compiler/bootstrap/translation
Feb 27 14:49:09 Finished compiler/bootstrap/translation                     7h56m41s  79GB
Feb 27 14:49:10 Starting semantics/ffi
Feb 27 14:49:18 Finished semantics/ffi                                            7s 701MB
Feb 27 14:49:19 Starting semantics
Feb 27 14:49:20 Finished semantics                                                0s  66MB
Feb 27 14:49:21 Starting semantics/proofs
Feb 27 14:49:57 Finished semantics/proofs                                        34s   2GB
Feb 27 14:49:58 Starting semantics/alt_semantics
Feb 27 14:50:36 Finished semantics/alt_semantics                                 37s   1GB
Feb 27 14:50:37 Starting semantics/alt_semantics/proofs
Feb 27 15:01:38 Finished semantics/alt_semantics/proofs                       10m59s   5GB
Feb 27 15:01:39 Starting basis/pure
Feb 27 15:01:40 Finished basis/pure                                               0s  68MB
Feb 27 15:01:41 Starting translator
Feb 27 15:03:26 Finished translator                                            1m43s   4GB
Feb 27 15:03:27 Starting compiler/parsing
Feb 27 15:03:28 Finished compiler/parsing                                         0s  67MB
Feb 27 15:03:29 Starting characteristic
Feb 27 15:03:31 Finished characteristic                                           0s  88MB
Feb 27 15:03:31 Starting translator/monadic
Feb 27 15:03:33 Finished translator/monadic                                       0s  90MB
Feb 27 15:03:34 Starting basis
Feb 27 15:07:08 Finished basis                                                 3m32s   5GB
Feb 27 15:07:09 Starting compiler/inference
Feb 27 15:07:10 Finished compiler/inference                                       0s  80MB
Feb 27 15:07:11 Starting compiler/backend/reg_alloc
Feb 27 15:07:12 Finished compiler/backend/reg_alloc                               0s  67MB
Feb 27 15:07:13 Starting compiler/backend/gc
Feb 27 15:07:15 Finished compiler/backend/gc                                      0s 137MB
Feb 27 15:07:16 Starting compiler/backend
Feb 27 15:07:34 Finished compiler/backend                                        16s   1GB
Feb 27 15:07:35 Starting compiler/encoders/asm
Feb 27 15:07:36 Finished compiler/encoders/asm                                    0s  95MB
Feb 27 15:07:37 Starting compiler/encoders/x64
Feb 27 15:07:39 Finished compiler/encoders/x64                                    0s  97MB
Feb 27 15:07:39 Starting compiler/encoders/arm7
Feb 27 15:07:41 Finished compiler/encoders/arm7                                   0s  93MB
Feb 27 15:07:42 Starting compiler/encoders/arm8
Feb 27 15:07:43 Finished compiler/encoders/arm8                                   0s  94MB
Feb 27 15:07:44 Starting compiler/encoders/arm8_asl
Feb 27 17:26:33 Finished compiler/encoders/arm8_asl                         2h18m47s  43GB
Feb 27 17:26:34 Starting compiler/encoders/mips
Feb 27 17:26:35 Finished compiler/encoders/mips                                   0s  93MB
Feb 27 17:26:36 Starting compiler/encoders/riscv
Feb 27 17:26:38 Finished compiler/encoders/riscv                                  0s  93MB
Feb 27 17:26:38 Starting compiler/encoders/ag32
Feb 27 17:26:40 Finished compiler/encoders/ag32                                   0s  94MB
Feb 27 17:26:41 Starting compiler/backend/x64
Feb 27 17:26:43 Finished compiler/backend/x64                                     0s 133MB
Feb 27 17:26:44 Starting compiler/backend/arm7
Feb 27 17:26:45 Finished compiler/backend/arm7                                    0s 133MB
Feb 27 17:26:46 Starting compiler/backend/arm8
Feb 27 17:26:48 Finished compiler/backend/arm8                                    0s 133MB
Feb 27 17:26:49 Starting compiler/backend/mips
Feb 27 17:26:51 Finished compiler/backend/mips                                    0s 133MB
Feb 27 17:26:52 Starting compiler/backend/riscv
Feb 27 17:26:53 Finished compiler/backend/riscv                                   0s 133MB
Feb 27 17:26:54 Starting compiler/backend/ag32
Feb 27 17:28:11 Finished compiler/backend/ag32                                 1m15s   2GB
Feb 27 17:28:12 Starting compiler/parsing/proofs
Feb 27 17:28:13 Finished compiler/parsing/proofs                                  0s  78MB
Feb 27 17:28:14 Starting compiler/inference/proofs
Feb 27 17:28:16 Finished compiler/inference/proofs                                0s  90MB
Feb 27 17:28:17 Starting compiler/backend/semantics
Feb 27 17:29:42 Finished compiler/backend/semantics                            1m24s   2GB
Feb 27 17:29:43 Starting compiler/backend/reg_alloc/proofs
Feb 27 17:29:44 Finished compiler/backend/reg_alloc/proofs                        0s  95MB
Feb 27 17:29:45 Starting compiler/backend/proofs
Feb 27 17:30:47 Finished compiler/backend/proofs                               1m00s   3GB
Feb 27 17:30:47 Starting compiler/backend/serialiser
Feb 27 17:30:50 Finished compiler/backend/serialiser                              1s 195MB
Feb 27 17:30:51 Starting compiler/encoders/x64/proofs
Feb 27 17:40:14 Finished compiler/encoders/x64/proofs                          9m22s   5GB
Feb 27 17:40:15 Starting compiler/encoders/arm7/proofs
Feb 27 17:53:03 Finished compiler/encoders/arm7/proofs                        12m46s   7GB
Feb 27 17:53:04 Starting compiler/encoders/arm8/proofs
Feb 27 17:59:23 Finished compiler/encoders/arm8/proofs                         6m18s   5GB
Feb 27 17:59:24 Starting compiler/encoders/arm8_asl/proofs
Feb 27 18:46:44 Finished compiler/encoders/arm8_asl/proofs                    47m19s  11GB
Feb 27 18:46:45 Starting compiler/encoders/mips/proofs
Feb 27 18:56:49 Finished compiler/encoders/mips/proofs                        10m02s   9GB
Feb 27 18:56:50 Starting compiler/encoders/riscv/proofs
Feb 27 19:05:22 Finished compiler/encoders/riscv/proofs                        8m30s   4GB
Feb 27 19:05:23 Starting compiler/encoders/ag32/proofs
Feb 27 19:07:44 Finished compiler/encoders/ag32/proofs                         2m20s   2GB
Feb 27 19:07:45 Starting compiler/backend/x64/proofs
Feb 27 19:08:25 Finished compiler/backend/x64/proofs                             39s   2GB
Feb 27 19:08:26 Starting compiler/backend/arm7/proofs
Feb 27 19:09:14 Finished compiler/backend/arm7/proofs                            46s   2GB
Feb 27 19:09:14 Starting compiler/backend/arm8/proofs
Feb 27 19:09:54 Finished compiler/backend/arm8/proofs                            38s   3GB
Feb 27 19:09:54 Starting compiler/backend/arm8_asl
Feb 27 19:10:24 Finished compiler/backend/arm8_asl                               28s   2GB
Feb 27 19:10:25 Starting compiler/backend/mips/proofs
Feb 27 19:11:08 Finished compiler/backend/mips/proofs                            42s   3GB
Feb 27 19:11:09 Starting compiler/backend/riscv/proofs
Feb 27 19:11:58 Finished compiler/backend/riscv/proofs                           48s   4GB
Feb 27 19:11:59 Starting compiler/backend/ag32/proofs
Feb 27 19:25:13 Finished compiler/backend/ag32/proofs                         13m12s   6GB
Feb 27 19:25:13 Starting candle/set-theory
Feb 27 19:25:59 Finished candle/set-theory                                       44s   1GB
Feb 27 19:26:00 Starting candle/syntax-lib
Feb 27 19:26:01 Finished candle/syntax-lib                                        0s  69MB
Feb 27 19:26:02 Starting candle/standard/syntax
Feb 27 19:26:17 Finished candle/standard/syntax                                  14s   1GB
Feb 27 19:26:18 Starting candle/standard/semantics
Feb 27 19:28:41 Finished candle/standard/semantics                             2m21s   2GB
Feb 27 19:28:42 Starting candle/standard/monadic
Feb 27 19:28:43 Finished candle/standard/monadic                                  0s  97MB
Feb 27 19:28:44 Starting candle/standard/ml_kernel
Feb 27 19:30:32 Finished candle/standard/ml_kernel                             1m46s   5GB
Feb 27 19:30:33 Starting candle/overloading/syntax
Feb 27 19:34:00 Finished candle/overloading/syntax                             3m26s   2GB
Feb 27 19:34:01 Starting candle/overloading/semantics
Feb 27 19:45:11 Finished candle/overloading/semantics                         11m08s   8GB
Feb 27 19:45:12 Starting candle/overloading/monadic
Feb 27 19:47:45 Finished candle/overloading/monadic                            2m32s   3GB
Feb 27 19:47:46 Starting candle/overloading/ml_kernel
Feb 27 19:55:15 Finished candle/overloading/ml_kernel                          7m27s   6GB
Feb 27 19:55:15 Starting candle/overloading/ml_checker
Feb 27 19:57:47 Finished candle/overloading/ml_checker                         2m30s   7GB
Feb 27 19:57:48 Starting candle/prover
Feb 27 20:07:36 Finished candle/prover                                         9m47s   5GB
Feb 27 20:07:37 Starting pancake
Feb 27 20:08:34 Finished pancake                                                 55s   1GB
Feb 27 20:08:35 Starting pancake/ffi
Feb 27 20:08:36 Finished pancake/ffi                                              0s  21MB
Feb 27 20:08:37 Starting pancake/semantics
Feb 27 20:10:54 Finished pancake/semantics                                     2m16s   2GB
Feb 27 20:10:55 Starting pancake/parser
Feb 27 20:11:22 Finished pancake/parser                                          26s   2GB
Feb 27 20:11:23 Starting pancake/proofs
Feb 27 20:41:01 Finished pancake/proofs                                       29m37s   8GB
Feb 27 20:41:02 Starting characteristic/examples
Feb 27 20:42:39 Finished characteristic/examples                               1m36s   5GB
Feb 27 20:42:40 Starting tutorial/solutions
Feb 27 20:58:17 Finished tutorial/solutions                                   15m36s  12GB
Feb 27 20:58:18 Starting translator/monadic/examples
Feb 27 21:02:05 Finished translator/monadic/examples                           3m45s   5GB
Feb 27 21:02:05 Starting examples
Feb 27 21:16:23 Finished examples                                             14m16s   7GB
Feb 27 21:16:24 Starting examples/compilation/x64
Feb 27 23:13:48 Finished examples/compilation/x64                           1h57m22s  36GB
Feb 27 23:13:49 Starting examples/compilation/x64/proofs
Feb 27 23:17:42 Finished examples/compilation/x64/proofs                       3m52s   5GB
Feb 27 23:17:43 Starting examples/compilation/ag32
Feb 27 23:47:12 Finished examples/compilation/ag32                            29m27s  14GB
Feb 27 23:47:13 Starting examples/compilation/ag32/proofs
Feb 27 23:48:40 Finished examples/compilation/ag32/proofs                      1m26s   6GB
Feb 27 23:48:41 Starting examples/compilation/to_word
Feb 27 23:52:33 Finished examples/compilation/to_word                          3m50s  11GB
Feb 27 23:52:34 Starting examples/lpr_checker
Feb 27 23:53:50 Finished examples/lpr_checker                                  1m14s   2GB
Feb 27 23:53:50 Starting examples/lpr_checker/array
Feb 28 00:23:29 Finished examples/lpr_checker/array                           29m37s   9GB
Feb 28 00:23:30 Starting examples/lpr_checker/array/compilation
Feb 28 00:58:00 Finished examples/lpr_checker/array/compilation               34m29s  70GB
Feb 28 00:58:01 Starting examples/lpr_checker/array/compilation/proofs
Feb 28 00:59:57 Finished examples/lpr_checker/array/compilation/proofs         1m54s   9GB
Feb 28 00:59:58 Starting examples/lpr_checker/array/compilation/proofsARM8
Feb 28 01:17:36 Finished examples/lpr_checker/array/compilation/proofsARM8    17m37s  51GB
Feb 28 01:17:37 Starting examples/xlrup_checker
Feb 28 01:18:45 Finished examples/xlrup_checker                                1m07s   2GB
Feb 28 01:18:46 Starting examples/xlrup_checker/array
Feb 28 01:35:14 Finished examples/xlrup_checker/array                         16m27s   8GB
Feb 28 01:35:15 Starting examples/xlrup_checker/array/compilation
Feb 28 01:55:53 Finished examples/xlrup_checker/array/compilation             20m37s  33GB
Feb 28 01:55:54 Starting examples/xlrup_checker/array/compilation/proofs
Feb 28 01:57:21 Finished examples/xlrup_checker/array/compilation/proofs       1m26s   6GB
Feb 28 01:57:23 Starting examples/pseudo_bool
Feb 28 01:59:24 Finished examples/pseudo_bool                                  2m00s   2GB
Feb 28 01:59:25 Starting examples/pseudo_bool/cnf_encoding
Feb 28 02:00:02 Finished examples/pseudo_bool/cnf_encoding                       35s   1GB
Feb 28 02:00:03 Starting examples/pseudo_bool/graph_encoding
Feb 28 02:00:52 Finished examples/pseudo_bool/graph_encoding                     48s   2GB
Feb 28 02:00:53 Starting examples/pseudo_bool/array
Feb 28 03:05:54 Finished examples/pseudo_bool/array                         1h04m59s  38GB
Feb 28 03:05:54 Starting examples/pseudo_bool/array/compilation
Feb 28 10:29:01 Finished examples/pseudo_bool/array/compilation             7h23m05s 130GB
Feb 28 10:29:02 Starting examples/pseudo_bool/array/compilation/proofs
Feb 28 10:32:16 Finished examples/pseudo_bool/array/compilation/proofs         3m12s   8GB
Feb 28 10:32:17 Starting examples/opentheory
Feb 28 10:42:44 Finished examples/opentheory                                  10m26s   7GB
Feb 28 10:42:45 Starting examples/opentheory
Feb 28 10:42:47 Finished examples/opentheory                                      0s 133MB
Feb 28 10:42:48 Starting examples/opentheory/compilation
Feb 28 11:18:14 Finished examples/opentheory/compilation                      35m25s  47GB
Feb 28 11:18:15 Starting examples/opentheory/compilation/proofs
Feb 28 11:19:42 Finished examples/opentheory/compilation/proofs                1m26s   6GB
Feb 28 11:19:43 Starting examples/opentheory/compilation/ag32
Feb 28 11:51:41 Finished examples/opentheory/compilation/ag32                 31m56s  49GB
Feb 28 11:51:41 Starting examples/opentheory/compilation/ag32/proofs
Feb 28 11:53:50 Finished examples/opentheory/compilation/ag32/proofs           2m07s  10GB
Feb 28 11:53:51 Starting examples/sat_encodings
Feb 28 11:56:27 Finished examples/sat_encodings                                2m34s   1GB
Feb 28 11:56:28 Starting examples/sat_encodings/case_studies
Feb 28 11:58:27 Finished examples/sat_encodings/case_studies                   1m57s   2GB
Feb 28 11:58:27 Starting examples/sat_encodings/translation
Feb 28 12:04:34 Finished examples/sat_encodings/translation                    6m05s   7GB
Feb 28 12:04:34 Starting examples/sat_encodings/translation/compilation
Feb 28 12:39:42 Finished examples/sat_encodings/translation/compilation       35m06s  35GB
Feb 28 12:39:43 Starting examples/deflate
Feb 28 12:41:00 Finished examples/deflate                                      1m15s   1GB
Feb 28 12:41:01 Starting examples/deflate/translation
Feb 28 12:42:40 Finished examples/deflate/translation                          1m38s   7GB
Feb 28 12:42:41 Starting examples/deflate/translation/compilation
Feb 28 12:59:24 Finished examples/deflate/translation/compilation             16m42s  20GB
Feb 28 12:59:25 Starting examples/vipr
Feb 28 13:03:27 Finished examples/vipr                                         4m01s   7GB
Feb 28 13:03:28 Starting examples/vipr/compilation
Feb 28 13:24:44 Finished examples/vipr/compilation                            21m15s  32GB
Feb 28 13:24:45 Starting translator/okasaki-examples
Feb 28 13:29:42 Finished translator/okasaki-examples                           4m55s   4GB
Feb 28 13:29:43 Starting translator/other-examples
Feb 28 13:34:23 Finished translator/other-examples                             4m39s   3GB
Feb 28 13:34:24 Starting compiler/parsing/tests
Feb 28 13:34:57 Finished compiler/parsing/tests                                  32s   1GB
Feb 28 13:34:58 Starting compiler/inference/tests
Feb 28 13:42:36 Finished compiler/inference/tests                              7m37s   8GB
Feb 28 13:42:37 Starting compiler/printing/test
Feb 28 13:46:08 Finished compiler/printing/test                                3m29s   6GB
Feb 28 13:46:09 Starting icing/flover
Feb 28 14:22:39 Finished icing/flover                                         36m28s   3GB
Feb 28 14:22:40 Starting icing/
Feb 28 15:17:47 Finished icing/                                               55m06s  35GB
Feb 28 15:17:48 Starting icing/examples
Feb 28 15:19:23 Finished icing/examples                                        1m33s   5GB
Feb 28 15:19:23 Starting compiler/repl
Feb 28 15:28:04 Finished compiler/repl                                         8m40s   9GB
Feb 28 15:28:05 Starting unverified/sexpr-bootstrap/x64/64
Feb 28 15:39:12 Finished unverified/sexpr-bootstrap/x64/64                    11m05s  17GB
Feb 28 15:39:13 Starting unverified/sexpr-bootstrap/x64/32
Feb 28 15:48:17 Finished unverified/sexpr-bootstrap/x64/32                     9m03s  14GB
Feb 28 15:48:18 Starting compiler/benchmarks
Feb 28 15:49:03 Finished compiler/benchmarks                                     44s 713MB
Feb 28 15:49:04 Starting compiler/bootstrap/compilation/x64/64
Feb 29 06:21:40 Finished compiler/bootstrap/compilation/x64/64             14h32m34s 148GB
Feb 29 06:21:40 Starting compiler/bootstrap/compilation/x64/64/proofs
Feb 29 06:42:10 Finished compiler/bootstrap/compilation/x64/64/proofs         20m28s  35GB
Feb 29 06:42:11 Starting compiler/bootstrap/compilation/x64/32
Feb 29 14:01:33 Finished compiler/bootstrap/compilation/x64/32              7h19m20s 112GB
Feb 29 14:01:34 Starting compiler/bootstrap/compilation/x64/32/proofs
Feb 29 14:05:00 Finished compiler/bootstrap/compilation/x64/32/proofs          3m25s  18GB
Feb 29 14:05:01 Starting compiler/bootstrap/compilation/ag32/32
Feb 29 21:48:04 Finished compiler/bootstrap/compilation/ag32/32             7h43m01s 126GB
Feb 29 21:48:04 Starting compiler/bootstrap/compilation/ag32/32/proofs
Feb 29 21:55:40 Finished compiler/bootstrap/compilation/ag32/32/proofs         7m34s  51GB
Feb 29 21:55:41 SUCCESS