changeset 1353:e948f92964b5

Speed up miniconfig by introducing "stride" (discard lines in batches).
author Rob Landley <rob@landley.net>
date Wed, 04 May 2011 02:04:17 -0500
parents 6da94a74a8a9
children 5ec7eb5b96ab
files sources/toys/miniconfig.sh
diffstat 1 files changed, 17 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/sources/toys/miniconfig.sh	Mon Apr 18 22:51:21 2011 -0500
+++ b/sources/toys/miniconfig.sh	Wed May 04 02:04:17 2011 -0500
@@ -80,19 +80,31 @@
   then
     break
   fi
-  sed -n "${I}!p" mini.config > .config.test
+  sed -n "$I,$(($I+${STRIDE:-1}-1))!p" mini.config > .config.test
   # Do a config with this file
   rm .config
-  make allnoconfig KCONFIG_ALLCONFIG=.config.test | head -n 1000000 > /dev/null
+  make allnoconfig KCONFIG_ALLCONFIG=.config.test 2>/dev/null | head -n 1000000 > /dev/null
   # Compare.  Because we normalized at the start, the files should be identical.
   if cmp -s .config .big.config
   then
+    # Found unneeded line(s)
     mv .config.test mini.config
-    LENGTH=$[$LENGTH-1]
+    LENGTH=$(($LENGTH-${STRIDE:-1}))
+    # Special case where we know the next line _is_ needed: stride 2 failed
+    # but we discarded the first line
+    [ -z "$STRIDE" ] && [ ${OLDSTRIDE:-1} -eq 2 ] && I=$(($I+1))
+    STRIDE=$(($STRIDE+1))
+    OLDSTRIDE=$STRIDE
   else
-    I=$[$I + 1]
+    # That hunk was needed
+    if [ ${STRIDE:-1} -le 1 ]
+    then
+      I=$(($I+1))
+      OLDSTRIDE=
+    fi
+    STRIDE=
   fi
-  echo -n -e "\r$[$I-1]/$LENGTH lines $(cat mini.config | wc -c) bytes $[100-((($LENGTH-$I)*100)/$OLDLENGTH)]% "
+  echo -n -e "\r[${STRIDE:-1}] $[$I-1]/$LENGTH lines $(cat mini.config | wc -c) bytes $[100-((($LENGTH-$I)*100)/$OLDLENGTH)]%    "
 done
 rm .big.config
 echo