why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2023-12-21T11:43:32+01:00https://gitlab.inria.fr/why3/why3/-/issues/822Allow extracting floating-point literals2023-12-21T11:43:32+01:00Guillaume MelquiondAllow extracting floating-point literalsThe extraction code (both in the common part `compile.ml` and in the specific parts `ocaml.ml` and `c.ml`) chokes on real literals.
```whyml
use ieee_float.Float64
let const = (2.0 : Float64.t)
(* why3 extract -D ocaml64 foo.mlw *)
```The extraction code (both in the common part `compile.ml` and in the specific parts `ocaml.ml` and `c.ml`) chokes on real literals.
```whyml
use ieee_float.Float64
let const = (2.0 : Float64.t)
(* why3 extract -D ocaml64 foo.mlw *)
```1.8.0https://gitlab.inria.fr/why3/why3/-/issues/482Spurious statements when extracting to C2020-04-29T18:13:47+02:00Guillaume MelquiondSpurious statements when extracting to CWhen extracted to C, file `multiprecision/sqrtrem.mlw` produces spurious statements such as
```c
res = wmpn_rshift(nr, nx, l, UINT64_C(1));
IGNORE2(sp,scratch);
res; // <- HERE
```
This comes from
let ghost r = wmpn_rshift_sep sp s...When extracted to C, file `multiprecision/sqrtrem.mlw` produces spurious statements such as
```c
res = wmpn_rshift(nr, nx, l, UINT64_C(1));
IGNORE2(sp,scratch);
res; // <- HERE
```
This comes from
let ghost r = wmpn_rshift_sep sp scratch l 1 in
This might be caused by an interaction between ghost results and function inlining.Raphaël Rieu-HelftRaphaël Rieu-Helfthttps://gitlab.inria.fr/why3/why3/-/issues/477Extraction of interface files is too conservative2020-04-14T09:09:04+02:00Guillaume MelquiondExtraction of interface files is too conservativeWhen extracting an interface file, all the modules used by the current module are considered as dependencies. This is correct but leaks implementation details. Ideally, only the modules that define types needed to typecheck the types and...When extracting an interface file, all the modules used by the current module are considered as dependencies. This is correct but leaks implementation details. Ideally, only the modules that define types needed to typecheck the types and function signatures of the current module should be dependencies.https://gitlab.inria.fr/why3/why3/-/issues/476Strange interaction between `remove module` and extraction to C2020-04-20T13:19:44+02:00Guillaume MelquiondStrange interaction between `remove module` and extraction to CCurrently, when extracting module `fxp.Fxp` to C, the resulting files `fxp.h` and `fxp.c` are basically empty. So, I tried adding `remove module` to the corresponding section of `drivers/c.drv`. Unfortunately, this breaks the extraction ...Currently, when extracting module `fxp.Fxp` to C, the resulting files `fxp.h` and `fxp.c` are basically empty. So, I tried adding `remove module` to the corresponding section of `drivers/c.drv`. Unfortunately, this breaks the extraction of `examples/multiprecision/sqrt.mlw` to C, as variables of type `fxp` are then ignored (silently!).Raphaël Rieu-HelftRaphaël Rieu-Helfthttps://gitlab.inria.fr/why3/why3/-/issues/475Extraction of top-level function alias2020-10-23T17:18:56+02:00Mário PereiraExtraction of top-level function aliasConsider the following example:
```
use mach.int.Int63
let f (x y: int63) = x + y
let g = f
let a = g 42 0
```
Extracting this program results in the following ill-typed OCaml code:
```
let f (x y: int) : int = x + y
let a = g 42 0
``...Consider the following example:
```
use mach.int.Int63
let f (x y: int63) = x + y
let g = f
let a = g 42 0
```
Extracting this program results in the following ill-typed OCaml code:
```
let f (x y: int) : int = x + y
let a = g 42 0
```
This problem happens because in `compile.ml` we are simply ignoring `PDlet (LDsym (_, cty))` nodes where `cty.c_node` is not a `Cfun`. For the above example, `c_node = Capp _`.
I thought we could not define any kind of partial application at top-level at all, but it seems that function aliasing is allowed. @paskevyc is it true that we can only have a `c_node = Capp _` at top-level if it is a function aliasing, such as the above `let g = f`? It that is the case, should this be compiled as a partial application, using @rrieuhel !364 merge request?https://gitlab.inria.fr/why3/why3/-/issues/403Localisation of errors during extraction of cloned module2019-10-31T11:25:06+01:00DAILLER SylvainLocalisation of errors during extraction of cloned moduleRecently, I tried to extract some code written in Why3 into OCaml. I did not manage to use modular extraction so I used flat extraction which seemed easier to handle. Something like:
`why3 extract -L . --recursive -D ocaml64 -D driver/o...Recently, I tried to extract some code written in Why3 into OCaml. I did not manage to use modular extraction so I used flat extraction which seemed easier to handle. Something like:
`why3 extract -L . --recursive -D ocaml64 -D driver/ocaml_ext.drv interface.mlw -o extract/all.ml`
In my Why3 code, I cloned the hasthbl.mlw file. So, I need to provide a driver for this cloned module so that I instantiate all axiomatic parts with real OCaml code. My feature wish would be to improve the error that `why3extract` outputs when it cannot find an implementation for a specific ident. I currently typically get:
```
File "$MY_PATH_TO_WHY3/why3/share/stdlib/hashtbl.mlw", line 30, characters 6-9:
Symbol mem1 cannot be extracted
```
I would like to know which chain of clone is used to find this error. For example, in my case, I clone this library two different times (not with the same key type) and in one of the cases I clone the resulting module. So, this gets pretty confusing. I would like something along the lines of:
```
Symbol mem1 cannot be extracted during cloning of Hashtbl at file my_hashtbl.mlw line 15 characters 42
The symbol is originally defined in
File "$MY_PATH_TO_WHY3/why3/share/stdlib/hashtbl.mlw", line 30, characters 6-9:
The chain of cloning is the following:
Hashtbl at file hashtbl.mlw ...
H at file my_hashtbl.mlw ...
Ha at file my_code.mlw ...
```
Looking at the code for extraction, I think that the cloning module can be tracked and the error could be better handled. I can try to look at how this could be done if there is no time ?https://gitlab.inria.fr/why3/why3/-/issues/246Allow "use ghost Foo"2019-05-21T15:37:41+02:00Guillaume 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 prog...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/215Extraction des foncteurs2021-02-11T10:41:17+01:00Franç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'ex...Les 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 drivershttps://gitlab.inria.fr/why3/why3/-/issues/171Extraction of absurd2020-10-23T17:36:51+02:00MARCHE ClaudeExtraction of absurdExtraction of ```absurd``` is currently ```assert false``` which is perfectly fine. Though, during development it happens that ```absurd``` is temporary used on "todo" branches as one uses ``` assert false``` in OCaml. In that case, it w...Extraction of ```absurd``` is currently ```assert false``` which is perfectly fine. Though, during development it happens that ```absurd``` is temporary used on "todo" branches as one uses ``` assert false``` in OCaml. In that case, it would be a very interesting feature if the line number of the original Why3 file be given so that the "Assert_failure" exception raised could point to the proper Why3 file and the proper line. This could be done easily by inserting
```
# <line number> <mlw file name>
```
on the line before ```assert false```PARREIRA PEREIRA Mário JoséPARREIRA PEREIRA Mário José