Skip to content
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.

Sign up for GitHub

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

Jump to bottom

Make pre-commit hooks talk to git #851

Merged
merged 20 commits into from
Nov 26, 2023
Merged

Make pre-commit hooks talk to git #851

merged 20 commits into from
Nov 26, 2023

Conversation

fredrik-bakke
Copy link
Collaborator

@fredrik-bakke fredrik-bakke commented Oct 16, 2023 •
edited
Loading

Resolves #664
Resolves #848

VojtechStep
VojtechStep reviewed Oct 16, 2023
View reviewed changes
Copy link
Collaborator

@VojtechStep VojtechStep left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think the implementation will require a bit more fiddling to get right, because we traded one class of bugs (including untracked files) for another (including unstaged deleted/renamed files).

scripts/generate_namespace_index_modules.py Show resolved Hide resolved
scripts/generate_main_index_file.py Outdated Show resolved Hide resolved
scripts/utils/__init__.py Show resolved Hide resolved
@fredrik-bakke
Copy link
Collaborator Author

Thanks for the comments, and sorry for my messy python code. For some reason, my patience grows really thin whenever I have to touch it.

@fredrik-bakke fredrik-bakke marked this pull request as draft October 17, 2023 20:43
@fredrik-bakke
Copy link
Collaborator Author

@VojtechStep If I recall correctly, you argued somewhere that this change in some sense trades one bug for another, and although both versions have their drawbacks, this PR at least makes the hooks consistent with each other, which I think is an overall improvement.

@fredrik-bakke fredrik-bakke marked this pull request as ready for review November 24, 2023 17:18
@fredrik-bakke fredrik-bakke marked this pull request as draft November 24, 2023 18:12
@fredrik-bakke
Copy link
Collaborator Author

Ah, never mind, this one's still unfinished.

VojtechStep
VojtechStep requested changes Nov 24, 2023
View reviewed changes
Copy link
Collaborator

@VojtechStep VojtechStep left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think it's OK to have the new behavior, and I think it's adequately documented. However the script itself doesn't really work and I get an "empty" SUMMARY.md, so that needs to be addressed; I left a comment on why it breaks.

CONTRIBUTING.md Outdated Show resolved Hide resolved
CONTRIBUTING.md Outdated Show resolved Hide resolved
CONTRIBUTING.md Outdated Show resolved Hide resolved
scripts/generate_main_index_file.py Outdated Show resolved Hide resolved
scripts/generate_main_index_file.py Outdated Show resolved Hide resolved
scripts/generate_main_index_file.py Outdated Show resolved Hide resolved
@fredrik-bakke fredrik-bakke marked this pull request as ready for review November 26, 2023 17:33
@fredrik-bakke
Copy link
Collaborator Author

I think I've adequately addressed all of your comments now, @VojtechStep. Thank you for your invaluable guidance, and let me know if there is anything more you think should be changed.
By the way, I think you deserve co-authorship over this PR, if you are comfortable with having your name on it.

VojtechStep
VojtechStep approved these changes Nov 26, 2023
View reviewed changes
Copy link
Collaborator

@VojtechStep VojtechStep left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks great! Thanks for taking the time to look into this. I'll be adding myself as a coauthor in the squashed commit then.

@VojtechStep VojtechStep merged commit 7de16af into UniMath:master Nov 26, 2023
4 checks passed
@fredrik-bakke fredrik-bakke deleted the pre-commit branch November 26, 2023 20:16
fredrik-bakke added a commit to fredrik-bakke/agda-unimath that referenced this pull request Nov 29, 2023
@fredrik-bakke @VojtechStep
Make pre-commit hooks talk to git (UniMath#851)
8934fbf 
Resolves UniMath#664
Resolves UniMath#848

Co-authored-by: Vojtěch Štěpančík <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@EgbertRijke EgbertRijke EgbertRijke left review comments

@VojtechStep VojtechStep VojtechStep approved these changes

Assignees
No one assigned
Labels
fix pre-commit
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Generate index files based only on tracked files Pre-commit hooks should ignore all junk files
3 participants
@fredrik-bakke @EgbertRijke @VojtechStep