Miscellaneous refactoring and small additions (#579)

### Highlights - Rename the binary operator for the wedge of pointed types from `_∨_` to `_∨*_`. - Add binary operator notation for the following - propositional disjunction `_∨_` - propositional conjunction `_∧_` - pointed homotopy `_~*_` - pointed function composition `_∘*_` - addition on natural numbers `_+ℕ_` - Define pointed cartesian product `_×*_` and pointed dependent sum `Σ*` (we could similarly add the notation `Π*`) - Cleanup of sign homomorphism delooping files (I don't know what's wrong with me, but please see questions below) - Rename `cone-pullbacks` to `cones-over-cospans`, and `cocone-pushouts` to `cocones-under-spans`, as this more closely represents what the files contain - Define pullback cones - Define preidempotent maps - Eradicate use of `i j k` for universe levels - Disambiguate Precat definitions from type definitions - Add `pre-commit` check for issue discussed in #573 - Add `generate-main-index-file` to `pre-commit`, resolves #552 - Print errors to `sys.stderr`. #532 may be fixed by this - Better `pre-commit` hook ordering - Fix a couple of mistakes in the Makefile - Remove unused imports - Fully capitalize the name of the universe of decidable propositions `Decidable-Prop` - Add `imports` task that minimizes module imports, and add details to all the tasks. Sorry for the mess!
UniMath · Apr 28, 2023 · e2100fb · e2100fb
1 parent f96ac15
commit e2100fb
Show file tree

Hide file tree

Showing 228 changed files with 4,157 additions and 4,084 deletions.
diff --git a/.pre-commit-config.yaml b/.pre-commit-config.yaml
@@ -10,19 +10,6 @@ repos:
       - id: check-case-conflict
       - id: check-merge-conflict
 
-  - repo: https://github.com/pre-commit/mirrors-autopep8
-    rev: "v2.0.2"
-    hooks:
-      - id: autopep8
-        name: Python scripts formatting
-
-  - repo: https://github.com/pre-commit/mirrors-prettier
-    rev: "v3.0.0-alpha.6"
-    hooks:
-      - id: prettier
-        name: CSS, JS, YAML and Markdown (no codeblocks) formatting
-        types_or: [css, javascript, yaml, markdown]
-
   - repo: local
     hooks:
       - id: remove-extra-blank-lines
@@ -57,6 +44,16 @@ repos:
         args: []
         require_serial: false
 
+      - id: generate-main-index-file
+        name: Generate main index file
+        entry: scripts/generate_main_index_file.py
+        language: python
+        always_run: true
+        verbose: true
+        types_or: [markdown, text]
+        args: []
+        require_serial: false
+
       - id: max-line-length
         name: Check the maximum line length is respected
         entry: scripts/max_line_length.py
@@ -66,6 +63,19 @@ repos:
         types_or: [markdown, text]
         require_serial: false
 
+  - repo: https://github.com/pre-commit/mirrors-autopep8
+    rev: "v2.0.2"
+    hooks:
+      - id: autopep8
+        name: Python scripts formatting
+
+  - repo: https://github.com/pre-commit/mirrors-prettier
+    rev: "v3.0.0-alpha.6"
+    hooks:
+      - id: prettier
+        name: CSS, JS, YAML and Markdown (no codeblocks) formatting
+        types_or: [css, javascript, yaml, markdown]
+
       # Experimental hooks
 
       # - id: spaces-convention

diff --git a/.vscode/extensions.json b/.vscode/extensions.json
@@ -2,12 +2,12 @@
   "recommendations": [
     "banacorn.agda-mode",
     "bbenoist.nix",
-    "ms-python.python",
-    "ms-python.vscode-pylance",
+    "dbankier.vscode-quick-select",
     "eamodio.gitlens",
     "esbenp.prettier-vscode",
-    "dbankier.vscode-quick-select",
+    "fredrikbakke.agda-syntax",
     "github.vscode-pull-request-github",
-    "fredrikbakke.agda-syntax"
+    "ms-python.python",
+    "ms-python.vscode-pylance"
   ]
 }
diff --git a/.vscode/settings.json b/.vscode/settings.json
@@ -11,9 +11,6 @@
   },
 
   // Snippet setup
-  "editor.quickSuggestions": {
-    "other": "inline"
-  },
   "editor.snippetSuggestions": "top",
   "editor.wordBasedSuggestions": false,
   "javascript.suggest.names": false,
@@ -36,6 +33,9 @@
     "editor.rulers": [80],
     "editor.formatOnType": true,
     "editor.formatOnSave": true,
+    "editor.quickSuggestions": {
+      "other": "inline"
+    },
     "editor.autoClosingBrackets": "never"
   },
   "[css]": {
@@ -60,6 +60,9 @@
   "[markdown]": {
     "editor.tabSize": 2,
     "editor.rulers": [80],
+    "editor.quickSuggestions": {
+      "other": "inline"
+    },
     "editor.autoClosingBrackets": "never"
   },
   "[python]": {

diff --git a/.vscode/tasks.json b/.vscode/tasks.json
@@ -3,14 +3,25 @@
   "tasks": [
     {
       "label": "check",
+      "detail": "Typecheck the entire library.",
       "type": "shell",
-      "command": "make check",
+      "command": "make",
+      "args": ["check"],
       "problemMatcher": []
     },
     {
       "label": "pre-commit",
+      "detail": "Quality assurance for the library.",
       "type": "shell",
-      "command": "make pre-commit",
+      "command": "make",
+      "args": ["pre-commit"],
+      "problemMatcher": []
+    },
+    {
+      "label": "imports",
+      "detail": "Search for and remove unused imports. Warning: very slow!",
+      "type": "shell",
+      "command": "python scripts/demote_foundation_imports.py && python scripts/remove_unused_imports.py",
       "problemMatcher": []
     }
   ]

diff --git a/Makefile b/Makefile
@@ -56,7 +56,7 @@ AGDAMDFILES: $(AGDAMDFILES)
 
 docs/%.md: src/%.lagda.md
 	@echo "... $@"
-	@${AGDA} ${AGDAHTMLFLAfoGS} $<
+	@${AGDA} ${AGDAHTMLFLAGS} $<
 
 agda-html: src/everything.lagda.md
 	@rm -rf docs/
@@ -72,7 +72,7 @@ website: agda-html \
 	@cp $(METAFILES) docs/
 	@mdbook build
 
-.phony: serve-website
+.PHONY: serve-website
 serve-website:
 	@mdbook serve -p 8080 --open -d ./book/html
 

diff --git a/scripts/demote_foundation_imports.py b/scripts/demote_foundation_imports.py
@@ -105,7 +105,7 @@ def process_agda_file(agda_file, agda_options, root, temp_dir):
                 file.write(content)
 
             utils.multithread.thread_safe_print(
-                f"'{agda_module}' ERROR! The temporary file '{temp_file} typechecked with imports {removed_imports} removed, but not the actual file '{agda_file}'. Please report this.")
+                f"'{agda_module}' ERROR! The temporary file '{temp_file} typechecked with imports {removed_imports} removed, but not the actual file '{agda_file}'. Please report this.", file=sys.stderr)
             return
 
         utils.multithread.thread_safe_print(

diff --git a/scripts/fix_imports.py b/scripts/fix_imports.py
@@ -34,7 +34,7 @@ def categorize_imports(block):
         if l.startswith('module') or l.startswith('{-# OPTIONS'):
             print(
                 'Error: module decl./pragmas can not be in the details import block\n\
-                Please put it in the first Agda block after the first header:\n\t' + str(fpath))
+                Please put it in the first Agda block after the first header:\n\t' + str(fpath), file=sys.stderr)
             sys.exit(1)
         elif 'open import' in l:
             if l.endswith('public'):
@@ -44,10 +44,11 @@ def categorize_imports(block):
         elif 'open' in l:
             openStatements.append(l)
         else:
-            print('Error: unknown statement in details import block:\n\t' + str(fpath))
+            print('Error: unknown statement in details import block:\n\t' +
+                  str(fpath), file=sys.stderr)
     if len(openStatements) > 0:
         print(
-            'Warning: Please review the imports block, it contains non-import statements:\n\t' + str(fpath))
+            'Warning: Please review the imports block, it contains non-import statements:\n\t' + str(fpath), file=sys.stderr)
 
     return (publicImports, nonPublicImports, openStatements)
 
@@ -130,7 +131,7 @@ def prettify_imports_block(block):
             agdaBlockStart = utils.find_index(contents, '```agda')
             if len(agdaBlockStart) > 1:
                 print(
-                    'Warning: No Agda import block found inside <details> block in:\n\t' + str(fpath))
+                    'Warning: No Agda import block found inside <details> block in:\n\t' + str(fpath), file=sys.stderr)
                 status |= 1  # Flag
             continue
 

diff --git a/scripts/generate_main_index_file.py b/scripts/generate_main_index_file.py
@@ -15,20 +15,23 @@
 
 def generate_namespace_entry_list(namespace):
     status = 0
+
     file_names = sorted(os.listdir(os.path.join(root, namespace)))
     file_paths = map(lambda m: pathlib.Path(
         os.path.join(root, namespace, m)), file_names)
     lagda_file_paths = tuple(filter(utils.is_agda_file, file_paths))
     modules = tuple(map(lambda p: p.name, lagda_file_paths))
-    module_titles = tuple(map(utils.get_lagda_file_title, lagda_file_paths))
+    module_titles = tuple(map(utils.get_lagda_md_file_title, lagda_file_paths))
+
     module_mdfiles = tuple(
         map(lambda m: utils.get_module_mdfile(namespace, m), modules))
 
     # Check for missing titles
     for title, module in zip(module_titles, modules):
         if title is None:
             status |= STATUS_FLAG_NO_TITLE
-            print(f"WARNING! {namespace}.{module} no title was found")
+            print(
+                f"WARNING! {namespace}.{module} no title was found", file=sys.stderr)
 
     # Check duplicate titles
     equal_titles = utils.get_equivalence_classes(
@@ -38,18 +41,18 @@ def generate_namespace_entry_list(namespace):
 
     if (len(equal_titles) > 0):
         status |= STATUS_FLAG_DUPLICATE_TITLE
-        print(f"WARNING! Duplicate titles in {namespace}:")
+        print(f"WARNING! Duplicate titles in {namespace}:", file=sys.stderr)
         for ec in equal_titles:
             print(
-                f"  Title '{ec[0][0]}': {', '.join(m[1][:m[1].rfind('.lagda.md')] for m in ec)}")
+                f"  Title '{ec[0][0]}': {', '.join(m[1][:m[1].rfind('.lagda.md')] for m in ec)}", file=sys.stderr)
 
     module_titles_and_mdfiles = sorted(
         zip(module_titles, module_mdfiles), key=lambda tm: (tm[1].split(".")))
 
     entry_list = ('  ' + entry_template.format(title=t, mdfile=md)
                   for t, md in module_titles_and_mdfiles)
 
-    namespace_title = utils.get_lagda_file_title(
+    namespace_title = utils.get_lagda_md_file_title(
         os.path.join(root, namespace) + ".lagda.md")
     namespace_entry = entry_template.format(
         title=namespace_title, mdfile=namespace + ".md")
@@ -62,6 +65,9 @@ def generate_index(root, header):
     status = 0
     entry_lists = []
     for namespace in sorted(utils.get_subdirectories_recursive(root)):
+        if namespace == "temp":
+            continue
+
         entry_list, s = generate_namespace_entry_list(namespace)
         entry_lists.append(entry_list)
         status |= s
@@ -102,8 +108,6 @@ def generate_index(root, header):
     summary_path = "SUMMARY.md"
     index_header = "# Formalisation in Agda"
 
-    print(f"Generating {summary_path}")
-
     index_content, status = generate_index(root, index_header)
     if status == 0:
         summary_contents = summary_template.format(module_index=index_content)

diff --git a/scripts/generate_namespace_index_modules.py b/scripts/generate_namespace_index_modules.py
@@ -38,6 +38,8 @@ def generate_agda_block(root, namespace):
 
 if __name__ == "__main__":
 
+    CHANGES_WERE_MADE_FLAG = 1
+    MISPLACED_TITLE_FLAG = 2
     status = 0
     root = "src"
 
@@ -57,7 +59,8 @@ def generate_agda_block(root, namespace):
         title_index = contents.find("# ")
         if title_index > 0:
             print(
-                f"Warning! Namespace file {namespace_filename} has title after first line.")
+                f"Warning! Namespace file {namespace_filename} has title after first line.", file=sys.stderr)
+            status |= MISPLACED_TITLE_FLAG
         elif title_index == -1:  # Missing title. Generate it
             contents = generate_title(namespace) + contents
 
@@ -76,15 +79,15 @@ def generate_agda_block(root, namespace):
                 # An agda block is opened but not closed.
                 # This is an error, but we can fix it
                 print(
-                    f"WARNING! agda-block was opened but not closed in {namespace_filename}.")
+                    f"WARNING! agda-block was opened but not closed in {namespace_filename}.", file=sys.stderr)
                 contents = contents[:agda_block_start] + generated_block
             else:
                 agda_block_end += len("\n```\n")
                 contents = contents[:agda_block_start] + \
                     generated_block + contents[agda_block_end:]
 
         if oldcontents != contents:
-            status |= 1
+            status |= CHANGES_WERE_MADE_FLAG
             with open(namespace_filename, "w") as f:
                 f.write(contents)
 

diff --git a/scripts/remove_extra_blank_lines.py b/scripts/remove_extra_blank_lines.py
@@ -68,7 +68,7 @@ def has_well_formed_blocks(mdcode, pos=0):
         # Remove blank lines after a code block starts, and blank lines before a code block ends
         if not has_well_formed_blocks(output):
             print(
-                f"Error! File '{fpath}' has ill-formed code blocks. Please check if there is an opening or closing code block tag (```) without a corresponding closing/opening tag.")
+                f"Error! File '{fpath}' has ill-formed code blocks. Please check if there is an opening or closing code block tag (```) without a corresponding closing/opening tag.", file=sys.stderr)
 
             status |= STATUS_FILES_WITH_ILL_FORMED_BLOCKS
         else:

diff --git a/scripts/update_contributors.py b/scripts/update_contributors.py
@@ -1,4 +1,5 @@
 import requests
+import sys
 import json
 
 s = requests.Session()
@@ -11,7 +12,7 @@
 
 if response.status_code != 200:
     print(f"Failed to retrieve contributors for repository {repo}. "
-          f"Status code: {response.status_code}")
+          f"Status code: {response.status_code}", file=sys.stderr)
     exit(1)
 
 contributors = json.loads(response.text)
@@ -38,7 +39,7 @@ def get_github_user_name(username):
 
     if response.status_code != 200:
         print(f"Failed to retrieve information for user {username}. "
-              f"Status code: {response.status_code}")
+              f"Status code: {response.status_code}", file=sys.stderr)
         return ""
 
     user_info = json.loads(response.text)

diff --git a/scripts/utils/__init__.py b/scripts/utils/__init__.py
@@ -72,7 +72,7 @@ def call_agda(options, filepath):
     return subprocess.call(f"agda {options} {filepath}", shell=True, stdout=subprocess.DEVNULL, stderr=subprocess.DEVNULL)
 
 
-def get_lagda_file_title(lagda_filepath):
+def get_lagda_md_file_title(lagda_filepath):
     with open(lagda_filepath, "r") as file:
         contents = file.read()
         title_index = contents.find("# ")