#!/bin/bash
set -e

TIME() {
    echo "# Preparing $1"
    make -j $(cat "$1".v.d | sed 's/^.*: //')
    rm -f "$1".vo
    echo "# Benchmarking $1"
    time make "$1.vo"
    echo
}

TIME iris_plog
TIME iris_meta
TIME iris_ht_rules