Fix missing sorries.md

.github/workflows/push.yml

@@ -78,6 +78,10 @@ jobs:
       - name: Remove .gitignore for gh-pages
         run: rm docs/.gitignore
 
+      - name: Count sorries
+        run: |
+          python scripts/count_sorry.py
+
       - name: Bundle dependencies
         uses: ruby/setup-ruby@v1
         with:

.gitignore

@@ -13,3 +13,4 @@ src/list_decls.lean
 src/.noisy_files
 /build
 /lake-packages/*
+docs/_includes/sorries.md

scripts/count_sorry.py

@@ -12,7 +12,7 @@ def pretty_file(file: str):
     url = f"https://github.com/YaelDillies/LeanAPAP/blob/master/{file}"
     return f"[{name}]({url})"
 
-files = [file for tree in os.walk("src") for file in glob(os.path.join(tree[0], '*.lean'))]
+files = [file for tree in os.walk("LeanAPAP") for file in glob(os.path.join(tree[0], '*.lean'))]
 sorries = {}
 
 for file in files: