Skip to content

Latest commit

 

History

History
118 lines (92 loc) · 5.4 KB

CONTRIBUTING.md

File metadata and controls

118 lines (92 loc) · 5.4 KB
Raw

CONTRIBUTING

We very much appreciate contributions in the form of pull requests (PRs). When preparing a PR here are some general guidelines:

  • To test your changes before submission, run make at the top level, which will generate all required Everything files in Cubical/README.agda and then typecheck the latter file. If you're using Windows, here are some instructions to get the make command working.

  • Please read through and clean your code before making a PR. Clean code has reasonable line length (<100 characters), good indentation, appropriate amounts of comments and consistent naming.

  • Local definitions should be put in where, let-in or private so that it is easy to see which are the main results of a file and which are just helper definitions.

  • If the code is based on some paper add a reference to the version of the paper that the file follows in a comment at the top of the file. Avoid calling top-level definitions thm123, lem321, etc., instead have informative names and put pointers to the theorems and lemmas in comments above the definition.

  • For guidelines how to name things see NAMING.md.

  • Use private variable to quantify over universe levels at the top of the file. All definitions should be maximally universe polymorphic.

  • Make reasonably many arguments implicit. If you find yourself having to provide some argument explicitly most of the time then it should not be implicit. The same applies the other way around, if some argument most often can be replaced by _ then it should be made implicit.

  • Use Type ℓ for universes (so Set ℓ is not allowed in order to avoid confusion with the type of h-sets).

  • All files should start with

    {-# OPTIONS --safe #-}

    unless there is a good reason for it not to. The --cubical and --no-import-sorts flags are added in the cubical.agda-lib file.

  • It is much easier for us to review and merge smaller and self-contained PRs. If a PR changes a lot of files all over the library then they will conflict with other PRs making it harder for us to merge them. It also takes longer to comment on the code if the PR is very big. If you have a large PR please consider splitting it into smaller parts that build on each other.

  • Large refactoring, renaming, etc., should be done in designated PRs that only do one thing.

  • Draft PRs are very appreciated so that we can discuss the code as it develops. It also helps with knowing who's working on what and reducing duplicate efforts. If your code contains postulates then it should be in a draft PR until the postulates have been filled in.

  • We automatically check for whitespace in the end of lines using Travis. It is easy to configure emacs so that this is visible while editing files by adding (setq-default show-trailing-whitespace t) to ~/.emacs. The command M-x delete-trailing-whitespace is also very useful. It is possible to add a hook that runs this command automatically when saving Agda files, by adding the following to your ~/.emacs:

    ;; delete trailing whitespace before saving in agda-mode
(defun agda-mode-delete-whitespace-before-save ()
  (when (eq major-mode 'agda2-mode)
    (delete-trailing-whitespace)))

(add-hook 'before-save-hook #'agda-mode-delete-whitespace-before-save)

  • Use copattern-matching when instantiating records for efficiency. This seems especially important when constructing Iso's.

  • New records should be defined with the no-eta-equality modifier, unless you have a good reason to drop it - keep in mind that dropping it can lead to type checking speed problems.

  • If typechecking starts becoming slow try to fix the efficiency problems directly. We don't want to merge files that are very slow to typecheck so they will have to optimized at some point and it's often much easier to fix these things directly. If you don't know what to try, make a draft PR and ask for help.

  • It is often useful to give explicit names to the Iso, Equiv and Path version of a result. Try to avoid switching between these when constructing something, for instance if you want to construct a Path out of a series of Iso's then compose the Isos first and then apply isoToPath once instead of converting all of them to paths and composing them as paths.

  • Some useful lemmas have specialized versions with higher arity to make code easier to read. See for example isPropΠ2 and isSetΠ2 in HLevels.agda as well as various versions of function extensionality in FunExtEquiv.agda.

  • Unless a file is in the Core, Foundations or Codata package you don't need to add it manually to the Everything file as it is automatically generated when running make.

  • For folders with Base and Properties submodules, the Base file can contain some basic consequences of the main definition, but shouldn't include theorems that would require additional imports.

  • Avoid public imports, except in modules that are specifically meant to collect and re-export results from several modules.

  • The Experiments folder contains various experiments and nothing in the library should depend on something from this folder.