-
Notifications
You must be signed in to change notification settings - Fork 52
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
chore: issue templates similar to lean4 repo
- Loading branch information
Showing
2 changed files
with
66 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,40 @@ | ||
--- | ||
name: Bug report | ||
about: Create a bug report | ||
title: '' | ||
labels: bug | ||
assignees: '' | ||
|
||
--- | ||
|
||
### 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] | ||
|
||
### Versions | ||
|
||
[Version of vscode-lean4 (Hover over 'lean4' in the 'Extensions' menu)] | ||
[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 | ||
|
||
Add :+1: to [issues you consider important](https://github.com/leanprover/vscode-lean4/issues?q=is%3Aissue+is%3Aopen+sort%3Areactions-%2B1-desc). If others are impacted by this issue, please ask them to add :+1: to it. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 | ||
|
||
Add :+1: to [issues you consider important](https://github.com/leanprover/vscode-lean4/issues?q=is%3Aissue+is%3Aopen+sort%3Areactions-%2B1-desc). If others benefit from the changes in this proposal being added, please ask them to add :+1: to it. |