From 126398ccb05190a20987750d7331c180b5550455 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 26 Nov 2014 11:41:00 -0800
Subject: [PATCH] feat(script): add script for collecting standard library
 compilation times

---
 script/lib_perf.sh | 13 +++++++++++++
 1 file changed, 13 insertions(+)
 create mode 100755 script/lib_perf.sh

diff --git a/script/lib_perf.sh b/script/lib_perf.sh
new file mode 100755
index 000000000..2dc4c4e5c
--- /dev/null
+++ b/script/lib_perf.sh
@@ -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