Skip to content

Latest commit

 

History

History
100 lines (78 loc) · 3.54 KB

CONTRIBUTING.md

File metadata and controls

100 lines (78 loc) · 3.54 KB
Raw

Contributing to Lambdapi

Contributions to lambdapi are very welcome! Here are some guidelines for contributing to this project.

For contributing to the VSCode extension, see editors/vscode/INSTALL.md and editors/vscode/CONTRIBUTING.md.

For contributing to the User Manual, see doc/README.md.

Branching and pull-request policy

For the moment, the Github repo uses only one branch, master. Releases are tagged.

Contributions to Lambdapi should be done by doing pull-requests from your forked repo of Lambdapi. Pull-requests are then reviewed, commented and eventually merged.

  • If the file structure is changed, doc/structure.rst should be changed as well.
  • Important contributions should update the file CHANGES.md.

General style and indentation

In the interest of code source uniformity, we require:

  • do not use tabulation characters
  • one indentation unit is equal to two spaces,
  • there should be no trailing spaces at the end of lines,
  • line length should be limited to 78 characters excluding newline (except for @see commands for ocamldoc)
  • do not align commas, arrow or comments in match constructions

You should run make sanity_check before committing anything. The script misc/git_hook_helper.sh helps setting up a git hook to run make sanity_check automatically before each commit. It is encouraged to set up such a hook. The script may be called with the -b option to include compilation in the hook. Please check that you have GNU awk (gawk) installed or another UTF-8 compatible implementation of the AWK programming language interpreter.

Naming convention

No plural forms in filenames, type names or module names (e.g. file term.ml and not terms.ml, type term and not terms, etc.).

For OCaml identifiers, we use the snake_case naming convention.

In Lambdapi files, objects should start with a lowercase letter while types should start with an uppercase letter.

Type annotations and interface files

Lambdapi does not use interface (or .mli) files. However, every function should be documented with its type, and an ocamldoc comment. We ask that the type of a function is given with the following syntax:

(** [a_function x y z] does some things with [x], [y] and [z]. *)
let a_function : int -> (bool -> bool) -> string -> unit = fun x y z ->
  ...

Changing the syntax of Lambdapi

When changing the syntax of Lambdapi, make sure to update the following files:

  • src/core/lpLexer.ml
  • src/core/lpParser.mly
  • src/core/pretty.ml
  • src/core/print.ml
  • editors/vim/syntax/lambdapi.vim
  • editors/emacs/lambdapi-vars.el (syntax coloring)
  • editors/emacs/lambdapi-smie.el (grammar and indentation)
  • editors/vscode/lp.configuration.json (comments configuration),
  • editors/vscode/syntaxes/lp.tmLanguage.json (syntax highlighting),
  • misc/lambdapi.tex
  • doc/Makefile.bnf
  • the User Manual files in the doc/ repository

and do make bnf to generate the BNF grammar, and make doc to generate the Sphynx documentation.

Note: the lambdapi.opam file is generated by dune using the dune-project file, it should not be edited manually. It is still versioned because opam still needs it, but it will probably become obsolete.

Debugging

Color codes:

  • blue: top-level type inference/checking
  • magenta: new constraint
  • green: constraint to solve
  • yellow: data from signature or context
  • red: instantiations and user commands