coq
Add CI for spell check and other linters
Following up with https://github.com/coq/platform/pull/173#issuecomment-968280695 and https://github.com/coq/platform/issues/197#issuecomment-1018479798
The linters currently point out some typos etc, see https://github.com/k4rtik/platform/runs/5667821385?check_suite_focus=true#step:4:254 but I have not fixed them in this PR to test the tool's auto PR support for those fixes.
Once this PR is merged, we may want to change VALIDATE_ALL_CODEBASE: true to VALIDATE_ALL_CODEBASE: ${{ github.event_name == 'push' && github.ref == 'refs/heads/main' }} so that CI only tests the new changes.
I have also disabled certain linters that may involve stylistic choices, namely:
DISABLE_LINTERS:
- SPELL_CSPELL
- ACTION_ACTIONLINT
- BASH_SHELLCHECK
- C_CPPLINT
- BASH_SHFMT
- MARKDOWN_MARKDOWNLINT
I will let you decide about enabling them.
Lo, it ran but needs permission to create a PR:
Identified PR#231 from environment [GitHub Comment Reporter] Unable to post pull request comment: 403 {"message": "Resource not accessible by integration", "documentation_url": "https://docs.github.com/rest/reference/issues#create-an-issue-comment"}. To enable this function, please :
- Create a Personal Access Token (https://docs.github.com/en/free-pro-team@latest/github/authenticating-to-github/creating-a-personal-access-token)
- Create a secret named PAT with its value on your repository (https://docs.github.com/en/free-pro-team@latest/actions/reference/encrypted-secrets#creating-encrypted-secrets-for-a-repository)3. Define PAT={{secrets.PAT}} in your GitHub action environment variables
@k4rtik : thanks I appreciate it - I belong to those people who have difficulties with languages which don't come with compilers.
I will take care of the access token.
@k4rtik : is there a way to avoid the chmod of the files in the shell-scripts folder? None of these files is intended to be called directly - they are all intended to be sourced. So the access mode 644 is intentional and a 755 mode would be more confusing than helpful.
Another issue is that issues in the auto generated Readme files should be flagged, but not corrected. All errors in auto generated files must be fixed somewhere else.
I added the secret, but it didn't do anything I guess because in the PR all changes are already fixed. So I guess to test the PR I need to undo all these changes?
@k4rtik : a last comment - can you please factor out the suggested changed from the CI procedure? The CI procedure I am happy to merge as is, but most of the suggested changes not.
@k4rtik : is there a way to avoid the chmod of the files in the shell-scripts folder? None of these files is intended to be called directly - they are all intended to be sourced. So the access mode 644 is intentional and a 755 mode would be more confusing than helpful.
Yes, pushing this change. Sorry about the confusion.
Another issue is that issues in the auto generated Readme files should be flagged, but not corrected. All errors in auto generated files must be fixed somewhere else.
They seem flagged, but there is still some permissions issue, see the error:
[GitHub Status Reporter] Error posting Status for MARKDOWNwith markdown-table-formatter: 401
GitHub API response: {"message":"Bad credentials","documentation_url":"https://docs.github.com/rest"}
[Text Reporter] Generated TEXT report: /github/workspace/report/linters_logs/SUCCESS-MARKDOWN_MARKDOWN_TABLE_FORMATTER.log
I think this might be because of the change you made at https://github.com/coq/platform/pull/231/commits/64269d4c0b5674c0d5ab7986ae196b20995f260d#diff-206ce5348d308a71dab8cdc132d6dc2babebc80b94a707a45a744909ed9367d4L44
- GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+ GITHUB_TOKEN: ${{ secrets.PAT_LINT_SPELL }}
According to the doc, this does not need to be touched. "GITHUB_TOKEN" is automatically set by GitHub.
I added the secret, but it didn't do anything I guess because in the PR all changes are already fixed. So I guess to test the PR I need to undo all these changes?
I think this will also require that the correct GITHUB_TOKEN is passed. I am reverting that small change. The changes are not in the PR. :)
can you please factor out the suggested changed from the CI procedure? The CI procedure I am happy to merge as is, but most of the suggested changes not.
To be clear, the only suggested changes that I included in the PR were file permissions, and those that could not be fixed automatically such as bad links/were leading to false positives such as _CoqProject. I took another look but there is nothing else to factor out.
We can decide about keeping automatic fixing of suggestions once we test this feature out.
@k4rtik : thanks:
regarding factoring: I want to strictly separate the CI procedure as such (I would think 2 files) and any changes it produces. E.g. the link changes in the .MD files should also be done differently (by creating a new section which covers the two). But any way, introducing these checks in CI and actually fixing them should be separate, independent steps.
P.S.: Please abort the main CI processes when you do changes - for this PR only the new CI step needs to run.
Hi @MSoegtropIMC can you manually cancel these platform CI runs, ie, all except the Megalinter one? As it may not get queued until much later.
Is there a way for me to abort them? I don't think I have permission.
Or did you mean to disable them while making the PR?
Ah I forgot that you don't have permission for this. I think it is better then to disable them for the PR - I will then piggy back the PR and reenable it before I merge.
Hi @MSoegtropIMC
I am getting this error with my latest change:
Error: Input required and not supplied: token
Can you please double-check if the personal access token you created is called PAT_LINT_SPELL?
Unsure what's happening here.
@k4rtik : can you please do the requested changes - or alternatively remove the ReadMe files from the commit.
Also can you please change the bad charter link in [maintainer_scripts/create_readme.sh] - I think this should go together with the same change in the auto generated files.
I will then take it from there - I guess this will run only on main (which I think is good enough).
AFAIK the secrets are not available in PRs from forks.
In that case let me try testing these features on my fork directly and then I will send a PR later.