Job 496

CakeML:06ed260af9472c0513a9e22e9c2af4e3a38e38a0
  Add optional timnig in ml_translatorLib [Sep 22 21:45:33]
#528 (fix-master)
Merging into:306e73e0ef0314393ecdbb996b50cf799375f15d
  Use Git's -C option [Sep 14 21:28:55]
HOL:2a42da875092fdec35e1cd69454995735c890117
  Merge pull request #590 from binghe/PSL.fix [Sep 20 03:54:57]
Machine:oven1 (2) 4.15.9-300.fc27.x86_64 x86_64 GNU/Linux

Sep 23 07:06:41 Claimed job
Sep 23 07:06:52 Reusing HOL
Sep 23 07:07:45 Starting developers/bin
Sep 23 07:08:21 Finished developers/bin                                          34s 912MB
Sep 23 07:08:21 Starting semantics/ffi
Sep 23 07:08:33 Finished semantics/ffi                                           11s 301MB
Sep 23 07:08:34 Starting semantics
Sep 23 07:09:45 Finished semantics                                             1m09s 915MB
Sep 23 07:09:45 Starting semantics/proofs
Sep 23 07:12:27 Finished semantics/proofs                                      2m41s   1GB
Sep 23 07:12:28 Starting basis/pure
Sep 23 07:13:18 Finished basis/pure                                              49s 780MB
Sep 23 07:13:19 Starting translator
Sep 23 07:14:24 Finished translator                                            1m05s 917MB
Sep 23 07:14:25 Starting compiler/parsing
Sep 23 07:15:58 Finished compiler/parsing                                      1m32s   1GB
Sep 23 07:15:59 Starting characteristic
Sep 23 07:18:26 Finished characteristic                                        2m26s   1GB
Sep 23 07:18:27 Starting translator/monadic
Sep 23 07:19:53 Finished translator/monadic                                    1m25s   1GB
Sep 23 07:19:54 Starting basis
Sep 23 07:36:31 Finished basis                                                16m36s   3GB
Sep 23 07:36:32 Starting compiler/inference
Sep 23 07:37:55 Finished compiler/inference                                    1m22s   1GB
Sep 23 07:37:56 Starting compiler/backend/reg_alloc
Sep 23 07:38:43 Finished compiler/backend/reg_alloc                              46s   1GB
Sep 23 07:38:44 Starting compiler/backend/gc
Sep 23 07:46:27 Finished compiler/backend/gc                                   7m42s   3GB
Sep 23 07:46:28 Starting compiler/backend
Sep 23 07:46:31 Finished compiler/backend                                         2s  15MB
Sep 23 07:46:32 Starting compiler/encoders/asm
Sep 23 07:46:34 Finished compiler/encoders/asm                                    1s  14MB
Sep 23 07:46:34 Starting compiler/encoders/x64
Sep 23 07:46:51 Finished compiler/encoders/x64                                   16s 404MB
Sep 23 07:46:52 Starting compiler/encoders/arm6
Sep 23 07:47:38 Finished compiler/encoders/arm6                                  45s 404MB
Sep 23 07:47:39 Starting compiler/encoders/arm8
Sep 23 07:47:47 Finished compiler/encoders/arm8                                   7s 333MB
Sep 23 07:47:48 Starting compiler/encoders/mips
Sep 23 07:47:58 Finished compiler/encoders/mips                                   9s 461MB
Sep 23 07:47:59 Starting compiler/encoders/riscv
Sep 23 07:48:08 Finished compiler/encoders/riscv                                  8s 408MB
Sep 23 07:48:09 Starting compiler/backend/x64
Sep 23 07:48:27 Finished compiler/backend/x64                                    17s   1GB
Sep 23 07:48:27 Starting compiler/backend/arm6
Sep 23 07:48:47 Finished compiler/backend/arm6                                   19s   1GB
Sep 23 07:48:48 Starting compiler/backend/arm8
Sep 23 07:49:07 Finished compiler/backend/arm8                                   18s   1GB
Sep 23 07:49:08 Starting compiler/backend/mips
Sep 23 07:49:27 Finished compiler/backend/mips                                   18s   1GB
Sep 23 07:49:28 Starting compiler/backend/riscv
Sep 23 07:49:46 Finished compiler/backend/riscv                                  17s 856MB
Sep 23 07:49:47 Starting compiler/parsing/proofs
Sep 23 07:55:56 Finished compiler/parsing/proofs                               6m09s 785MB
Sep 23 07:55:57 Starting compiler/inference/proofs
Sep 23 07:58:48 Finished compiler/inference/proofs                             2m49s   1GB
Sep 23 07:58:48 Starting compiler/backend/semantics
Sep 23 08:07:46 Finished compiler/backend/semantics                            8m57s   2GB
Sep 23 08:07:47 Starting compiler/backend/reg_alloc/proofs
Sep 23 08:15:14 Finished compiler/backend/reg_alloc/proofs                     7m26s 570MB
Sep 23 08:15:15 Starting compiler/backend/proofs
Sep 23 08:51:03 Finished compiler/backend/proofs                              35m48s   3GB
Sep 23 08:51:04 Starting compiler/encoders/x64/proofs
Sep 23 08:58:29 Finished compiler/encoders/x64/proofs                          7m23s   4GB
Sep 23 08:58:30 Starting compiler/encoders/arm6/proofs
Sep 23 09:06:07 Finished compiler/encoders/arm6/proofs                         7m36s   3GB
Sep 23 09:06:07 Starting compiler/encoders/arm8/proofs
Sep 23 09:11:25 Finished compiler/encoders/arm8/proofs                         5m16s   1GB
Sep 23 09:11:26 Starting compiler/encoders/mips/proofs
Sep 23 09:18:51 Finished compiler/encoders/mips/proofs                         7m24s   1GB
Sep 23 09:18:52 Starting compiler/encoders/riscv/proofs
Sep 23 09:27:07 Finished compiler/encoders/riscv/proofs                        8m14s 766MB
Sep 23 09:27:08 Starting compiler/backend/x64/proofs
Sep 23 09:27:29 Finished compiler/backend/x64/proofs                             20s   1GB
Sep 23 09:27:30 Starting compiler/backend/arm6/proofs
Sep 23 09:27:53 Finished compiler/backend/arm6/proofs                            22s 868MB
Sep 23 09:27:53 Starting compiler/backend/arm8/proofs
Sep 23 09:28:13 Finished compiler/backend/arm8/proofs                            19s 727MB
Sep 23 09:28:14 Starting compiler/backend/mips/proofs
Sep 23 09:28:35 Finished compiler/backend/mips/proofs                            20s   1GB
Sep 23 09:28:35 Starting compiler/backend/riscv/proofs
Sep 23 09:28:57 Finished compiler/backend/riscv/proofs                           20s   1GB
Sep 23 09:28:57 Starting compiler/proofs
Sep 23 09:30:15 Finished compiler/proofs                                       1m17s   2GB
Sep 23 09:30:16 Starting candle/set-theory
Sep 23 09:30:42 Finished candle/set-theory                                       25s 623MB
Sep 23 09:30:43 Starting candle/syntax-lib
Sep 23 09:30:54 Finished candle/syntax-lib                                       10s 565MB
Sep 23 09:30:54 Starting candle/standard/syntax
Sep 23 09:32:28 Finished candle/standard/syntax                                1m33s   1GB
Sep 23 09:32:29 Starting candle/standard/semantics
Sep 23 09:33:53 Finished candle/standard/semantics                             1m23s 915MB
Sep 23 09:33:54 Starting candle/standard/monadic
Sep 23 09:35:29 Finished candle/standard/monadic                               1m34s 944MB
Sep 23 09:35:30 Starting candle/standard/ml_kernel
Sep 23 09:51:27 Finished candle/standard/ml_kernel                            15m56s   5GB
Sep 23 09:51:28 Starting candle/standard/opentheory
Sep 23 10:00:07 Finished candle/standard/opentheory                            8m38s   5GB
Sep 23 10:00:07 Starting characteristic/examples
Sep 23 10:01:42 Finished characteristic/examples                               1m34s   2GB
Sep 23 10:01:43 Starting tutorial/solutions
Sep 23 10:15:02 Finished tutorial/solutions                                   13m17s   6GB
Sep 23 10:15:03 Starting translator/monadic/examples
Sep 23 10:16:47 Finished translator/monadic/examples                           1m43s   2GB
Sep 23 10:16:48 Starting examples
Sep 23 10:22:25 Finished examples                                              5m36s   4GB
Sep 23 10:22:26 Starting examples/compilation
Sep 23 12:20:07 Finished examples/compilation                               1h57m39s  10GB
Sep 23 12:20:07 Starting examples/compilation/proofs
Sep 23 12:21:58 Finished examples/compilation/proofs                           1m50s   3GB
Sep 23 12:21:59 Starting compiler/benchmarks
Sep 23 12:22:00 Finished compiler/benchmarks                                      0s   5MB
Sep 23 12:22:01 Starting translator/okasaki-examples
Sep 24 11:20:29 FAILED: translator/okasaki-examples
]0;Holmake: ~/regression_2/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/formal-languages/regular]0;Holmake: ~/regression_2/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/formal-languages]0;Holmake: ~/regression_2/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/formal-languages[1mWorking in $(HOLDIR)/examples/formal-languages[0m
]0;Holmake: ~/regression_2/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/formal-languages/regular]0;Holmake: ~/regression_2/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/formal-languages/context-free]0;Holmake: ~/regression_2/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/formal-languages/context-free[1mWorking in $(HOLDIR)/examples/formal-languages/context-free[0m
]0;Holmake: ~/regression_2/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/formal-languages/regular]0;Holmake: ~/regression_2/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/formal-languages/regular[1mWorking in $(HOLDIR)/examples/formal-languages/regular[0m
]0;Holmake: ../../basis/pure]0;Holmake: ../../misc]0;Holmake: ~/regression_2/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/fun-op-sem/lprefix_lub]0;Holmake: ~/regression_2/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/fun-op-sem/lprefix_lub[1mWorking in $(HOLDIR)/examples/fun-op-sem/lprefix_lub[0m
]0;Holmake: ../../misc]0;Holmake: ~/regression_2/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/machine-code/hoare-triple]0;Holmake: ~/regression_2/HOL-2a42da875092fdec35e1cd69454995735c890117/examples/machine-code/hoare-triple[1mWorking in $(HOLDIR)/examples/machine-code/hoare-triple[0m
]0;Holmake: ../../misc]0;Holmake: ../../developers]0;Holmake: ../../developers[1mWorking in ../../developers[0m
]0;Holmake: ../../misc]0;Holmake: ../../misc/lem_lib_stub]0;Holmake: ../../misc/lem_lib_stub[1mWorking in $(CAKEMLDIR)/misc/lem_lib_stub[0m
]0;Holmake: ../../misc]0;Holmake: ../../misc[1mWorking in $(CAKEMLDIR)/misc[0m
]0;Holmake: ../../basis/pure]0;Holmake: ../../basis/pure[1mWorking in $(CAKEMLDIR)/basis/pure[0m
]0;Holmake: ../../basis]0;Holmake: ../../characteristic]0;Holmake: ../../compiler/parsing]0;Holmake: ../../semantics]0;Holmake: ../../semantics/ffi]0;Holmake: ../../semantics/ffi[1mWorking in $(CAKEMLDIR)/semantics/ffi[0m
]0;Holmake: ../../semantics]0;Holmake: ../../semantics[1mWorking in $(CAKEMLDIR)/semantics[0m
]0;Holmake: ../../compiler/parsing]0;Holmake: ../../compiler/parsing[1mWorking in $(CAKEMLDIR)/compiler/parsing[0m
]0;Holmake: ../../characteristic]0;Holmake: ../../translator]0;Holmake: ../../semantics/proofs]0;Holmake: ../../semantics/proofs[1mWorking in $(CAKEMLDIR)/semantics/proofs[0m
]0;Holmake: ../../translator]0;Holmake: ../../translator[1mWorking in $(CAKEMLDIR)/translator[0m
]0;Holmake: ../../characteristic]0;Holmake: ../../characteristic[1mWorking in $(CAKEMLDIR)/characteristic[0m
]0;Holmake: ../../basis]0;Holmake: ../../translator/monadic]0;Holmake: ../../translator/monadic[1mWorking in $(CAKEMLDIR)/translator/monadic[0m
]0;Holmake: ../../basis]0;Holmake: ../../basis[1mWorking in $(CAKEMLDIR)/basis[0m
]0;Holmake: .]0;Holmake: .[1mWorking in $(CAKEMLDIR)/translator/okasaki-examples[0m
Starting work on heap
heap                                                                                                                                                                                                             OK
Starting work on BankersQueueTheory
Starting work on BatchedQueueTheory
Starting work on okasaki_miscTheory
Starting work on HoodMelvilleQueueTheory
okasaki_miscTheory                                                                                                                                                                                               OK
Starting work on BinaryRandomAccessListsTheory
BatchedQueueTheory                                                                                                                                                                                               OK
Starting work on BinomialHeapTheory
HoodMelvilleQueueTheory                                                                                                                                                                                          OK
Starting work on BottomUpMergeSortTheory
BinaryRandomAccessListsTheory                                                                                                                                                                                    OK
Starting work on ImplicitQueueTheory
BottomUpMergeSortTheory                                                                                                                                                                                          OK
Starting work on LazyPairingHeapTheory
BinomialHeapTheory                                                                                                                                                                                               OK
Starting work on LeftistHeapTheory
LazyPairingHeapTheory                                                                                                                                                                                            OK
Starting work on PairingHeapTheory
ImplicitQueueTheory                                                                                                                                                                                              OK
Starting work on PhysicistsQueueTheory
LeftistHeapTheory                                                                                                                                                                                                OK
Starting work on RealTimeQueueTheory
PhysicistsQueueTheory                                                                                                                                                                                            OK
Starting work on RedBlackSetTheory
RealTimeQueueTheory                                                                                                                                                                                              OK
Starting work on SplayHeapTheory
PairingHeapTheory                                                                                                                                                                                                OK
Starting work on UnbalancedSetTheory
UnbalancedSetTheory                                                                                                                                                                                              OK
Starting work on benchmarkTheory
SplayHeapTheory                                                                                                                                                                                                  OK
benchmarkTheory                                                                                                                                                                                                  OK
RedBlackSetTheory                                                                                                                                                                                                OK