From 7eb3eb189fa2ac3ce124ffd9226e294cdf26e18b Mon Sep 17 00:00:00 2001
From: mhuisi <mhuisi@protonmail.com>
Date: Thu, 7 Sep 2023 10:56:17 +0200
Subject: [PATCH] chore: add new issue templates

---
 .github/ISSUE_TEMPLATE.md            | 30 ------------------
 .github/ISSUE_TEMPLATE/bug_report.md | 47 ++++++++++++++++++++++++++++
 .github/ISSUE_TEMPLATE/rfc.md        | 26 +++++++++++++++
 3 files changed, 73 insertions(+), 30 deletions(-)
 delete mode 100644 .github/ISSUE_TEMPLATE.md
 create mode 100644 .github/ISSUE_TEMPLATE/bug_report.md
 create mode 100644 .github/ISSUE_TEMPLATE/rfc.md

diff --git a/.github/ISSUE_TEMPLATE.md b/.github/ISSUE_TEMPLATE.md
deleted file mode 100644
index 88f86f4db0..0000000000
--- a/.github/ISSUE_TEMPLATE.md
+++ /dev/null
@@ -1,30 +0,0 @@
-### Prerequisites
-
-* [ ] Put an X between the brackets on this line if you have done all of the following:
-    * Checked that your issue isn't already [filed](https://github.com/leanprover/lean4/issues).
-    * Reduced the issue to a self-contained, reproducible test case.
-
-### Description
-
-[Description of the issue]
-
-### Steps to Reproduce
-
-1. [First Step]
-2. [Second Step]
-3. [and so on...]
-
-**Expected behavior:** [What you expect to happen]
-
-**Actual behavior:** [What actually happens]
-
-**Reproduces how often:** [What percentage of the time does it reproduce?]
-
-### Versions
-
-You can get this information from copy and pasting the output of `lean --version`,
-please include the OS and what version of the OS you're running.
-
-### Additional Information
-
-Any additional information, configuration or data that might be necessary to reproduce the issue.
diff --git a/.github/ISSUE_TEMPLATE/bug_report.md b/.github/ISSUE_TEMPLATE/bug_report.md
new file mode 100644
index 0000000000..7605ecb9b5
--- /dev/null
+++ b/.github/ISSUE_TEMPLATE/bug_report.md
@@ -0,0 +1,47 @@
+---
+name: Bug report
+about: Create a bug report
+title: ''
+labels: bug
+assignees: ''
+
+---
+
+### Prerequisites
+
+* [ ] Put an X between the brackets on this line if you have done all of the following:
+    * Check that your issue is not already [filed](https://github.com/leanprover/lean4/issues).
+    * Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.
+
+### Description
+
+[Clear and concise description of the issue]
+
+### Context
+
+[Broader context that the issue occured in. If there was any prior discussion on [the Lean Zulip](https://leanprover.zulipchat.com), link it here as well.]
+
+### Steps to Reproduce
+
+1.
+2.
+3.
+
+**Expected behavior:** [Clear and concise description of what you expect to happen]
+
+**Actual behavior:** [Clear and concise description of what actually happens]
+
+**Reproduces how often:** [Percentage of times the issue reproduces]
+
+### Versions
+
+[Output of `lean --version` in the folder that the issue occured in]
+[OS version]
+
+### Additional Information
+
+[Additional information, configuration or data that might be necessary to reproduce the issue]
+
+
+
+[Impact: If others are affected by this problem, ask them to add :+1: to this issue. Add :+1: to [other issues you consider important](https://github.com/leanprover/lean4/issues?q=is%3Aissue+is%3Aopen+sort%3Areactions-%2B1-desc).]
diff --git a/.github/ISSUE_TEMPLATE/rfc.md b/.github/ISSUE_TEMPLATE/rfc.md
new file mode 100644
index 0000000000..a6d9ad10e5
--- /dev/null
+++ b/.github/ISSUE_TEMPLATE/rfc.md
@@ -0,0 +1,26 @@
+---
+name: Request for comments
+about: Create a feature proposal
+title: 'RFC: '
+labels: RFC
+assignees: ''
+
+---
+
+### Proposal
+
+Clear and detailed description of the proposal. Consider the following questions:
+
+  - **User Experience**: How does this feature improve the user experience?
+
+  - **Beneficiaries**: Which Lean users and projects benefit most from this feature/change?
+
+  - **Maintainability**: Will this change streamline code maintenance or simplify its structure?
+
+### Community Feedback
+
+Ideas should be discussed on [the Lean Zulip](https://leanprover.zulipchat.com) prior to submitting a proposal. Summarize all prior discussions and link them here.
+
+
+
+[Impact: If others are interested in adding the suggestions from this proposal, ask them to add :+1: to this issue. Add :+1: to [other issues you consider important](https://github.com/leanprover/lean4/issues?q=is%3Aissue+is%3Aopen+sort%3Areactions-%2B1-desc).]