Skip to content

CI check for committing files in .gitignore#11346

Merged
shindere merged 1 commit intoocaml:trunkfrom
dra27:commit-ignored
Dec 23, 2022
Merged

CI check for committing files in .gitignore#11346
shindere merged 1 commit intoocaml:trunkfrom
dra27:commit-ignored

Conversation

@dra27
Copy link
Copy Markdown
Member

@dra27 dra27 commented Jun 22, 2022

This is a follow-on for #11343: if we stop committing configure, we should ensure that it doesn't accidentally (or nefariously) get recommitted.

There was one place in the testsuite where we commit a broken .cmi file which I've worked-around by using copy and there are .gitignore files in the manual's directories which had incorrect patterns.

An example of this test failing can be seen at https://github.com/dra27/ocaml/runs/7002042376?check_suite_focus=true#step:6:8.

@dra27
Copy link
Copy Markdown
Member Author

dra27 commented Jun 22, 2022

It's possible to add an ignored file by using git add -f, however, I think the most likely way that a configure script would leak in would be from a cherry-pick or a rebase of an existing patch.

@dra27 dra27 force-pushed the commit-ignored branch 2 times, most recently from 545b9d3 to 0a48b2f Compare July 30, 2022 09:50
@shindere
Copy link
Copy Markdown
Contributor

shindere commented Oct 11, 2022 via email

@dra27
Copy link
Copy Markdown
Member Author

dra27 commented Oct 11, 2022

It would seem a better alternative to me to melt all the .gitignore files in the toplevel one, ven those of the manual. What do you think?

I agree, the prefixing forward-slashes look very strange! I think I reviewed the original PR for that change and didn't notice the problem then, either.

I'd certainly see no problem with either merging all the .gitignore files under manual/ into manual/.gitignore (if we are still trying to keep the manual/ tree semi-independent of the rest of the tree, @Octachron?) or just merging all the files into the root .gitignore.

@Octachron
Copy link
Copy Markdown
Member

I am fine with both merging the .gitignore rule in the manual or moving them, prefixed by manual/ in the root .gitignore. Both variants seem quite similar to me.

@dra27
Copy link
Copy Markdown
Member Author

dra27 commented Oct 14, 2022

Rebased to remove the commits now subsumed by #11617. If we do go ahead with #11343 (and stop committing the configure script by default) then I think we should definitely have this CI check - git add configure will warn that the file isn't supposed to be added (it can be overridden with -f) but git cherry-pick or git rebase (i.e. for any existing work) doesn't carry out this check, so I think there's potential for the file to be accidentally included in a PR.

That said, this could be merged now and we can have the check regardless.

@shindere
Copy link
Copy Markdown
Contributor

shindere commented Oct 18, 2022 via email

@dra27
Copy link
Copy Markdown
Member Author

dra27 commented Dec 14, 2022

Oops, I seem to have dropped this one:

Suggestion: Check no ignored files committed: how about using singular (file) rather than plural (files) andadding "is" before committed?

Agree with having a sentence, but not with making it singular (I think it reads too pedantically, even for me!). I changed the message to match the commit message that it's just "Check that no ignored files have been committed"

Question: wouldn't it be worth adding this check to the pre-commit hook? If that's being done, am I correct that the addition of an ignored file oculd be caught during a cherry-pick or a rebase?

The pre-commit hooks aren't run during cherry-pick or rebase, sadly.

@shindere
Copy link
Copy Markdown
Contributor

shindere commented Dec 19, 2022 via email

@dra27
Copy link
Copy Markdown
Member Author

dra27 commented Dec 22, 2022

As a last suggestion, which is slightly orthogonal to the previous one, I'd like to suggest to isolate the test in its own script under tools/ to make it easier to invoke it from several places, rather than having the logic embedded in only one file from which it can't be re-used.

Good idea! Done as tools/ci/actions/check-no-ignored-files.sh

@shindere
Copy link
Copy Markdown
Contributor

shindere commented Dec 23, 2022 via email

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