Job 712

CakeML:ff9234ce6dab5d457db7abe6790a62faff2b74b2
  Replace now-removed "of" syntax when declaring exceptions in cf_examples [Feb 01 09:06:04]
#613 (gh611)
Merging into:2d7c75fa02a5b1347dd76fa2b7150e0af74d940b
  Fix some uses of Theorem syntax [Jan 31 16:15:24]
HOL:e53c040a60b6ad258c99b0887434bda862eb81a8
  Build sequences must have src/finite_maps before src/integer [Jan 31 01:43:52]
Machine:oven1 (2) 4.17.17-100.fc27.x86_64 x86_64

Feb 01 14:53:23 Claimed job
Feb 01 14:53:27 Reusing HOL
Feb 01 14:54:15 Starting developers
Feb 01 14:54:18 Finished developers                                               2s  20MB
Feb 01 14:54:19 Starting developers/bin
Feb 01 14:55:31 Finished developers/bin                                        1m11s 918MB
Feb 01 14:55:32 Starting semantics/ffi
Feb 01 14:55:42 Finished semantics/ffi                                            9s 255MB
Feb 01 14:55:43 Starting semantics
Feb 01 14:57:04 Finished semantics                                             1m20s   1GB
Feb 01 14:57:04 Starting semantics/proofs
Feb 01 15:00:14 Finished semantics/proofs                                      3m08s   1GB
Feb 01 15:00:14 Starting basis/pure
Feb 01 15:01:02 Finished basis/pure                                              47s 603MB
Feb 01 15:01:03 Starting translator
Feb 01 15:02:41 Finished translator                                            1m37s   1GB
Feb 01 15:02:42 Starting compiler/parsing
Feb 01 15:03:40 Finished compiler/parsing                                        57s   2GB
Feb 01 15:03:41 Starting characteristic
Feb 01 15:07:59 Finished characteristic                                        4m17s   1GB
Feb 01 15:08:00 Starting translator/monadic
Feb 01 15:09:29 Finished translator/monadic                                    1m28s   1GB
Feb 01 15:09:30 Starting basis
Feb 01 15:25:52 Finished basis                                                16m22s   3GB
Feb 01 15:25:53 Starting compiler/inference
Feb 01 15:27:26 Finished compiler/inference                                    1m32s   1GB
Feb 01 15:27:26 Starting compiler/backend/reg_alloc
Feb 01 15:28:19 Finished compiler/backend/reg_alloc                              51s   1GB
Feb 01 15:28:19 Starting compiler/backend/gc
Feb 01 15:36:07 Finished compiler/backend/gc                                   7m46s   2GB
Feb 01 15:36:07 Starting compiler/backend
Feb 01 15:36:10 Finished compiler/backend                                         2s  22MB
Feb 01 15:36:11 Starting compiler/encoders/asm
Feb 01 15:36:13 Finished compiler/encoders/asm                                    1s  15MB
Feb 01 15:36:13 Starting compiler/encoders/x64
Feb 01 15:36:38 Finished compiler/encoders/x64                                   24s 724MB
Feb 01 15:36:39 Starting compiler/encoders/arm6
Feb 01 15:37:28 Finished compiler/encoders/arm6                                  48s 769MB
Feb 01 15:37:28 Starting compiler/encoders/arm8
Feb 01 15:37:42 Finished compiler/encoders/arm8                                  13s 860MB
Feb 01 15:37:43 Starting compiler/encoders/mips
Feb 01 15:38:00 Finished compiler/encoders/mips                                  16s 768MB
Feb 01 15:38:00 Starting compiler/encoders/riscv
Feb 01 15:38:16 Finished compiler/encoders/riscv                                 14s 922MB
Feb 01 15:38:16 Starting compiler/encoders/ag32
Feb 01 15:38:34 Finished compiler/encoders/ag32                                  17s 788MB
Feb 01 15:38:35 Starting compiler/backend/x64
Feb 01 15:38:52 Finished compiler/backend/x64                                    16s 841MB
Feb 01 15:38:53 Starting compiler/backend/arm6
Feb 01 15:39:13 Finished compiler/backend/arm6                                   19s   1GB
Feb 01 15:39:14 Starting compiler/backend/arm8
Feb 01 15:39:33 Finished compiler/backend/arm8                                   18s   1GB
Feb 01 15:39:33 Starting compiler/backend/mips
Feb 01 15:39:53 Finished compiler/backend/mips                                   18s   1GB
Feb 01 15:39:53 Starting compiler/backend/riscv
Feb 01 15:40:12 Finished compiler/backend/riscv                                  18s   1GB
Feb 01 15:40:13 Starting compiler/backend/ag32
Feb 01 15:41:19 Finished compiler/backend/ag32                                 1m06s   1GB
Feb 01 15:41:20 Starting compiler/parsing/proofs
Feb 01 15:46:47 Finished compiler/parsing/proofs                               5m26s 898MB
Feb 01 15:46:48 Starting compiler/inference/proofs
Feb 01 15:49:30 Finished compiler/inference/proofs                             2m40s   1GB
Feb 01 15:49:30 Starting compiler/backend/semantics
Feb 01 15:56:17 Finished compiler/backend/semantics                            6m45s   2GB
Feb 01 15:56:17 Starting compiler/backend/reg_alloc/proofs
Feb 01 15:58:51 Finished compiler/backend/reg_alloc/proofs                     2m33s 846MB
Feb 01 15:58:52 Starting compiler/backend/proofs
Feb 01 16:34:47 Finished compiler/backend/proofs                              35m54s   3GB
Feb 01 16:34:48 Starting compiler/encoders/x64/proofs
Feb 01 16:43:38 Finished compiler/encoders/x64/proofs                          8m49s   5GB
Feb 01 16:43:38 Starting compiler/encoders/arm6/proofs
Feb 01 16:55:39 Finished compiler/encoders/arm6/proofs                        11m59s   3GB
Feb 01 16:55:39 Starting compiler/encoders/arm8/proofs
Feb 01 17:01:06 Finished compiler/encoders/arm8/proofs                         5m25s   1GB
Feb 01 17:01:06 Starting compiler/encoders/mips/proofs
Feb 01 17:10:29 Finished compiler/encoders/mips/proofs                         9m21s   2GB
Feb 01 17:10:29 Starting compiler/encoders/riscv/proofs
Feb 01 17:17:46 Finished compiler/encoders/riscv/proofs                        7m16s   1GB
Feb 01 17:17:47 Starting compiler/encoders/ag32/proofs
Feb 01 17:20:13 Finished compiler/encoders/ag32/proofs                         2m25s 622MB
Feb 01 17:20:14 Starting compiler/backend/x64/proofs
Feb 01 17:20:34 Finished compiler/backend/x64/proofs                             20s   1GB
Feb 01 17:20:35 Starting compiler/backend/arm6/proofs
Feb 01 17:21:02 Finished compiler/backend/arm6/proofs                            26s   1GB
Feb 01 17:21:02 Starting compiler/backend/arm8/proofs
Feb 01 17:21:23 Finished compiler/backend/arm8/proofs                            19s   1GB
Feb 01 17:21:24 Starting compiler/backend/mips/proofs
Feb 01 17:21:44 Finished compiler/backend/mips/proofs                            19s 868MB
Feb 01 17:21:45 Starting compiler/backend/riscv/proofs
Feb 01 17:22:06 Finished compiler/backend/riscv/proofs                           19s   1GB
Feb 01 17:22:06 Starting compiler/backend/ag32/proofs
Feb 01 17:30:35 Finished compiler/backend/ag32/proofs                          8m27s   3GB
Feb 01 17:30:35 Starting compiler/proofs
Feb 01 17:31:58 Finished compiler/proofs                                       1m21s   3GB
Feb 01 17:31:58 Starting candle/set-theory
Feb 01 17:32:25 Finished candle/set-theory                                       26s 742MB
Feb 01 17:32:26 Starting candle/syntax-lib
Feb 01 17:32:37 Finished candle/syntax-lib                                       10s 467MB
Feb 01 17:32:38 Starting candle/standard/syntax
Feb 01 17:34:22 Finished candle/standard/syntax                                1m42s 997MB
Feb 01 17:34:22 Starting candle/standard/semantics
Feb 01 17:35:59 Finished candle/standard/semantics                             1m36s   1GB
Feb 01 17:36:00 Starting candle/standard/monadic
Feb 01 17:37:32 Finished candle/standard/monadic                               1m31s   1GB
Feb 01 17:37:33 Starting candle/standard/ml_kernel
Feb 01 17:41:21 Finished candle/standard/ml_kernel                             3m47s   3GB
Feb 01 17:41:22 Starting candle/standard/opentheory
Feb 01 17:49:47 Finished candle/standard/opentheory                            8m24s   5GB
Feb 01 17:49:48 Starting candle/standard/opentheory/compilation
Feb 01 18:18:36 Finished candle/standard/opentheory/compilation               28m47s  23GB
Feb 01 18:18:37 Starting candle/standard/opentheory/compilation/proofs
Feb 01 18:19:28 Finished candle/standard/opentheory/compilation/proofs           50s   6GB
Feb 01 18:19:28 Starting characteristic/examples
Feb 01 18:21:00 Finished characteristic/examples                               1m31s   2GB
Feb 01 18:21:01 Starting tutorial/solutions
Feb 01 18:34:07 Finished tutorial/solutions                                   13m05s   6GB
Feb 01 18:34:08 Starting translator/monadic/examples
Feb 01 18:36:24 Finished translator/monadic/examples                           2m15s   2GB
Feb 01 18:36:25 Starting examples
Feb 01 18:44:03 Finished examples                                              7m37s   4GB
Feb 01 18:44:03 Starting examples/compilation/x64
Feb 01 20:37:32 Finished examples/compilation/x64                           1h53m28s  14GB
Feb 01 20:37:33 Starting examples/compilation/x64/proofs
Feb 01 20:39:24 Finished examples/compilation/x64/proofs                       1m50s   4GB
Feb 01 20:39:24 Starting examples/compilation/ag32
Feb 01 21:07:24 Finished examples/compilation/ag32                            27m59s   6GB
Feb 01 21:07:25 Starting examples/compilation/ag32/proofs
Feb 01 21:08:14 Finished examples/compilation/ag32/proofs                        48s   4GB
Feb 01 21:08:15 Starting translator/okasaki-examples
Feb 01 21:12:19 Finished translator/okasaki-examples                           4m03s   1GB
Feb 01 21:12:20 Starting translator/other-examples
Feb 01 21:15:55 Finished translator/other-examples                             3m34s   1GB
Feb 01 21:15:56 Starting compiler/parsing/tests
Feb 01 21:16:22 Finished compiler/parsing/tests                                  25s 558MB
Feb 01 21:16:23 Starting compiler/inference/tests
Feb 01 21:20:27 Finished compiler/inference/tests                              4m03s   3GB
Feb 01 21:20:27 Starting compiler/bootstrap/translation
Feb 01 23:46:44 Finished compiler/bootstrap/translation                     2h26m15s  47GB
Feb 01 23:46:44 Starting unverified/sexpr-bootstrap/x64/64
Feb 01 23:55:33 Finished unverified/sexpr-bootstrap/x64/64                     8m47s  15GB
Feb 01 23:55:33 Starting unverified/sexpr-bootstrap/x64/32
Feb 02 00:00:37 Finished unverified/sexpr-bootstrap/x64/32                     5m02s  18GB
Feb 02 00:00:38 Starting compiler/benchmarks/cakeml_benchmarks/cakeml
Feb 02 00:01:10 Finished compiler/benchmarks/cakeml_benchmarks/cakeml            32s   1GB
Feb 02 00:01:11 Starting compiler/benchmarks/mlton_benchmarks/cakeml
Feb 02 00:01:16 FAILED: compiler/benchmarks/mlton_benchmarks/cakeml
Starting work on cake.S
cake.S                                                                       OK
Starting work on cake
README.md                                                                    OK
cake                                                                         OK
Starting work on build-benchmarks
build-benchmarks                                                    FAILED! <2>
 ./cake  < smith-normal-form.sml > smith-normal-form.S
 ### ERROR: parse error
 make: *** [Makefile:28: cake_smith-normal-form] Error 1