Merge pull request #5 from rzk-lang/formatting-support

Formatting support
rzk-lang · Dec 9, 2023 · 9c68e93 · 9c68e93
2 parents 818758c + c521d28
commit 9c68e93
Show file tree

Hide file tree

Showing 4 changed files with 36 additions and 9 deletions.
diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
@@ -13,7 +13,7 @@ jobs:
           - ubuntu-latest
 
         rzk-version:
-          - v0.6.6
+          - v0.7.1
           - latest
 
         files:
@@ -30,6 +30,14 @@ jobs:
         with:
           rzk-version: ${{ matrix.rzk-version }}
           files: ${{ matrix.files }}
+
+      - name: Check formatting only
+        uses: ./
+        with:
+          rzk-version: ${{ matrix.rzk-version }}
+          files: ${{ matrix.files }}
+          typecheck: false
+          check-formatting: true
 
       - name: Check action's output
         shell: bash

diff --git a/README.md b/README.md
@@ -23,11 +23,15 @@ The following example runs `rzk typecheck` on all literate Rzk Markdown files in
 
 ## Inputs
 
-| Name          | Required | Description                                          | Type    | Default                       |
-| ------------- | :------: | ---------------------------------------------------- | ------- | ----------------------------- |
-| `rzk-version` |    No    | `rzk` version to use, ex. `latest` or `v0.5.3`       | string  | `latest`                      |
-| `files`       |    No    | Files to process, ex. `lib/**/*.rzk src/**/*.rzk.md` | string  | Rely on local `rzk.yaml` file |
-| `system-rzk`  |    No    | Use `rzk` executable provided by the system          | boolean | `false`                       |
+| Name               | Required | Description                                          | Type    | Default                       |
+| ------------------ | :------: | ---------------------------------------------------- | ------- | ----------------------------- |
+| `rzk-version`      |    No    | `rzk` version to use, ex. `latest` or `v0.5.3`       | string  | `latest`                      |
+| `files`            |    No    | Files to process, ex. `lib/**/*.rzk src/**/*.rzk.md` | string  | Rely on local `rzk.yaml` file |
+| `system-rzk`       |    No    | Use `rzk` executable provided by the system          | boolean | `false`                       |
+| `typecheck`        |    No    | Typecheck the input files                            | boolean | `true`                        |
+| `check-formatting` |    No    | Check that the input files are well-formatted        | boolean | `false`                       |
+
+It only makes sense to turn off typechecking when checking the formatting.
 
 ## Outputs
 

diff --git a/action.yml b/action.yml
@@ -17,6 +17,14 @@ inputs:
     description: "Files to check (rely on rzk.yaml by default)"
     required: false
     default: ""
+  typecheck:
+    description: "Enable typechecking the files (on by default)"
+    required: false
+    default: true
+  check-formatting:
+    description: "Enable checking the formatting (off by default)"
+    required: false
+    default: false
 
 outputs:
   rzk-version:
@@ -41,7 +49,14 @@ runs:
       run: |
         echo "rzk-version=$(rzk version)" >> $GITHUB_OUTPUT
 
-    - name: 🔨 Check Rzk files
+    - name: 🔨 Check Rzk files definitions
       shell: bash
+      if: ${{ inputs.typecheck == 'true' }}
       run: |
         rzk typecheck ${{ inputs.files }}
+
+    - name: 🔬 Check Rzk files formatting
+      shell: bash
+      if: ${{ inputs.check-formatting == 'true' }}
+      run: |
+        rzk format --check ${{ inputs.files }}
diff --git a/example/1-example.rzk.md b/example/1-example.rzk.md
@@ -8,7 +8,7 @@ Here's a sample definition to typecheck:
 
 ```rzk
 #define modus-ponens
-  (A B : U)
-  : (A → B) → A → B
+  ( A B : U)
+  : ( A → B) → A → B
   := \ f x → f x
 ```