From 0b364bb5b065ae4e29c047c8f9f323fa9e232ba7 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 15 Oct 2015 19:04:55 +0200
Subject: [PATCH] improve benchmark script
---
benchmark | 17 +++++++++--------
1 file changed, 9 insertions(+), 8 deletions(-)
diff --git a/benchmark b/benchmark
index 0ba0d9f54..35b42e6e8 100755
--- a/benchmark
+++ b/benchmark
@@ -2,13 +2,14 @@
set -e
TIME() {
- rm -f "$1" && time make "$1"
+ echo "# Preparing $1"
+ make -j $(cat "$1".v.d | sed 's/^.*: //')
+ rm -f "$1".vo
+ echo "# Benchmarking $1"
+ time make "$1.vo"
+ echo
}
-make -j lib/ModuRes/{RA,UPred}.vo # BI dependencies
-TIME lib/ModuRes/BI.vo
-
-make -j {lang,masks,iris_core}.vo # iris_plog dependencies
-TIME iris_plog.vo
-TIME iris_meta.vo
-TIME iris_ht_rules.vo
+TIME iris_plog
+TIME iris_meta
+TIME iris_ht_rules
--
GitLab