| #!/bin/bash | |
| # Script for collecting compilation times for the standard library | |
| # It assumes the lean binary is at the bin directory | |
| # It assumes the programs time and realpath are available | |
| set -eu | |
| TIME=/usr/bin/time | |
| REALPATH=realpath | |
| if ! command -v $TIME 2> /dev/null > /dev/null; then | |
| TIME=gtime | |
| fi | |
| MY_PATH="`dirname \"$0\"`" | |
| LEAN=$MY_PATH/../bin/lean | |
| LIB=$MY_PATH/../library | |
| for f in `find $LIB -name '*.lean'`; do | |
| rf=`$REALPATH $f` | |
| cp $rf tmp.lean | |
| $TIME --format="$rf %e" $LEAN -j 0 tmp.lean > /dev/null | |
| done |