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

feat(script/lib_perf): show time spent on HoTT library files

Browse source
This commit is contained in:
Leonardo de Moura 2015-02-25 10:50:30 -08:00
parent 577a6da119
commit 2b1d67f717
1 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
script/lib_perf.sh
View file

@ -11,3 +11,9 @@ for f in `find $LIB -name '*.lean'`; do
rf=`$REALPATH $f`
$TIME --format="$rf %e" $LEAN $rf > /dev/null
done
LIB=$MY_PATH/../hott
for f in `find $LIB -name '*.hlean'`; do
rf=`$REALPATH $f`
$TIME --format="$rf %e" $LEAN $rf > /dev/null
done