doc: commit conventions and Mathlib CI
diff --git a/doc/dev/commit_convention.md b/doc/dev/commit_convention.md index 80362c1..9793350 100644 --- a/doc/dev/commit_convention.md +++ b/doc/dev/commit_convention.md
@@ -33,6 +33,9 @@ - chore (maintain, ex: travis-ci) - perf (performance improvement, optimization, ...) +Every `feat` or `fix` commit must have a `changelog-*` label, and a commit message +beginning with "This PR " that will be included in the changelog. + ``<subject>`` has the following constraints: - use imperative, present tense: "change" not "changed" nor "changes" @@ -44,6 +47,7 @@ - just as in ``<subject>``, use imperative, present tense - includes motivation for the change and contrasts with previous behavior + - If a `changelog-*` label is present, the body must begin with "This PR ". ``<footer>`` is optional and may contain two items: @@ -60,17 +64,21 @@ fix: add declarations for operator<<(std::ostream&, expr const&) and operator<<(std::ostream&, context const&) in the kernel +This PR adds declarations `operator<<` for raw printing. The actual implementation of these two operators is outside of the -kernel. They are implemented in the file 'library/printer.cpp'. We -declare them in the kernel to prevent the following problem. Suppose -there is a file 'foo.cpp' that does not include 'library/printer.h', -but contains +kernel. They are implemented in the file 'library/printer.cpp'. - expr a; - ... - std::cout << a << "\n"; - ... +We declare them in the kernel to prevent the following problem. +Suppose there is a file 'foo.cpp' that does not include 'library/printer.h', +but contains +```cpp +expr a; +... +std::cout << a << "\n"; +... +``` The compiler does not generate an error message. It silently uses the operator bool() to coerce the expression into a Boolean. This produces counter-intuitive behavior, and may confuse developers. +
diff --git a/doc/dev/index.md b/doc/dev/index.md index 999591a..ea626f2 100644 --- a/doc/dev/index.md +++ b/doc/dev/index.md
@@ -80,3 +80,10 @@ `prelude` keyword. This disables the automated import of `Init`, meaning that developers need to figure out their own subset of `Init` to import. This is done such that changing files in `Init` doesn't force a full rebuild of `Lean`. + +### Testing against Mathlib/Batteries +You can test a Lean PR against Mathlib and Batteries by rebasing your PR +on to `nightly-with-mathlib` branch. (It is fine to force push after rebasing.) +CI will generate a branch of Mathlib and Batteries called `lean-pr-testing-NNNN` +that uses the toolchain for your PR, and will report back to the Lean PR with results from Mathlib CI. +See https://leanprover-community.github.io/contribute/tags_and_branches.html for more details.