Job 537

CakeML:2dbbedaaf12c5d667f10593bb3c9014b0969ec23
  Put semantics/proofs into characteristic's INCLUDES [Oct 16 03:56:40]
#543 (characteristic-hmakefile-fix)
Merging into:eade0f2f7ccfe17bb7042cdc67f8379ff7edd270
  Add OpenTheory compiler proofs to build-sequence [Oct 16 04:15:06]
HOL:1b4a5d5506b74451f62ba916ec8e07ecac2aad6a
  Merge pull request #603 from thtuerk/fix_pattern_match_demo [Oct 17 23:30:26]
Machine:oven2 4.13.0-37-generic x86_64 GNU/Linux

Oct 18 19:09:05 Claimed job
Oct 18 19:10:27 Building HOL
Oct 18 19:18:11 Starting developers/bin
Oct 18 19:18:47 Finished developers/bin                                          35s 138MB
Oct 18 19:18:47 Starting semantics/ffi
Oct 18 19:19:23 Finished semantics/ffi                                           34s 410MB
Oct 18 19:19:24 Starting semantics
Oct 18 19:20:44 Finished semantics                                             1m19s 839MB
Oct 18 19:20:45 Starting semantics/proofs
Oct 18 19:23:26 Finished semantics/proofs                                      2m40s 896MB
Oct 18 19:23:27 Starting basis/pure
Oct 18 19:26:55 Finished basis/pure                                            3m27s 658MB
Oct 18 19:26:56 Starting translator
Oct 18 19:29:56 Finished translator                                            2m59s 944MB
Oct 18 19:29:57 Starting compiler/parsing
Oct 18 19:31:12 Finished compiler/parsing                                      1m13s   2GB
Oct 18 19:31:13 Starting characteristic
Oct 18 19:33:35 Finished characteristic                                        2m21s   1GB
Oct 18 19:33:36 Starting translator/monadic
Oct 18 19:35:01 Finished translator/monadic                                    1m23s   1GB
Oct 18 19:35:01 Starting basis
Oct 18 19:51:25 Finished basis                                                16m22s   3GB
Oct 18 19:51:26 Starting compiler/inference
Oct 18 19:53:03 Finished compiler/inference                                    1m36s 965MB
Oct 18 19:53:04 Starting compiler/backend/reg_alloc
Oct 18 19:53:50 Finished compiler/backend/reg_alloc                              45s   1GB
Oct 18 19:53:51 Starting compiler/backend/gc
Oct 18 20:00:58 Finished compiler/backend/gc                                   7m06s   1GB
Oct 18 20:00:59 Starting compiler/backend
Oct 18 20:01:02 Finished compiler/backend                                         2s  17MB
Oct 18 20:01:03 Starting compiler/encoders/asm
Oct 18 20:01:05 Finished compiler/encoders/asm                                    0s  20MB
Oct 18 20:01:05 Starting compiler/encoders/x64
Oct 18 20:01:55 Finished compiler/encoders/x64                                   48s 592MB
Oct 18 20:01:55 Starting compiler/encoders/arm6
Oct 18 20:03:39 Finished compiler/encoders/arm6                                1m42s   1GB
Oct 18 20:03:40 Starting compiler/encoders/arm8
Oct 18 20:04:04 Finished compiler/encoders/arm8                                  23s 465MB
Oct 18 20:04:04 Starting compiler/encoders/mips
Oct 18 20:05:01 Finished compiler/encoders/mips                                  55s 756MB
Oct 18 20:05:02 Starting compiler/encoders/riscv
Oct 18 20:06:01 Finished compiler/encoders/riscv                                 58s 648MB
Oct 18 20:06:02 Starting compiler/backend/x64
Oct 18 20:06:21 Finished compiler/backend/x64                                    17s   1GB
Oct 18 20:06:21 Starting compiler/backend/arm6
Oct 18 20:06:41 Finished compiler/backend/arm6                                   18s 977MB
Oct 18 20:06:42 Starting compiler/backend/arm8
Oct 18 20:07:00 Finished compiler/backend/arm8                                   17s   1GB
Oct 18 20:07:01 Starting compiler/backend/mips
Oct 18 20:07:19 Finished compiler/backend/mips                                   18s   1GB
Oct 18 20:07:20 Starting compiler/backend/riscv
Oct 18 20:07:40 Finished compiler/backend/riscv                                  18s   1GB
Oct 18 20:07:41 Starting compiler/parsing/proofs
Oct 18 20:13:38 Finished compiler/parsing/proofs                               5m56s 952MB
Oct 18 20:13:39 Starting compiler/inference/proofs
Oct 18 20:16:29 Finished compiler/inference/proofs                             2m49s   1GB
Oct 18 20:16:30 Starting compiler/backend/semantics
Oct 18 20:25:27 Finished compiler/backend/semantics                            8m56s   3GB
Oct 18 20:25:28 Starting compiler/backend/reg_alloc/proofs
Oct 18 20:32:51 Finished compiler/backend/reg_alloc/proofs                     7m22s 492MB
Oct 18 20:32:51 Starting compiler/backend/proofs
Oct 18 21:14:04 Finished compiler/backend/proofs                              41m11s   4GB
Oct 18 21:14:05 Starting compiler/encoders/x64/proofs
Oct 18 21:21:28 Finished compiler/encoders/x64/proofs                          7m21s   4GB
Oct 18 21:21:29 Starting compiler/encoders/arm6/proofs
Oct 18 21:28:57 Finished compiler/encoders/arm6/proofs                         7m27s   3GB
Oct 18 21:28:58 Starting compiler/encoders/arm8/proofs
Oct 18 21:34:20 Finished compiler/encoders/arm8/proofs                         5m21s 992MB
Oct 18 21:34:21 Starting compiler/encoders/mips/proofs
Oct 18 21:41:39 Finished compiler/encoders/mips/proofs                         7m17s   3GB
Oct 18 21:41:39 Starting compiler/encoders/riscv/proofs
Oct 18 21:49:33 Finished compiler/encoders/riscv/proofs                        7m52s 757MB
Oct 18 21:49:34 Starting compiler/backend/x64/proofs
Oct 18 21:49:54 Finished compiler/backend/x64/proofs                             19s   1GB
Oct 18 21:49:55 Starting compiler/backend/arm6/proofs
Oct 18 21:50:16 Finished compiler/backend/arm6/proofs                            20s 988MB
Oct 18 21:50:17 Starting compiler/backend/arm8/proofs
Oct 18 21:50:37 Finished compiler/backend/arm8/proofs                            19s   1GB
Oct 18 21:50:38 Starting compiler/backend/mips/proofs
Oct 18 21:51:00 Finished compiler/backend/mips/proofs                            21s   1GB
Oct 18 21:51:01 Starting compiler/backend/riscv/proofs
Oct 18 21:51:22 Finished compiler/backend/riscv/proofs                           19s   1GB
Oct 18 21:51:23 Starting compiler/proofs
Oct 18 21:52:40 Finished compiler/proofs                                       1m16s   1GB
Oct 18 21:52:41 Starting candle/set-theory
Oct 18 21:53:10 Finished candle/set-theory                                       28s 598MB
Oct 18 21:53:10 Starting candle/syntax-lib
Oct 18 21:53:21 Finished candle/syntax-lib                                        9s 558MB
Oct 18 21:53:22 Starting candle/standard/syntax
Oct 18 21:54:52 Finished candle/standard/syntax                                1m29s 670MB
Oct 18 21:54:53 Starting candle/standard/semantics
Oct 18 21:56:12 Finished candle/standard/semantics                             1m18s   1GB
Oct 18 21:56:13 Starting candle/standard/monadic
Oct 18 21:57:46 Finished candle/standard/monadic                               1m31s   1GB
Oct 18 21:57:46 Starting candle/standard/ml_kernel
Oct 18 22:14:26 Finished candle/standard/ml_kernel                            16m38s   5GB
Oct 18 22:14:27 Starting candle/standard/opentheory
Oct 18 22:23:10 Finished candle/standard/opentheory                            8m42s   6GB
Oct 18 22:23:10 Starting candle/standard/opentheory/compilation
Oct 18 22:58:13 Finished candle/standard/opentheory/compilation               35m01s  21GB
Oct 18 22:58:14 Starting candle/standard/opentheory/compilation/proofs
Oct 18 22:58:50 Finished candle/standard/opentheory/compilation/proofs           35s   4GB
Oct 18 22:58:51 Starting characteristic/examples
Oct 18 23:00:26 Finished characteristic/examples                               1m34s   1GB
Oct 18 23:00:27 Starting tutorial/solutions
Oct 18 23:13:48 Finished tutorial/solutions                                   13m19s   7GB
Oct 18 23:13:48 Starting translator/monadic/examples
Oct 18 23:15:33 Finished translator/monadic/examples                           1m43s   2GB
Oct 18 23:15:34 Starting examples
Oct 18 23:21:17 Finished examples                                              5m41s   3GB
Oct 18 23:21:17 Starting examples/compilation
Oct 19 01:16:23 Finished examples/compilation                               1h55m05s  11GB
Oct 19 01:16:24 Starting examples/compilation/proofs
Oct 19 01:18:13 Finished examples/compilation/proofs                           1m47s   3GB
Oct 19 01:18:14 Starting compiler/benchmarks
Oct 19 01:18:15 Finished compiler/benchmarks                                      0s   4MB
Oct 19 01:18:16 Starting translator/okasaki-examples
Oct 19 01:21:48 Finished translator/okasaki-examples                           3m31s   1GB
Oct 19 01:21:49 Starting translator/other-examples
Oct 19 01:25:08 Finished translator/other-examples                             3m18s 799MB
Oct 19 01:25:09 Starting compiler/parsing/tests
Oct 19 01:25:33 Finished compiler/parsing/tests                                  23s 320MB
Oct 19 01:25:34 Starting compiler/inference/tests
Oct 19 01:29:39 Finished compiler/inference/tests                              4m03s   3GB
Oct 19 01:29:39 Starting compiler/bootstrap/translation Oct 19 01:29:39 32430s