-
Notifications
You must be signed in to change notification settings - Fork 259
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - chore: ensure all instances referred to directly have explicit names #6423
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks 🎉
bors merge
bors r- bors d+ |
✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with |
…6423) Per leanprover/lean4#2343, we are going to need to change the automatic generation of instance names, as they become too long. This PR ensures that everywhere in Mathlib that refers to an instance by name, that name is given explicitly, rather than being automatically generated. There are four exceptions, which are now commented, with links to leanprover/lean4#2343. This was implemented by running Mathlib against a modified Lean that appended `_ᾰ` to all automatically generated names, and fixing everything. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Canceled. |
bors merge |
…6423) Per leanprover/lean4#2343, we are going to need to change the automatic generation of instance names, as they become too long. This PR ensures that everywhere in Mathlib that refers to an instance by name, that name is given explicitly, rather than being automatically generated. There are four exceptions, which are now commented, with links to leanprover/lean4#2343. This was implemented by running Mathlib against a modified Lean that appended `_ᾰ` to all automatically generated names, and fixing everything. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Build failed (retrying...): |
…6423) Per leanprover/lean4#2343, we are going to need to change the automatic generation of instance names, as they become too long. This PR ensures that everywhere in Mathlib that refers to an instance by name, that name is given explicitly, rather than being automatically generated. There are four exceptions, which are now commented, with links to leanprover/lean4#2343. This was implemented by running Mathlib against a modified Lean that appended `_ᾰ` to all automatically generated names, and fixing everything. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
My PR #6423 modified the lakefile to point to a branch of the `Qq` library, but this had only been necessary during my local testing against a patched version of Lean. I should not have committed this change, and we should not have merged it to `master`. It's harmless, I think, but should be reverted asap. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
…6423) Per leanprover/lean4#2343, we are going to need to change the automatic generation of instance names, as they become too long. This PR ensures that everywhere in Mathlib that refers to an instance by name, that name is given explicitly, rather than being automatically generated. There are four exceptions, which are now commented, with links to leanprover/lean4#2343. This was implemented by running Mathlib against a modified Lean that appended `_ᾰ` to all automatically generated names, and fixing everything. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
My PR #6423 modified the lakefile to point to a branch of the `Qq` library, but this had only been necessary during my local testing against a patched version of Lean. I should not have committed this change, and we should not have merged it to `master`. It's harmless, I think, but should be reverted asap. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
My PR #6423 modified the lakefile to point to a branch of the `Qq` library, but this had only been necessary during my local testing against a patched version of Lean. I should not have committed this change, and we should not have merged it to `master`. It's harmless, I think, but should be reverted asap. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
…6423) Per leanprover/lean4#2343, we are going to need to change the automatic generation of instance names, as they become too long. This PR ensures that everywhere in Mathlib that refers to an instance by name, that name is given explicitly, rather than being automatically generated. There are four exceptions, which are now commented, with links to leanprover/lean4#2343. This was implemented by running Mathlib against a modified Lean that appended `_ᾰ` to all automatically generated names, and fixing everything. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
My PR #6423 modified the lakefile to point to a branch of the `Qq` library, but this had only been necessary during my local testing against a patched version of Lean. I should not have committed this change, and we should not have merged it to `master`. It's harmless, I think, but should be reverted asap. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
My PR #6423 modified the lakefile to point to a branch of the `Qq` library, but this had only been necessary during my local testing against a patched version of Lean. I should not have committed this change, and we should not have merged it to `master`. It's harmless, I think, but should be reverted asap. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Per leanprover/lean4#2343, we are going to need to change the automatic generation of instance names, as they become too long.
This PR ensures that everywhere in Mathlib that refers to an instance by name, that name is given explicitly, rather than being automatically generated.
There are four exceptions, which are now commented, with links to leanprover/lean4#2343.
This was implemented by running Mathlib against a modified Lean that appended
_ᾰ
to all automatically generated names, and fixing everything.