diff --git a/bench.sh b/bench.sh index 7a4f3a7..cfcf964 100755 --- a/bench.sh +++ b/bench.sh @@ -14,7 +14,7 @@ alloc_libs="sys=" # mapping from allocator to its .so as "= 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" diff --git a/build-bench-env.sh b/build-bench-env.sh index 74e67d0..00829e0 100755 --- a/build-bench-env.sh +++ b/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`