Job 1092

CakeML:d61723d68aba28f45b1e327ebbff162449f2975c
  Fix a proof in examples/div [Nov 12 09:38:21]
#703 (cfletautolib-fix)
Merging into:dee8a5c2ef96f2f6ba0c0a583d7d6a655470840d
  Merge pull request #704 from CakeML/sexpr-bootstrap-fix [Nov 14 07:43:57]
HOL:ca71e46c32fd6a11162c9640ee7006dfe1c6fabd
  Remove unnecessary CLINE_OPTIONS in tests that break Moscow ML build [Nov 13 22:33:35]
Machine:oven2 4.15.0-34-generic x86_64 GNU/Linux

Nov 14 12:33:35 Claimed job
Nov 14 12:33:38 Reusing HOL
Nov 14 12:33:49 Starting developers
Nov 14 12:33:51 Finished developers                                               2s 100MB
Nov 14 12:33:51 Starting developers/bin
Nov 14 12:33:55 Finished developers/bin                                           3s 164MB
Nov 14 12:33:55 Starting semantics/ffi
Nov 14 12:34:03 Finished semantics/ffi                                            7s 197MB
Nov 14 12:34:03 Starting semantics
Nov 14 12:35:23 Finished semantics                                             1m18s   1GB
Nov 14 12:35:23 Starting semantics/proofs
Nov 14 12:38:25 Finished semantics/proofs                                      3m02s   1GB
Nov 14 12:38:26 Starting semantics/alt_semantics
Nov 14 12:38:32 Finished semantics/alt_semantics                                  6s 294MB
Nov 14 12:38:33 Starting semantics/alt_semantics/proofs
Nov 14 12:40:23 Finished semantics/alt_semantics/proofs                        1m50s   1GB
Nov 14 12:40:23 Starting basis/pure
Nov 14 12:41:10 Finished basis/pure                                              46s 828MB
Nov 14 12:41:10 Starting translator
Nov 14 12:43:00 Finished translator                                            1m48s   1GB
Nov 14 12:43:00 Starting compiler/parsing
Nov 14 12:44:01 Finished compiler/parsing                                      1m00s   2GB
Nov 14 12:44:01 Starting characteristic
Nov 14 12:49:22 Finished characteristic                                        5m20s   1GB
Nov 14 12:49:22 Starting translator/monadic
Nov 14 12:50:49 Finished translator/monadic                                    1m26s   1GB
Nov 14 12:50:49 Starting basis
Nov 14 13:11:28 Finished basis                                                20m38s   2GB
Nov 14 13:11:28 Starting compiler/inference
Nov 14 13:13:10 Finished compiler/inference                                    1m41s   1GB
Nov 14 13:13:10 Starting compiler/backend/reg_alloc
Nov 14 13:14:12 Finished compiler/backend/reg_alloc                            1m01s   1GB
Nov 14 13:14:12 Starting compiler/backend/gc
Nov 14 13:17:21 Finished compiler/backend/gc                                   3m08s   2GB
Nov 14 13:17:22 Starting compiler/backend
Nov 14 13:21:32 Finished compiler/backend                                      4m09s   2GB
Nov 14 13:21:32 Starting compiler/encoders/asm
Nov 14 13:21:52 Finished compiler/encoders/asm                                   20s 757MB
Nov 14 13:21:53 Starting compiler/encoders/x64
Nov 14 13:22:17 Finished compiler/encoders/x64                                   23s 698MB
Nov 14 13:22:17 Starting compiler/encoders/arm7
Nov 14 13:23:05 Finished compiler/encoders/arm7                                  47s 705MB
Nov 14 13:23:05 Starting compiler/encoders/arm8
Nov 14 13:23:18 Finished compiler/encoders/arm8                                  11s 525MB
Nov 14 13:23:18 Starting compiler/encoders/mips
Nov 14 13:23:35 Finished compiler/encoders/mips                                  16s   1GB
Nov 14 13:23:35 Starting compiler/encoders/riscv
Nov 14 13:23:49 Finished compiler/encoders/riscv                                 14s   1GB
Nov 14 13:23:50 Starting compiler/encoders/ag32
Nov 14 13:24:06 Finished compiler/encoders/ag32                                  15s 812MB
Nov 14 13:24:06 Starting compiler/backend/x64
Nov 14 13:24:24 Finished compiler/backend/x64                                    17s 985MB
Nov 14 13:24:24 Starting compiler/backend/arm7
Nov 14 13:24:43 Finished compiler/backend/arm7                                   19s   1GB
Nov 14 13:24:44 Starting compiler/backend/arm8
Nov 14 13:25:00 Finished compiler/backend/arm8                                   16s   1GB
Nov 14 13:25:00 Starting compiler/backend/mips
Nov 14 13:25:17 Finished compiler/backend/mips                                   16s 982MB
Nov 14 13:25:17 Starting compiler/backend/riscv
Nov 14 13:25:34 Finished compiler/backend/riscv                                  16s   1GB
Nov 14 13:25:35 Starting compiler/backend/ag32
Nov 14 13:26:44 Finished compiler/backend/ag32                                 1m08s   1GB
Nov 14 13:26:44 Starting compiler/parsing/proofs
Nov 14 13:32:34 Finished compiler/parsing/proofs                               5m49s   1GB
Nov 14 13:32:34 Starting compiler/inference/proofs
Nov 14 13:35:46 Finished compiler/inference/proofs                             3m11s 898MB
Nov 14 13:35:46 Starting compiler/backend/semantics
Nov 14 13:43:43 Finished compiler/backend/semantics                            7m56s   1GB
Nov 14 13:43:43 Starting compiler/backend/reg_alloc/proofs
Nov 14 13:47:13 Finished compiler/backend/reg_alloc/proofs                     3m30s 770MB
Nov 14 13:47:13 Starting compiler/backend/proofs
Nov 14 14:35:44 Finished compiler/backend/proofs                              48m28s   3GB
Nov 14 14:35:44 Starting compiler/encoders/x64/proofs
Nov 14 14:45:39 Finished compiler/encoders/x64/proofs                          9m54s   5GB
Nov 14 14:45:40 Starting compiler/encoders/arm7/proofs
Nov 14 14:59:06 Finished compiler/encoders/arm7/proofs                        13m26s   5GB
Nov 14 14:59:06 Starting compiler/encoders/arm8/proofs
Nov 14 15:05:56 Finished compiler/encoders/arm8/proofs                         6m49s   1GB
Nov 14 15:05:56 Starting compiler/encoders/mips/proofs
Nov 14 15:15:56 Finished compiler/encoders/mips/proofs                         9m59s   3GB
Nov 14 15:15:56 Starting compiler/encoders/riscv/proofs
Nov 14 15:24:41 Finished compiler/encoders/riscv/proofs                        8m44s   1GB
Nov 14 15:24:42 Starting compiler/encoders/ag32/proofs
Nov 14 15:27:12 Finished compiler/encoders/ag32/proofs                         2m29s 886MB
Nov 14 15:27:12 Starting compiler/backend/x64/proofs
Nov 14 15:27:30 Finished compiler/backend/x64/proofs                             17s   1GB
Nov 14 15:27:30 Starting compiler/backend/arm7/proofs
Nov 14 15:27:49 Finished compiler/backend/arm7/proofs                            18s   1GB
Nov 14 15:27:50 Starting compiler/backend/arm8/proofs
Nov 14 15:28:07 Finished compiler/backend/arm8/proofs                            16s   1GB
Nov 14 15:28:07 Starting compiler/backend/mips/proofs
Nov 14 15:28:25 Finished compiler/backend/mips/proofs                            17s   1GB
Nov 14 15:28:25 Starting compiler/backend/riscv/proofs
Nov 14 15:28:43 Finished compiler/backend/riscv/proofs                           17s   1GB
Nov 14 15:28:43 Starting compiler/backend/ag32/proofs
Nov 14 15:38:10 Finished compiler/backend/ag32/proofs                          9m25s   2GB
Nov 14 15:38:10 Starting compiler/proofs
Nov 14 15:39:42 Finished compiler/proofs                                       1m31s   3GB
Nov 14 15:39:42 Starting candle/set-theory
Nov 14 15:40:09 Finished candle/set-theory                                       26s 756MB
Nov 14 15:40:09 Starting candle/syntax-lib
Nov 14 15:40:19 Finished candle/syntax-lib                                        9s 632MB
Nov 14 15:40:19 Starting candle/standard/syntax
Nov 14 15:42:03 Finished candle/standard/syntax                                1m43s 831MB
Nov 14 15:42:03 Starting candle/standard/semantics
Nov 14 15:43:39 Finished candle/standard/semantics                             1m35s   1GB
Nov 14 15:43:39 Starting candle/standard/monadic
Nov 14 15:45:15 Finished candle/standard/monadic                               1m35s   1GB
Nov 14 15:45:15 Starting candle/standard/ml_kernel
Nov 14 15:49:14 Finished candle/standard/ml_kernel                             3m58s   3GB
Nov 14 15:49:15 Starting candle/standard/opentheory
Nov 14 15:58:05 Finished candle/standard/opentheory                            8m50s   4GB
Nov 14 15:58:06 Starting candle/standard/opentheory/compilation
Nov 14 16:28:31 Finished candle/standard/opentheory/compilation               30m24s  23GB
Nov 14 16:28:31 Starting candle/standard/opentheory/compilation/proofs
Nov 14 16:29:16 Finished candle/standard/opentheory/compilation/proofs           45s   2GB
Nov 14 16:29:17 Starting characteristic/examples
Nov 14 16:30:44 Finished characteristic/examples                               1m26s   2GB
Nov 14 16:30:44 Starting tutorial/solutions
Nov 14 16:44:18 Finished tutorial/solutions                                   13m33s   7GB
Nov 14 16:44:19 Starting translator/monadic/examples
Nov 14 16:47:18 Finished translator/monadic/examples                           2m58s   2GB
Nov 14 16:47:18 Starting examples
Nov 14 16:56:43 Finished examples                                              9m24s   2GB
Nov 14 16:56:43 Starting examples/compilation/x64
Nov 14 19:01:53 Finished examples/compilation/x64                           2h05m07s  14GB
Nov 14 19:01:53 Starting examples/compilation/x64/proofs
Nov 14 19:03:46 Finished examples/compilation/x64/proofs                       1m52s   3GB
Nov 14 19:03:46 Starting examples/compilation/ag32
Nov 14 19:32:44 Finished examples/compilation/ag32                            28m57s   7GB
Nov 14 19:32:45 Starting examples/compilation/ag32/proofs
Nov 14 19:33:35 Finished examples/compilation/ag32/proofs                        50s   2GB
Nov 14 19:33:36 Starting translator/okasaki-examples
Nov 14 19:37:53 Finished translator/okasaki-examples                           4m17s   1GB
Nov 14 19:37:54 Starting translator/other-examples
Nov 14 19:39:41 Finished translator/other-examples                             1m47s   1GB
Nov 14 19:39:42 Starting compiler/parsing/tests
Nov 14 19:40:06 Finished compiler/parsing/tests                                  24s 549MB
Nov 14 19:40:06 Starting compiler/inference/tests
Nov 14 19:44:32 Finished compiler/inference/tests                              4m24s   6GB
Nov 14 19:44:32 Starting compiler/bootstrap/translation
Nov 14 22:19:28 Finished compiler/bootstrap/translation                     2h34m53s  42GB
Nov 14 22:19:28 Starting unverified/sexpr-bootstrap/x64/64
Nov 14 22:33:36 Finished unverified/sexpr-bootstrap/x64/64                    14m07s   4GB
Nov 14 22:33:36 Starting unverified/sexpr-bootstrap/x64/32
Nov 14 22:43:07 Finished unverified/sexpr-bootstrap/x64/32                     9m29s   7GB
Nov 14 22:43:07 Starting compiler/benchmarks
Nov 14 23:22:06 Finished compiler/benchmarks                                  38m58s   2GB
Nov 14 23:22:06 Starting compiler/bootstrap/compilation/x64/64
Nov 15 12:38:15 Finished compiler/bootstrap/compilation/x64/64             13h16m08s  63GB
Nov 15 12:38:16 Starting compiler/bootstrap/compilation/x64/64/proofs
Nov 15 12:41:46 Finished compiler/bootstrap/compilation/x64/64/proofs          3m29s   5GB
Nov 15 12:41:46 Starting compiler/bootstrap/compilation/x64/32
Nov 16 00:27:56 Finished compiler/bootstrap/compilation/x64/32             11h46m09s  64GB
Nov 16 00:27:57 Starting compiler/bootstrap/compilation/x64/32/proofs
Nov 16 00:31:14 Finished compiler/bootstrap/compilation/x64/32/proofs          3m17s   4GB
Nov 16 00:31:15 Starting compiler/bootstrap/compilation/ag32/32
Nov 16 14:18:15 Finished compiler/bootstrap/compilation/ag32/32            13h47m00s  60GB
Nov 16 14:18:16 Starting compiler/bootstrap/compilation/ag32/32/proofs
Nov 16 15:10:42 Finished compiler/bootstrap/compilation/ag32/32/proofs        52m26s  18GB
Nov 16 15:10:42 SUCCESS