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@groupes.renater.fr). We are 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`, `zarith`, 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 ## Building Documentation
  17
  18 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:
  19
  20 ```
  21 pip3 install sphinx sphinxcontrib-bibtex
  22 ```
  23
  24 You will need to re-configure Why3 to enable documentation building. Once it has been configured, documentation can be built by running `make doc`.
  25
  26 # Testing
  27
  28 To execute the Why3 tests run:
  29
  30 ```
  31 ./bench/bench
  32 ```
  33
  34 ## Running specific tests
  35
  36 You may run specific classes of tests by specifying them on the command line.
  37 The full listing of classes can be obtained from `-help`.
  38
  39 For example to run the 'good file' and 'bad file' tests, use:
  40
  41 ```
  42 ./bench/bench goodfiles badfiles
  43 ```
  44
  45 ## Gitlab CI
  46
  47 Every new commit pushed on the gitlab repository invokes an continuous
  48 integration check. The description on how to upgrade this CI procedure
  49 is specifically done in `misc/ci.md`
  50
  51 ## Adding new test suites
  52
  53 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.
  54
  55 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.
  56
  57 ## Nightly CI
  58
  59 Every night, the latest master is tested against a series of standard
  60 configurations, on Moloch (`moloch.lri.fr`). This ensures that
  61 regressions are caught across a wide array of different prover
  62 versions and families. The results of Nightly CI are emailed to a set
  63 of selected developers emails each morning.
  64
  65 If you require access to Moloch in order to update sessions or test a new prover, ask one of the maintainers for help.
  66
  67 # Standards
  68
  69 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.
  70
  71 While code review is not strictly enforced it is *highly* encouraged.
  72
  73 ## Commits
  74
  75 Every commit should:
  76 - Compile, and pass CI.
  77 - Be stripped of trailing whitespace.
  78 - Use appropriate indentation.
  79 - Be limited to 80 columns.
  80 - Have a clear and relevant commit message
  81 - Be as functionally isolated as possible
  82
  83 # Contributing to counterexamples generation and checking
  84
  85 The module `src/core/model_parser` contains the main data structure
  86 for counterexamples.
  87
  88 Parser functions for counterexamples must be declared in driver files
  89 (e.g. declaring `model_parser "smtv2"` somewhere).  Such functions
  90 should first be registered using `Model_parser.register_model_parser`.
  91 The latter function takes as input a so-called `raw_model_parser`
  92 (e.g. `Smtv2_model_parser.parse`).  This `raw_model_parser` is an
  93 input of the internal function `Model_parser.model_parser`, which is
  94 the main function for counterexamples generation.  A
  95 `raw_model_parser` is a function that processes a solver textual
  96 output and produces a preliminary structure for counterexamples, which
  97 is completed by `Model_parser.model_parser`.
  98
  99 So, as mentioned above, an example of a `raw_model_parser`, for SMTv2
 100 solvers, is `Smtv2_model_parser.parse`, which makes use of another
 101 data type `Smtv2_model_defs.function_def`.  This specific
 102 `Smtv2_model_parser.parse` function proceeds in 2 main phases:
 103 - first transforms the textual output into an S-expression,
 104 - then the latter S-expression is transformed into a
 105   `Model_parser.model_element list`.
 106
 107 The `raw_model_parser` functions are using the variable names as
 108 printed by the printer.  It is only the `Model_parser.build_model_rec`
 109 function that recovers the original Why3 name from the
 110 `printing_info`.  The type `printing_info` is declared in module
 111 `src/core/printer`.  Task printers are taking as arguments a record of
 112 type `Printer.printer_args`.  The field `printing_info` is supposed to
 113 be modified in place by printers.
 114
 115 # profiling
 116
 117 Profiling execution of Why3 can be performed out-of-the-box using
 118 under Linux using `perf`. A typical usage is
 119
 120 ```
 121 perf record --call-graph=dwarf -- why3 command <options> <arguments>
 122 perf report
 123 ```
 124 Note that perf may complain you don't have enough priviledges. A typical configuration change required is, for the session only, execute
 125 ```
 126 sysctl kernel.perf_event_paranoid=2
 127 ```
 128 or, to make this setting permanent, add the line
 129 ```
 130 kernel.perf_event_paranoid = 2
 131 ```
 132 to `sys/sysctl.conf`.