michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(script): add script for collecting standard library compilation times

Browse source
This commit is contained in:
Leonardo de Moura 2014-11-26 11:41:00 -08:00
parent ea63136434
commit 126398ccb0
1 changed files with 13 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
script/lib_perf.sh Executable file
View file

@ -0,0 +1,13 @@
# 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
TIME=/usr/bin/time
REALPATH=realpath
MY_PATH="`dirname \"$0\"`"
LEAN=$MY_PATH/../bin/lean
LIB=$MY_PATH/../library
for f in `find $LIB -name '*.lean'`; do
rf=`$REALPATH $f`
$TIME --format="$rf %e" $LEAN $rf > /dev/null
done