Job 376

CakeML:bacdfd84c86ee6dd48ef9740a9cc3e5246e3ac48
  Use symbolic names for word shift funs [Jul 12 04:31:41]
#498 (basis-word-ops)
Merging into:b33717e6844a56fad2e249cb1f2787e006735c3d
  fix duplicate rule name [Jul 21 23:15:57]
HOL:741148f614f5435da2a53e84dedd0c7a5e33d6d4
  Merge pull request #565 from AndreasLoow/holkernel-sort_vars-doc [Jul 21 09:28:01]
Machine:cakeml1795 4.4.0-98-generic x86_64 GNU/Linux

Jul 22 13:16:42 Claimed job
Jul 22 13:16:50 Reusing HOL
Jul 22 13:17:07 Starting developers/bin
Jul 22 13:17:19 Finished developers/bin                                           9s 224MB
Jul 22 13:17:21 Starting semantics/ffi
Jul 22 13:17:41 Finished semantics/ffi                                           17s 272MB
Jul 22 13:17:43 Starting semantics
Jul 22 13:19:47 Finished semantics                                             2m02s   1GB
Jul 22 13:19:49 Starting semantics/proofs
Jul 22 13:23:09 Finished semantics/proofs                                      3m17s   1GB
Jul 22 13:23:11 Starting basis/pure
Jul 22 13:24:42 Finished basis/pure                                            1m29s 855MB
Jul 22 13:24:45 Starting translator
Jul 22 13:31:34 Finished translator                                            6m47s   1GB
Jul 22 13:31:36 Starting compiler/parsing
Jul 22 13:33:47 Finished compiler/parsing                                      2m09s   2GB
Jul 22 13:33:49 Starting characteristic
Jul 22 13:38:17 Finished characteristic                                        4m26s   2GB
Jul 22 13:38:19 Starting basis
Jul 22 14:07:28 Finished basis                                                29m06s   2GB
Jul 22 14:07:30 Starting translator/monadic
Jul 22 14:07:34 Finished translator/monadic                                       2s  15MB
Jul 22 14:07:36 Starting compiler/inference
Jul 22 14:09:46 Finished compiler/inference                                    2m07s   1GB
Jul 22 14:09:48 Starting compiler/backend/reg_alloc
Jul 22 14:10:45 Finished compiler/backend/reg_alloc                              55s   1GB
Jul 22 14:10:47 Starting compiler/backend/gc
Jul 22 14:24:02 Finished compiler/backend/gc                                  13m13s   3GB
Jul 22 14:24:04 Starting compiler/backend
Jul 22 14:24:09 Finished compiler/backend                                         3s  20MB
Jul 22 14:24:11 Starting compiler/encoders/asm
Jul 22 14:24:14 Finished compiler/encoders/asm                                    0s  11MB
Jul 22 14:24:16 Starting compiler/encoders/x64
Jul 22 14:24:42 Finished compiler/encoders/x64                                   24s 434MB
Jul 22 14:24:44 Starting compiler/encoders/arm6
Jul 22 14:25:57 Finished compiler/encoders/arm6                                1m10s 398MB
Jul 22 14:25:59 Starting compiler/encoders/arm8
Jul 22 14:26:11 Finished compiler/encoders/arm8                                  10s 346MB
Jul 22 14:26:13 Starting compiler/encoders/mips
Jul 22 14:26:29 Finished compiler/encoders/mips                                  13s 496MB
Jul 22 14:26:31 Starting compiler/encoders/riscv
Jul 22 14:26:44 Finished compiler/encoders/riscv                                 11s 431MB
Jul 22 14:26:46 Starting compiler/backend/x64
Jul 22 14:27:19 Finished compiler/backend/x64                                    31s   1GB
Jul 22 14:27:21 Starting compiler/backend/arm6
Jul 22 14:27:57 Finished compiler/backend/arm6                                   33s   1GB
Jul 22 14:27:59 Starting compiler/backend/arm8
Jul 22 14:28:36 Finished compiler/backend/arm8                                   35s 956MB
Jul 22 14:28:38 Starting compiler/backend/mips
Jul 22 14:29:11 Finished compiler/backend/mips                                   31s 976MB
Jul 22 14:29:13 Starting compiler/backend/riscv
Jul 22 14:29:48 Finished compiler/backend/riscv                                  32s   1GB
Jul 22 14:29:50 Starting compiler/parsing/proofs
Jul 22 14:34:07 Finished compiler/parsing/proofs                               4m15s 649MB
Jul 22 14:34:09 Starting compiler/inference/proofs
Jul 22 14:38:10 Finished compiler/inference/proofs                             3m58s   1GB
Jul 22 14:38:12 Starting compiler/backend/semantics
Jul 22 14:52:44 Finished compiler/backend/semantics                           14m30s   2GB
Jul 22 14:52:46 Starting compiler/backend/reg_alloc/proofs
Jul 22 14:54:12 Finished compiler/backend/reg_alloc/proofs                     1m23s 425MB
Jul 22 14:54:14 Starting compiler/backend/proofs
Jul 22 15:50:30 Finished compiler/backend/proofs                              56m13s   3GB
Jul 22 15:50:32 Starting compiler/encoders/x64/proofs
Jul 22 16:00:16 Finished compiler/encoders/x64/proofs                          9m41s   1GB
Jul 22 16:00:18 Starting compiler/encoders/arm6/proofs
Jul 22 16:10:09 Finished compiler/encoders/arm6/proofs                         9m48s   1GB
Jul 22 16:10:11 Starting compiler/encoders/arm8/proofs
Jul 22 16:18:13 Finished compiler/encoders/arm8/proofs                         8m00s   1GB
Jul 22 16:18:15 Starting compiler/encoders/mips/proofs
Jul 22 16:28:54 Finished compiler/encoders/mips/proofs                        10m36s   2GB
Jul 22 16:28:55 Starting compiler/encoders/riscv/proofs
Jul 22 16:41:15 Finished compiler/encoders/riscv/proofs                       12m17s   1GB
Jul 22 16:41:17 Starting compiler/backend/x64/proofs
Jul 22 16:41:54 Finished compiler/backend/x64/proofs                             34s   1GB
Jul 22 16:41:56 Starting compiler/backend/arm6/proofs
Jul 22 16:42:35 Finished compiler/backend/arm6/proofs                            37s   1GB
Jul 22 16:42:37 Starting compiler/backend/arm8/proofs
Jul 22 16:43:12 Finished compiler/backend/arm8/proofs                            32s   1GB
Jul 22 16:43:14 Starting compiler/backend/mips/proofs
Jul 22 16:43:50 Finished compiler/backend/mips/proofs                            34s   1GB
Jul 22 16:43:52 Starting compiler/backend/riscv/proofs
Jul 22 16:44:29 Finished compiler/backend/riscv/proofs                           34s   1GB
Jul 22 16:44:31 Starting compiler/proofs
Jul 22 16:46:56 Finished compiler/proofs                                       2m23s   2GB
Jul 22 16:46:58 Starting candle/set-theory
Jul 22 16:47:44 Finished candle/set-theory                                       43s 632MB
Jul 22 16:47:46 Starting candle/syntax-lib
Jul 22 16:48:05 Finished candle/syntax-lib                                       17s 410MB
Jul 22 16:48:07 Starting candle/standard/syntax
Jul 22 16:50:52 Finished candle/standard/syntax                                2m42s 643MB
Jul 22 16:50:54 Starting candle/standard/semantics
Jul 22 16:53:12 Finished candle/standard/semantics                             2m16s   1GB
Jul 22 16:53:14 Starting candle/standard/monadic
Jul 22 16:55:38 Finished candle/standard/monadic                               2m21s 928MB
Jul 22 16:55:40 Starting candle/standard/ml_kernel
Jul 22 17:06:12 Finished candle/standard/ml_kernel                            10m24s   2GB
Jul 22 17:06:14 Starting candle/standard/opentheory
Jul 22 17:06:47 Finished candle/standard/opentheory                              24s 803MB
Jul 22 17:06:54 Starting characteristic/examples
Jul 22 17:09:23 Finished characteristic/examples                               2m26s   1GB
Jul 22 17:09:25 Starting tutorial/solutions
Jul 22 17:45:24 Finished tutorial/solutions                                   35m57s  14GB
Jul 22 17:45:26 Starting translator/monadic/examples
Jul 22 17:48:24 Finished translator/monadic/examples                           2m56s   3GB
Jul 22 17:48:26 Starting examples
Jul 22 17:56:45 Finished examples                                              8m16s   2GB
Jul 22 17:56:47 Starting examples/compilation
Jul 22 23:55:46 Finished examples/compilation                               5h58m57s  20GB
Jul 22 23:55:48 Starting examples/compilation/proofs
Jul 23 00:01:22 Finished examples/compilation/proofs                           5m31s   5GB
Jul 23 00:01:24 Starting compiler/benchmarks
Jul 23 00:01:26 Finished compiler/benchmarks                                      0s   4MB
Jul 23 00:01:28 Starting translator/okasaki-examples
Jul 23 00:08:08 Finished translator/okasaki-examples                           6m37s   1GB
Jul 23 00:08:10 Starting translator/other-examples
Jul 23 00:09:04 Finished translator/other-examples                               52s 848MB
Jul 23 00:09:06 Starting compiler/parsing/tests
Jul 23 00:09:49 Finished compiler/parsing/tests                                  41s 345MB
Jul 23 00:09:51 Starting compiler/bootstrap/translation
Jul 23 08:22:38 Finished compiler/bootstrap/translation                     8h12m44s  46GB
Jul 23 08:22:40 Starting unverified/sexpr-bootstrap/x64/64
Jul 23 08:33:53 Finished unverified/sexpr-bootstrap/x64/64                    11m11s  14GB
Jul 23 08:33:55 Starting unverified/sexpr-bootstrap/x64/32
Jul 23 08:43:15 Finished unverified/sexpr-bootstrap/x64/32                     9m18s  13GB
Jul 23 08:43:17 Starting compiler/bootstrap/compilation/x64/64
Jul 26 03:48:42 Resuming compiler/bootstrap/compilation/x64/64
Jul 26 07:15:45 Finished compiler/bootstrap/compilation/x64/64              3h27m01s  58GB
Jul 26 07:15:47 Starting compiler/bootstrap/compilation/x64/64/proofs
Jul 26 07:21:16 Finished compiler/bootstrap/compilation/x64/64/proofs          5m26s  26GB
Jul 26 07:21:18 Starting compiler/bootstrap/compilation/x64/32
Jul 27 08:54:39 Finished compiler/bootstrap/compilation/x64/32             25h33m18s  88GB
Jul 27 08:54:41 Starting compiler/bootstrap/compilation/x64/32/proofs
Jul 27 08:58:33 Finished compiler/bootstrap/compilation/x64/32/proofs          3m50s  38GB
Jul 27 08:58:35 SUCCESS