Job 1293

CakeML:f5f6e11d3f150553348468ac990aff1bd58bf820
  address comments from @xrchz [Jun 25 15:20:41]
#738 (export_update)
Merging into:e558e892c7e1e214d93bc43b8ad3bfc8dc5f4183
  Make terms greater! (great_tm --> greater_tm) [Jun 23 12:02:34]
HOL:0aae6443b97e2d1bd0ea728d27ca72d0913aa763
  Prove a chunk of Rutten's Theorem 7.1 (First Isomorphism theorem) [Jun 23 08:07:27]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Jun 25 15:35:05 Claimed job
Jun 25 15:35:08 Reusing HOL
Jun 25 15:36:01 Starting developers
Jun 25 15:36:05 Finished developers                                               4s 114MB
Jun 25 15:36:06 Starting developers/bin
Jun 25 15:36:13 Finished developers/bin                                           7s   1GB
Jun 25 15:36:13 Starting semantics/ffi
Jun 25 15:36:26 Finished semantics/ffi                                           12s 228MB
Jun 25 15:36:26 Starting semantics
Jun 25 15:38:01 Finished semantics                                             1m35s   1GB
Jun 25 15:38:01 Starting semantics/proofs
Jun 25 15:41:44 Finished semantics/proofs                                      3m42s 842MB
Jun 25 15:41:44 Starting semantics/alt_semantics
Jun 25 15:41:54 Finished semantics/alt_semantics                                  9s 297MB
Jun 25 15:41:54 Starting semantics/alt_semantics/proofs
Jun 25 15:44:18 Finished semantics/alt_semantics/proofs                        2m23s 782MB
Jun 25 15:44:19 Starting basis/pure
Jun 25 15:45:14 Finished basis/pure                                              55s 861MB
Jun 25 15:45:15 Starting translator
Jun 25 15:48:12 Finished translator                                            2m57s   1GB
Jun 25 15:48:12 Starting compiler/parsing
Jun 25 15:49:38 Finished compiler/parsing                                      1m25s   1GB
Jun 25 15:49:38 Starting characteristic
Jun 25 15:56:10 Finished characteristic                                        6m31s   1GB
Jun 25 15:56:10 Starting translator/monadic
Jun 25 15:58:00 Finished translator/monadic                                    1m49s   1GB
Jun 25 15:58:00 Starting basis
Jun 25 16:35:34 Finished basis                                                37m33s  11GB
Jun 25 16:35:34 Starting compiler/inference
Jun 25 16:36:43 Finished compiler/inference                                    1m08s   1GB
Jun 25 16:36:44 Starting compiler/backend/reg_alloc
Jun 25 16:37:55 Finished compiler/backend/reg_alloc                            1m10s   1GB
Jun 25 16:37:55 Starting compiler/backend/gc
Jun 25 16:41:51 Finished compiler/backend/gc                                   3m55s   2GB
Jun 25 16:41:51 Starting compiler/backend
Jun 25 16:47:22 Finished compiler/backend                                      5m31s   4GB
Jun 25 16:47:22 Starting compiler/encoders/asm
Jun 25 16:47:48 Finished compiler/encoders/asm                                   25s 726MB
Jun 25 16:47:48 Starting compiler/encoders/x64
Jun 25 16:48:17 Finished compiler/encoders/x64                                   28s 970MB
Jun 25 16:48:17 Starting compiler/encoders/arm7
Jun 25 16:49:11 Finished compiler/encoders/arm7                                  54s 659MB
Jun 25 16:49:12 Starting compiler/encoders/arm8
Jun 25 16:49:26 Finished compiler/encoders/arm8                                  13s 645MB
Jun 25 16:49:26 Starting compiler/encoders/mips
Jun 25 16:49:45 Finished compiler/encoders/mips                                  19s   1GB
Jun 25 16:49:46 Starting compiler/encoders/riscv
Jun 25 16:50:02 Finished compiler/encoders/riscv                                 15s 746MB
Jun 25 16:50:02 Starting compiler/encoders/ag32
Jun 25 16:50:22 Finished compiler/encoders/ag32                                  20s 703MB
Jun 25 16:50:22 Starting compiler/backend/x64
Jun 25 16:50:43 Finished compiler/backend/x64                                    20s   1GB
Jun 25 16:50:43 Starting compiler/backend/arm7
Jun 25 16:51:06 Finished compiler/backend/arm7                                   22s   1GB
Jun 25 16:51:06 Starting compiler/backend/arm8
Jun 25 16:51:25 Finished compiler/backend/arm8                                   19s   1GB
Jun 25 16:51:26 Starting compiler/backend/mips
Jun 25 16:51:47 Finished compiler/backend/mips                                   21s   1GB
Jun 25 16:51:47 Starting compiler/backend/riscv
Jun 25 16:52:09 Finished compiler/backend/riscv                                  21s   1GB
Jun 25 16:52:09 Starting compiler/backend/ag32
Jun 25 16:53:26 Finished compiler/backend/ag32                                 1m16s   1GB
Jun 25 16:53:26 Starting compiler/parsing/proofs
Jun 25 16:59:43 Finished compiler/parsing/proofs                               6m15s   1GB
Jun 25 16:59:43 Starting compiler/inference/proofs
Jun 25 17:02:29 Finished compiler/inference/proofs                             2m45s 924MB
Jun 25 17:02:29 Starting compiler/backend/semantics
Jun 25 17:37:33 Finished compiler/backend/semantics                           35m03s   2GB
Jun 25 17:37:33 Starting compiler/backend/reg_alloc/proofs
Jun 25 17:41:32 Finished compiler/backend/reg_alloc/proofs                     3m58s 776MB
Jun 25 17:41:32 Starting compiler/backend/proofs
Jun 25 18:49:05 Finished compiler/backend/proofs                            1h07m30s  10GB
Jun 25 18:49:05 Starting compiler/encoders/x64/proofs
Jun 25 18:59:50 Finished compiler/encoders/x64/proofs                         10m45s   4GB
Jun 25 18:59:51 Starting compiler/encoders/arm7/proofs
Jun 25 19:14:12 Finished compiler/encoders/arm7/proofs                        14m21s   2GB
Jun 25 19:14:12 Starting compiler/encoders/arm8/proofs
Jun 25 19:21:25 Finished compiler/encoders/arm8/proofs                         7m12s   1GB
Jun 25 19:21:25 Starting compiler/encoders/mips/proofs
Jun 25 19:32:36 Finished compiler/encoders/mips/proofs                        11m10s   1GB
Jun 25 19:32:36 Starting compiler/encoders/riscv/proofs
Jun 25 19:42:20 Finished compiler/encoders/riscv/proofs                        9m44s   1GB
Jun 25 19:42:20 Starting compiler/encoders/ag32/proofs
Jun 25 19:45:15 Finished compiler/encoders/ag32/proofs                         2m54s 648MB
Jun 25 19:45:16 Starting compiler/backend/x64/proofs
Jun 25 19:45:38 Finished compiler/backend/x64/proofs                             22s   1GB
Jun 25 19:45:38 Starting compiler/backend/arm7/proofs
Jun 25 19:46:03 Finished compiler/backend/arm7/proofs                            24s   1GB
Jun 25 19:46:03 Starting compiler/backend/arm8/proofs
Jun 25 19:46:25 Finished compiler/backend/arm8/proofs                            21s   1GB
Jun 25 19:46:26 Starting compiler/backend/mips/proofs
Jun 25 19:46:47 Finished compiler/backend/mips/proofs                            21s   1GB
Jun 25 19:46:48 Starting compiler/backend/riscv/proofs
Jun 25 19:47:10 Finished compiler/backend/riscv/proofs                           22s   1GB
Jun 25 19:47:11 Starting compiler/backend/ag32/proofs
Jun 25 20:01:43 Finished compiler/backend/ag32/proofs                         14m31s   2GB
Jun 25 20:01:43 Starting compiler/proofs
Jun 26 13:14:16 Resuming compiler/proofs
Jun 26 13:15:52 Finished compiler/proofs                                       1m36s   3GB
Jun 26 13:15:53 Starting candle/set-theory
Jun 26 13:16:24 Finished candle/set-theory                                       31s 858MB
Jun 26 13:16:24 Starting candle/syntax-lib
Jun 26 13:16:35 Finished candle/syntax-lib                                       10s 426MB
Jun 26 13:16:35 Starting candle/standard/syntax
Jun 26 13:18:38 Finished candle/standard/syntax                                2m02s   1GB
Jun 26 13:18:38 Starting candle/standard/semantics
Jun 26 13:20:35 Finished candle/standard/semantics                             1m57s   1GB
Jun 26 13:20:35 Starting candle/standard/monadic
Jun 26 13:22:27 Finished candle/standard/monadic                               1m51s   1GB
Jun 26 13:22:28 Starting candle/standard/ml_kernel
Jun 26 13:28:34 Finished candle/standard/ml_kernel                             6m06s   3GB
Jun 26 13:28:34 Starting candle/standard/opentheory
Jun 26 13:38:52 Finished candle/standard/opentheory                           10m17s   5GB
Jun 26 13:38:52 Starting candle/standard/opentheory/compilation
Jun 26 14:15:47 Finished candle/standard/opentheory/compilation               36m54s  10GB
Jun 26 14:15:47 Starting candle/standard/opentheory/compilation/proofs
Jun 26 14:16:49 Finished candle/standard/opentheory/compilation/proofs         1m01s   1GB
Jun 26 14:16:49 Starting candle/overloading/syntax
Jun 26 14:20:16 Finished candle/overloading/syntax                             3m27s 986MB
Jun 26 14:20:17 Starting candle/overloading/semantics
Jun 26 14:28:04 Finished candle/overloading/semantics                          7m46s   3GB
Jun 26 14:28:04 Starting characteristic/examples
Jun 26 14:29:27 Finished characteristic/examples                               1m22s   2GB
Jun 26 14:29:27 Starting tutorial/solutions
Jun 26 14:45:41 Finished tutorial/solutions                                   16m13s   6GB
Jun 26 14:45:41 Starting translator/monadic/examples
Jun 26 14:49:32 Finished translator/monadic/examples                           3m50s   2GB
Jun 26 14:49:32 Starting examples
Jun 26 14:59:42 Finished examples                                             10m09s   4GB
Jun 26 14:59:42 Starting examples/compilation/x64
Jun 26 17:27:59 Finished examples/compilation/x64                           2h28m17s  14GB
Jun 26 17:28:00 Starting examples/compilation/x64/proofs
Jun 26 17:29:46 Finished examples/compilation/x64/proofs                       1m46s   2GB
Jun 26 17:29:47 Starting examples/compilation/ag32
Jun 26 18:03:15 Finished examples/compilation/ag32                            33m28s   6GB
Jun 26 18:03:16 Starting examples/compilation/ag32/proofs
Jun 26 18:04:04 Finished examples/compilation/ag32/proofs                        48s   2GB
Jun 26 18:04:04 Starting examples/cost
Jun 26 19:00:16 Finished examples/cost                                        56m11s   5GB
Jun 26 19:00:16 Starting examples/lpr_checker
Jun 26 19:04:22 Finished examples/lpr_checker                                  4m05s   2GB
Jun 26 19:04:22 Starting examples/lpr_checker/compilation
Jun 26 19:24:36 Finished examples/lpr_checker/compilation                     20m13s  10GB
Jun 26 19:24:36 Starting examples/lpr_checker/compilation/proofs
Jun 26 19:25:43 Finished examples/lpr_checker/compilation/proofs               1m06s   1GB
Jun 26 19:25:43 Starting examples/lpr_checker/array
Jun 26 19:36:53 Finished examples/lpr_checker/array                           11m08s   2GB
Jun 26 19:36:53 Starting examples/lpr_checker/array/compilation
Jun 26 19:56:29 Finished examples/lpr_checker/array/compilation               19m35s   9GB
Jun 26 19:56:29 Starting examples/lpr_checker/array/compilation/proofs
Jun 26 19:57:20 Finished examples/lpr_checker/array/compilation/proofs           50s   3GB
Jun 26 19:57:20 Starting translator/okasaki-examples
Jun 26 20:02:06 Finished translator/okasaki-examples                           4m46s   1GB
Jun 26 20:02:06 Starting translator/other-examples
Jun 26 20:02:54 Finished translator/other-examples                               47s   1GB
Jun 26 20:02:54 Starting compiler/parsing/tests
Jun 26 20:03:21 Finished compiler/parsing/tests                                  26s 606MB
Jun 26 20:03:21 Starting compiler/inference/tests
Jun 26 20:08:02 Finished compiler/inference/tests                              4m40s   3GB
Jun 26 20:08:02 Starting compiler/bootstrap/translation
Jun 26 23:12:33 Finished compiler/bootstrap/translation                     3h04m31s  30GB
Jun 26 23:12:33 Starting unverified/sexpr-bootstrap/x64/64
Jun 26 23:22:00 Finished unverified/sexpr-bootstrap/x64/64                     9m26s   8GB
Jun 26 23:22:00 Starting unverified/sexpr-bootstrap/x64/32
Jun 26 23:29:29 Finished unverified/sexpr-bootstrap/x64/32                     7m28s   8GB
Jun 26 23:29:29 Starting compiler/benchmarks
Jun 26 23:29:33 Finished compiler/benchmarks                                      4s  32MB
Jun 26 23:29:33 Starting compiler/bootstrap/compilation/x64/64
Jun 27 17:47:27 Finished compiler/bootstrap/compilation/x64/64             18h17m53s  41GB
Jun 27 17:47:27 Starting compiler/bootstrap/compilation/x64/64/proofs
Jun 27 17:50:56 Finished compiler/bootstrap/compilation/x64/64/proofs          3m28s  13GB
Jun 27 17:50:56 Starting compiler/bootstrap/compilation/x64/32
Jun 28 11:40:28 Finished compiler/bootstrap/compilation/x64/32             17h49m30s  38GB
Jun 28 11:40:28 Starting compiler/bootstrap/compilation/x64/32/proofs
Jun 28 11:43:43 Finished compiler/bootstrap/compilation/x64/32/proofs          3m14s  13GB
Jun 28 11:43:43 Starting compiler/bootstrap/compilation/ag32/32
Jun 29 07:17:37 Finished compiler/bootstrap/compilation/ag32/32            19h33m53s  41GB
Jun 29 07:17:37 Starting compiler/bootstrap/compilation/ag32/32/proofs
Jun 29 07:34:58 Finished compiler/bootstrap/compilation/ag32/32/proofs        17m19s  31GB
Jun 29 07:34:58 SUCCESS