We employ several tools to maintain our library. This guide will walk you through their usage and help ensure your contributions meet our standards.
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.
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
pass all checks and initiate the verification of the entire library via
make check
.
Below is a summary of the tasks this tool performs:
-
Trailing whitespace: Identifies and removes any trailing whitespace.
-
End of files: Ensures that a file is either empty, or ends with one new line.
-
Mixed line ending: Ensures consistent use of line endings (LF vs CRLF).
-
Double quoted strings: Replaces double quoted strings with single quoted strings.
-
Python AST: Checks whether Python scripts parse as valid Python.
-
YAML: Checks yaml files for parseable syntax.
-
Case conflicts: Checks for files that would conflict in case-insensitive filesystems.
-
Merge conflicts: Checks for any merge conflict artifacts in the code.
-
Markdown conventions: Checks/enforces various of our conventions related to markdown code. This includes removing punctuation in section headers, removing empty code blocks, ensuring that there is only one top-level header and that this is placed on the first line of the file, and checking that no section is void of contents.
-
Blank line conventions: Searches for and removes any double or multiple blank lines.
-
Agda space conventions: Corrects some common spacing mistakes according to our conventions. This includes removing repeat whitespace characters between two non-whitespace characters in a line, having whitespace before an opening brace or semicolon if it is not preceeded by a dot or another opening brace, and having whitespace after a closing brace or semicolon if it is not succeeded by a closing brace.
-
Indentation conventions: Verifies that the indentation level is always a 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 definition.
-
Maximum line length: Detects any violations of the 80-character line limit and reports them. Note that single tokens such as long names can exceed this limit.
-
Create index of modules: Generates and maintains the index of modules for each folder in
src
. For example, thegroup-theory/
folder has a correspondingsrc/group-theory.lagda.md
file that imports all the modules ingroup-theory/
publicly. You do not need to maintain these files manually. -
Generate index file for the entire library: Generates
src/everything.lagda.md
, which imports all formalization files across the library. This file is also regenerated bymake check
each time it's run. No manual maintenance is required for this file. -
Python scripts formatting: Performs
autopep8
formatting on Python scripts. Note that this script takes care of most formatting for Python scripts, so you should not worry about formatting them. -
CSS, JS, YAML and Markdown (no codeblocks) formatting: Performs basic formatting tasks such as enforcing the 80-character line limit, formatting markdown tables, among others. Note that this script takes care of all formatting for these file types, so you should not worry about formatting such files.
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.
Installation instructions for the make website
tool can be found
here
Once all checks are passed, you're ready to submit your pull request. Please provide a brief description of the significant changes you made. Keep in mind that the individual commits in your pull request will be squashed into a single commit, and its commit message will be the description you provide in your pull request.