why3 issueshttps://gitlab.inria.fr/why3/why3/issues2019-10-04T09:33:19Zhttps://gitlab.inria.fr/why3/why3/issues/287Add injectivity for type invariant2019-10-04T09:33:19ZFrançois BobotAdd injectivity for type invariant```
type t = {
v: int;
} invariant { 0 <= v }
```
It is currently not possible to prove that:
```
forall x1 x2:t. x1.v = x2.v -> x1 = x2
```
Which is compiled to:
```
forall x1 x2:t. (view x1).v = (view x2).v -> x1 = x2
```
We need to add the property that `view` is injective, for example using `mk` its inverse:
```
forall x:t [view x]. mk (view x) = x
``````
type t = {
v: int;
} invariant { 0 <= v }
```
It is currently not possible to prove that:
```
forall x1 x2:t. x1.v = x2.v -> x1 = x2
```
Which is compiled to:
```
forall x1 x2:t. (view x1).v = (view x2).v -> x1 = x2
```
We need to add the property that `view` is injective, for example using `mk` its inverse:
```
forall x:t [view x]. mk (view x) = x
```François BobotFrançois Bobothttps://gitlab.inria.fr/why3/why3/issues/286Extend witness grammar for type invariant2019-03-26T16:35:06ZFrançois BobotExtend witness grammar for type invariantThe proposal is to extend the current grammar for the `by` construct.
Currently:
```
type t = { f1: ...; f2: ... } invariant { ... } by { f1 = ...; f2 = ...}
```
proposed:
```
type t = { ... } invariant { ... } by e
```
where all leaf of `e` in result position have the shape `{ f1 = ...; f2 = ...}`
The implementation:
- parsing e as an expression
- typing check that all the leaf define all the fields of the record, and translate the leaf into a tuple in the order of the field definition. So the witness is well-typed and doesn't use the defined type.
- check the properties on e
The properties on e checked, currently (not complete, nor correct?):
- no side effect
- pure
I don't see why we have these restrictions, we just want to prove that such element is buildable so any non-ghost computation should be acceptable.The proposal is to extend the current grammar for the `by` construct.
Currently:
```
type t = { f1: ...; f2: ... } invariant { ... } by { f1 = ...; f2 = ...}
```
proposed:
```
type t = { ... } invariant { ... } by e
```
where all leaf of `e` in result position have the shape `{ f1 = ...; f2 = ...}`
The implementation:
- parsing e as an expression
- typing check that all the leaf define all the fields of the record, and translate the leaf into a tuple in the order of the field definition. So the witness is well-typed and doesn't use the defined type.
- check the properties on e
The properties on e checked, currently (not complete, nor correct?):
- no side effect
- pure
I don't see why we have these restrictions, we just want to prove that such element is buildable so any non-ghost computation should be acceptable.François BobotFrançois Bobothttps://gitlab.inria.fr/why3/why3/issues/285split_all_full raises out of memory on float theory2019-03-24T14:05:23ZDAILLER Sylvainsplit_all_full raises out of memory on float theoryHello,
Using split_all_full on goals containing the ieee_float theory can result in out of memory (see attached file [b.mlw](/uploads/777dac8832951acc1eacf6a489be58ba/b.mlw) ). Most likely, on the hypothesis fma_special, the negative monoid generated by split_core grows exponentially (which eventually eat all available memory).
I encountered this problem when launching the strategy "1" (problem which should be solved by #282).
Is it possible to optimize the generation of monoids during the transformation, stop the splitting done by the transformation when it grows to a critical size, or disallow part of the splitting ?Hello,
Using split_all_full on goals containing the ieee_float theory can result in out of memory (see attached file [b.mlw](/uploads/777dac8832951acc1eacf6a489be58ba/b.mlw) ). Most likely, on the hypothesis fma_special, the negative monoid generated by split_core grows exponentially (which eventually eat all available memory).
I encountered this problem when launching the strategy "1" (problem which should be solved by #282).
Is it possible to optimize the generation of monoids during the transformation, stop the splitting done by the transformation when it grows to a critical size, or disallow part of the splitting ?https://gitlab.inria.fr/why3/why3/issues/279Disappearance of keep_on_simp2019-03-01T10:09:10ZDAILLER SylvainDisappearance of keep_on_simpHello,
The attribute keep_on_simp disappeared from 0.88 to 1.0. Are there mechanisms to retrieve the behaviour it was used for ? Why was it dropped ?
I think it prevented simplifications of formulas under this attribute.Hello,
The attribute keep_on_simp disappeared from 0.88 to 1.0. Are there mechanisms to retrieve the behaviour it was used for ? Why was it dropped ?
I think it prevented simplifications of formulas under this attribute.https://gitlab.inria.fr/why3/why3/issues/278Parsing on attributes in programs2019-03-01T13:37:02ZDAILLER SylvainParsing on attributes in programsHello,
This issue is to keep track of discussions.
The question is the following. On why3 0.88, it was possible to add attributes to the program in order to retrieve them later in goals. This behaviour disappeared: it seems to be needed by SPARK for tracability of goals (goals A contains stuff that originate from this and that part of the code).
```
module Test
use int.Int
type d = {mutable contents: int; mutable useless: int}
let f c
ensures { c.contents = 1 }
= (*[@vc_sp]*)
c.contents <- 2;
[@This disappears] (c.contents <- 3);
c.contents <- 4
end
```
Copying potentially interested persons: @paskevyc @marche
PS: If you think people from SPARK should be involved, I can ask them to comment on this.Hello,
This issue is to keep track of discussions.
The question is the following. On why3 0.88, it was possible to add attributes to the program in order to retrieve them later in goals. This behaviour disappeared: it seems to be needed by SPARK for tracability of goals (goals A contains stuff that originate from this and that part of the code).
```
module Test
use int.Int
type d = {mutable contents: int; mutable useless: int}
let f c
ensures { c.contents = 1 }
= (*[@vc_sp]*)
c.contents <- 2;
[@This disappears] (c.contents <- 3);
c.contents <- 4
end
```
Copying potentially interested persons: @paskevyc @marche
PS: If you think people from SPARK should be involved, I can ask them to comment on this.https://gitlab.inria.fr/why3/why3/issues/272CVC4 for smtlib 2.62019-02-12T11:44:55ZDAILLER SylvainCVC4 for smtlib 2.6Apparently, the semantics of bvurem changed from smtlib 2.5 to 2.6 quoting Andres Nötzli from cvc-users mailing list:
> Yes, the semantics changed in version 2.6 [0]. `(bvurem s t)` returns `s` if `t` is zero (before, the value was a fresh constant). CVC4 automatically chooses the semantics that matches the SMT-LIB version. You can manually toggle the behavior with --(no-)bv-div-zero-const (enabling the flag corresponds to the 2.6 version, disabling to earlier versions). If your problems only use QF_BV, you can also improve performance by compiling CVC4 with support for CaDiCaL (run the `contrib/get-cadical` script, then configure with `--cadical`) and then using the flags `--bitblast=eager --bv-sat-solver=cadical` (eager bitblasting and using CaDiCaL as the SAT solver).
Is that possible that we now need to add the option "--(no-)bv-div-zero-const" to the smt-lib provers using 2.6 ? It seems to help SPARK users.
Additional question:
Will there be a problem with the following axiom because urem seems to be linked to bvurem by smt-lib drivers ? (axioms about "mod ?x 0" do not seem to exist so I guess it is ok unless mod is also mapped by a driver?)
```
val function urem (v1 v2 : t) : t
axiom to_uint_urem:
forall v1 v2. to_uint (urem v1 v2) = mod (to_uint v1) (to_uint v2)
```Apparently, the semantics of bvurem changed from smtlib 2.5 to 2.6 quoting Andres Nötzli from cvc-users mailing list:
> Yes, the semantics changed in version 2.6 [0]. `(bvurem s t)` returns `s` if `t` is zero (before, the value was a fresh constant). CVC4 automatically chooses the semantics that matches the SMT-LIB version. You can manually toggle the behavior with --(no-)bv-div-zero-const (enabling the flag corresponds to the 2.6 version, disabling to earlier versions). If your problems only use QF_BV, you can also improve performance by compiling CVC4 with support for CaDiCaL (run the `contrib/get-cadical` script, then configure with `--cadical`) and then using the flags `--bitblast=eager --bv-sat-solver=cadical` (eager bitblasting and using CaDiCaL as the SAT solver).
Is that possible that we now need to add the option "--(no-)bv-div-zero-const" to the smt-lib provers using 2.6 ? It seems to help SPARK users.
Additional question:
Will there be a problem with the following axiom because urem seems to be linked to bvurem by smt-lib drivers ? (axioms about "mod ?x 0" do not seem to exist so I guess it is ok unless mod is also mapped by a driver?)
```
val function urem (v1 v2 : t) : t
axiom to_uint_urem:
forall v1 v2. to_uint (urem v1 v2) = mod (to_uint v1) (to_uint v2)
```https://gitlab.inria.fr/why3/why3/issues/262Parsing bug: vc_sp attribute/assignment2019-01-30T13:54:53ZDAILLER SylvainParsing bug: vc_sp attribute/assignmentThere is apparently a parsing bug in the following file when uncommenting `[@vc_sp]`:
```
module Test
use int.Int
type d = {mutable contents: int; mutable useless: int}
let f c
ensures { c.contents = 1 }
= (*[@vc_sp]*)
c.contents <- 2
end
```There is apparently a parsing bug in the following file when uncommenting `[@vc_sp]`:
```
module Test
use int.Int
type d = {mutable contents: int; mutable useless: int}
let f c
ensures { c.contents = 1 }
= (*[@vc_sp]*)
c.contents <- 2
end
```Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/issues/256Warn about trivially spurious conter-example2019-01-30T11:11:48ZFrançois BobotWarn about trivially spurious conter-exampleThe given counter-example is given by CVC4:
```
module FF
use real.Truncate
use real.RealInfix
use int.Int
lemma floor: forall x. x <. 1. -> floor x = 0
(* x = 0.0 *)
end
```
But CVC4 will immediately prove the validity of the goal, `goal: forall x. x = 0.0 -> x <. 1. -> floor x = 0` . So it would be great if after getting a counter-example we could send the instantiated goal back to the prover. If it proves the validity of the goal we can add a warning to the user that the counter-example is misleading and that it is a wrong counter-example. It is similar to one iteration of a CEGAR loop.The given counter-example is given by CVC4:
```
module FF
use real.Truncate
use real.RealInfix
use int.Int
lemma floor: forall x. x <. 1. -> floor x = 0
(* x = 0.0 *)
end
```
But CVC4 will immediately prove the validity of the goal, `goal: forall x. x = 0.0 -> x <. 1. -> floor x = 0` . So it would be great if after getting a counter-example we could send the instantiated goal back to the prover. If it proves the validity of the goal we can add a warning to the user that the counter-example is misleading and that it is a wrong counter-example. It is similar to one iteration of a CEGAR loop.https://gitlab.inria.fr/why3/why3/issues/255Automake error : missing Makefile.am2019-06-24T07:31:04ZHenri de BOUTRAYAutomake error : missing Makefile.amThe automake step of the installation (`automake --add-missing`) returns the following error:
`automake: warning: autoconf input should be named 'configure.ac', not 'configure.in'
configure.in: error: no proper invocation of AM_INIT_AUTOMAKE was found.
configure.in: You should verify that configure.in invokes AM_INIT_AUTOMAKE,
configure.in: that aclocal.m4 is present in the top-level directory,
configure.in: and that aclocal.m4 was recently regenerated (using aclocal)
configure.in:171: installing './install-sh'
automake: error: no 'Makefile.am' found for any configure output`
I am trying to make a Dockerfile for Why3, and this is preventing the build process to carry on.
I found a way to ignore the error (appending `; exit 0` behind the command) but it seems very dirty).
This error is not blocking (after running the command, the other steps run properly) but it seems that there you be a better way to handle this ...
Thanks in advance.The automake step of the installation (`automake --add-missing`) returns the following error:
`automake: warning: autoconf input should be named 'configure.ac', not 'configure.in'
configure.in: error: no proper invocation of AM_INIT_AUTOMAKE was found.
configure.in: You should verify that configure.in invokes AM_INIT_AUTOMAKE,
configure.in: that aclocal.m4 is present in the top-level directory,
configure.in: and that aclocal.m4 was recently regenerated (using aclocal)
configure.in:171: installing './install-sh'
automake: error: no 'Makefile.am' found for any configure output`
I am trying to make a Dockerfile for Why3, and this is preventing the build process to carry on.
I found a way to ignore the error (appending `; exit 0` behind the command) but it seems very dirty).
This error is not blocking (after running the command, the other steps run properly) but it seems that there you be a better way to handle this ...
Thanks in advance.https://gitlab.inria.fr/why3/why3/issues/253Roadmap for counterexamples2019-06-11T11:49:23ZDAILLER SylvainRoadmap for counterexamples* [ ] Solve bugs in ce Why3:
* [ ] bug in the task for location of terms which are dereferenced with "!" -> records.mlw ? #344
* [ ] Solve problems with polymorphism ? How ?
* [x] Write the docs ( #237 is related)
* [ ] issue #252
* [ ] Interface:
* [ ] Add a boolean in proofattempt result to indicate if counterexamples can be launched on proofattempt
* [ ] Change the status image in the ide to show that counterexamples can be queried* [ ] Solve bugs in ce Why3:
* [ ] bug in the task for location of terms which are dereferenced with "!" -> records.mlw ? #344
* [ ] Solve problems with polymorphism ? How ?
* [x] Write the docs ( #237 is related)
* [ ] issue #252
* [ ] Interface:
* [ ] Add a boolean in proofattempt result to indicate if counterexamples can be launched on proofattempt
* [ ] Change the status image in the ide to show that counterexamples can be queriedDAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/issues/252Check counterexamples benchmark2019-06-25T14:59:04ZDAILLER SylvainCheck counterexamples benchmarkThis is the list of examples for counterexamples that needs to be checked for good counterexamples:
Scalar types:
- [x] int.mlw
- [x] int32.mlw
- [x] int_overflow.mlw
- [ ] jlamp0.mlw : fails because of #348
- [x] real.mlw
- [ ] floats.mlw see #349
- [x] range_type.mlw
- [ ] jlamp_projections.mlw #351
- [ ] bv32.mlw #352
- [ ] result.mlw #353
- [ ] if_assign.mlw solve #353 first
- [x] if_decision_branch.mlw
Maps:
- [ ] map.mlw #354
Records:
- [ ] ref_mono.mlw #355
- [ ] record_map.mlw model error in 4.8.4: #359
- [ ] record_one_field.mlw
- [ ] ref.mlw
- [ ] records_inv.mlw
- [ ] records_label.mlw
- [ ] record_nested_one_field.mlw
- [ ] records.mlw
Arrays:
- [ ] array_mono.mlw
- [ ] jlamp_array.mlw
- [ ] simple_array.mlw
- [ ] arrays.mlw
- [ ] array_records.mlw
Algebraic types:
- [x] algebraic_types_mono.mlw
- [ ] algebraic_types_poly.mlw: fails because of polymorphism
- [ ] list.mlw
- [ ] polymorphism.mlwThis is the list of examples for counterexamples that needs to be checked for good counterexamples:
Scalar types:
- [x] int.mlw
- [x] int32.mlw
- [x] int_overflow.mlw
- [ ] jlamp0.mlw : fails because of #348
- [x] real.mlw
- [ ] floats.mlw see #349
- [x] range_type.mlw
- [ ] jlamp_projections.mlw #351
- [ ] bv32.mlw #352
- [ ] result.mlw #353
- [ ] if_assign.mlw solve #353 first
- [x] if_decision_branch.mlw
Maps:
- [ ] map.mlw #354
Records:
- [ ] ref_mono.mlw #355
- [ ] record_map.mlw model error in 4.8.4: #359
- [ ] record_one_field.mlw
- [ ] ref.mlw
- [ ] records_inv.mlw
- [ ] records_label.mlw
- [ ] record_nested_one_field.mlw
- [ ] records.mlw
Arrays:
- [ ] array_mono.mlw
- [ ] jlamp_array.mlw
- [ ] simple_array.mlw
- [ ] arrays.mlw
- [ ] array_records.mlw
Algebraic types:
- [x] algebraic_types_mono.mlw
- [ ] algebraic_types_poly.mlw: fails because of polymorphism
- [ ] list.mlw
- [ ] polymorphism.mlwMARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/issues/251Emit a warning when "old" does nothing in a specification2018-12-17T10:14:51ZRaphaël Rieu-HelftEmit a warning when "old" does nothing in a specification```
val swap (t : array int) (i j : int): unit
requires { 0 <= i < length t /\ 0 <= j < length t }
ensures { t = (old t)[i <- old t[j]][j <- old t[i]] }
```
In the example above, I wrote a specification for the swap function but forgot the `writes` clause. My impression is that an `old` in a specification where nothing under the `old` is in the writes is almost always a user error, and that we should emit a "Maybe you forgot a `writes` clause" warning.```
val swap (t : array int) (i j : int): unit
requires { 0 <= i < length t /\ 0 <= j < length t }
ensures { t = (old t)[i <- old t[j]][j <- old t[i]] }
```
In the example above, I wrote a specification for the swap function but forgot the `writes` clause. My impression is that an `old` in a specification where nothing under the `old` is in the writes is almost always a user error, and that we should emit a "Maybe you forgot a `writes` clause" warning.https://gitlab.inria.fr/why3/why3/issues/246Allow "use ghost Foo"2019-05-21T13:37:41ZGuillaume MelquiondAllow "use ghost Foo"It might happen that one wants to use a module for specification and ghost code, but not for actual code (and a fortiori extraction). A good example is `int.Int` which is ubiquitous in WhyML programs but not necessarily in extracted programs.
It would be good to have a way in the surface language to express and enforce that such a module is not meant to be actually used. Proposed syntax: `use ghost int.Int`. This would also make the extraction a lot less adhoc with respect to these modules.
A possible implementation would be to flag the corresponding scopes as being restricted. Any symbol accessed through such a scope would be forbidden to occur in non-ghost code. The change in `Why3extract.use_fold` would be trivial.
Open questions:
- what if the user do both `use` and `use ghost`?
- what if the user do `use ghost` on a module with toplevel side effects?It might happen that one wants to use a module for specification and ghost code, but not for actual code (and a fortiori extraction). A good example is `int.Int` which is ubiquitous in WhyML programs but not necessarily in extracted programs.
It would be good to have a way in the surface language to express and enforce that such a module is not meant to be actually used. Proposed syntax: `use ghost int.Int`. This would also make the extraction a lot less adhoc with respect to these modules.
A possible implementation would be to flag the corresponding scopes as being restricted. Any symbol accessed through such a scope would be forbidden to occur in non-ghost code. The change in `Why3extract.use_fold` would be trivial.
Open questions:
- what if the user do both `use` and `use ghost`?
- what if the user do `use ghost` on a module with toplevel side effects?https://gitlab.inria.fr/why3/why3/issues/242Division and comparison in SMT and Alt-ergo2018-11-26T15:28:50ZFrançois BobotDivision and comparison in SMT and Alt-ergoIt seems that we have no lemmas that relate real division and comparison. It is the case for provers that doesn't have built-in these symbol because `/.` is defined with `inv` and `*.`, and because `*.` is said monotone.It seems that we have no lemmas that relate real division and comparison. It is the case for provers that doesn't have built-in these symbol because `/.` is defined with `inv` and `*.`, and because `*.` is said monotone.https://gitlab.inria.fr/why3/why3/issues/233Improve apply2018-11-07T10:08:46ZDAILLER SylvainImprove applyIn some cases, we would like apply to perform matching on hypothesis too. Coq can do that in:
```
Goal forall P Q, (forall x y, P x y -> Q) -> P 3 4 -> Q.
intros P Q H H1.
apply H with (1:=H1).
```
We could imagine:
`apply H with_hyp H1`
To be investigated.In some cases, we would like apply to perform matching on hypothesis too. Coq can do that in:
```
Goal forall P Q, (forall x y, P x y -> Q) -> P 3 4 -> Q.
intros P Q H H1.
apply H with (1:=H1).
```
We could imagine:
`apply H with_hyp H1`
To be investigated.MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/issues/230Add warning to anonymous function without ensures2018-11-07T08:52:46ZDAILLER SylvainAdd warning to anonymous function without ensuresIn the following program, the contract of the intermediate function is not inferred automatically by Why3 (it apparently cannot be in the general case): in particular, the assignment to b is not reflected in the generated tasks. This issue is for generating a warning when such function do not carry a postcondition:
```
use int.Int
use int.MinMax
use ref.Ref
let f3 (a b : ref int) (c d: int)
requires { c < d }
ensures { result = min c d /\ !b = 22 }
=
a :=
(fun () -> if c < d then
(b := 4; c)
else
d) (* Here we should probably add a postcondition *) ();
!a + !b
```In the following program, the contract of the intermediate function is not inferred automatically by Why3 (it apparently cannot be in the general case): in particular, the assignment to b is not reflected in the generated tasks. This issue is for generating a warning when such function do not carry a postcondition:
```
use int.Int
use int.MinMax
use ref.Ref
let f3 (a b : ref int) (c d: int)
requires { c < d }
ensures { result = min c d /\ !b = 22 }
=
a :=
(fun () -> if c < d then
(b := 4; c)
else
d) (* Here we should probably add a postcondition *) ();
!a + !b
```Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/issues/229Adding location to SP generated variables2018-11-07T08:44:13ZDAILLER SylvainAdding location to SP generated variablesHello,
I don't know if I already opened an issue for this but there should be locations for ident generated by the sp_expr function in vc.ml. In this part of the code, I would like the None locations to be replaced by the appropriate locations:
```
let fresh_wr2 v _ = clone_pv None v in
let fresh_rd2 v _ = if v.pv_ity.ity_pure then None
else Some (clone_pv None v) in
```
This is apparently possible to do by adding a location to constructor Kseq and then propagating it.
A test for checking that it works is simply to create several assignments in a function and look at the generated task. If the constants of the generated task don't have locations, it does not work.Hello,
I don't know if I already opened an issue for this but there should be locations for ident generated by the sp_expr function in vc.ml. In this part of the code, I would like the None locations to be replaced by the appropriate locations:
```
let fresh_wr2 v _ = clone_pv None v in
let fresh_rd2 v _ = if v.pv_ity.ity_pure then None
else Some (clone_pv None v) in
```
This is apparently possible to do by adding a location to constructor Kseq and then propagating it.
A test for checking that it works is simply to create several assignments in a function and look at the generated task. If the constants of the generated task don't have locations, it does not work.Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/issues/228ieee_float library2018-10-30T12:58:00ZDAILLER Sylvainieee_float libraryHello,
The file ieee_float.mlw contains a number of `TODO` related to `axiom .` lines. Are the corresponding axioms going to change in the future ? Are they going to be kept as axioms ?Hello,
The file ieee_float.mlw contains a number of `TODO` related to `axiom .` lines. Are the corresponding axioms going to change in the future ? Are they going to be kept as axioms ?https://gitlab.inria.fr/why3/why3/issues/222syntax function in extraction drivers2019-05-21T09:26:54ZJean-Christophe Filliâtresyntax function in extraction driversSince 1.0.0, it makes no sense to use "syntax function" in extraction drivers. It should be "syntax val" instead.Since 1.0.0, it makes no sense to use "syntax function" in extraction drivers. It should be "syntax val" instead.PARREIRA PEREIRA Mário JoséPARREIRA PEREIRA Mário Joséhttps://gitlab.inria.fr/why3/why3/issues/215Extraction des foncteurs2018-10-19T14:55:13ZFrançois BobotExtraction des foncteursLes clones et l'extraction vers les foncteurs sont expérimentales. Pour les utilisateurs expert on pourrait essayer d'ajouter des exemples. On pourrait également réfléchir a ajouter des constructions dans les drivers pour simplifier l'extraction des modules (juste "module M va vers module N") et foncteurs (juste "c'est un foncteur avec ce mapping des arguments").
- [ ] Ajouter des exemples d'utilisation
- [ ] Ajouter un printer de mli dans l'extraction OCaml
- [ ] Réflexion sur extension des driversLes clones et l'extraction vers les foncteurs sont expérimentales. Pour les utilisateurs expert on pourrait essayer d'ajouter des exemples. On pourrait également réfléchir a ajouter des constructions dans les drivers pour simplifier l'extraction des modules (juste "module M va vers module N") et foncteurs (juste "c'est un foncteur avec ce mapping des arguments").
- [ ] Ajouter des exemples d'utilisation
- [ ] Ajouter un printer de mli dans l'extraction OCaml
- [ ] Réflexion sur extension des drivers