Job 1849

CakeML:e9bb6e2eb7baa3a75974d58445d4de7b68e81999
  Make Int.gcd return non-negative result [Apr 06 05:30:09]
#873 (issue871)
Merging into:4317d3f1cb4cafc7b1ea154c0e89e4dcae2700ba
  Update COPYING [Apr 04 06:16:57]
HOL:6d938663389537576efe0d6e2eeee81911702d3d
  Extend COPYRIGHT into 2022 [Apr 03 23:12:02]
Machine:oven3

Apr 06 10:57:33 Claimed job
Apr 06 10:57:35 Reusing HOL
Apr 06 10:58:27 Starting developers
Apr 06 10:58:36 Finished developers                                               8s 106MB
Apr 06 10:58:36 Starting developers/bin
Apr 06 10:59:34 Finished developers/bin                                          58s   1GB
Apr 06 10:59:35 Starting semantics/ffi
Apr 06 10:59:58 Finished semantics/ffi                                           23s 256MB
Apr 06 10:59:58 Starting semantics
Apr 06 11:03:54 Finished semantics                                             3m55s   1GB
Apr 06 11:03:55 Starting semantics/proofs
Apr 06 11:12:53 Finished semantics/proofs                                      8m58s   2GB
Apr 06 11:12:53 Starting semantics/alt_semantics
Apr 06 11:13:49 Finished semantics/alt_semantics                                 55s 466MB
Apr 06 11:13:49 Starting semantics/alt_semantics/proofs
Apr 06 11:20:47 Finished semantics/alt_semantics/proofs                        6m57s   1GB
Apr 06 11:20:47 Starting basis/pure
Apr 06 11:23:02 Finished basis/pure                                            2m15s 962MB
Apr 06 11:23:03 Starting translator
Apr 06 11:29:19 Finished translator                                            6m16s   2GB
Apr 06 11:29:19 Starting compiler/parsing
Apr 06 11:32:03 Finished compiler/parsing                                      2m44s   2GB
Apr 06 11:32:04 Starting characteristic
Apr 06 11:45:22 Finished characteristic                                       13m17s   2GB
Apr 06 11:45:22 Starting translator/monadic
Apr 06 11:49:21 Finished translator/monadic                                    3m59s   1GB
Apr 06 11:49:21 Starting basis
Apr 06 13:32:08 Finished basis                                              1h42m46s  12GB
Apr 06 13:32:08 Starting compiler/inference
Apr 06 13:35:20 Finished compiler/inference                                    3m11s   1GB
Apr 06 13:35:20 Starting compiler/backend/reg_alloc
Apr 06 13:38:36 Finished compiler/backend/reg_alloc                            3m15s   1GB
Apr 06 13:38:36 Starting compiler/backend/gc
Apr 06 13:46:58 Finished compiler/backend/gc                                   8m21s   2GB
Apr 06 13:46:58 Starting compiler/backend
Apr 06 13:57:46 Finished compiler/backend                                     10m47s   2GB
Apr 06 13:57:46 Starting compiler/encoders/asm
Apr 06 13:58:49 Finished compiler/encoders/asm                                 1m02s 927MB
Apr 06 13:58:50 Starting compiler/encoders/x64
Apr 06 14:01:21 Finished compiler/encoders/x64                                 2m31s   1GB
Apr 06 14:01:21 Starting compiler/encoders/arm7
Apr 06 14:06:43 Finished compiler/encoders/arm7                                5m21s   1GB
Apr 06 14:06:43 Starting compiler/encoders/arm8
Apr 06 14:08:17 Finished compiler/encoders/arm8                                1m34s   1GB
Apr 06 14:08:17 Starting compiler/encoders/arm8_asl
Apr 06 18:21:15 Finished compiler/encoders/arm8_asl                         4h12m56s  50GB
Apr 06 18:21:15 Starting compiler/encoders/mips
Apr 06 18:24:39 Finished compiler/encoders/mips                                3m23s   1GB
Apr 06 18:24:39 Starting compiler/encoders/riscv
Apr 06 18:28:31 Finished compiler/encoders/riscv                               3m51s 885MB
Apr 06 18:28:31 Starting compiler/encoders/ag32
Apr 06 18:29:20 Finished compiler/encoders/ag32                                  48s 723MB
Apr 06 18:29:20 Starting compiler/backend/x64
Apr 06 18:30:08 Finished compiler/backend/x64                                    48s   1GB
Apr 06 18:30:08 Starting compiler/backend/arm7
Apr 06 18:30:58 Finished compiler/backend/arm7                                   49s   1GB
Apr 06 18:30:59 Starting compiler/backend/arm8
Apr 06 18:31:47 Finished compiler/backend/arm8                                   47s   1GB
Apr 06 18:31:47 Starting compiler/backend/mips
Apr 06 18:32:34 Finished compiler/backend/mips                                   47s   1GB
Apr 06 18:32:34 Starting compiler/backend/riscv
Apr 06 18:33:23 Finished compiler/backend/riscv                                  48s   1GB
Apr 06 18:33:23 Starting compiler/backend/ag32
Apr 06 18:36:35 Finished compiler/backend/ag32                                 3m11s   1GB
Apr 06 18:36:35 Starting compiler/parsing/proofs
Apr 06 18:45:03 Finished compiler/parsing/proofs                               8m27s   1GB
Apr 06 18:45:03 Starting compiler/inference/proofs
Apr 06 18:50:38 Finished compiler/inference/proofs                             5m34s   1GB
Apr 06 18:50:38 Starting compiler/backend/semantics
Apr 06 19:53:42 Finished compiler/backend/semantics                         1h03m03s   2GB
Apr 06 19:53:42 Starting compiler/backend/reg_alloc/proofs
Apr 06 20:01:33 Finished compiler/backend/reg_alloc/proofs                     7m51s 976MB
Apr 06 20:01:34 Starting compiler/backend/proofs
Apr 06 21:42:42 Finished compiler/backend/proofs                            1h41m08s  12GB
Apr 06 21:42:43 Starting compiler/backend/serialiser
Apr 06 21:46:02 Finished compiler/backend/serialiser                           3m19s   2GB
Apr 06 21:46:02 Starting compiler/encoders/x64/proofs
Apr 06 22:07:29 Finished compiler/encoders/x64/proofs                         21m26s   5GB
Apr 06 22:07:29 Starting compiler/encoders/arm7/proofs
Apr 06 22:36:51 Finished compiler/encoders/arm7/proofs                        29m21s   4GB
Apr 06 22:36:51 Starting compiler/encoders/arm8/proofs
Apr 06 22:52:14 Finished compiler/encoders/arm8/proofs                        15m22s   1GB
Apr 06 22:52:14 Starting compiler/encoders/arm8_asl/proofs
Apr 07 00:46:38 Finished compiler/encoders/arm8_asl/proofs                  1h54m23s   6GB
Apr 07 00:46:39 Starting compiler/encoders/mips/proofs
Apr 07 01:08:55 Finished compiler/encoders/mips/proofs                        22m16s   3GB
Apr 07 01:08:55 Starting compiler/encoders/riscv/proofs
Apr 07 01:28:51 Finished compiler/encoders/riscv/proofs                       19m55s   1GB
Apr 07 01:28:51 Starting compiler/encoders/ag32/proofs
Apr 07 01:34:39 Finished compiler/encoders/ag32/proofs                         5m48s   1GB
Apr 07 01:34:39 Starting compiler/backend/x64/proofs
Apr 07 01:35:37 Finished compiler/backend/x64/proofs                             57s   1GB
Apr 07 01:35:38 Starting compiler/backend/arm7/proofs
Apr 07 01:36:44 Finished compiler/backend/arm7/proofs                          1m06s   1GB
Apr 07 01:36:44 Starting compiler/backend/arm8/proofs
Apr 07 01:37:46 Finished compiler/backend/arm8/proofs                          1m01s   1GB
Apr 07 01:37:46 Starting compiler/backend/arm8_asl
Apr 07 01:38:36 Finished compiler/backend/arm8_asl                               49s   1GB
Apr 07 01:38:37 Starting compiler/backend/mips/proofs
Apr 07 01:39:39 Finished compiler/backend/mips/proofs                          1m02s   1GB
Apr 07 01:39:39 Starting compiler/backend/riscv/proofs
Apr 07 01:40:41 Finished compiler/backend/riscv/proofs                         1m01s   1GB
Apr 07 01:40:41 Starting compiler/backend/ag32/proofs
Apr 07 02:09:09 Finished compiler/backend/ag32/proofs                         28m27s   2GB
Apr 07 02:09:09 Starting compiler/proofs
Apr 07 02:14:11 Finished compiler/proofs                                       5m01s   3GB
Apr 07 02:14:11 Starting candle/set-theory
Apr 07 02:15:24 Finished candle/set-theory                                     1m13s 902MB
Apr 07 02:15:24 Starting candle/syntax-lib
Apr 07 02:15:54 Finished candle/syntax-lib                                       29s 708MB
Apr 07 02:15:54 Starting candle/standard/syntax
Apr 07 02:20:18 Finished candle/standard/syntax                                4m23s   1GB
Apr 07 02:20:19 Starting candle/standard/semantics
Apr 07 02:24:29 Finished candle/standard/semantics                             4m10s   1GB
Apr 07 02:24:29 Starting candle/standard/monadic
Apr 07 02:28:30 Finished candle/standard/monadic                               4m00s   1GB
Apr 07 02:28:30 Starting candle/standard/ml_kernel
Apr 07 02:41:33 Finished candle/standard/ml_kernel                            13m03s   3GB
Apr 07 02:41:33 Starting candle/overloading/syntax
Apr 07 02:48:21 Finished candle/overloading/syntax                             6m47s   1GB
Apr 07 02:48:21 Starting candle/overloading/semantics
Apr 07 03:14:30 Finished candle/overloading/semantics                         26m08s   2GB
Apr 07 03:14:31 Starting candle/overloading/monadic
Apr 07 03:19:56 Finished candle/overloading/monadic                            5m25s   1GB
Apr 07 03:19:56 Starting candle/overloading/ml_kernel
Apr 07 03:34:51 Finished candle/overloading/ml_kernel                         14m54s   3GB
Apr 07 03:34:51 Starting candle/overloading/ml_checker
Apr 07 03:40:09 Finished candle/overloading/ml_checker                         5m17s   3GB
Apr 07 03:40:09 Starting candle/prover
Apr 07 03:57:46 Finished candle/prover                                        17m36s   2GB
Apr 07 03:57:46 Starting pancake
Apr 07 04:05:25 Finished pancake                                               7m39s   3GB
Apr 07 04:05:25 Starting pancake/ffi
Apr 07 04:05:26 Finished pancake/ffi                                              0s  32MB
Apr 07 04:05:26 Starting pancake/semantics
Apr 07 04:10:48 Finished pancake/semantics                                     5m21s   1GB
Apr 07 04:10:48 Starting pancake/proofs
Apr 07 04:36:58 Finished pancake/proofs                                       26m09s   6GB
Apr 07 04:36:58 Starting characteristic/examples
Apr 07 04:39:53 Finished characteristic/examples                               2m54s   2GB
Apr 07 04:39:53 Starting tutorial/solutions
Apr 07 05:16:21 Finished tutorial/solutions                                   36m28s  11GB
Apr 07 05:16:22 Starting translator/monadic/examples
Apr 07 05:23:26 Finished translator/monadic/examples                           7m04s   2GB
Apr 07 05:23:26 Starting examples
Apr 07 05:41:44 Finished examples                                             18m17s   4GB
Apr 07 05:41:44 Starting examples/compilation/x64
Apr 07 11:17:35 Finished examples/compilation/x64                           5h35m50s  25GB
Apr 07 11:17:35 Starting examples/compilation/x64/proofs
Apr 07 11:21:49 Finished examples/compilation/x64/proofs                       4m13s   3GB
Apr 07 11:21:49 Starting examples/compilation/ag32
Apr 07 12:40:10 Finished examples/compilation/ag32                          1h18m20s  13GB
Apr 07 12:40:10 Starting examples/compilation/ag32/proofs
Apr 07 12:42:05 Finished examples/compilation/ag32/proofs                      1m54s   3GB
Apr 07 12:42:05 Starting examples/cost
Apr 07 14:41:01 Finished examples/cost                                      1h58m54s   8GB
Apr 07 14:41:01 Starting examples/lpr_checker
Apr 07 14:43:10 Finished examples/lpr_checker                                  2m08s   1GB
Apr 07 14:43:10 Starting examples/lpr_checker/array
Apr 07 15:47:19 Finished examples/lpr_checker/array                         1h04m08s   5GB
Apr 07 15:47:19 Starting examples/lpr_checker/array/compilation
Apr 07 18:55:28 Finished examples/lpr_checker/array/compilation             3h08m07s  41GB
Apr 07 18:55:28 Starting examples/lpr_checker/array/compilation/proofs
Apr 07 18:58:26 Finished examples/lpr_checker/array/compilation/proofs         2m58s   6GB
Apr 07 18:58:27 Starting examples/opentheory
Apr 07 19:19:49 Finished examples/opentheory                                  21m22s   4GB
Apr 07 19:19:49 Starting examples/opentheory
Apr 07 19:19:52 Finished examples/opentheory                                      2s  32MB
Apr 07 19:19:53 Starting examples/opentheory/compilation
Apr 07 20:51:28 Finished examples/opentheory/compilation                    1h31m33s  36GB
Apr 07 20:51:28 Starting examples/opentheory/compilation/proofs
Apr 07 20:53:45 Finished examples/opentheory/compilation/proofs                2m16s   3GB
Apr 07 20:53:45 Starting examples/opentheory/compilation/ag32
Apr 07 22:22:21 Finished examples/opentheory/compilation/ag32               1h28m35s  36GB
Apr 07 22:22:21 Starting examples/opentheory/compilation/ag32/proofs
Apr 07 22:26:09 Finished examples/opentheory/compilation/ag32/proofs           3m47s   5GB
Apr 07 22:26:09 Starting examples/sat_encodings
Apr 07 22:30:28 Finished examples/sat_encodings                                4m19s 944MB
Apr 07 22:30:29 Starting examples/sat_encodings/case_studies
Apr 07 22:34:02 Finished examples/sat_encodings/case_studies                   3m33s   1GB
Apr 07 22:34:02 Starting examples/sat_encodings/translation
Apr 07 22:45:53 Finished examples/sat_encodings/translation                   11m50s   3GB
Apr 07 22:45:53 Starting examples/sat_encodings/translation/compilation
Apr 08 00:14:24 Finished examples/sat_encodings/translation/compilation     1h28m29s  23GB
Apr 08 00:14:24 Starting translator/okasaki-examples
Apr 08 00:24:07 Finished translator/okasaki-examples                           9m43s   1GB
Apr 08 00:24:07 Starting translator/other-examples
Apr 08 00:27:56 Finished translator/other-examples                             3m48s   1GB
Apr 08 00:27:56 Starting compiler/parsing/tests
Apr 08 00:29:04 Finished compiler/parsing/tests                                1m07s 552MB
Apr 08 00:29:04 Starting compiler/inference/tests
Apr 08 00:44:51 Finished compiler/inference/tests                             15m46s   4GB
Apr 08 00:44:51 Starting compiler/printing/test
Apr 08 00:52:06 Finished compiler/printing/test                                7m14s   3GB
Apr 08 00:52:07 Starting compiler/repl
Apr 08 01:17:15 Finished compiler/repl                                        25m08s   5GB
Apr 08 01:17:15 Starting compiler/bootstrap/translation
Apr 08 09:53:16 Finished compiler/bootstrap/translation                     8h36m00s  36GB
Apr 08 09:53:17 Starting unverified/sexpr-bootstrap/x64/64
Apr 08 10:15:53 Finished unverified/sexpr-bootstrap/x64/64                    22m36s  11GB
Apr 08 10:15:53 Starting unverified/sexpr-bootstrap/x64/32
Apr 08 10:34:29 Finished unverified/sexpr-bootstrap/x64/32                    18m35s  10GB
Apr 08 10:34:29 Starting compiler/benchmarks
Apr 08 10:34:34 Finished compiler/benchmarks                                      5s  68MB
Apr 08 10:34:35 Starting compiler/bootstrap/compilation/x64/64 Apr 08 10:34:35 2641s