chore: word count reports in CI (#35)

leanprover · Sep 11, 2024 · bab544a · bab544a
1 parent 57e9c52
commit bab544a
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 3 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -50,7 +50,21 @@ jobs:
 
       - name: Generate HTML
         run: |
-          lake exe generate-manual --depth 2
+          lake exe generate-manual --depth 2 --with-word-count "words.txt"
+
+      - name: Report word count
+        run: |
+          echo "Word Counts"
+          echo "-----------"
+          cat words.txt
+
+      - name: Save word count
+        run: |
+          echo "# Word Counts" >> $GITHUB_STEP_SUMMARY
+          echo "" >> $GITHUB_STEP_SUMMARY
+          echo "\`\`\`" >> $GITHUB_STEP_SUMMARY
+          cat words.txt >> $GITHUB_STEP_SUMMARY
+          echo "\`\`\`" >> $GITHUB_STEP_SUMMARY
 
       - name: Offline link checker
         uses: lycheeverse/[email protected]

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "84302ae695e0e3b21f1f0ad24b5420b12ee1312c",
+   "rev": "82bdbe1dbb4df2e666e9a62d7f1302ac5cc23768",
    "name": "subverso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "099f82f9faa3f550f242df55dbacba160bf86fa4",
+   "rev": "04444b853eeacdde5392dc37488a1e6e6dd90acb",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",