CONTRIBUTING.md

   1 Welcome, contributor, to the Why3 verification platform!
   2
   3 If you wish to contribute, open an issue or otherwise interact with our [Gitlab](https://gitlab.inria.fr/why3/why3), you will need to have an INRIA account.
   4 External users can file bug reports using our [mailing list](mailto:why3-club@lists.gforge.inria.fr). We're sorry for the inconvenience.
   5
   6 # Building
   7
   8 To build Why3 locally you will need a functional installation of OCaml (at least 4.08), `menhir`, `num` and `autoconf`. You can set up your developer build using the following commands:
   9
  10 ```
  11 autoconf
  12 ./configure --enable-local # stores the built binaries under ./bin
  13 make
  14 ```
  15
  16 Note: there can be issues around Num, recall and document those.
  17
  18
  19 ## Building Documentation
  20
  21 Building the Why3 documentation requires an installation of Sphinx, as well as the `sphinxcontrib-bibtex` package. If your package manager does not have up to date versions of these packages, or they otherwise fail to install, you can install them using `pip3` as follows:
  22
  23 ```
  24 pip3 install sphinx sphinxcontrib-bibtex
  25 ```
  26
  27 You will need to re-configure Why3 to enable documentation building. Once it has been configured, documentation can be built by running `make doc`.
  28
  29 # Testing
  30
  31 To execute the Why3 tests run:
  32
  33 ```
  34 ./bench/bench
  35 ```
  36
  37 ## Running specific tests
  38
  39 You may run specific classes of tests through the `-only` flag, the full listing of classes can be obtained from `-help`.
  40
  41 For example to run the 'good file' tests, use:
  42
  43 ```
  44 ./bench/bench -only goodfiles
  45 ```
  46
  47 ## Gitlab CI
  48
  49 Every new commit pushed on the gitlab repository invokes an continuous
  50 integration check. The description on how to upgrade this CI procedure
  51 is specifically done in `misc/ci.md`
  52
  53 ## Adding new test suites
  54
  55 To add a new directory of tests add a new line in `bench/bench`. The suite should be added to the relevant block, which is determined by the kind of assertion it performs. For example, if you wished to add a set of files which should successfully prove, add a line like `goods path/to/tests` to the appropriate block.
  56
  57 Certain tests, those in `examples/`, `examples/bts`, `examples/programs` and `examples/check-builtin` are replayed every night on Moloch. To ensure accuracy and avoid flakiness, the sessions for these tests must be created on Moloch as well.
  58
  59 ## Nightly CI
  60
  61 Every night, the latest master is tested against a series of standard
  62 configurations, on Moloch (`moloch.lri.fr`). This ensures that
  63 regressions are caught across a wide array of different prover
  64 versions and families. The results of Nightly CI are emailed to a set
  65 of selected developers emails each morning.
  66
  67 If you require access to Moloch in order to update sessions or test a new prover, ask one of the maintainers for help.
  68
  69 # Standards
  70
  71 Why3 uses a Pull Request development model. Contributions should be made to separate branches and a Merge Request should be opened in Gitlab, explaining the contents and purpose of its contents.
  72
  73 While code review is not strictly enforced it is *highly* encouraged.
  74
  75 ## Commits
  76
  77 Every commit should:
  78 - Compile, and pass CI.
  79 - Be stripped of trailing whitespace.
  80 - Use appropriate indentation.
  81 - Be limited to 80 columns.
  82 - Have a clear and relevant commit message
  83 - Be as functionally isolated as possible
  84
  85 # Contributing to counterexamples generation and checking
  86
  87 The module `src/core/model_parser` contains the main data structure
  88 for counterexamples.
  89
  90 Parser functions for counterexamples must be declared in driver files
  91 (e.g. declaring `model_parser "smtv2"` somewhere).  Such functions
  92 should first be registered using `Model_parser.register_model_parser`.
  93 The latter function takes as input a so-called `raw_model_parser`
  94 (e.g. `Smtv2_model_parser.parse`).  This `raw_model_parser` is an
  95 input of the internal function `Model_parser.model_parser`, which is
  96 the main function for counterexamples generation.  A
  97 `raw_model_parser` is a function that processes a solver textual
  98 output and produces a preliminary structure for counterexamples, which
  99 is completed by `Model_parser.model_parser`.
 100
 101 So, as mentioned above, an example of a `raw_model_parser`, for SMTv2
 102 solvers, is `Smtv2_model_parser.parse`, which makes use of another
 103 data type `Smtv2_model_defs.function_def`.  This specific
 104 `Smtv2_model_parser.parse` function proceeds in 2 main phases:
 105 - first transforms the textual output into an S-expression,
 106 - then the latter S-expression is transformed into a
 107   `Model_parser.model_element list`.
 108
 109 The `raw_model_parser` functions are using the variable names as
 110 printed by the printer.  It is only the `Model_parser.build_model_rec`
 111 function that recovers the original Why3 name from the
 112 `printing_info`.  The type `printing_info` is declared in module
 113 `src/core/printer`.  Task printers are taking as arguments a record of
 114 type `Printer.printer_args`.  The field `printing_info` is supposed to
 115 be modified in place by printers.
 116
 117 # profiling
 118
 119 Profiling execution of Why3 can be performed out-of-the-box using
 120 under Linux using `perf`. A typical usage is
 121
 122 ```
 123 perf record --call-graph=dwarf -- why3 command <options> <arguments>
 124 perf report
 125 ```
 126 Note that perf may complain you don't have enough priviledges. A typical configuration change required is, for the session only, execute
 127 ```
 128 sysctl kernel.perf_event_paranoid=2
 129 ```
 130 or, to make this setting permanent, add the line
 131 ```
 132 kernel.perf_event_paranoid = 2
 133 ```
 134 to `sys/sysctl.conf`.