Job 1195

CakeML:e601a7b5e675a8f4f760735cee79c04e1692598d
  Merge pull request #724 from talsewell/constrain_op_case [Feb 23 19:40:17]
HOL:48feab678f6fc7755c459eab159ef9230a569734
  Merge remote-tracking branch 'origin/develop' into thibault-wip [Feb 21 13:30:53]
Machine:oven3 4.19.67.1.amd64-smp
Artefacts:cake-x64-32.tar.gz
cake-unverified-x64-64.tar.gz
cake-unverified-x64-32.tar.gz
cake-x64-64.tar.gz

Feb 23 19:54:28 Claimed job
Feb 23 19:54:34 Building HOL
Feb 23 20:19:48 Starting developers
Feb 23 20:19:55 Finished developers                                               7s 114MB
Feb 23 20:19:56 Starting developers/bin
Feb 23 20:20:11 Finished developers/bin                                          15s   1GB
Feb 23 20:20:11 Starting semantics/ffi
Feb 23 20:20:34 Finished semantics/ffi                                           23s 261MB
Feb 23 20:20:35 Starting semantics
Feb 23 20:23:33 Finished semantics                                             2m58s 942MB
Feb 23 20:23:33 Starting semantics/proofs
Feb 23 20:30:45 Finished semantics/proofs                                      7m11s   1GB
Feb 23 20:30:45 Starting semantics/alt_semantics
Feb 23 20:31:03 Finished semantics/alt_semantics                                 17s 317MB
Feb 23 20:31:04 Starting semantics/alt_semantics/proofs
Feb 23 20:35:23 Finished semantics/alt_semantics/proofs                        4m19s 867MB
Feb 23 20:35:24 Starting basis/pure
Feb 23 20:41:24 Finished basis/pure                                            5m59s 876MB
Feb 23 20:41:24 Starting translator
Feb 23 20:46:34 Finished translator                                            5m10s   1GB
Feb 23 20:46:34 Starting compiler/parsing
Feb 23 20:48:50 Finished compiler/parsing                                      2m15s   3GB
Feb 23 20:48:51 Starting characteristic
Feb 23 21:00:53 Finished characteristic                                       12m02s   2GB
Feb 23 21:00:53 Starting translator/monadic
Feb 23 21:04:07 Finished translator/monadic                                    3m13s   1GB
Feb 23 21:04:07 Starting basis
Feb 23 22:09:08 Finished basis                                              1h04m59s  29GB
Feb 23 22:09:08 Starting compiler/inference
Feb 23 22:11:36 Finished compiler/inference                                    2m28s   1GB
Feb 23 22:11:37 Starting compiler/backend/reg_alloc
Feb 23 22:13:35 Finished compiler/backend/reg_alloc                            1m57s   1GB
Feb 23 22:13:35 Starting compiler/backend/gc
Feb 23 22:19:57 Finished compiler/backend/gc                                   6m21s   1GB
Feb 23 22:19:57 Starting compiler/backend
Feb 23 22:28:20 Finished compiler/backend                                      8m22s   3GB
Feb 23 22:28:20 Starting compiler/encoders/asm
Feb 23 22:29:07 Finished compiler/encoders/asm                                   47s 784MB
Feb 23 22:29:07 Starting compiler/encoders/x64
Feb 23 22:31:13 Finished compiler/encoders/x64                                 2m05s 912MB
Feb 23 22:31:14 Starting compiler/encoders/arm7
Feb 23 22:34:59 Finished compiler/encoders/arm7                                3m45s   1GB
Feb 23 22:34:59 Starting compiler/encoders/arm8
Feb 23 22:36:12 Finished compiler/encoders/arm8                                1m12s 931MB
Feb 23 22:36:12 Starting compiler/encoders/mips
Feb 23 22:38:37 Finished compiler/encoders/mips                                2m24s   1GB
Feb 23 22:38:37 Starting compiler/encoders/riscv
Feb 23 22:41:31 Finished compiler/encoders/riscv                               2m53s 773MB
Feb 23 22:41:31 Starting compiler/encoders/ag32
Feb 23 22:42:10 Finished compiler/encoders/ag32                                  38s 562MB
Feb 23 22:42:10 Starting compiler/backend/x64
Feb 23 22:42:49 Finished compiler/backend/x64                                    39s   1GB
Feb 23 22:42:49 Starting compiler/backend/arm7
Feb 23 22:43:34 Finished compiler/backend/arm7                                   44s   1GB
Feb 23 22:43:34 Starting compiler/backend/arm8
Feb 23 22:44:13 Finished compiler/backend/arm8                                   38s   1GB
Feb 23 22:44:13 Starting compiler/backend/mips
Feb 23 22:44:54 Finished compiler/backend/mips                                   41s   1GB
Feb 23 22:44:55 Starting compiler/backend/riscv
Feb 23 22:45:36 Finished compiler/backend/riscv                                  41s   1GB
Feb 23 22:45:36 Starting compiler/backend/ag32
Feb 23 22:47:58 Finished compiler/backend/ag32                                 2m20s   1GB
Feb 23 22:47:58 Starting compiler/parsing/proofs
Feb 23 22:59:54 Finished compiler/parsing/proofs                              11m56s 996MB
Feb 23 22:59:55 Starting compiler/inference/proofs
Feb 23 23:05:09 Finished compiler/inference/proofs                             5m14s   2GB
Feb 23 23:05:10 Starting compiler/backend/semantics
Feb 24 00:02:14 Finished compiler/backend/semantics                           57m04s   1GB
Feb 24 00:02:14 Starting compiler/backend/reg_alloc/proofs
Feb 24 00:09:30 Finished compiler/backend/reg_alloc/proofs                     7m15s 812MB
Feb 24 00:09:30 Starting compiler/backend/proofs
Feb 24 02:10:13 Finished compiler/backend/proofs                            2h00m43s  13GB
Feb 24 02:10:14 Starting compiler/encoders/x64/proofs
Feb 24 02:30:19 Finished compiler/encoders/x64/proofs                         20m04s   4GB
Feb 24 02:30:19 Starting compiler/encoders/arm7/proofs
Feb 24 02:57:27 Finished compiler/encoders/arm7/proofs                        27m07s   3GB
Feb 24 02:57:27 Starting compiler/encoders/arm8/proofs
Feb 24 03:11:37 Finished compiler/encoders/arm8/proofs                        14m09s   1GB
Feb 24 03:11:37 Starting compiler/encoders/mips/proofs
Feb 24 03:32:45 Finished compiler/encoders/mips/proofs                        21m07s   2GB
Feb 24 03:32:45 Starting compiler/encoders/riscv/proofs
Feb 24 03:51:44 Finished compiler/encoders/riscv/proofs                       18m58s   1GB
Feb 24 03:51:44 Starting compiler/encoders/ag32/proofs
Feb 24 03:57:02 Finished compiler/encoders/ag32/proofs                         5m18s 820MB
Feb 24 03:57:03 Starting compiler/backend/x64/proofs
Feb 24 03:57:45 Finished compiler/backend/x64/proofs                             42s   1GB
Feb 24 03:57:45 Starting compiler/backend/arm7/proofs
Feb 24 03:58:33 Finished compiler/backend/arm7/proofs                            47s   1GB
Feb 24 03:58:33 Starting compiler/backend/arm8/proofs
Feb 24 03:59:15 Finished compiler/backend/arm8/proofs                            42s   1GB
Feb 24 03:59:15 Starting compiler/backend/mips/proofs
Feb 24 04:00:00 Finished compiler/backend/mips/proofs                            44s   1GB
Feb 24 04:00:00 Starting compiler/backend/riscv/proofs
Feb 24 04:00:44 Finished compiler/backend/riscv/proofs                           43s   1GB
Feb 24 04:00:44 Starting compiler/backend/ag32/proofs
Feb 24 04:27:25 Finished compiler/backend/ag32/proofs                         26m40s   2GB
Feb 24 04:27:25 Starting compiler/proofs
Feb 24 04:31:02 Finished compiler/proofs                                       3m36s   3GB
Feb 24 04:31:02 Starting candle/set-theory
Feb 24 04:31:57 Finished candle/set-theory                                       55s 981MB
Feb 24 04:31:58 Starting candle/syntax-lib
Feb 24 04:32:19 Finished candle/syntax-lib                                       21s 675MB
Feb 24 04:32:19 Starting candle/standard/syntax
Feb 24 04:36:02 Finished candle/standard/syntax                                3m42s   1GB
Feb 24 04:36:02 Starting candle/standard/semantics
Feb 24 04:39:38 Finished candle/standard/semantics                             3m35s   1GB
Feb 24 04:39:38 Starting candle/standard/monadic
Feb 24 04:43:06 Finished candle/standard/monadic                               3m27s   1GB
Feb 24 04:43:06 Starting candle/standard/ml_kernel
Feb 24 04:53:48 Finished candle/standard/ml_kernel                            10m42s   3GB
Feb 24 04:53:49 Starting candle/standard/opentheory
Feb 24 05:12:47 Finished candle/standard/opentheory                           18m58s   3GB
Feb 24 05:12:47 Starting candle/standard/opentheory/compilation
Feb 24 06:16:02 Finished candle/standard/opentheory/compilation             1h03m14s  28GB
Feb 24 06:16:02 Starting candle/standard/opentheory/compilation/proofs
Feb 24 06:17:21 Finished candle/standard/opentheory/compilation/proofs         1m18s   3GB
Feb 24 06:17:21 Starting candle/overloading/syntax
Feb 24 06:23:35 Finished candle/overloading/syntax                             6m14s   1GB
Feb 24 06:23:36 Starting candle/overloading/semantics
Feb 24 06:38:13 Finished candle/overloading/semantics                         14m37s   3GB
Feb 24 06:38:13 Starting characteristic/examples
Feb 24 06:41:01 Finished characteristic/examples                               2m47s   2GB
Feb 24 06:41:01 Starting tutorial/solutions
Feb 24 07:11:27 Finished tutorial/solutions                                   30m26s   7GB
Feb 24 07:11:28 Starting translator/monadic/examples
Feb 24 07:16:41 Finished translator/monadic/examples                           5m13s   2GB
Feb 24 07:16:41 Starting examples
Feb 24 07:31:32 Finished examples                                             14m50s   5GB
Feb 24 07:31:32 Starting examples/compilation/x64
Feb 24 12:18:51 Finished examples/compilation/x64                           4h47m18s  11GB
Feb 24 12:18:51 Starting examples/compilation/x64/proofs
Feb 24 12:21:44 Finished examples/compilation/x64/proofs                       2m52s   2GB
Feb 24 12:21:45 Starting examples/compilation/ag32
Feb 24 13:28:27 Finished examples/compilation/ag32                          1h06m41s   6GB
Feb 24 13:28:27 Starting examples/compilation/ag32/proofs
Feb 24 13:29:50 Finished examples/compilation/ag32/proofs                      1m22s   2GB
Feb 24 13:29:50 Starting examples/cost
Feb 24 14:54:56 Finished examples/cost                                      1h25m05s   6GB
Feb 24 14:54:57 Starting examples/lpr_checker
Feb 24 15:02:18 Finished examples/lpr_checker                                  7m21s   2GB
Feb 24 15:02:18 Starting examples/lpr_checker/compilation
Feb 24 15:34:09 Finished examples/lpr_checker/compilation                     31m50s   8GB
Feb 24 15:34:09 Starting examples/lpr_checker/compilation/proofs
Feb 24 15:35:27 Finished examples/lpr_checker/compilation/proofs               1m17s   2GB
Feb 24 15:35:27 Starting examples/lpr_checker/array
Feb 24 15:52:08 Finished examples/lpr_checker/array                           16m40s   2GB
Feb 24 15:52:08 Starting examples/lpr_checker/array/compilation
Feb 24 16:24:51 Finished examples/lpr_checker/array/compilation               32m42s   9GB
Feb 24 16:24:51 Starting examples/lpr_checker/array/compilation/proofs
Feb 24 16:26:19 Finished examples/lpr_checker/array/compilation/proofs         1m27s   3GB
Feb 24 16:26:19 Starting translator/okasaki-examples
Feb 24 16:34:44 Finished translator/okasaki-examples                           8m24s   1GB
Feb 24 16:34:44 Starting translator/other-examples
Feb 24 16:38:26 Finished translator/other-examples                             3m41s   1GB
Feb 24 16:38:26 Starting compiler/parsing/tests
Feb 24 16:39:22 Finished compiler/parsing/tests                                  56s 621MB
Feb 24 16:39:22 Starting compiler/inference/tests
Feb 24 16:47:59 Finished compiler/inference/tests                              8m35s   2GB
Feb 24 16:47:59 Starting compiler/bootstrap/translation
Feb 24 22:11:13 Finished compiler/bootstrap/translation                     5h23m13s  55GB
Feb 24 22:11:13 Starting unverified/sexpr-bootstrap/x64/64
Feb 24 22:37:39 Finished unverified/sexpr-bootstrap/x64/64                    26m25s   7GB
Feb 24 22:37:40 Starting unverified/sexpr-bootstrap/x64/32
Feb 24 22:57:32 Finished unverified/sexpr-bootstrap/x64/32                    19m52s   8GB
Feb 24 22:57:33 Starting compiler/benchmarks
Feb 24 22:57:36 Finished compiler/benchmarks                                      3s  33MB
Feb 24 22:57:37 Starting compiler/bootstrap/compilation/x64/64
Feb 26 06:54:15 Finished compiler/bootstrap/compilation/x64/64             31h56m36s 109GB
Feb 26 06:54:15 Starting compiler/bootstrap/compilation/x64/64/proofs
Feb 26 06:58:40 Finished compiler/bootstrap/compilation/x64/64/proofs          4m25s  18GB
Feb 26 06:58:41 Starting compiler/bootstrap/compilation/x64/32
Feb 27 08:59:02 Finished compiler/bootstrap/compilation/x64/32             26h00m20s 106GB
Feb 27 08:59:02 Starting compiler/bootstrap/compilation/x64/32/proofs
Feb 27 09:03:11 Finished compiler/bootstrap/compilation/x64/32/proofs          4m09s  18GB
Feb 27 09:03:12 Starting compiler/bootstrap/compilation/ag32/32
Feb 28 16:03:14 Finished compiler/bootstrap/compilation/ag32/32            31h00m01s 109GB
Feb 28 16:03:14 Starting compiler/bootstrap/compilation/ag32/32/proofs
Feb 28 16:29:23 Finished compiler/bootstrap/compilation/ag32/32/proofs        26m08s  45GB
Feb 28 16:29:23 SUCCESS