<commit_before>Coding Style
============

[C++11](http://en.wikipedia.org/wiki/C%2B%2B11) features
--------------------------------------------------------

We make extensive use of new features in the C++ 11 standard.
Developers must be familiar with the standard to be able to understand
the code.
Here are some of the features that are extensively used.

- Type inference (aka `auto` keyword).
- Initializer lists.
- Lambda functions and expressions.
- `nullptr` constant.
- Strongly typed enumerations.
- Right angle bracket.
- Thread local storage.
- Threading facilities.
- Tuple types.

Comments
--------

The comments in the Lean codebase contain
[Doxygen](http://www.stack.nl/~dimitri/doxygen/) commands.
Doxygen is the de facto standard tool for generating documentation from
annotated C++ sources.

Namespaces
----------

All code is in the `lean` namespace. Each frontend is stored in a
separate nested namespace. For example, the SMT 2.0 frontend is stored
in the `lean::smt` namespace.

Exception: some debugging functions are stored outside of the `lean`
namespace. These functions are called `print` and are meant to be used
when debugging Lean using `gdb`.

Smart pointers
--------------

We only use `std::shared_ptr` template for class `C` only if we expect
to create only a few objects (< 1000) of class `C`. Otherwise, we
implement our own intrusive smart pointer. For example, the class
`expr` is an intrusive smart pointer to `expr_cell`. We may have
millions of `expr` objects. We say it is intrusive because the
reference counter is stored in `expr_cell`.

We use `std::unique_ptr` to make sure unique resources will be freed
correctly.

Idioms
------

We use some popular C++ idioms:

- [Pimpl](http://c2.com/cgi/wiki?PimplIdiom)
- [RAII](http://en.wikipedia.org/wiki/Resource_Acquisition_Is_Initialization) Resource Acquisition Is Initialization

Formatting
----------
<commit_msg>doc(coding_style): add how to organize template source code<commit_after>Coding Style
============

[C++11](http://en.wikipedia.org/wiki/C%2B%2B11) features
--------------------------------------------------------

We make extensive use of new features in the C++ 11 standard.
Developers must be familiar with the standard to be able to understand
the code.
Here are some of the features that are extensively used.

- Type inference (aka `auto` keyword).
- Initializer lists.
- Lambda functions and expressions.
- `nullptr` constant.
- Strongly typed enumerations.
- Right angle bracket.
- Thread local storage.
- Threading facilities.
- Tuple types.

Comments
--------

The comments in the Lean codebase contain
[Doxygen](http://www.stack.nl/~dimitri/doxygen/) commands.
Doxygen is the de facto standard tool for generating documentation from
annotated C++ sources.

Namespaces
----------

All code is in the `lean` namespace. Each frontend is stored in a
separate nested namespace. For example, the SMT 2.0 frontend is stored
in the `lean::smt` namespace.

Exception: some debugging functions are stored outside of the `lean`
namespace. These functions are called `print` and are meant to be used
when debugging Lean using `gdb`.

Smart pointers
--------------

We only use `std::shared_ptr` template for class `C` only if we expect
to create only a few objects (< 1000) of class `C`. Otherwise, we
implement our own intrusive smart pointer. For example, the class
`expr` is an intrusive smart pointer to `expr_cell`. We may have
millions of `expr` objects. We say it is intrusive because the
reference counter is stored in `expr_cell`.

We use `std::unique_ptr` to make sure unique resources will be freed
correctly.

Template
--------
We organize template source code using the approach described at http://www.codeproject.com/Articles/3515/How-To-Organize-Template-Source-Code

Idioms
------

We use some popular C++ idioms:

- [Pimpl](http://c2.com/cgi/wiki?PimplIdiom)
- [RAII](http://en.wikipedia.org/wiki/Resource_Acquisition_Is_Initialization) Resource Acquisition Is Initialization

Formatting
----------

{'fraction_non_alphanumeric': 0.1341948310139165, 'fraction_numerical': 0.008449304174950299, 'mean_word_length': 3.4133771929824563, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 3, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3470275', 'n_tokens_mistral': 1149, 'n_tokens_neox': 1101, 'n_words': 491}