Skip to content

chore(how-to-contribute): remove portion about (re)moving declarations#849

Open
grunweg wants to merge 1 commit into
leanprover-community:lean4from
grunweg:remove-move
Open

chore(how-to-contribute): remove portion about (re)moving declarations#849
grunweg wants to merge 1 commit into
leanprover-community:lean4from
grunweg:remove-move

Conversation

@grunweg
Copy link
Copy Markdown
Contributor

@grunweg grunweg commented May 22, 2026

from the PR description. This clogs up the template and has not been used in practice at all. In the future, semantic diffing will provide this information.

from the PR description. This clogs up the template and has not been used
in practice at all. In the future, semantic diffing will provide this information.
@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented May 22, 2026

Needs discussion about reviewers first: there was support in-person at the MI retreat.

@grunweg grunweg requested a review from b-mehta May 22, 2026 21:15
@faenuccio
Copy link
Copy Markdown
Contributor

Needs discussion about reviewers first: there was support in-person at the MI retreat.

What do you mean? That this PR is actually on hold?

@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented May 23, 2026

Perhaps I meant "I want to ask more reviewers for their opinion". What do you think? This changes written policy, although one we hardly ever followed.

@b-mehta
Copy link
Copy Markdown
Contributor

b-mehta commented May 23, 2026

I'm not sure about this, I find the "moves" section helpful to read and particularly helpful in the changelog.

@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented May 23, 2026

As discussed in person: a solution satisfying both needs could be to have a Lean-aware declarations diff (and then remove this portion of the PR message as it would be redundant). @adomani worked on Lean-aware declarations diff and thinks it's doable --- I think it would be great to have!

@faenuccio
Copy link
Copy Markdown
Contributor

Perhaps I meant "I want to ask more reviewers for their opinion". What do you think? This changes written policy, although one we hardly ever followed.

I realise I don't have a strong opinion and I'm happy to delegate the group of people who seem to be actively discussing this.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants