search

rzk-lang / sHoTT

Formalisations for simplicial HoTT and synthetic ∞-categories.
https://rzk-lang.github.io/sHoTT/
44 stars 12 forks source link

Error instead of commit on bad format #97

Closed fredrik-bakke closed 1 year ago

fredrik-bakke commented 1 year ago

Turns out it's not as easy as expected to set up invisible autoformatting. Thus, instead, this PR makes it so the workflow just blocks ill-formatted PRs. Contributors will then have to install an autoformatter (e.g. Prettier) locally to fix the issue.

emilyriehl commented 1 year ago

Hi @fizruk @fredrik-bakke I've lost track of what's up with autoformating. Now whenever I merge something I'm getting an error message about autoformating failure. Can someone explain the current status?

fredrik-bakke commented 1 year ago

Hi, the error can be safely ignored. The workflow is just not set up properly.

fredrik-bakke commented 1 year ago

This pr makes it so other prs are blocked until they are properly formatted. The recommended procedure should then be for contributors to set up autoformatting in their ide. Given that you agree we should have this feature/rule of course.

fredrik-bakke commented 1 year ago

Currently I think it is a good idea to wait until there are few other prs in the pipeline to merge this, so people aren't surprised by it and get weird merge conflicts.

fizruk commented 1 year ago

Hi @fizruk @fredrik-bakke I've lost track of what's up with autoformating. Now whenever I merge something I'm getting an error message about autoformating failure. Can someone explain the current status?

  1. Currently we have an autoformatting workflow, but it always fails because it does not have proper permissions to modify main branch`.
  2. The error is benign and can be safely ignored, as @fredrik-bakke mentioned.
  3. This PR changes the behaviour of the workflow: instead of autoformatting and committing to main (modifying the code), the workflow will now only check if formatting is correct and issue (which we can check for incoming PRs and ask contributors to apply autoformatting to the modified files before merging their changes)
  4. If the workflow error (and emails about it) are too bothering, we could disable the workflow (just remove the .github/workflows/format.yml file) until this PR is merged. But I think, this should just be merged soon.
  5. To merge this PR, it is a good idea to merge currently open PRs first (as @fredrik-bakke mentioned, otherwise, contributors might have unpleasant conflicts to resolve locally). Otherwise, I think we could help update PRs that will have conflicts after merging this one.

Note that here we only talk about formatting of config files and text in Markdown (including *.rzk.md), but not Rzk code.

fizruk commented 1 year ago

@fredrik-bakke can you please update/fix the formatting (I have updated the branch, and it needs some formatting now)?

@fredrik-bakke @emilyriehl I suggest that we merge this before #103 (which supersedes #100) and help @cesarbm03 with his PR in case of conflicts.

fredrik-bakke commented 1 year ago

I'll be at my computer in a couple of hours. I can fix it then

fredrik-bakke commented 1 year ago

Okay, this one should be ready for merging again now. Apologies if this has caused problems for anyone. In #94, I'm adding a remark to the documentation that we enforce autoformatting rules and that contributors should install an autoformatter.