From 2b8a7576b689b50023b8a2253e99f7f3f6575921 Mon Sep 17 00:00:00 2001
From: Cyril Cohen <cohen@crans.org>
Date: Mon, 18 Dec 2023 16:20:11 +0100
Subject: [PATCH 1/2] initial commit for the metadata CEP

---
 text/000-metadata.md | 60 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 60 insertions(+)
 create mode 100644 text/000-metadata.md

diff --git a/text/000-metadata.md b/text/000-metadata.md
new file mode 100644
index 00000000..7e40d286
--- /dev/null
+++ b/text/000-metadata.md
@@ -0,0 +1,60 @@
+- Title: Adding MetaData to Coq
+
+- Drivers: @CohenCyril @palmskog @gares @TDiazT @pi8027 @ejgallego @SkySkimmer
+
+----
+
+# Summary
+
+The purpose is to add several kind of metadata, attached to constants,
+modules, files, etc.
+
+
+# Motivation
+
+This metadata should be usable and used to enhance search,
+documentation generation, and build database for Coq libraries.
+
+
+# Detailed design
+
+## For search
+
+- adding docstrings (that search can grep inside)
+  ```coq
+  #[docstring="foo is a dummy lemma"]
+  Lemma foo : True. by []. Qed.
+  ```
+- aliasing of statements so that search can find a statement which is
+  convertible but not syntactically equal.
+  ```coq
+  #[alias="forall x y, x * y = y * x"]
+  Lemma mulrC : commutative mul. ...
+  ```
+  or
+  ```coq
+  #[alias(unfold="commutative")]
+  Lemma mulrC : commutative mul. ...
+  ```
+  and we could have several aliases (`#[alias=..., alias=..., ...]`).
+- Give a name from the litterature (searchable again)
+  ```coq
+  #[name="Abel-Ruffini Theorem", name="Abel's Theorem"]
+  Lemma unsolvable_quintic : ...
+  ```
+- Have a way to refer to a bibliography from a definition or its proof
+  E.g via a `#[ref="name"]` attribute with a bibtex (for example),
+  shared accross one or several projects.
+
+# Drawbacks
+
+TODO
+
+# Alternatives
+
+TODO
+
+# Unresolved questions
+
+Where to store this?
+TODO

From 8abf3b099126e0d56e0a35a34eefb49ba0fb2b9e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Mon, 18 Dec 2023 16:25:13 +0100
Subject: [PATCH 2/2] Update 000-metadata.md

---
 text/000-metadata.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/text/000-metadata.md b/text/000-metadata.md
index 7e40d286..78c8e8ea 100644
--- a/text/000-metadata.md
+++ b/text/000-metadata.md
@@ -30,6 +30,8 @@ documentation generation, and build database for Coq libraries.
   ```coq
   #[alias="forall x y, x * y = y * x"]
   Lemma mulrC : commutative mul. ...
+
+  Search (_ * _ = _ * _). (* mulrC appears *)
   ```
   or
   ```coq