update build system

build/opam-ci.sh

 #!/bin/bash
 set -e
+set -x
 ## This script installs the build dependencies for CI builds.
-function run_and_print() {
-    echo "$ $@"
-    "$@"
-}
 
 # Prepare OPAM configuration
 export OPAMROOT="$(pwd)/opamroot"
@@ -12,27 +9,27 @@ export OPAMJOBS="$((2*$CPU_CORES))"
 export OPAM_EDITOR="$(which false)"
 
 # Make sure we got a good OPAM.
-test -d "$OPAMROOT" || (mkdir "$OPAMROOT" && run_and_print opam init --no-setup -y)
+test -d "$OPAMROOT" || (mkdir "$OPAMROOT" && opam init --no-setup -y)
 eval `opam conf env`
 
 # Make sure the pin for the builddep package is not stale.
-run_and_print make build-dep/opam
+make build-dep/opam
 
 # Update repositories
-run_and_print opam update
+opam update
 
 # Make sure we got the right set of repositories registered
-if echo "$@" | fgrep "dev"; then
+if echo "$@" | fgrep "dev" > /dev/null; then
     # We are compiling against a dev version of something.  Get ourselves the dev repositories.
-    test -d "$OPAMROOT/repo/coq-extra-dev" || run_and_print opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev -p 0
-    test -d "$OPAMROOT/repo/coq-core-dev" || run_and_print opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev -p 5
+    test -d "$OPAMROOT/repo/coq-extra-dev" || opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev -p 0
+    test -d "$OPAMROOT/repo/coq-core-dev" || opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev -p 5
 else
     # No dev version, make sure we do not have the dev repositories.
-    test -d "$OPAMROOT/repo/coq-extra-dev" && run_and_print opam repo remove coq-extra-dev
-    test -d "$OPAMROOT/repo/coq-core-dev" && run_and_print opam repo remove coq-core-dev
+    test -d "$OPAMROOT/repo/coq-extra-dev" && opam repo remove coq-extra-dev
+    test -d "$OPAMROOT/repo/coq-core-dev" && opam repo remove coq-core-dev
 fi
-test -d "$OPAMROOT/repo/coq-released" || run_and_print opam repo add coq-released https://coq.inria.fr/opam/released -p 10
-test -d "$OPAMROOT/repo/iris-dev" || run_and_print opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git -p 20
+test -d "$OPAMROOT/repo/coq-released" || opam repo add coq-released https://coq.inria.fr/opam/released -p 10
+test -d "$OPAMROOT/repo/iris-dev" || opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git -p 20
 echo
 
 # We really want to run all of the following in one opam transaction, but due to opam limitations,
@@ -51,14 +48,14 @@ while (( "$#" )); do # while there are arguments left
         echo "[opam-ci] $PACKAGE already $KIND-pinned to $VERSION"
     else
         echo "[opam-ci] $KIND-pinning $PACKAGE to $VERSION"
-        run_and_print opam pin add -y -k "$KIND" "$PACKAGE" "$VERSION"
+        opam pin add -y -k "$KIND" "$PACKAGE" "$VERSION"
     fi
 done
 
 # Upgrade cached things.
 echo
 echo "[opam-ci] Upgrading opam"
-run_and_print opam upgrade -y
+opam upgrade -y --fixup
 
 # Install build-dependencies.
 echo

theories/base_logic/fixpoint.v

-From iris.base_logic Require Import base_logic.
-From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type*".
-Import uPred.
-
-(** Least and greatest fixpoint of a monotone function, defined entirely inside
-    the logic.  *)
-Class BIMonoPred {M} {A : ofeT} (F : (A → uPred M) → (A → uPred M)) := {
-  bi_mono_pred Φ Ψ : ((□ ∀ x, Φ x -∗ Ψ x) → ∀ x, F Φ x -∗ F Ψ x)%I;
-  bi_mono_pred_ne Φ : NonExpansive Φ → NonExpansive (F Φ)
-}.
-Arguments bi_mono_pred {_ _ _ _} _ _.
-Local Existing Instance bi_mono_pred_ne.
-
-Definition uPred_least_fixpoint {M} {A : ofeT}
-    (F : (A → uPred M) → (A → uPred M)) (x : A) : uPred M :=
-  (∀ Φ : A -n> uPredC M, □ (∀ x, F Φ x → Φ x) → Φ x)%I.
-
-Definition uPred_greatest_fixpoint {M} {A : ofeT}
-    (F : (A → uPred M) → (A → uPred M)) (x : A) : uPred M :=
-  (∃ Φ : A -n> uPredC M, □ (∀ x, Φ x → F Φ x) ∧ Φ x)%I.
-
-Section least.
-  Context {M} {A : ofeT} (F : (A → uPred M) → (A → uPred M)) `{!BIMonoPred F}.
-
-  Global Instance least_fixpoint_ne : NonExpansive (uPred_least_fixpoint F).
-  Proof. solve_proper. Qed.
-
-  Lemma least_fixpoint_unfold_2 x : F (uPred_least_fixpoint F) x ⊢ uPred_least_fixpoint F x.
-  Proof.
-    iIntros "HF" (Φ) "#Hincl".
-    iApply "Hincl". iApply (bi_mono_pred _ Φ); last done.
-    iIntros "!#" (y) "Hy". iApply "Hy". done.
-  Qed.
-
-  Lemma least_fixpoint_unfold_1 x :
-    uPred_least_fixpoint F x ⊢ F (uPred_least_fixpoint F) x.
-  Proof.
-    iIntros "HF". iApply ("HF" $! (CofeMor (F (uPred_least_fixpoint F))) with "[#]").
-    iIntros "!#" (y) "Hy". iApply bi_mono_pred; last done. iIntros "!#" (z) "?".
-    by iApply least_fixpoint_unfold_2.
-  Qed.
-
-  Corollary least_fixpoint_unfold x :
-    uPred_least_fixpoint F x ≡ F (uPred_least_fixpoint F) x.
-  Proof.
-    apply (anti_symm _); auto using least_fixpoint_unfold_1, least_fixpoint_unfold_2.
-  Qed.
-
-  Lemma least_fixpoint_ind (Φ : A → uPred M) `{!NonExpansive Φ} :
-    □ (∀ y, F Φ y → Φ y) ⊢ ∀ x, uPred_least_fixpoint F x → Φ x.
-  Proof.
-    iIntros "#HΦ" (x) "HF". by iApply ("HF" $! (CofeMor Φ) with "[#]").
-  Qed.
-
-  Lemma least_fixpoint_strong_ind (Φ : A → uPred M) `{!NonExpansive Φ} :
-    □ (∀ y, F (λ x, Φ x ∧ uPred_least_fixpoint F x) y → Φ y)
-    ⊢ ∀ x, uPred_least_fixpoint F x → Φ x.
-  Proof.
-    trans (∀ x, uPred_least_fixpoint F x → Φ x ∧ uPred_least_fixpoint F x)%I.
-    { iIntros "#HΦ". iApply least_fixpoint_ind; first solve_proper.
-      iIntros "!#" (y) "H". iSplit; first by iApply "HΦ".
-      iApply least_fixpoint_unfold_2. iApply (bi_mono_pred with "[] H").
-      by iIntros "!# * [_ ?]". }
-    by setoid_rewrite and_elim_l.
-  Qed.
-End least.
-
-Section greatest.
-  Context {M} {A : ofeT} (F : (A → uPred M) → (A → uPred M)) `{!BIMonoPred F}.
-
-  Global Instance greatest_fixpoint_ne : NonExpansive (uPred_greatest_fixpoint F).
-  Proof. solve_proper. Qed.
-
-  Lemma greatest_fixpoint_unfold_1 x :
-    uPred_greatest_fixpoint F x ⊢ F (uPred_greatest_fixpoint F) x.
-  Proof.
-    iDestruct 1 as (Φ) "[#Hincl HΦ]".
-    iApply (bi_mono_pred Φ (uPred_greatest_fixpoint F)).
-    - iIntros "!#" (y) "Hy". iExists Φ. auto.
-    - by iApply "Hincl".
-  Qed.
-
-  Lemma greatest_fixpoint_unfold_2 x :
-    F (uPred_greatest_fixpoint F) x ⊢ uPred_greatest_fixpoint F x.
-  Proof.
-    iIntros "HF". iExists (CofeMor (F (uPred_greatest_fixpoint F))).
-    iIntros "{$HF} !#" (y) "Hy". iApply (bi_mono_pred with "[] Hy").
-    iIntros "!#" (z) "?". by iApply greatest_fixpoint_unfold_1.
-  Qed.
-
-  Corollary greatest_fixpoint_unfold x :
-    uPred_greatest_fixpoint F x ≡ F (uPred_greatest_fixpoint F) x.
-  Proof.
-    apply (anti_symm _); auto using greatest_fixpoint_unfold_1, greatest_fixpoint_unfold_2.
-  Qed.
-
-  Lemma greatest_fixpoint_coind (Φ : A → uPred M) `{!NonExpansive Φ} :
-    □ (∀ y, Φ y → F Φ y) ⊢ ∀ x, Φ x → uPred_greatest_fixpoint F x.
-  Proof. iIntros "#HΦ" (x) "Hx". iExists (CofeMor Φ). by iIntros "{$Hx} !#". Qed.
-End greatest.