Commit bfca339f authored by Ralf Jung's avatar Ralf Jung

more opaque wp; add a benchmark script

parent 6e7d84ad
#!/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
......@@ -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.
......
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.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment