why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2019-12-12T07:19:07+01:00https://gitlab.inria.fr/why3/why3/-/issues/416Stop support for GTK22019-12-12T07:19:07+01:00DAILLER SylvainStop support for GTK2Quick summary of mail discussion:
This issue is to stop supporting GTK2, the constraint is to stay compatible with Debian stable.
The original issue was triggered by commit 9a47cae5e which is incompatible with lablgtk <= 2.18.6. For th...Quick summary of mail discussion:
This issue is to stop supporting GTK2, the constraint is to stay compatible with Debian stable.
The original issue was triggered by commit 9a47cae5e which is incompatible with lablgtk <= 2.18.6. For the record, Debian is using version 2.18.5.
In this issue, we should check if the Debian stable package for GTK3 supports Why3:
- if it does, disable GTK2 entirely,
- if it does not, revert 9a47cae5e and other potentially failing commit.https://gitlab.inria.fr/why3/why3/-/issues/415strings, chars, and OCaml2019-12-09T12:53:01+01:00Jean-Christophe Filliâtrestrings, chars, and OCamlNote: This related to module string.OCaml in the standard library. May be the module name string.OCaml is not the right one. Any suggestion for a better name is welcome.
Regarding OCaml characters, here is a proposal: in string.OCaml, d...Note: This related to module string.OCaml in the standard library. May be the module name string.OCaml is not the right one. Any suggestion for a better name is welcome.
Regarding OCaml characters, here is a proposal: in string.OCaml, declare a type `char` such as
type char = private {
char: string;
) invariant { length char = 1 }
so that we could declare a function
val ([]) (s: string) (i: int63) : char
requires { 0 <= i < length s }
ensures { result.char = s[i] }
which would be mapped to String.get directly (and not to "String.make 1 (String.get ...)" as it is currently) in the OCaml driver.Claudio Belo LourencoClaudio Belo Lourencohttps://gitlab.inria.fr/why3/why3/-/issues/414Bad contract for local function inside recursive functions2019-11-26T18:51:38+01:00DAILLER SylvainBad contract for local function inside recursive functionsIn this example, Why3 should force `f` to have `raises {TODO}` in its contract. It should be consistent with the non-recursive case.
```
use int.Int
exception TODO
let rec e (a : int) : int
ensures { result = a }
raises { TODO -> ...In this example, Why3 should force `f` to have `raises {TODO}` in its contract. It should be consistent with the non-recursive case.
```
use int.Int
exception TODO
let rec e (a : int) : int
ensures { result = a }
raises { TODO -> a = 1 }
=
let f (a : int) : int
=
e 1 in
if a = 1 then
raise TODO
else f 2
```https://gitlab.inria.fr/why3/why3/-/issues/413needlessly long pathnames from sessions2019-11-29T15:20:20+01:00Johannes Kanigneedlessly long pathnames from sessionsWe have trouble with long path names. On windows, paths longer than 250 chars (or so) don't work. That's a known limitation of the win32 API.
In why3 sessions, usually the file name of the .mlw file(s) is stored like this:
```
<file>
<p...We have trouble with long path names. On windows, paths longer than 250 chars (or so) don't work. That's a known limitation of the win32 API.
In why3 sessions, usually the file name of the .mlw file(s) is stored like this:
```
<file>
<path name=".."/><path name="example.mlw"/>
...
```
which leads the session mechanism to look for a file name `/path/to/session_file/../example.mlw`. In our case (and I think that's in fact the default in Why3), the last component of `/path/to/session_file/` is in fact derived from the .mlw file and has the same name. So the real path looks more like `/path/to/example/../example.mlw`.
In our use case, "example" can become quite long, so we have something like this: `/path/to/really_long_example_name_with_many_components/../really_long_example_name_with_many_components.mlw`. So we would like to contract the `..` and remove one copy of the long name: `/path/to/really_long_example_name_with_many_components.mlw`.
The code that constructs the path name is `Sysutil.system_dependent_absolute_path`. I think this function should remove occurrences of `..` (and the parent dir). Does somebody know why it doesn't?
I recall some discussions about symlinks, but inside the same process, contracting `a/../b/` to `b/` should always be correct even in the presence of symlinks, and if two processes (e.g. the why3 process creating the session file and the why3 process later reading it) disagree what the prefix `a/` is because of symlinks, I don't see why not contracting helps - the path `../b` is still wrong if the wrong prefix is applied, even if not contracted.
I will suggest a patch on this ticket later.https://gitlab.inria.fr/why3/why3/-/issues/412Shadowing (e.g., mutable variables) makes sessions unstable2020-02-12T00:36:15+01:00Guillaume MelquiondShadowing (e.g., mutable variables) makes sessions unstableOpen the following script in the IDE, perform `split_vc`, then `apply trans with x2`. This produces two subgoals; perform `apply trans with x1` on the first one. Save the session, restore the assertion, and reload the session. Transforma...Open the following script in the IDE, perform `split_vc`, then `apply trans with x2`. This produces two subgoals; perform `apply trans with x1` on the first one. Save the session, restore the assertion, and reload the session. Transformation `apply trans with x1` has now moved from the first subgoal to the second one. This happens randomly, so you might have to comment and reload again for it to occur.
```
type t = { mutable f:int }
predicate p int int
axiom trans: forall a b c. p a b -> p b c -> p a c
val q (x:t): unit
writes { x }
ensures { p x.f (old x.f) }
let foo (x:t)
ensures { p x.f (old x).f }
=
q x;
q x;
q x;
(*assert { true };*)
()
```
Presumably, this is caused by all the subgoals ending up with the exact same shape:
```
apV0V2IapV1V2IapV0V1F
apaxax
apply premises
postcondition
apV6V3IapV6V5FIapV5V4FIapV4V3FF
VC for foo
a97120fa31e7091252dd64bd73d61a64 5H4H0
e1d390651f7c12707fca160af9f2c85a 3H1H1H1H1H0
d4e7240950bed98e2516c724019fc9ef 2H1H1H1H1H0
c43c0cfc6afdfd35614f3bb4a51a9d7e 2H1H1H1H1H0
8f803408c1b99aef55c9955b7691760d 2H1H1H1H1H0
28c8a786d26365e6c894c3d9b72f6400 2H1H1H1H1H0
```1.3.0Guillaume MelquiondGuillaume Melquiondhttps://gitlab.inria.fr/why3/why3/-/issues/410add realizations for modules in library fmap2020-10-28T14:05:39+01:00Jean-Christophe Filliâtreadd realizations for modules in library fmaphttps://gitlab.inria.fr/why3/why3/-/issues/409remove deprecated library appmap and impmap2020-02-11T23:58:34+01:00Jean-Christophe Filliâtreremove deprecated library appmap and impmapthey are now subsumed by fmap.XXX modulesthey are now subsumed by fmap.XXX modulesJean-Christophe FilliâtreJean-Christophe Filliâtrehttps://gitlab.inria.fr/why3/why3/-/issues/408Make bench/ce in CI more stable2019-11-15T11:07:50+01:00DAILLER SylvainMake bench/ce in CI more stablebench/ce/records sometimes appears in diff in the continuous integration: this issue to either fix the problem or allow it to fail on integer values.bench/ce/records sometimes appears in diff in the continuous integration: this issue to either fix the problem or allow it to fail on integer values.https://gitlab.inria.fr/why3/why3/-/issues/406avoid jumping after deleting a detached subgoal2019-11-12T09:33:44+01:00LAWALL Juliaavoid jumping after deleting a detached subgoalDetached subgoals come at the end of the list of subgoals, which can be very long. When deleting such a subgoal it would be better to stay in the same place rather than jumping back up to the parent.Detached subgoals come at the end of the list of subgoals, which can be very long. When deleting such a subgoal it would be better to stay in the same place rather than jumping back up to the parent.Claudio Belo LourencoClaudio Belo Lourencohttps://gitlab.inria.fr/why3/why3/-/issues/405Hide does not work2019-11-04T13:43:00+01:00DAILLER SylvainHide does not workOn the following simple goal, `hide t 1` does not work. It should be investigated.
```
axiom h: 1 = 3
goal G: forall x. x = 1
```On the following simple goal, `hide t 1` does not work. It should be investigated.
```
axiom h: 1 = 3
goal G: forall x. x = 1
```https://gitlab.inria.fr/why3/why3/-/issues/404Theory "string.String" is unsound2019-11-12T11:12:27+01:00Guillaume MelquiondTheory "string.String" is unsoundBut more likely, it should really be disabled for some provers:
```
use string.String
goal g : false
```
```
$ bin/why3 prove foo.mlw -P Z3,4.6.0
foo.mlw Top g: Valid (0.04s, 24607 steps)
```But more likely, it should really be disabled for some provers:
```
use string.String
goal g : false
```
```
$ bin/why3 prove foo.mlw -P Z3,4.6.0
foo.mlw Top g: Valid (0.04s, 24607 steps)
```1.3.0Claudio Belo LourencoClaudio Belo Lourencohttps://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/401set logic to ALL_SUPPORTED for CVC42020-02-13T12:00:44+01:00MARCHE Claudeset logic to ALL_SUPPORTED for CVC4replace the hardcoded logic AUFBVDTFPNIRA by ALL_SUPPORTED
this requires:
* fix the driver for the built-in sqrt function on real numbers
* decide from which version of CVC4 this is accepted. Maybe only from version 1.7replace the hardcoded logic AUFBVDTFPNIRA by ALL_SUPPORTED
this requires:
* fix the driver for the built-in sqrt function on real numbers
* decide from which version of CVC4 this is accepted. Maybe only from version 1.71.3.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/400Improve shape structures2019-10-25T16:55:23+02:00Guillaume MelquiondImprove shape structuresAs explained by @paskevyc in #276, the following could improve the situation with respect to the part of the shapes that is really needed for pairing:
"The idea is that a transformation that produces several tasks that only differ in pr...As explained by @paskevyc in #276, the following could improve the situation with respect to the part of the shapes that is really needed for pairing:
"The idea is that a transformation that produces several tasks that only differ in premises (e.g., destruct or split_vc when the goal is no more splittable) should mark these differing premises, and only them, to be included into the shape."https://gitlab.inria.fr/why3/why3/-/issues/399`apply with` and `rewrite with` should give more details (e.g., quantifier na...2019-10-28T12:38:53+01:00Guillaume Melquiond`apply with` and `rewrite with` should give more details (e.g., quantifier names) when the number of arguments do not matchhttps://gitlab.inria.fr/why3/why3/-/issues/398Modifying source in IDE should remove error marks2019-11-08T14:54:28+01:00Guillaume MelquiondModifying source in IDE should remove error marks1.3.0https://gitlab.inria.fr/why3/why3/-/issues/397Allow modifying colors directly in IDE2019-11-10T16:41:34+01:00Guillaume MelquiondAllow modifying colors directly in IDEhttps://gitlab.inria.fr/why3/why3/-/issues/396Fix module cloning with respect to effects2021-02-05T14:26:32+01:00Guillaume MelquiondFix module cloning with respect to effectsAndrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/395Extraction using a driver on the extracted file2019-10-17T16:27:59+02:00DAILLER SylvainExtraction using a driver on the extracted fileI am trying to use `why3extract` and a custom driver to extract a Why3 module that would partly depends on an OCaml implementation. I cannot manage to use the driver to change the extraction of this module with the driver.
My file `a.ml...I am trying to use `why3extract` and a custom driver to extract a Why3 module that would partly depends on an OCaml implementation. I cannot manage to use the driver to change the extraction of this module with the driver.
My file `a.mlw` is as follows:
```
module A
type a
val eq_elt (e1 e2: a) : bool
ensures { e1 = e2 <-> result}
end
```
I took the driver `ocaml64.drv` which I copied (into `driver/ocaml_ext.drv` and added the following at the end:
```
module a.A
syntax val eq_elt "TODO"
end
```
I tried to extract with the following command:
`why3 extract --modular -D driver/ocaml_ext.drv a.mlw -o todo1`
I first get:
`Library file not found: a`
So, I added the option "-L ." to workaround this problem then the driver is read with no problems but, during printing, I get:
`Symbol eq_elt cannot be extracted`
I looked in more details and it seems that in this case, the extraction reads the file `a.mlw` twice: once as a library which is used to fill the syntax map during the driver parsing; and once during the printing of the file `a.mlw`. This leads to the element `eq_elt` being generated twice and the extraction using the second one instead of the first when trying to query the syntax map.
I have a solution which would ensures that this cannot happen by calling both the file and the libraries with the same memoized call (`Env.read_library`) but I am not sure this is how the code was intended.
So, is there currently a way to do what I tried ? If not, is it something that should be allowed ? If yes, a solution is to read all files with read_library (seems to register its result) instead of read_file (seems not to register its result). Does this look like a good enough solution ?
PS: I looked at 1-2 examples that use why3 extract but they do not seem to need this kind of extraction.https://gitlab.inria.fr/why3/why3/-/issues/394Warning on useless exception catching2019-11-08T09:19:06+01:00DAILLER SylvainWarning on useless exception catchingThis is a feature request and I don't know if it would easily be doable (it seems to be possible as the converse is notified to the user: exceptions that are raised but not caught must appear in the `raises` contract).
In the following,...This is a feature request and I don't know if it would easily be doable (it seems to be possible as the converse is notified to the user: exceptions that are raised but not caught must appear in the `raises` contract).
In the following, I would like a warning on the last line telling me that `TODO` is caught but never raised:
```
use int.Int
use ref.Ref
exception TODO
exception TODO2
let f (a: ref int)
ensures { !a = 3 }
=
try raise TODO2 with
| TODO2 -> a := 3
| TODO -> a := 4 end
```