CONTRIBUTING.md

Contributing to the library

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

The make pre-commit tool checks library conventions and performs basic tasks. Our installation instructions for the make pre-commit tool can be found here.

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 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).

• 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.

• 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 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, the group-theory/ folder has a corresponding src/group-theory.lagda.md file that imports all the modules in group-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 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.

• 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.

The make website tool

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.

Adding yourself as a contributor {#add-contributor}

When you submit changes to the library, you have every right to call yourself a contributor. We can attribute your work to you by listing your preferred name on our list of contributors, and by including your name on the source pages you helped create.

This attribution process is automated, so all you need to do is add a section to the CONTRIBUTORS.toml file, where you can customize how you appear on the website. If you do not want to be mentioned on the website, simply leave yourself out of this file. For most contributors, the new section will look like the following:

[[contributors]]
displayName = "Vojtěch Štěpančík"
usernames = [ "Vojtěch Štěpančík", "VojtechStep" ]
github = "VojtechStep"

The displayName field tells our tooling how to display your name - be it on the Contributors page, the source page headers, or in the list of recent changes. The github field is optional, and when included it makes you name on the Contributors page into a link to your GitHub profile.

The usernames list is very important - that's how you tell the build process which commits belong to you. Because of some peculiarities with GitHub's handling of author and co-author information, this list will very often include two names: your local git username, which you can get by running git config user.name from the command-line in your local clone of the repository; and your GitHub display name, which you can get by navigating to your user profile on GitHub, where it's the one directly under your profile picture. If you change your GitHub display name, the old commits will still use the old name, but your new changes will use the new name, so if you keep contributing to the library, you'll need to add that new name to the list. If you have any doubts or questions, feel free to reach out on the Discord server or in the comments of your pull request.

Additional fields you can add are all optional strings, and they are extra, homepage and bio. Currently they have no effect on how your information is displayed on the website.

Submitting your pull request on GitHub

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.