rzk-lang / sHoTT

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

Add autoformatting to CI (for Markdown, YAML, JSON) #95

Closed fredrik-bakke closed 1 year ago

fredrik-bakke commented 1 year ago

If I didn't mess this up, it will autoformat markdown (and json and yaml) files according to our settings in .prettierrc.json on commits to the main branch, i.e. when merging pull requests.

fredrik-bakke commented 1 year ago

In the Rzk workflow, we currently explicitly pass the files that are checked:

      - name: Check all files
        uses: rzk-lang/rzk-action@v1
        with:
          rzk-version: latest
          # rzk-version: v0.4.1.1   # example of a specific version
          files: src/hott/* src/simplicial-hott/*

Has this action been updated to be able to recognize that there is an rzk.yml file in the root so we can use that instead, @fizruk?

EDIT: I made a pull request: https://github.com/rzk-lang/rzk-action/pull/3 :)

fizruk commented 1 year ago

I've updated the title of the PR, since I originally thought this will autoformat Rzk code somehow.

fredrik-bakke commented 1 year ago

Thanks! I wish...

fizruk commented 1 year ago

Thanks! I wish...

I think it should not be too difficult to implement most of the styleguide in a pretty-printer/autoformatter in rzk itself, and making it available via the VS Code extension. I think even some checks for the naming conventions can be automated. We'll look into that at some point, I think. But probably not in October :)

fizruk commented 1 year ago

I'm not sure how autoformatting after this is merged will affect current PRs. Perhaps, we should merge #93 first, then this.

fredrik-bakke commented 1 year ago

There's no rush, but it should minimally affect PRs. The workflow only activates on commits to the main branch, i.e. after the PR is merged. It is also configured only to autoformat files touched by the relevant PR.

fizruk commented 1 year ago

The workflow only activates on commits to the main branch, i.e. after the PR is merged.

Isn't it activated on the merge commit that happens when we merge this PR?

fredrik-bakke commented 1 year ago

I assume it does, but this PR doesn't touch any of the files that the other PR touches.

fredrik-bakke commented 1 year ago

This is of course assuming the workflow is set up properly.

emilyriehl commented 1 year ago

I don't entirely understand what is going on here so I'll leave it for you to decide :)

fredrik-bakke commented 1 year ago

This is of course assuming the workflow is set up properly.

Turns out I didn't 🙃

fizruk commented 1 year ago

@fredrik-bakke you can create a separate branch and test it out in it. You should have Write access to create new branches in this repo directly, instead of using a fork.

fredrik-bakke commented 1 year ago

Ah, thanks! Yep, this wasn't the best approach

fredrik-bakke commented 1 year ago

Turns out the workflow needs a github token with write access, but I don't think I have the privilege to generate those

fizruk commented 1 year ago

@fredrik-bakke you should be able to just add something like the following to the job in the workflow file:

  permissions:
    contents: write

For example, see https://github.com/rzk-lang/rzk/blob/530666653a308a131da9225f7f9426d1b0a65a3b/.github/workflows/mkdocs.yml#L13-L14

fredrik-bakke commented 1 year ago

Ah, wow, thanks! That seems to have fixed it. I made a new pull request #96.