From 182311e6d7104153d282d574c94cfdb2dc757a63 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 10 Mar 2021 17:14:25 +0100
Subject: [PATCH] check that Iris works with name mangling

---
 .gitlab-ci.yml            | 1 +
 tests/atomic.v            | 2 ++
 tests/heap_lang.v         | 2 ++
 tests/heap_lang2.v        | 2 ++
 tests/ipm_paper.v         | 2 ++
 tests/list_reverse.v      | 2 ++
 tests/mosel_paper.v       | 2 ++
 tests/one_shot.v          | 2 ++
 tests/one_shot_once.v     | 2 ++
 tests/proofmode.v         | 2 ++
 tests/proofmode_ascii.v   | 1 +
 tests/proofmode_iris.v    | 2 ++
 tests/proofmode_monpred.v | 2 ++
 tests/telescopes.v        | 2 ++
 14 files changed, 26 insertions(+)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 22e846f04..d39314f07 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -31,6 +31,7 @@ build-coq.dev:
   <<: *template
   variables:
     OPAM_PINS: "coq version dev"
+    MANGLE_NAMES: "1"
 
 build-coq.8.13.1:
   <<: *template
diff --git a/tests/atomic.v b/tests/atomic.v
index f9881ffcd..00d34adde 100644
--- a/tests/atomic.v
+++ b/tests/atomic.v
@@ -3,6 +3,8 @@ From iris.program_logic Require Export atomic.
 From iris.heap_lang Require Import proofmode notation atomic_heap.
 Set Default Proof Using "Type".
 
+Unset Mangle Names.
+
 Section tests.
   Context `{!heapG Σ} {aheap: atomic_heap Σ}.
   Import atomic_heap.notation.
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 4fd2570e8..a05b855a2 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -5,6 +5,8 @@ From iris.heap_lang Require Import lang adequacy proofmode notation.
 From iris.heap_lang Require Import lang.
 Set Default Proof Using "Type".
 
+Unset Mangle Names.
+
 Section tests.
   Context `{!heapG Σ}.
   Implicit Types P Q : iProp Σ.
diff --git a/tests/heap_lang2.v b/tests/heap_lang2.v
index 334732089..85b25b90b 100644
--- a/tests/heap_lang2.v
+++ b/tests/heap_lang2.v
@@ -5,6 +5,8 @@ From iris.heap_lang Require Export primitive_laws notation.
 From iris.heap_lang Require Import proofmode notation.
 Set Default Proof Using "Type".
 
+Unset Mangle Names.
+
 Section printing_tests.
   Context `{!heapG Σ}.
 
diff --git a/tests/ipm_paper.v b/tests/ipm_paper.v
index b1a5d2d61..9f2cc5842 100644
--- a/tests/ipm_paper.v
+++ b/tests/ipm_paper.v
@@ -9,6 +9,8 @@ From iris.deprecated.program_logic Require Import hoare.
 From iris.heap_lang Require Import proofmode notation.
 Set Default Proof Using "Type".
 
+Unset Mangle Names.
+
 (** The proofs from Section 3.1 *)
 Section demo.
   Context {M : ucmra}.
diff --git a/tests/list_reverse.v b/tests/list_reverse.v
index ba12c8599..3ecdbbe08 100644
--- a/tests/list_reverse.v
+++ b/tests/list_reverse.v
@@ -5,6 +5,8 @@ From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
 Set Default Proof Using "Type".
 
+Unset Mangle Names.
+
 Section list_reverse.
 Context `{!heapG Σ}.
 Implicit Types l : loc.
diff --git a/tests/mosel_paper.v b/tests/mosel_paper.v
index bb9eb5b42..00a84f31f 100644
--- a/tests/mosel_paper.v
+++ b/tests/mosel_paper.v
@@ -8,6 +8,8 @@ ICFP 2018 *)
 From iris.bi Require Import monpred.
 From iris.proofmode Require Import tactics monpred.
 
+Unset Mangle Names.
+
 Lemma example_1 {PROP : bi} {A : Type} (P : PROP) (Φ Ψ : A → PROP) :
   P ∗ (∃ a, Φ a ∨ Ψ a) -∗ ∃ a, (P ∗ Φ a) ∨ (P ∗ Ψ a).
 Proof.
diff --git a/tests/one_shot.v b/tests/one_shot.v
index 59df90b75..0f93ccabf 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -10,6 +10,8 @@ Set Default Proof Using "Type".
 (** This is the introductory example from the "Iris from the Ground Up" journal
 paper. *)
 
+Unset Mangle Names.
+
 Definition one_shot_example : val := λ: <>,
   let: "x" := ref NONE in (
   (* tryset *) (λ: "n",
diff --git a/tests/one_shot_once.v b/tests/one_shot_once.v
index 72d1e4dcc..4b858ca73 100644
--- a/tests/one_shot_once.v
+++ b/tests/one_shot_once.v
@@ -10,6 +10,8 @@ Set Default Proof Using "Type".
 (** This is the introductory example from Ralf's PhD thesis.
 The difference to [one_shot] is that [set] asserts to be called only once. *)
 
+Unset Mangle Names.
+
 Definition one_shot_example : val := λ: <>,
   let: "x" := ref NONE in (
   (* set *) (λ: "n",
diff --git a/tests/proofmode.v b/tests/proofmode.v
index c6bb9934c..bf5c427a0 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1,6 +1,8 @@
 From iris.proofmode Require Import tactics intro_patterns.
 Set Default Proof Using "Type".
 
+Unset Mangle Names.
+
 Section tests.
 Context {PROP : bi}.
 Implicit Types P Q R : PROP.
diff --git a/tests/proofmode_ascii.v b/tests/proofmode_ascii.v
index cab53ecec..ebc45c6e5 100644
--- a/tests/proofmode_ascii.v
+++ b/tests/proofmode_ascii.v
@@ -5,6 +5,7 @@ From iris.base_logic.lib Require Import invariants cancelable_invariants na_inva
 From iris.bi Require Import ascii.
 
 Set Default Proof Using "Type".
+Unset Mangle Names.
 
 (* Remove this and the [Set Printing Raw Literals.] below once we require Coq
 8.14. *)
diff --git a/tests/proofmode_iris.v b/tests/proofmode_iris.v
index 700ffde50..f88ea6e87 100644
--- a/tests/proofmode_iris.v
+++ b/tests/proofmode_iris.v
@@ -3,6 +3,8 @@ From iris.proofmode Require Import tactics monpred.
 From iris.base_logic Require Import base_logic.
 From iris.base_logic.lib Require Import invariants cancelable_invariants na_invariants.
 
+Unset Mangle Names.
+
 Section base_logic_tests.
   Context {M : ucmra}.
   Implicit Types P Q R : uPred M.
diff --git a/tests/proofmode_monpred.v b/tests/proofmode_monpred.v
index 5b0cc65a3..6e69c5c88 100644
--- a/tests/proofmode_monpred.v
+++ b/tests/proofmode_monpred.v
@@ -1,6 +1,8 @@
 From iris.proofmode Require Import tactics monpred.
 From iris.base_logic.lib Require Import invariants.
 
+Unset Mangle Names.
+
 Section tests.
   Context {I : biIndex} {PROP : bi}.
   Local Notation monPred := (monPred I PROP).
diff --git a/tests/telescopes.v b/tests/telescopes.v
index 897592b18..ce3a0290b 100644
--- a/tests/telescopes.v
+++ b/tests/telescopes.v
@@ -2,6 +2,8 @@ From stdpp Require Import coPset namespaces.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
+Unset Mangle Names.
+
 Section basic_tests.
   Context {PROP : bi}.
   Implicit Types P Q R : PROP.
-- 
GitLab