Job 1942

CakeML:cb0e2ef96602bb903072c5e781bfe859a664a563
  Update perms_ok file for changes to QSORT in basis [Jun 22 06:48:54]
#891 (boot-trans)
Merging into:fbd56dc0d32e0e8b24d8ea10dd77112eee529460
  Fix a bunch of real$abs --> realax$abs (also for min, max) [Jun 23 20:53:47]
HOL:3810cf53c6050c5b2748cb042415145bd842957f
  Make parsing in RealField properly independent of context [Jun 21 00:55:21]
Machine:oven3

Jun 23 20:54:04 Claimed job
Jun 23 20:54:11 Reusing HOL
Jun 23 20:55:04 Starting developers
Jun 23 20:55:14 Finished developers                                               9s 139MB
Jun 23 20:55:15 Starting developers/bin
Jun 23 20:55:28 Finished developers/bin                                          12s   1GB
Jun 23 20:55:28 Starting semantics/ffi
Jun 23 20:55:52 Finished semantics/ffi                                           24s 248MB
Jun 23 20:55:52 Starting semantics
Jun 23 21:00:51 Finished semantics                                             4m58s   1GB
Jun 23 21:00:51 Starting semantics/proofs
Jun 23 21:16:13 Finished semantics/proofs                                     15m22s   1GB
Jun 23 21:16:14 Starting semantics/alt_semantics
Jun 23 21:17:10 Finished semantics/alt_semantics                                 56s 586MB
Jun 23 21:17:10 Starting semantics/alt_semantics/proofs
Jun 23 21:42:31 Finished semantics/alt_semantics/proofs                       25m21s   1GB
Jun 23 21:42:32 Starting basis/pure
Jun 23 21:44:48 Finished basis/pure                                            2m16s 969MB
Jun 23 21:44:48 Starting translator
Jun 23 21:52:37 Finished translator                                            7m48s   1GB
Jun 23 21:52:38 Starting compiler/parsing
Jun 23 21:55:30 Finished compiler/parsing                                      2m52s   4GB
Jun 23 21:55:30 Starting characteristic
Jun 23 22:10:03 Finished characteristic                                       14m32s   2GB
Jun 23 22:10:03 Starting translator/monadic
Jun 23 22:14:28 Finished translator/monadic                                    4m25s   2GB
Jun 23 22:14:29 Starting basis
Jun 24 00:10:28 Finished basis                                              1h55m58s  20GB
Jun 24 00:10:28 Starting compiler/inference
Jun 24 00:13:40 Finished compiler/inference                                    3m12s   1GB
Jun 24 00:13:41 Starting compiler/backend/reg_alloc
Jun 24 00:16:55 Finished compiler/backend/reg_alloc                            3m14s   1GB
Jun 24 00:16:55 Starting compiler/backend/gc
Jun 24 00:25:47 Finished compiler/backend/gc                                   8m51s   2GB
Jun 24 00:25:47 Starting compiler/backend
Jun 24 00:38:01 Finished compiler/backend                                     12m14s   2GB
Jun 24 00:38:02 Starting compiler/encoders/asm
Jun 24 00:39:09 Finished compiler/encoders/asm                                 1m06s 762MB
Jun 24 00:39:09 Starting compiler/encoders/x64
Jun 24 00:40:14 Finished compiler/encoders/x64                                 1m04s   1GB
Jun 24 00:40:14 Starting compiler/encoders/arm7
Jun 24 00:42:22 Finished compiler/encoders/arm7                                2m07s 835MB
Jun 24 00:42:22 Starting compiler/encoders/arm8
Jun 24 00:43:00 Finished compiler/encoders/arm8                                  38s 746MB
Jun 24 00:43:01 Starting compiler/encoders/arm8_asl
Jun 24 00:50:35 Finished compiler/encoders/arm8_asl                            7m34s   1GB
Jun 24 00:50:36 Starting compiler/encoders/mips
Jun 24 00:51:20 Finished compiler/encoders/mips                                  44s   1GB
Jun 24 00:51:20 Starting compiler/encoders/riscv
Jun 24 00:52:03 Finished compiler/encoders/riscv                                 42s 805MB
Jun 24 00:52:03 Starting compiler/encoders/ag32
Jun 24 00:52:52 Finished compiler/encoders/ag32                                  48s 649MB
Jun 24 00:52:52 Starting compiler/backend/x64
Jun 24 00:53:39 Finished compiler/backend/x64                                    47s   1GB
Jun 24 00:53:40 Starting compiler/backend/arm7
Jun 24 00:54:30 Finished compiler/backend/arm7                                   50s   1GB
Jun 24 00:54:31 Starting compiler/backend/arm8
Jun 24 00:55:20 Finished compiler/backend/arm8                                   49s   1GB
Jun 24 00:55:20 Starting compiler/backend/mips
Jun 24 00:56:11 Finished compiler/backend/mips                                   50s   1GB
Jun 24 00:56:11 Starting compiler/backend/riscv
Jun 24 00:56:59 Finished compiler/backend/riscv                                  47s   1GB
Jun 24 00:56:59 Starting compiler/backend/ag32
Jun 24 00:59:59 Finished compiler/backend/ag32                                 2m59s   1GB
Jun 24 00:59:59 Starting compiler/parsing/proofs
Jun 24 01:08:30 Finished compiler/parsing/proofs                               8m31s   1GB
Jun 24 01:08:31 Starting compiler/inference/proofs
Jun 24 01:14:29 Finished compiler/inference/proofs                             5m57s   1GB
Jun 24 01:14:29 Starting compiler/backend/semantics
Jun 24 02:10:40 Finished compiler/backend/semantics                           56m10s   2GB
Jun 24 02:10:41 Starting compiler/backend/reg_alloc/proofs
Jun 24 02:18:25 Finished compiler/backend/reg_alloc/proofs                     7m43s   1GB
Jun 24 02:18:25 Starting compiler/backend/proofs
Jun 24 04:10:08 Finished compiler/backend/proofs                            1h51m42s  19GB
Jun 24 04:10:09 Starting compiler/backend/serialiser
Jun 24 04:13:37 Finished compiler/backend/serialiser                           3m28s   2GB
Jun 24 04:13:38 Starting compiler/encoders/x64/proofs
Jun 24 04:35:18 Finished compiler/encoders/x64/proofs                         21m40s   4GB
Jun 24 04:35:18 Starting compiler/encoders/arm7/proofs
Jun 24 05:04:58 Finished compiler/encoders/arm7/proofs                        29m39s   6GB
Jun 24 05:04:58 Starting compiler/encoders/arm8/proofs
Jun 24 05:20:42 Finished compiler/encoders/arm8/proofs                        15m42s   1GB
Jun 24 05:20:42 Starting compiler/encoders/arm8_asl/proofs
Jun 24 05:54:54 Finished compiler/encoders/arm8_asl/proofs                    34m12s   2GB
Jun 24 05:54:54 Starting compiler/encoders/mips/proofs
Jun 24 06:17:47 Finished compiler/encoders/mips/proofs                        22m52s   3GB
Jun 24 06:17:47 Starting compiler/encoders/riscv/proofs
Jun 24 06:37:34 Finished compiler/encoders/riscv/proofs                       19m46s   1GB
Jun 24 06:37:34 Starting compiler/encoders/ag32/proofs
Jun 24 06:43:19 Finished compiler/encoders/ag32/proofs                         5m44s   1GB
Jun 24 06:43:19 Starting compiler/backend/x64/proofs
Jun 24 06:44:20 Finished compiler/backend/x64/proofs                           1m00s   1GB
Jun 24 06:44:20 Starting compiler/backend/arm7/proofs
Jun 24 06:45:26 Finished compiler/backend/arm7/proofs                          1m04s   1GB
Jun 24 06:45:26 Starting compiler/backend/arm8/proofs
Jun 24 06:46:31 Finished compiler/backend/arm8/proofs                          1m05s   1GB
Jun 24 06:46:32 Starting compiler/backend/arm8_asl
Jun 24 06:47:27 Finished compiler/backend/arm8_asl                               54s   1GB
Jun 24 06:47:27 Starting compiler/backend/mips/proofs
Jun 24 06:48:28 Finished compiler/backend/mips/proofs                          1m01s   1GB
Jun 24 06:48:29 Starting compiler/backend/riscv/proofs
Jun 24 06:49:32 Finished compiler/backend/riscv/proofs                         1m03s   1GB
Jun 24 06:49:32 Starting compiler/backend/ag32/proofs
Jun 24 07:19:58 Finished compiler/backend/ag32/proofs                         30m25s   2GB
Jun 24 07:19:59 Starting compiler/proofs
Jun 24 07:24:45 Finished compiler/proofs                                       4m46s   4GB
Jun 24 07:24:45 Starting candle/set-theory
Jun 24 07:25:58 Finished candle/set-theory                                     1m12s 931MB
Jun 24 07:25:58 Starting candle/syntax-lib
Jun 24 07:26:29 Finished candle/syntax-lib                                       30s 675MB
Jun 24 07:26:29 Starting candle/standard/syntax
Jun 24 07:30:44 Finished candle/standard/syntax                                4m14s   1GB
Jun 24 07:30:45 Starting candle/standard/semantics
Jun 24 07:34:54 Finished candle/standard/semantics                             4m09s   1GB
Jun 24 07:34:55 Starting candle/standard/monadic
Jun 24 07:38:55 Finished candle/standard/monadic                               3m59s   1GB
Jun 24 07:38:55 Starting candle/standard/ml_kernel
Jun 24 07:52:47 Finished candle/standard/ml_kernel                            13m51s   3GB
Jun 24 07:52:47 Starting candle/overloading/syntax
Jun 24 07:59:51 Finished candle/overloading/syntax                             7m03s   1GB
Jun 24 07:59:51 Starting candle/overloading/semantics
Jun 24 08:26:28 Finished candle/overloading/semantics                         26m36s   3GB
Jun 24 08:26:28 Starting candle/overloading/monadic
Jun 24 08:31:59 Finished candle/overloading/monadic                            5m30s   1GB
Jun 24 08:31:59 Starting candle/overloading/ml_kernel
Jun 24 08:47:31 Finished candle/overloading/ml_kernel                         15m31s   3GB
Jun 24 08:47:31 Starting candle/overloading/ml_checker
Jun 24 08:52:53 Finished candle/overloading/ml_checker                         5m21s   3GB
Jun 24 08:52:53 Starting candle/prover
Jun 24 09:16:51 Finished candle/prover                                        23m58s   3GB
Jun 24 09:16:52 Starting pancake
Jun 24 09:24:48 Finished pancake                                               7m56s   4GB
Jun 24 09:24:48 Starting pancake/ffi
Jun 24 09:24:49 Finished pancake/ffi                                              0s  31MB
Jun 24 09:24:49 Starting pancake/semantics
Jun 24 09:30:17 Finished pancake/semantics                                     5m27s   1GB
Jun 24 09:30:18 Starting pancake/proofs
Jun 24 09:56:16 Finished pancake/proofs                                       25m58s   5GB
Jun 24 09:56:16 Starting characteristic/examples
Jun 24 09:59:15 Finished characteristic/examples                               2m58s   3GB
Jun 24 09:59:16 Starting tutorial/solutions
Jun 24 10:34:41 Finished tutorial/solutions                                   35m25s  10GB
Jun 24 10:34:41 Starting translator/monadic/examples
Jun 24 10:41:45 Finished translator/monadic/examples                           7m03s   2GB
Jun 24 10:41:45 Starting examples
Jun 24 11:01:37 Finished examples                                             19m51s   4GB
Jun 24 11:01:37 Starting examples/compilation/x64
Jun 24 15:37:11 Finished examples/compilation/x64                           4h35m33s  14GB
Jun 24 15:37:11 Starting examples/compilation/x64/proofs
Jun 24 15:41:44 Finished examples/compilation/x64/proofs                       4m32s   3GB
Jun 24 15:41:44 Starting examples/compilation/ag32
Jun 24 16:55:36 Finished examples/compilation/ag32                          1h13m51s   9GB
Jun 24 16:55:36 Starting examples/compilation/ag32/proofs
Jun 24 16:57:30 Finished examples/compilation/ag32/proofs                      1m54s   3GB
Jun 24 16:57:31 Starting examples/lpr_checker
Jun 24 16:59:52 Finished examples/lpr_checker                                  2m20s   1GB
Jun 24 16:59:52 Starting examples/lpr_checker/array
Jun 24 18:15:04 Finished examples/lpr_checker/array                         1h15m11s   6GB
Jun 24 18:15:04 Starting examples/lpr_checker/array/compilation
Jun 24 19:34:38 Finished examples/lpr_checker/array/compilation             1h19m33s  35GB
Jun 24 19:34:38 Starting examples/lpr_checker/array/compilation/proofs
Jun 24 19:37:24 Finished examples/lpr_checker/array/compilation/proofs         2m46s   5GB
Jun 24 19:37:24 Starting examples/opentheory
Jun 24 20:00:03 Finished examples/opentheory                                  22m38s   4GB
Jun 24 20:00:03 Starting examples/opentheory
Jun 24 20:00:06 Finished examples/opentheory                                      2s  32MB
Jun 24 20:00:06 Starting examples/opentheory/compilation
Jun 24 21:26:00 Finished examples/opentheory/compilation                    1h25m52s  39GB
Jun 24 21:26:00 Starting examples/opentheory/compilation/proofs
Jun 24 21:28:43 Finished examples/opentheory/compilation/proofs                2m43s   3GB
Jun 24 21:28:44 Starting examples/opentheory/compilation/ag32
Jun 24 22:49:28 Finished examples/opentheory/compilation/ag32               1h20m43s  41GB
Jun 24 22:49:28 Starting examples/opentheory/compilation/ag32/proofs
Jun 24 22:53:20 Finished examples/opentheory/compilation/ag32/proofs           3m51s   5GB
Jun 24 22:53:20 Starting examples/sat_encodings
Jun 24 22:57:47 Finished examples/sat_encodings                                4m27s 998MB
Jun 24 22:57:48 Starting examples/sat_encodings/case_studies
Jun 24 23:01:35 Finished examples/sat_encodings/case_studies                   3m46s 720MB
Jun 24 23:01:35 Starting examples/sat_encodings/translation
Jun 24 23:13:28 Finished examples/sat_encodings/translation                   11m52s   3GB
Jun 24 23:13:28 Starting examples/sat_encodings/translation/compilation
Jun 25 00:38:29 Finished examples/sat_encodings/translation/compilation     1h25m00s  22GB
Jun 25 00:38:29 Starting examples/deflate
Jun 25 00:40:32 Finished examples/deflate                                      2m03s 694MB
Jun 25 00:40:32 Starting examples/deflate/translation
Jun 25 00:43:38 Finished examples/deflate/translation                          3m05s   3GB
Jun 25 00:43:38 Starting examples/deflate/translation/compilation
Jun 25 01:22:30 Finished examples/deflate/translation/compilation             38m52s  14GB
Jun 25 01:22:30 Starting translator/okasaki-examples
Jun 25 01:32:50 Finished translator/okasaki-examples                          10m19s   1GB
Jun 25 01:32:50 Starting translator/other-examples
Jun 25 01:37:45 Finished translator/other-examples                             4m54s   1GB
Jun 25 01:37:45 Starting compiler/parsing/tests
Jun 25 01:38:53 Finished compiler/parsing/tests                                1m07s 518MB
Jun 25 01:38:54 Starting compiler/inference/tests
Jun 25 01:55:48 Finished compiler/inference/tests                             16m53s   7GB
Jun 25 01:55:48 Starting compiler/printing/test
Jun 25 02:03:27 Finished compiler/printing/test                                7m38s   3GB
Jun 25 02:03:27 Starting icing/flover
Jun 25 03:37:27 Finished icing/flover                                       1h33m59s   1GB
Jun 25 03:37:28 Starting icing/
Jun 25 05:52:05 Finished icing/                                             2h14m37s   8GB
Jun 25 05:52:05 Starting icing/examples
Jun 25 05:55:26 Finished icing/examples                                        3m19s   4GB
Jun 25 05:55:26 Starting compiler/repl
Jun 25 06:21:40 Finished compiler/repl                                        26m13s   4GB
Jun 25 06:21:40 Starting compiler/bootstrap/translation
Jun 25 15:47:47 Finished compiler/bootstrap/translation                     9h26m06s  37GB
Jun 25 15:47:47 Starting unverified/sexpr-bootstrap/x64/64
Jun 25 16:09:43 Finished unverified/sexpr-bootstrap/x64/64                    21m55s  10GB
Jun 25 16:09:44 Starting unverified/sexpr-bootstrap/x64/32
Jun 25 16:28:52 Finished unverified/sexpr-bootstrap/x64/32                    19m08s  10GB
Jun 25 16:28:52 Starting compiler/benchmarks
Jun 25 16:28:57 Finished compiler/benchmarks                                      5s  46MB
Jun 25 16:28:58 Starting compiler/bootstrap/compilation/x64/64
Jun 26 16:48:24 Finished compiler/bootstrap/compilation/x64/64             24h19m25s  93GB
Jun 26 16:48:25 Starting compiler/bootstrap/compilation/x64/64/proofs
Jun 26 17:33:41 Finished compiler/bootstrap/compilation/x64/64/proofs         45m16s  26GB
Jun 26 17:33:42 Starting compiler/bootstrap/compilation/x64/32
Jun 27 07:56:55 Finished compiler/bootstrap/compilation/x64/32             14h23m12s  80GB
Jun 27 07:56:55 Starting compiler/bootstrap/compilation/x64/32/proofs
Jun 27 08:02:45 Finished compiler/bootstrap/compilation/x64/32/proofs          5m49s  14GB
Jun 27 08:02:45 Starting compiler/bootstrap/compilation/ag32/32
Jun 27 22:35:56 Finished compiler/bootstrap/compilation/ag32/32            14h33m10s  93GB
Jun 27 22:35:57 Starting compiler/bootstrap/compilation/ag32/32/proofs
Jun 27 22:59:55 Finished compiler/bootstrap/compilation/ag32/32/proofs        23m58s  18GB
Jun 27 22:59:56 SUCCESS