Print minimal files in import tree in CI (#10)

This PR adds a CI step that prints the names of all `sorry`-free files in the `LeanCamCombi` source directory (except those under `ExampleSheets`) whose list of imports does not contain any import from `LeanCamCombi`. These files are good candidates to be upstreamed to mathlib.

.github/workflows/push_main.yml

@@ -21,6 +21,13 @@ jobs:
         with:
           fetch-depth: 0
 
+      - name: print files to upstream
+        run: |
+          grep -r --exclude-dir=ExampleSheets --files-without-match 'import LeanCamCombi' LeanCamCombi | sort > 1.txt
+          grep -r --exclude-dir=ExampleSheets --files-with-match 'sorry' LeanCamCombi | sort > 2.txt
+          comm -23 1.txt 2.txt | sed -e 's/^\(.*\)$/- [`\1`](https:\/\/github.com\/YaelDillies\/LeanCamCombi\/blob\/main\/\1)/' > docs/_includes/files_to_upstream.md
+          rm 1.txt 2.txt
+
       - name: install elan
         run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.0.0
 

docs/.gitignore

@@ -6,3 +6,6 @@ vendor
 blueprint/
 blueprint.pdf
 docs/
+
+# Noisy files that are generated by CI.
+_includes/files_to_upstream.md

docs/index.md

@@ -17,6 +17,10 @@ The project is not yet finished. The following table details live which files ar
 
 {% include sorries.md %}
 
+## Files to upstream to mathlib
+
+{% include files_to_upstream.md %}
+
 ## The source
 
 The definitions, theorems and proofs in this repository are taken from three Cambridge courses: