Add compiling linux as a benchmark

bench.sh

@@ -14,7 +14,7 @@ alloc_libs="sys="      # mapping from allocator to its .so as "<allocator>=<sofi
 
 readonly tests_all1="cfrac espresso barnes redis lean larson-sized mstress rptest gs lua"
 readonly tests_all2="alloc-test sh6bench sh8bench xmalloc-test cscratch glibc-simple glibc-thread rocksdb"
-readonly tests_all3="larson lean-mathlib malloc-large mleak rbstress cthrash"
+readonly tests_all3="larson lean-mathlib linux malloc-large mleak rbstress cthrash"
 readonly tests_all4="z3 spec spec-bench security"
 
 readonly tests_all="$tests_all1 $tests_all2 $tests_all3 $tests_all4"
@@ -30,6 +30,7 @@ readonly tests_exclude_macos="sh6bench sh8bench redis"
 
 readonly version_redis=6.2.7
 readonly version_rocksdb=8.1.1
+readonly version_linux=6.5.1
 
 # --------------------------------------------------------------------
 # Environment
@@ -164,6 +165,7 @@ readonly leanmldir="$leandir/../mathlib"
 readonly redis_dir="$localdevdir/redis-$version_redis/src"
 readonly pdfdoc="$localdevdir/large.pdf" 
 readonly rocksdb_dir="$localdevdir/rocksdb-$version_rocksdb"
+readonly linux_dir="$localdevdir/linux-$version_linux"
 
 readonly spec_dir="$localdevdir/../../spec2017"
 readonly spec_base="base"
@@ -545,6 +547,13 @@ function run_test_env_cmd { # <test name> <allocator name> <environment args> <c
       outfile="$1-$2-out.txt";;
     barnes)
       infile="$benchdir/barnes/input";;
+    linux)
+      builddir="/tmp/linux_build"
+      pushd "$linux_dir"
+      mkdir -p $builddir
+      make O=$builddir distclean
+      make O=$builddir allnoconfig
+      popd;;
   esac
   case "$1" in
     redis*)
@@ -679,6 +688,11 @@ function run_test {  # <test>
       pushd "$leanmldir"
       run_test_cmd "mathlib" "$leandir/bin/leanpkg build"
       popd;;
+    linux)
+      builddir="/tmp/linux_build"
+      pushd "$linux_dir"
+      run_test_cmd "linux" "make O=$builddir -j $procs"
+      popd;;
     redis)
       # https://redis.io/docs/reference/optimization/benchmarks/
       redis_tail="1"

build-bench-env.sh

@@ -69,6 +69,7 @@ readonly version_redis=6.2.7
 readonly version_lean=21d264a66d53b0a910178ae7d9529cb5886a39b6 # build fix for recent compilers
 readonly version_rocksdb=8.1.1
 readonly version_lua=v5.4.4
+readonly version_linux=6.5.1
 
 # HTTP-downloaded files checksums
 readonly sha256sum_sh6bench="506354d66b9eebef105d757e055bc55e8d4aea1e7b51faab3da35b0466c923a1"
@@ -107,6 +108,7 @@ setup_bench=0
 setup_lean=0
 setup_redis=0
 setup_rocksdb=0
+setup_linux=0
 
 # various
 setup_packages=0
@@ -165,6 +167,7 @@ while : ; do
         setup_lean=$flag_arg
         setup_redis=$flag_arg
         setup_rocksdb=$flag_arg
+        setup_linux=$flag_arg
         setup_bench=$flag_arg
         setup_packages=$flag_arg
         ;;
@@ -212,6 +215,8 @@ while : ; do
         setup_redis=$flag_arg;;
     rocksdb)
         setup_rocksdb=$flag_arg;;
+    linux)
+        setup_linux=$flag_arg;;
     rp)
         setup_rp=$flag_arg;;
     sc)
@@ -274,6 +279,7 @@ while : ; do
         echo "  packages                     setup required packages"
         echo "  redis                        setup redis benchmark"
         echo "  rocksdb                      setup rocksdb benchmark"
+        echo "  linux                        setup linux benchmark"
         echo ""
         echo "Prefix an option with 'no-' to disable an option"
         exit 0;;
@@ -842,6 +848,18 @@ if test "$setup_bench" = "1"; then
   cmake --build out/bench --parallel $procs
 fi
 
+if test "$setup_linux" = "1"; then
+  phase "fetch linux"
+  pushd "$devdir"
+  if test -d "linux-$version_linux"; then
+    echo "$devdir/linux-$version_linux already exists; no need to download it"
+  else
+    wget --no-verbose "https://cdn.kernel.org/pub/linux/kernel/v6.x/linux-$version_linux.tar.xz"
+    tar xf "linux-$version_linux.tar.xz"
+    rm "./linux-$version_linux.tar.xz"
+  fi
+  popd
+fi
 
 curdir=`pwd`