merge

CONTRIBUTING.md

@@ -6,9 +6,13 @@ through their usage and help ensure your contributions meet our standards.
 ## The `make pre-commit` tool
 
 The `make pre-commit` tool checks library conventions and performs basic tasks.
-Before you run it, ensure your new files have been added to the `git`
-repository. Installation instructions for the `make pre-commit` tool can be
-found [here](HOWTO-INSTALL.md#after-the-setup).
+Our installation instructions for the `make pre-commit` tool can be found
+[here](HOWTO-INSTALL.md#contributor-setup).
+
+Before you run the tool, ensure that your files are properly tracked by git by
+staging any relevant file additions or deletions. This is what the commands
+`git add <path-to-new-file>` and `git add <path-to-deleted-file>` do
+respectively.
 
 The `make pre-commit` tool can generate errors during the first run while
 correcting some of them automatically. If all goes well, the second run should
@@ -59,9 +63,9 @@ Below is a summary of the tasks this tool performs:
   multiple of two. If inconsistencies are found, it provides an error report
   indicating the location of the issues.
 
-- **Fix simply wrappable long lines**: Scans for any lines exceeding the
-  80-character limit that can be resolved by inserting line breaks. It inserts
-  line breaks at the beginning of any definition, but not in the middle of a
+- **Wrap long lines**: Scans for any lines exceeding the 80-character limit that
+  can be resolved by simple rules for inserting line breaks. It inserts line
+  breaks at the beginning of any definition, but not in the middle of a
   definition.
 
 - **Maximum line length**: Detects any violations of the 80-character line limit
@@ -78,6 +82,12 @@ Below is a summary of the tasks this tool performs:
   library. This file is also regenerated by `make check` each time it's run. No
   manual maintenance is required for this file.
 
+**Note**: The previous two hooks only detect tracked files. This means that if
+you add or delete files, they must be staged for these hooks to take these
+changes into consideration. This gives you finer control over your commits. For
+instance, if a file is not ready to be committed, you can still use the
+pre-commit tool and just not stage that file.
+
 <!--
 - **Python scripts formatting**: Performs `autopep8` formatting on Python
   scripts. Note that this script takes care of most formatting for Python
@@ -92,13 +102,14 @@ Below is a summary of the tasks this tool performs:
 
 ## The `make website` tool
 
-After you complete the `make pre-commit` process, run `make website` to verify
-that the current changes will not interfere with the website's compilation. This
-tool starts by running `make check` and then builds the website, reporting any
-broken internal links that may prevent the website build from completing.
+After you complete the `make pre-commit` process, you can run `make website` to
+verify that the current changes will not interfere with the website's
+compilation. This tool starts by running `make check` and then builds the
+website, reporting any broken internal links that may prevent the website build
+from completing.
 
 Installation instructions for the `make website` tool can be found
-[here](HOWTO-INSTALL.md#after-the-setup).
+[here](HOWTO-INSTALL.md#contributor-setup).
 
 ## Adding yourself as a contributor {#add-contributor}
 

scripts/generate_main_index_file.py

@@ -6,32 +6,42 @@
 import sys
 import utils
 import pathlib
+import subprocess
 
-STATUS_FLAG_NO_TITLE = 1
-STATUS_FLAG_DUPLICATE_TITLE = 2
+STATUS_FLAG_GIT_ERROR = 1
+STATUS_FLAG_NO_TITLE = 2
+STATUS_FLAG_DUPLICATE_TITLE = 4
 
 entry_template = '- [{title}]({mdfile})'
 
 
-def generate_namespace_entry_list(namespace):
+def generate_namespace_entry_list(root_path, 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_md_file_title, lagda_file_paths))
+    try:
+        git_tracked_files = utils.get_git_tracked_files()
+    except subprocess.CalledProcessError:
+        utils.eprint('Failed to get Git-tracked files')
+        sys.exit(STATUS_FLAG_GIT_ERROR)
 
-    module_mdfiles = tuple(
-        map(lambda m: utils.get_module_mdfile(namespace, m), modules))
+    namespace_path = root_path.joinpath(namespace)
+
+    # Filter out the relevant files in the given namespace
+    relevant_files = tuple(
+        f for f in git_tracked_files if namespace_path in f.parents)
+
+    lagda_file_paths = tuple(f for f in relevant_files if utils.is_agda_file(f))
+    modules = tuple(p.name for p in lagda_file_paths)
+    module_titles = tuple(utils.get_lagda_md_file_title(f)
+                     for f in lagda_file_paths)
+    module_mdfiles = tuple(utils.get_module_mdfile(namespace, m) for m in 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', file=sys.stderr)
+            utils.eprint(
+                f'WARNING! {namespace}.{module} no title was found')
 
     # Check duplicate titles
     equal_titles = utils.get_equivalence_classes(
@@ -41,35 +51,32 @@ def generate_namespace_entry_list(namespace):
 
     if (len(equal_titles) > 0):
         status |= STATUS_FLAG_DUPLICATE_TITLE
-        print(f'WARNING! Duplicate titles in {namespace}:', file=sys.stderr)
+        utils.eprint(f'WARNING! Duplicate titles in {namespace}:')
         for ec in equal_titles:
-            print(
-                f"  Title '{ec[0][0]}': {', '.join(m[1][:m[1].rfind('.lagda.md')] for m in ec)}", file=sys.stderr)
+            utils.eprint(
+                f"  Title '{ec[0][0]}': {', '.join(m[1][:m[1].rfind('.lagda.md')] for m in ec)}")
 
     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_md_file_title(
-        os.path.join(root, namespace) + '.lagda.md')
+    namespace_title = utils.get_lagda_md_file_title(str(namespace_path.with_suffix('.lagda.md')))
     namespace_entry = entry_template.format(
         title=namespace_title, mdfile=namespace + '.md')
 
     namespace_entry_list = namespace_entry + '\n' + '\n'.join(entry_list)
     return namespace_entry_list, status
 
 
-def generate_index(root, header):
+def generate_index(root_path, header):
     status = 0
     entry_lists = []
-    namespaces = sorted(set(utils.get_subdirectories_recursive(root)))
+    namespaces = sorted(set(utils.get_subdirectories_recursive(root_path)))
 
     for namespace in namespaces:
-        if namespace == 'temp' or 'MAlonzo' in namespace:
-            continue
-        entry_list, s = generate_namespace_entry_list(namespace)
+        entry_list, s = generate_namespace_entry_list(root_path, namespace)
         entry_lists.append(entry_list)
         status |= s
 
@@ -116,7 +123,9 @@ def generate_index(root, header):
     summary_path = 'SUMMARY.md'
     index_header = '# The agda-unimath library'
 
-    index_content, status = generate_index(root, index_header)
+    root_path = pathlib.Path(root)
+
+    index_content, status = generate_index(root_path, index_header)
     if status == 0:
         summary_contents = summary_template.format(module_index=index_content)
         with open(summary_path, 'w') as summary_file:

scripts/generate_namespace_index_modules.py

@@ -4,21 +4,20 @@
 
 # * Remember to update the script's entry in `CONTRIBUTING.md` on changes
 
-import os
 import pathlib
 import sys
 import utils
+import subprocess
 
 
 def generate_title(namespace):
     return '# ' + namespace.capitalize().replace('-', ' ') + '\n'
 
 
-def generate_imports(root, namespace):
-    namespace_path = os.path.join(root, namespace)
-    def agda_file_filter(f): return utils.is_agda_file(
-        pathlib.Path(os.path.join(namespace_path, f)))
-    namespace_files = filter(agda_file_filter, os.listdir(namespace_path))
+def generate_imports(root, namespace, git_tracked_files):
+    namespace_path = root.joinpath(namespace)
+    namespace_files = (f.name for f in namespace_path.iterdir(
+    ) if utils.is_agda_file(f) and f in git_tracked_files)
 
     import_statements = (utils.get_import_statement(
         namespace, module_file, public=True) for module_file in namespace_files)
@@ -34,24 +33,29 @@ def agda_file_filter(f): return utils.is_agda_file(
 '''
 
 
-def generate_agda_block(root, namespace):
-    return agda_block_template.format(namespace=namespace, imports=generate_imports(root, namespace))
+def generate_agda_block(root, namespace, git_tracked_files):
+    return agda_block_template.format(namespace=namespace, imports=generate_imports(root, namespace, git_tracked_files))
 
 
 if __name__ == '__main__':
-    CHANGES_WERE_MADE_FLAG = 1
-    MISPLACED_TITLE_FLAG = 2
+    STATUS_FLAG_GIT_ERROR = 1
+    CHANGES_WERE_MADE_FLAG = 2
+    MISPLACED_TITLE_FLAG = 4
     status = 0
-    root = 'src'
+    root = pathlib.Path('src')
+
+    try:
+        git_tracked_files = set(utils.get_git_tracked_files())
+    except subprocess.CalledProcessError:
+        utils.eprint('Failed to get Git-tracked files')
+        sys.exit(STATUS_FLAG_GIT_ERROR)
 
     for namespace in utils.get_subdirectories_recursive(root):
-        if namespace == 'temp' or 'MAlonzo' in namespace:
-            continue
 
-        namespace_filename = os.path.join(root, namespace) + '.lagda.md'
+        namespace_filename = root.joinpath(namespace).with_suffix('.lagda.md')
 
-        if os.path.isfile(namespace_filename):
-            with open(namespace_filename, 'r+') as namespace_file:
+        if namespace_filename.is_file():
+            with namespace_filename.open('r+') as namespace_file:
                 contents = namespace_file.read()
         else:
             contents = ''
@@ -60,8 +64,8 @@ def generate_agda_block(root, namespace):
 
         title_index = contents.find('# ')
         if title_index > 0:
-            print(
-                f'Warning! Namespace file {namespace_filename} should start with a top-level title.', file=sys.stderr)
+            utils.eprint(
+                f'Warning! Namespace file {namespace_filename} should start with a top-level title.')
             status |= MISPLACED_TITLE_FLAG
         elif title_index == -1:  # Missing title, generate it
             contents = generate_title(namespace) + contents
@@ -71,17 +75,19 @@ def generate_agda_block(root, namespace):
         if agda_block_start == -1:
             # Must add agda block
             # Add at the end of the file
-            contents += '\n' + generate_agda_block(root, namespace)
+            contents += '\n' + \
+                generate_agda_block(root, namespace, git_tracked_files)
         else:
             agda_block_end = contents.find(
                 '\n```\n', agda_block_start + len('```agda\n'))
-            generated_block = generate_agda_block(root, namespace)
+            generated_block = generate_agda_block(
+                root, namespace, git_tracked_files)
 
             if agda_block_end == -1:
                 # 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}.', file=sys.stderr)
+                utils.eprint(
+                    f'WARNING! agda block was opened but not closed in {namespace_filename}.')
                 contents = contents[:agda_block_start] + generated_block
             else:
                 agda_block_end += len('\n```\n')
@@ -90,7 +96,7 @@ def generate_agda_block(root, namespace):
 
         if oldcontents != contents:
             status |= CHANGES_WERE_MADE_FLAG
-            with open(namespace_filename, 'w') as f:
+            with namespace_filename.open('w') as f:
                 f.write(contents)
 
     sys.exit(status)

scripts/spaces_conventions_simple.py

@@ -30,6 +30,11 @@ def no_whitespace_before_closing_curly_brace(line):
     return re.sub(r'(?![-!}])(\S)\s+\}', r'\1}', line)
 
 
+def no_whitespace_after_opening_brace_inside_line(line):
+    # TODO: this is very slow currently
+    return utils.recursive_sub(r'^(\s*.*(?!--)[^\s({]{2,}.*[({])\s+', r'\1', line)
+
+
 if __name__ == '__main__':
 
     status = 0
@@ -60,6 +65,8 @@ def no_whitespace_before_closing_curly_brace(line):
                     line = space_before_special_symbols(line)
                     line = no_whitespace_before_closing_parenthesis(line)
                     line = no_whitespace_before_closing_curly_brace(line)
+                    # line = no_whitespace_after_opening_brace_inside_line(
+                    #     line)
                     # line = space_after_opening_parenthesis_on_new_line(line)
 
                 block_comment_level -= block_comment_delta_neg

scripts/utils/__init__.py

@@ -32,13 +32,18 @@ def get_files_recursive(startpath):
 
 
 def get_subdirectories_recursive(startpath):
-    for root, dirs, files in os.walk(startpath):
-        for d in dirs:
-            try:
-                os.listdir(os.path.join(startpath, d))
-            except FileNotFoundError:
-                continue
-            yield d
+    # Get list of Git-tracked files
+    git_tracked_files = get_git_tracked_files()
+    rootlen = len(str(startpath)) + 1
+    # Filter out directories
+    subdirectories = set()
+    for path in git_tracked_files:
+        if startpath in path.parents:
+            relative_path = str(path.parent)[rootlen:]
+            if relative_path:
+                subdirectories.add(relative_path)
+
+    return map(str, subdirectories)
 
 
 def find_index(s: str, t: str) -> List[int]:
@@ -206,3 +211,10 @@ def is_agda_opening_or_closing_tag(line):
     """
     tag_match = agda_block_tag_regex.match(line)
     return bool(tag_match), tag_match and bool(tag_match.group(1))
+
+
+def get_git_tracked_files():
+    # Get list of Git-tracked files
+    git_output = subprocess.check_output(['git', 'ls-files'], text=True)
+    git_tracked_files = map(pathlib.Path, git_output.strip().split('\n'))
+    return git_tracked_files

src/category-theory.lagda.md

@@ -115,9 +115,11 @@ open import category-theory.natural-transformations-maps-precategories public
 open import category-theory.nonunital-precategories public
 open import category-theory.one-object-precategories public
 open import category-theory.opposite-categories public
+open import category-theory.opposite-large-precategories public
 open import category-theory.opposite-precategories public
 open import category-theory.opposite-preunivalent-categories public
 open import category-theory.precategories public
+open import category-theory.precategory-of-elements-of-a-presheaf public
 open import category-theory.precategory-of-functors public
 open import category-theory.precategory-of-functors-from-small-to-large-precategories public
 open import category-theory.precategory-of-maps-from-small-to-large-precategories public