From bfca339f241361b60659068267db30366b272a79 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 24 Mar 2015 14:02:58 +0100
Subject: [PATCH] more opaque wp; add a benchmark script

---
 benchmark        | 14 ++++++++++++++
 iris_plog.v      |  2 +-
 lib/ModuRes/BI.v |  3 +--
 3 files changed, 16 insertions(+), 3 deletions(-)
 create mode 100755 benchmark

diff --git a/benchmark b/benchmark
new file mode 100755
index 000000000..0ba0d9f54
--- /dev/null
+++ b/benchmark
@@ -0,0 +1,14 @@
+#!/bin/bash
+set -e
+
+TIME() {
+    rm -f "$1" && time make "$1"
+}
+
+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
diff --git a/iris_plog.v b/iris_plog.v
index 76a45a33f..32ac509f9 100644
--- a/iris_plog.v
+++ b/iris_plog.v
@@ -438,7 +438,7 @@ Module Type IRIS_PLOG (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
       unfold wp; apply fixp_eq.
     Qed.
 
-    Opaque wp.
+    Global Opaque wp.
 
     Lemma wpO {safe m e φ w r} : wp safe m e φ w O r.
     Proof.
diff --git a/lib/ModuRes/BI.v b/lib/ModuRes/BI.v
index 4532920c0..b3f9298f9 100644
--- a/lib/ModuRes/BI.v
+++ b/lib/ModuRes/BI.v
@@ -1,5 +1,6 @@
 Require Import PreoMet.
 Require Import RA.
+Require Import UPred.
 
 Section CompleteBI.
   Context {T : Type}.
@@ -116,8 +117,6 @@ Notation "∃ x , p" := (xist n[(fun x => p)]) (at level 60, x ident, right asso
 Notation "∀ x : T , p" := (all n[(fun x : T => p)]) (at level 60, x ident, right associativity) : bi_scope.
 Notation "∃ x : T , p" := (xist n[(fun x : T => p)]) (at level 60, x ident, right associativity) : bi_scope.
 
-Require Import UPred.
-
 Section UPredLater.
   Context Res `{preoRes : preoType Res}.
   Local Obligation Tactic := intros; resp_set || eauto with typeclass_instances.
-- 
GitLab