Overview

Job 496

CakeML:06ed260af9472c0513a9e22e9c2af4e3a38e38a0
  Add optional timnig in ml_translatorLib
#528 (fix-master)
Merging into:306e73e0ef0314393ecdbb996b50cf799375f15d
  Use Git's -C option
HOL:2a42da875092fdec35e1cd69454995735c890117
  Merge pull request #590 from binghe/PSL.fix
Machine:oven1 (2) 4.15.9-300.fc27.x86_64 x86_64 GNU/Linux

 Claimed job
 Reusing HOL
 Starting developers/bin
 Finished developers/bin                                          34s 912MB
 Starting semantics/ffi
 Finished semantics/ffi                                           11s 301MB
 Starting semantics
 Finished semantics                                             1m09s 915MB
 Starting semantics/proofs
 Finished semantics/proofs                                      2m41s   1GB
 Starting basis/pure
 Finished basis/pure                                              49s 780MB
 Starting translator
 Finished translator                                            1m05s 917MB
 Starting compiler/parsing
 Finished compiler/parsing                                      1m32s   1GB
 Starting characteristic
 Finished characteristic                                        2m26s   1GB
 Starting translator/monadic
 Finished translator/monadic                                    1m25s   1GB
 Starting basis
 Finished basis                                                16m36s   3GB
 Starting compiler/inference
 Finished compiler/inference                                    1m22s   1GB
 Starting compiler/backend/reg_alloc
 Finished compiler/backend/reg_alloc                              46s   1GB
 Starting compiler/backend/gc
 Finished compiler/backend/gc                                   7m42s   3GB
 Starting compiler/backend
 Finished compiler/backend                                         2s  15MB
 Starting compiler/encoders/asm
 Finished compiler/encoders/asm                                    1s  14MB
 Starting compiler/encoders/x64
 Finished compiler/encoders/x64                                   16s 404MB
 Starting compiler/encoders/arm6
 Finished compiler/encoders/arm6                                  45s 404MB
 Starting compiler/encoders/arm8
 Finished compiler/encoders/arm8                                   7s 333MB
 Starting compiler/encoders/mips
 Finished compiler/encoders/mips                                   9s 461MB
 Starting compiler/encoders/riscv
 Finished compiler/encoders/riscv                                  8s 408MB
 Starting compiler/backend/x64
 Finished compiler/backend/x64                                    17s   1GB
 Starting compiler/backend/arm6
 Finished compiler/backend/arm6                                   19s   1GB
 Starting compiler/backend/arm8
 Finished compiler/backend/arm8                                   18s   1GB
 Starting compiler/backend/mips
 Finished compiler/backend/mips                                   18s   1GB
 Starting compiler/backend/riscv
 Finished compiler/backend/riscv                                  17s 856MB
 Starting compiler/parsing/proofs
 Finished compiler/parsing/proofs                               6m09s 785MB
 Starting compiler/inference/proofs
 Finished compiler/inference/proofs                             2m49s   1GB
 Starting compiler/backend/semantics
 Finished compiler/backend/semantics                            8m57s   2GB
 Starting compiler/backend/reg_alloc/proofs
 Finished compiler/backend/reg_alloc/proofs                     7m26s 570MB
 Starting compiler/backend/proofs
 Finished compiler/backend/proofs                              35m48s   3GB
 Starting compiler/encoders/x64/proofs
 Finished compiler/encoders/x64/proofs                          7m23s   4GB
 Starting compiler/encoders/arm6/proofs
 Finished compiler/encoders/arm6/proofs                         7m36s   3GB
 Starting compiler/encoders/arm8/proofs
 Finished compiler/encoders/arm8/proofs                         5m16s   1GB
 Starting compiler/encoders/mips/proofs
 Finished compiler/encoders/mips/proofs                         7m24s   1GB
 Starting compiler/encoders/riscv/proofs
 Finished compiler/encoders/riscv/proofs                        8m14s 766MB
 Starting compiler/backend/x64/proofs
 Finished compiler/backend/x64/proofs                             20s   1GB
 Starting compiler/backend/arm6/proofs
 Finished compiler/backend/arm6/proofs                            22s 868MB
 Starting compiler/backend/arm8/proofs
 Finished compiler/backend/arm8/proofs                            19s 727MB
 Starting compiler/backend/mips/proofs
 Finished compiler/backend/mips/proofs                            20s   1GB
 Starting compiler/backend/riscv/proofs
 Finished compiler/backend/riscv/proofs                           20s   1GB
 Starting compiler/proofs
 Finished compiler/proofs                                       1m17s   2GB
 Starting candle/set-theory
 Finished candle/set-theory                                       25s 623MB
 Starting candle/syntax-lib
 Finished candle/syntax-lib                                       10s 565MB
 Starting candle/standard/syntax
 Finished candle/standard/syntax                                1m33s   1GB
 Starting candle/standard/semantics
 Finished candle/standard/semantics                             1m23s 915MB
 Starting candle/standard/monadic
 Finished candle/standard/monadic                               1m34s 944MB
 Starting candle/standard/ml_kernel
 Finished candle/standard/ml_kernel                            15m56s   5GB
 Starting candle/standard/opentheory
 Finished candle/standard/opentheory                            8m38s   5GB
 Starting characteristic/examples
 Finished characteristic/examples                               1m34s   2GB
 Starting tutorial/solutions
 Finished tutorial/solutions                                   13m17s   6GB
 Starting translator/monadic/examples
 Finished translator/monadic/examples                           1m43s   2GB
 Starting examples
 Finished examples                                              5m36s   4GB
 Starting examples/compilation
 Finished examples/compilation                               1h57m39s  10GB
 Starting examples/compilation/proofs
 Finished examples/compilation/proofs                           1m50s   3GB
 Starting compiler/benchmarks
 Finished compiler/benchmarks                                      0s   5MB
 Starting translator/okasaki-examples
 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