Job 747

CakeML:465aae4e3ae9643e44fd7bf01bdca6b14c7728fc
  Move machinecode soundness into readerProgProof [Mar 02 19:17:45]
#619 (reader-jlamp)
Merging into:733a34d499eb121628e888ad1aa7a30599b91311
  Merge pull request #618 from CakeML/monadic-trans-cleanup [Feb 25 11:13:00]
HOL:cc3d97c25b76afb8588059447f401e3803586076
  Remove language suggesting tyops may have different suffix strengths [Feb 28 05:32:51]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Mar 04 09:00:37 Claimed job
Mar 04 09:01:12 Building HOL
Mar 04 09:10:27 Starting developers
Mar 04 09:10:30 Finished developers                                               2s  20MB
Mar 04 09:10:31 Starting developers/bin
Mar 04 09:11:37 Finished developers/bin                                        1m05s 918MB
Mar 04 09:11:38 Starting semantics/ffi
Mar 04 09:12:17 Finished semantics/ffi                                           37s 359MB
Mar 04 09:12:17 Starting semantics
Mar 04 09:13:53 Finished semantics                                             1m34s   1GB
Mar 04 09:13:53 Starting semantics/proofs
Mar 04 09:16:47 Finished semantics/proofs                                      2m53s   1GB
Mar 04 09:16:48 Starting basis/pure
Mar 04 09:20:23 Finished basis/pure                                            3m34s 594MB
Mar 04 09:20:24 Starting translator
Mar 04 09:22:03 Finished translator                                            1m39s   1GB
Mar 04 09:22:04 Starting compiler/parsing
Mar 04 09:23:01 Finished compiler/parsing                                        56s   1GB
Mar 04 09:23:02 Starting characteristic
Mar 04 09:27:18 Finished characteristic                                        4m15s   1GB
Mar 04 09:27:19 Starting translator/monadic
Mar 04 09:28:46 Finished translator/monadic                                    1m26s   1GB
Mar 04 09:28:47 Starting basis
Mar 04 09:45:04 Finished basis                                                16m16s   2GB
Mar 04 09:45:05 Starting compiler/inference
Mar 04 09:46:57 Finished compiler/inference                                    1m51s   1GB
Mar 04 09:46:58 Starting compiler/backend/reg_alloc
Mar 04 09:47:50 Finished compiler/backend/reg_alloc                              51s   1GB
Mar 04 09:47:50 Starting compiler/backend/gc
Mar 04 09:56:52 Finished compiler/backend/gc                                   9m00s   1GB
Mar 04 09:56:53 Starting compiler/backend
Mar 04 09:56:56 Finished compiler/backend                                         2s  22MB
Mar 04 09:56:56 Starting compiler/encoders/asm
Mar 04 09:56:58 Finished compiler/encoders/asm                                    1s  16MB
Mar 04 09:56:59 Starting compiler/encoders/x64
Mar 04 09:57:59 Finished compiler/encoders/x64                                   59s 637MB
Mar 04 09:58:00 Starting compiler/encoders/arm6
Mar 04 09:59:41 Finished compiler/encoders/arm6                                1m40s   1GB
Mar 04 09:59:42 Starting compiler/encoders/arm8
Mar 04 10:00:14 Finished compiler/encoders/arm8                                  31s 561MB
Mar 04 10:00:14 Starting compiler/encoders/mips
Mar 04 10:01:20 Finished compiler/encoders/mips                                1m05s   1GB
Mar 04 10:01:21 Starting compiler/encoders/riscv
Mar 04 10:02:28 Finished compiler/encoders/riscv                               1m06s 836MB
Mar 04 10:02:29 Starting compiler/encoders/ag32
Mar 04 10:02:46 Finished compiler/encoders/ag32                                  17s 646MB
Mar 04 10:02:47 Starting compiler/backend/x64
Mar 04 10:03:06 Finished compiler/backend/x64                                    17s   1GB
Mar 04 10:03:06 Starting compiler/backend/arm6
Mar 04 10:03:25 Finished compiler/backend/arm6                                   18s   1GB
Mar 04 10:03:26 Starting compiler/backend/arm8
Mar 04 10:03:45 Finished compiler/backend/arm8                                   18s   1GB
Mar 04 10:03:45 Starting compiler/backend/mips
Mar 04 10:04:03 Finished compiler/backend/mips                                   17s 784MB
Mar 04 10:04:04 Starting compiler/backend/riscv
Mar 04 10:04:22 Finished compiler/backend/riscv                                  17s 982MB
Mar 04 10:04:23 Starting compiler/backend/ag32
Mar 04 10:05:30 Finished compiler/backend/ag32                                 1m06s   1GB
Mar 04 10:05:30 Starting compiler/parsing/proofs
Mar 04 10:11:09 Finished compiler/parsing/proofs                               5m37s 834MB
Mar 04 10:11:10 Starting compiler/inference/proofs
Mar 04 10:13:47 Finished compiler/inference/proofs                             2m36s   1GB
Mar 04 10:13:48 Starting compiler/backend/semantics
Mar 04 10:20:38 Finished compiler/backend/semantics                            6m49s   1GB
Mar 04 10:20:38 Starting compiler/backend/reg_alloc/proofs
Mar 04 10:23:15 Finished compiler/backend/reg_alloc/proofs                     2m36s 843MB
Mar 04 10:23:16 Starting compiler/backend/proofs
Mar 04 11:00:08 Finished compiler/backend/proofs                              36m51s   3GB
Mar 04 11:00:09 Starting compiler/encoders/x64/proofs
Mar 04 11:10:02 Finished compiler/encoders/x64/proofs                          9m52s   5GB
Mar 04 11:10:03 Starting compiler/encoders/arm6/proofs
Mar 04 11:23:23 Finished compiler/encoders/arm6/proofs                        13m19s   3GB
Mar 04 11:23:24 Starting compiler/encoders/arm8/proofs
Mar 04 11:29:08 Finished compiler/encoders/arm8/proofs                         5m44s   1GB
Mar 04 11:29:09 Starting compiler/encoders/mips/proofs
Mar 04 11:39:02 Finished compiler/encoders/mips/proofs                         9m52s   2GB
Mar 04 11:39:03 Starting compiler/encoders/riscv/proofs
Mar 04 11:46:34 Finished compiler/encoders/riscv/proofs                        7m31s   1GB
Mar 04 11:46:35 Starting compiler/encoders/ag32/proofs
Mar 04 11:49:03 Finished compiler/encoders/ag32/proofs                         2m27s 697MB
Mar 04 11:49:04 Starting compiler/backend/x64/proofs
Mar 04 11:49:23 Finished compiler/backend/x64/proofs                             18s 788MB
Mar 04 11:49:24 Starting compiler/backend/arm6/proofs
Mar 04 11:49:46 Finished compiler/backend/arm6/proofs                            21s   1GB
Mar 04 11:49:47 Starting compiler/backend/arm8/proofs
Mar 04 11:50:06 Finished compiler/backend/arm8/proofs                            19s   1GB
Mar 04 11:50:07 Starting compiler/backend/mips/proofs
Mar 04 11:50:28 Finished compiler/backend/mips/proofs                            20s   1GB
Mar 04 11:50:29 Starting compiler/backend/riscv/proofs
Mar 04 11:50:50 Finished compiler/backend/riscv/proofs                           19s   1GB
Mar 04 11:50:50 Starting compiler/backend/ag32/proofs
Mar 04 11:59:34 Finished compiler/backend/ag32/proofs                          8m43s   2GB
Mar 04 11:59:35 Starting compiler/proofs
Mar 04 12:01:14 Finished compiler/proofs                                       1m38s   2GB
Mar 04 12:01:15 Starting candle/set-theory
Mar 04 12:01:41 Finished candle/set-theory                                       26s 694MB
Mar 04 12:01:42 Starting candle/syntax-lib
Mar 04 12:01:54 Finished candle/syntax-lib                                       11s 557MB
Mar 04 12:01:54 Starting candle/standard/syntax
Mar 04 12:03:40 Finished candle/standard/syntax                                1m44s   1GB
Mar 04 12:03:41 Starting candle/standard/semantics
Mar 04 12:05:18 Finished candle/standard/semantics                             1m36s   1GB
Mar 04 12:05:19 Starting candle/standard/monadic
Mar 04 12:06:52 Finished candle/standard/monadic                               1m32s   1GB
Mar 04 12:06:52 Starting candle/standard/ml_kernel
Mar 04 12:10:30 Finished candle/standard/ml_kernel                             3m36s   3GB
Mar 04 12:10:31 Starting candle/standard/opentheory
Mar 04 12:18:46 Finished candle/standard/opentheory                            8m15s   3GB
Mar 04 12:18:47 Starting candle/standard/opentheory/compilation
Mar 04 12:47:27 Finished candle/standard/opentheory/compilation               28m39s  14GB
Mar 04 12:47:28 Starting candle/standard/opentheory/compilation/proofs
Mar 04 12:48:09 Finished candle/standard/opentheory/compilation/proofs           40s   3GB
Mar 04 12:48:09 Starting characteristic/examples
Mar 04 12:49:31 Finished characteristic/examples                               1m21s   2GB
Mar 04 12:49:32 Starting tutorial/solutions
Mar 04 13:02:51 Finished tutorial/solutions                                   13m18s   6GB
Mar 04 13:02:51 Starting translator/monadic/examples
Mar 04 13:05:17 Finished translator/monadic/examples                           2m24s   2GB
Mar 04 13:05:17 Starting examples
Mar 04 13:12:42 Finished examples                                              7m24s   3GB
Mar 04 13:12:43 Starting examples/compilation/x64
Mar 04 15:05:45 Finished examples/compilation/x64                           1h53m01s  11GB
Mar 04 15:05:46 Starting examples/compilation/x64/proofs
Mar 04 15:07:11 Finished examples/compilation/x64/proofs                       1m24s   2GB
Mar 04 15:07:12 Starting examples/compilation/ag32
Mar 04 15:34:49 Finished examples/compilation/ag32                            27m36s   6GB
Mar 04 15:34:50 Starting examples/compilation/ag32/proofs
Mar 04 15:35:33 Finished examples/compilation/ag32/proofs                        42s   3GB
Mar 04 15:35:34 Starting translator/okasaki-examples
Mar 04 15:39:35 Finished translator/okasaki-examples                           4m00s   1GB
Mar 04 15:39:36 Starting translator/other-examples
Mar 04 15:43:11 Finished translator/other-examples                             3m34s   1GB
Mar 04 15:43:12 Starting compiler/parsing/tests
Mar 04 15:43:38 Finished compiler/parsing/tests                                  25s 439MB
Mar 04 15:43:39 Starting compiler/inference/tests
Mar 04 15:47:37 Finished compiler/inference/tests                              3m57s   4GB
Mar 04 15:47:37 Starting compiler/bootstrap/translation
Mar 04 18:08:49 Finished compiler/bootstrap/translation                     2h21m10s  44GB
Mar 04 18:08:50 Starting unverified/sexpr-bootstrap/x64/64
Mar 04 18:16:16 Finished unverified/sexpr-bootstrap/x64/64                     7m25s   2GB
Mar 04 18:16:16 Starting unverified/sexpr-bootstrap/x64/32
Mar 04 18:21:31 Finished unverified/sexpr-bootstrap/x64/32                     5m13s   5GB
Mar 04 18:21:32 Starting compiler/benchmarks
Mar 04 18:21:39 Finished compiler/benchmarks                                      6s  34MB
Mar 04 18:21:40 Starting compiler/bootstrap/compilation/x64/64
Mar 05 05:45:08 Finished compiler/bootstrap/compilation/x64/64             11h23m26s  64GB
Mar 05 05:45:08 Starting compiler/bootstrap/compilation/x64/64/proofs
Mar 05 05:48:15 Finished compiler/bootstrap/compilation/x64/64/proofs          3m06s   4GB
Mar 05 05:48:16 Starting compiler/bootstrap/compilation/x64/32
Mar 05 15:56:36 Finished compiler/bootstrap/compilation/x64/32             10h08m19s  64GB
Mar 05 15:56:37 Starting compiler/bootstrap/compilation/x64/32/proofs
Mar 05 15:59:38 Finished compiler/bootstrap/compilation/x64/32/proofs          3m00s   5GB
Mar 05 15:59:38 Starting compiler/bootstrap/compilation/ag32/32
Mar 06 01:44:41 Finished compiler/bootstrap/compilation/ag32/32             9h45m01s  64GB
Mar 06 01:44:41 Starting compiler/bootstrap/compilation/ag32/32/proofs
Mar 06 01:59:58 Finished compiler/bootstrap/compilation/ag32/32/proofs        15m16s  12GB
Mar 06 01:59:59 SUCCESS