Commit 3fc3d3ff authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'ci/ralf/name-mangling' into 'master'

Make Iris compatible with name mangling

Closes #343

See merge request iris/iris!647
parents f53bcfd3 182311e6
...@@ -31,6 +31,7 @@ build-coq.dev: ...@@ -31,6 +31,7 @@ build-coq.dev:
<<: *template <<: *template
variables: variables:
OPAM_PINS: "coq version dev" OPAM_PINS: "coq version dev"
MANGLE_NAMES: "1"
build-coq.8.13.1: build-coq.8.13.1:
<<: *template <<: *template
......
...@@ -2948,13 +2948,13 @@ Tactic Notation "iInvCore" constr(select) "with" constr(pats) "as" open_constr(H ...@@ -2948,13 +2948,13 @@ Tactic Notation "iInvCore" constr(select) "with" constr(pats) "as" open_constr(H
end in end in
lazymatch type of select with lazymatch type of select with
| string => | string =>
eapply @tac_inv_elim with (i:=select) (j:=H) (Pclose:=Pclose_pat); notypeclasses refine (tac_inv_elim _ select H _ _ _ _ _ Pclose_pat _ _ _ _ _ _);
[ (by iAssumptionCore) || fail "iInv: invariant" select "not found" |..] [ (by iAssumptionCore) || fail "iInv: invariant" select "not found" |..]
| ident => | ident =>
eapply @tac_inv_elim with (i:=select) (j:=H) (Pclose:=Pclose_pat); notypeclasses refine (tac_inv_elim _ select H _ _ _ _ _ Pclose_pat _ _ _ _ _ _);
[ (by iAssumptionCore) || fail "iInv: invariant" select "not found" |..] [ (by iAssumptionCore) || fail "iInv: invariant" select "not found" |..]
| namespace => | namespace =>
eapply @tac_inv_elim with (j:=H) (Pclose:=Pclose_pat); notypeclasses refine (tac_inv_elim _ _ H _ _ _ _ _ Pclose_pat _ _ _ _ _ _);
[ (by iAssumptionInv select) || fail "iInv: invariant" select "not found" |..] [ (by iAssumptionInv select) || fail "iInv: invariant" select "not found" |..]
| _ => fail "iInv: selector" select "is not of the right type " | _ => fail "iInv: selector" select "is not of the right type "
end; end;
......
...@@ -3,6 +3,8 @@ From iris.program_logic Require Export atomic. ...@@ -3,6 +3,8 @@ From iris.program_logic Require Export atomic.
From iris.heap_lang Require Import proofmode notation atomic_heap. From iris.heap_lang Require Import proofmode notation atomic_heap.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Unset Mangle Names.
Section tests. Section tests.
Context `{!heapG Σ} {aheap: atomic_heap Σ}. Context `{!heapG Σ} {aheap: atomic_heap Σ}.
Import atomic_heap.notation. Import atomic_heap.notation.
......
...@@ -5,6 +5,8 @@ From iris.heap_lang Require Import lang adequacy proofmode notation. ...@@ -5,6 +5,8 @@ From iris.heap_lang Require Import lang adequacy proofmode notation.
From iris.heap_lang Require Import lang. From iris.heap_lang Require Import lang.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Unset Mangle Names.
Section tests. Section tests.
Context `{!heapG Σ}. Context `{!heapG Σ}.
Implicit Types P Q : iProp Σ. Implicit Types P Q : iProp Σ.
......
...@@ -5,6 +5,8 @@ From iris.heap_lang Require Export primitive_laws notation. ...@@ -5,6 +5,8 @@ From iris.heap_lang Require Export primitive_laws notation.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Unset Mangle Names.
Section printing_tests. Section printing_tests.
Context `{!heapG Σ}. Context `{!heapG Σ}.
......
...@@ -9,6 +9,8 @@ From iris.deprecated.program_logic Require Import hoare. ...@@ -9,6 +9,8 @@ From iris.deprecated.program_logic Require Import hoare.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Unset Mangle Names.
(** The proofs from Section 3.1 *) (** The proofs from Section 3.1 *)
Section demo. Section demo.
Context {M : ucmra}. Context {M : ucmra}.
......
...@@ -5,6 +5,8 @@ From iris.heap_lang Require Export lang. ...@@ -5,6 +5,8 @@ From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Unset Mangle Names.
Section list_reverse. Section list_reverse.
Context `{!heapG Σ}. Context `{!heapG Σ}.
Implicit Types l : loc. Implicit Types l : loc.
......
...@@ -8,6 +8,8 @@ ICFP 2018 *) ...@@ -8,6 +8,8 @@ ICFP 2018 *)
From iris.bi Require Import monpred. From iris.bi Require Import monpred.
From iris.proofmode Require Import tactics monpred. From iris.proofmode Require Import tactics monpred.
Unset Mangle Names.
Lemma example_1 {PROP : bi} {A : Type} (P : PROP) (Φ Ψ : A PROP) : Lemma example_1 {PROP : bi} {A : Type} (P : PROP) (Φ Ψ : A PROP) :
P ( a, Φ a Ψ a) - a, (P Φ a) (P Ψ a). P ( a, Φ a Ψ a) - a, (P Φ a) (P Ψ a).
Proof. Proof.
......
...@@ -10,6 +10,8 @@ Set Default Proof Using "Type". ...@@ -10,6 +10,8 @@ Set Default Proof Using "Type".
(** This is the introductory example from the "Iris from the Ground Up" journal (** This is the introductory example from the "Iris from the Ground Up" journal
paper. *) paper. *)
Unset Mangle Names.
Definition one_shot_example : val := λ: <>, Definition one_shot_example : val := λ: <>,
let: "x" := ref NONE in ( let: "x" := ref NONE in (
(* tryset *) (λ: "n", (* tryset *) (λ: "n",
......
...@@ -10,6 +10,8 @@ Set Default Proof Using "Type". ...@@ -10,6 +10,8 @@ Set Default Proof Using "Type".
(** This is the introductory example from Ralf's PhD thesis. (** This is the introductory example from Ralf's PhD thesis.
The difference to [one_shot] is that [set] asserts to be called only once. *) The difference to [one_shot] is that [set] asserts to be called only once. *)
Unset Mangle Names.
Definition one_shot_example : val := λ: <>, Definition one_shot_example : val := λ: <>,
let: "x" := ref NONE in ( let: "x" := ref NONE in (
(* set *) (λ: "n", (* set *) (λ: "n",
......
From iris.proofmode Require Import tactics intro_patterns. From iris.proofmode Require Import tactics intro_patterns.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Unset Mangle Names.
Section tests. Section tests.
Context {PROP : bi}. Context {PROP : bi}.
Implicit Types P Q R : PROP. Implicit Types P Q R : PROP.
......
...@@ -5,6 +5,7 @@ From iris.base_logic.lib Require Import invariants cancelable_invariants na_inva ...@@ -5,6 +5,7 @@ From iris.base_logic.lib Require Import invariants cancelable_invariants na_inva
From iris.bi Require Import ascii. From iris.bi Require Import ascii.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Unset Mangle Names.
(* Remove this and the [Set Printing Raw Literals.] below once we require Coq (* Remove this and the [Set Printing Raw Literals.] below once we require Coq
8.14. *) 8.14. *)
......
...@@ -3,6 +3,8 @@ From iris.proofmode Require Import tactics monpred. ...@@ -3,6 +3,8 @@ From iris.proofmode Require Import tactics monpred.
From iris.base_logic Require Import base_logic. From iris.base_logic Require Import base_logic.
From iris.base_logic.lib Require Import invariants cancelable_invariants na_invariants. From iris.base_logic.lib Require Import invariants cancelable_invariants na_invariants.
Unset Mangle Names.
Section base_logic_tests. Section base_logic_tests.
Context {M : ucmra}. Context {M : ucmra}.
Implicit Types P Q R : uPred M. Implicit Types P Q R : uPred M.
......
From iris.proofmode Require Import tactics monpred. From iris.proofmode Require Import tactics monpred.
From iris.base_logic.lib Require Import invariants. From iris.base_logic.lib Require Import invariants.
Unset Mangle Names.
Section tests. Section tests.
Context {I : biIndex} {PROP : bi}. Context {I : biIndex} {PROP : bi}.
Local Notation monPred := (monPred I PROP). Local Notation monPred := (monPred I PROP).
......
...@@ -2,6 +2,8 @@ From stdpp Require Import coPset namespaces. ...@@ -2,6 +2,8 @@ From stdpp Require Import coPset namespaces.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Unset Mangle Names.
Section basic_tests. Section basic_tests.
Context {PROP : bi}. Context {PROP : bi}.
Implicit Types P Q R : PROP. Implicit Types P Q R : PROP.
......
Supports Markdown
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