why3 issueshttps://gitlab.inria.fr/why3/why3/issues2019-06-05T13:22:45Zhttps://gitlab.inria.fr/why3/why3/issues/334Missing warning for useless pattern in quantifier.2019-06-05T13:22:45ZLéo AndrèsMissing warning for useless pattern in quantifier.When writing
```ml
invariant { forall k. true }
```
We got: `This variable has polymorphic type 'xi2 where type variable 'xi2 is never
named explicitly`.
When doing:
```ml
invariant { forall k: int. true }
```
We got: `unused variable k`.
But when doing:
```ml
invariant { forall _: int. true }
```
There's nothing displayed. I don't see a case where one would do this on purpose, so adding a warning seems like something we could do.When writing
```ml
invariant { forall k. true }
```
We got: `This variable has polymorphic type 'xi2 where type variable 'xi2 is never
named explicitly`.
When doing:
```ml
invariant { forall k: int. true }
```
We got: `unused variable k`.
But when doing:
```ml
invariant { forall _: int. true }
```
There's nothing displayed. I don't see a case where one would do this on purpose, so adding a warning seems like something we could do.https://gitlab.inria.fr/why3/why3/issues/332[patch] teach Array.append to Pinterp2019-06-06T09:58:33ZSCHERER Gabriel[patch] teach Array.append to PinterpI'm going through the why3 tutorial in the manual, now at the MaxAndSum problem ( http://why3.lri.fr/doc/whyml.html#sec17 ). The manual does not give an example of how to actually test the program! I wrote some test code
```ocaml
let test () =
let one x = Array.make 1 x in
let (++) a b = Array.append a b in
max_sum (one 1 ++ one 3 ++ one 2)
```
and I found some documentation in how to actually run the test in section 7.1 ( http://why3.lri.fr/doc/exec.html#sec101 ). But running my test code (which is different from the one in 7.1) exhibits the following behavior:
```
File "../buffer/max_and_sum.mlw", line 3, characters 2-20:
warning: the keyword `import' is redundant here and can be omitted
File "../buffer/max_and_sum.mlw", line 4, characters 2-20:
warning: the keyword `import' is redundant here and can be omitted
File "../buffer/max_and_sum.mlw", line 5, characters 2-24:
warning: the keyword `import' is redundant here and can be omitted
Execution of MaxAndSum.test ():
type: (int, int)
anomaly: Why3.Pinterp.CannotCompute
```
After scratching my head, I figured out that the problem is with the Array.append function, which is defined as a built-in in the standard library. The following patch (suitable for `git am` application)
[0001-teach-Array.append-to-Pinterp.patch](/uploads/1b66a911b50c092a939425898b7eb606/0001-teach-Array.append-to-Pinterp.patch)
lets pinterp.ml know about Array.append, and now my code above successfully computes the expected result.
## Question
There is also a `mlinterp.ml` file which looks very similar and also lacks an `Array.append` primitive. What is this file used for? Should I also add the primitive there?I'm going through the why3 tutorial in the manual, now at the MaxAndSum problem ( http://why3.lri.fr/doc/whyml.html#sec17 ). The manual does not give an example of how to actually test the program! I wrote some test code
```ocaml
let test () =
let one x = Array.make 1 x in
let (++) a b = Array.append a b in
max_sum (one 1 ++ one 3 ++ one 2)
```
and I found some documentation in how to actually run the test in section 7.1 ( http://why3.lri.fr/doc/exec.html#sec101 ). But running my test code (which is different from the one in 7.1) exhibits the following behavior:
```
File "../buffer/max_and_sum.mlw", line 3, characters 2-20:
warning: the keyword `import' is redundant here and can be omitted
File "../buffer/max_and_sum.mlw", line 4, characters 2-20:
warning: the keyword `import' is redundant here and can be omitted
File "../buffer/max_and_sum.mlw", line 5, characters 2-24:
warning: the keyword `import' is redundant here and can be omitted
Execution of MaxAndSum.test ():
type: (int, int)
anomaly: Why3.Pinterp.CannotCompute
```
After scratching my head, I figured out that the problem is with the Array.append function, which is defined as a built-in in the standard library. The following patch (suitable for `git am` application)
[0001-teach-Array.append-to-Pinterp.patch](/uploads/1b66a911b50c092a939425898b7eb606/0001-teach-Array.append-to-Pinterp.patch)
lets pinterp.ml know about Array.append, and now my code above successfully computes the expected result.
## Question
There is also a `mlinterp.ml` file which looks very similar and also lacks an `Array.append` primitive. What is this file used for? Should I also add the primitive there?MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/issues/331Extraction of pattern contained in driver2019-06-25T09:37:47ZPARREIRA PEREIRA Mário JoséExtraction of pattern contained in driverThe following example:
```
use list.List
type t = T (list int)
let f (t: t) = match t with T (Cons x Nil) -> x | _ -> absurd end
```
gets extracted to:
```
type t =
| T of (Z.t) list
let f (t1: t) : Z.t =
match t1 with
| T x :: [] -> x
| _ -> assert false (* absurd *)
```
Since `Cons` is defined in the driver as `%1 :: %2`, the OCaml printer does not put the needed parentheses around `x :: []`.The following example:
```
use list.List
type t = T (list int)
let f (t: t) = match t with T (Cons x Nil) -> x | _ -> absurd end
```
gets extracted to:
```
type t =
| T of (Z.t) list
let f (t1: t) : Z.t =
match t1 with
| T x :: [] -> x
| _ -> assert false (* absurd *)
```
Since `Cons` is defined in the driver as `%1 :: %2`, the OCaml printer does not put the needed parentheses around `x :: []`.Raphaël Rieu-HelftRaphaël Rieu-Helfthttps://gitlab.inria.fr/why3/why3/issues/329Missing lots of standard modules in the documentation2019-06-05T20:37:51ZGuillaume MelquiondMissing lots of standard modules in the documentationThe following WhyML modules are not documented (see the `stdlibdoc` target in [Makefile.in](Makefile.in)):
- `cursor`, `debug`, `exn`, `for_drivers`, `function`, `io`, `null`, `ocaml`, `regexp`, `tptp`, `tree`
- `mach/`: `bv`, `c`, `float`, `fxp`, `tagset`
Some of them are presumably not documented on purpose (e.g., `for_drivers`) and they should be explicitly marked as such. The other ones are in need of documentation.The following WhyML modules are not documented (see the `stdlibdoc` target in [Makefile.in](Makefile.in)):
- `cursor`, `debug`, `exn`, `for_drivers`, `function`, `io`, `null`, `ocaml`, `regexp`, `tptp`, `tree`
- `mach/`: `bv`, `c`, `float`, `fxp`, `tagset`
Some of them are presumably not documented on purpose (e.g., `for_drivers`) and they should be explicitly marked as such. The other ones are in need of documentation.1.3.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/issues/328[patch] why3 tutorial: use numbered list for Einstein hints2019-06-05T14:39:02ZSCHERER Gabriel[patch] why3 tutorial: use numbered list for Einstein hintsPlease see the attached patch suitable for `git am` application:
[0001-why3-manual-Einstein-problem-use-a-numbered-list-for.patch](/uploads/acc6c0e1d376b4c0b7493f2373091380/0001-why3-manual-Einstein-problem-use-a-numbered-list-for.patch).
I could send this (small) patch as a Merge Request directly, but only because I happen to be an INRIA employee. For other contributors, using gitlab.inria.fr does not let them create Merge Requests, leading to the creation of forks on other hosting platforms (for example https://github.com/kit-ty-kate/why3). In solidarity to these suppressed contributors, I won't use the Merge Request feature myself. I think it would be nice to consider using a platform that is actually open to external contributors, for example https://framagit.org/ (also gitlab, also the Open Source version)
Please see the attached patch suitable for `git am` application:
[0001-why3-manual-Einstein-problem-use-a-numbered-list-for.patch](/uploads/acc6c0e1d376b4c0b7493f2373091380/0001-why3-manual-Einstein-problem-use-a-numbered-list-for.patch).
I could send this (small) patch as a Merge Request directly, but only because I happen to be an INRIA employee. For other contributors, using gitlab.inria.fr does not let them create Merge Requests, leading to the creation of forks on other hosting platforms (for example https://github.com/kit-ty-kate/why3). In solidarity to these suppressed contributors, I won't use the Merge Request feature myself. I think it would be nice to consider using a platform that is actually open to external contributors, for example https://framagit.org/ (also gitlab, also the Open Source version)
https://gitlab.inria.fr/why3/why3/issues/327Anomaly when trying to locally open a non-imported module2019-07-29T08:28:06ZPARREIRA PEREIRA Mário JoséAnomaly when trying to locally open a non-imported moduleWhen I try to "locally open" a module to evaluate an expression, if that module is not imported then Why3 fails with `anomaly: Not_found`.
The following one-line program is enough in order to reproduce the problem:
```
let f (x: int) = Z.(x)
```When I try to "locally open" a module to evaluate an expression, if that module is not imported then Why3 fails with `anomaly: Not_found`.
The following one-line program is enough in order to reproduce the problem:
```
let f (x: int) = Z.(x)
```https://gitlab.inria.fr/why3/why3/issues/326extraction of records fields used as functions2019-06-07T12:09:06ZLéo Andrèsextraction of records fields used as functionsThe following is allowed by Why3:
```ml
use int.Int
type t = {
is_p: bool;
n: int;
}
let f (x: t) (pred: t -> bool) : int
=
if pred x then x.n else 0
let g () =
f { is_p = true; n = 42 } is_p
```
But then, when extracted using:
```sh
why3 extract -L . -D ocaml64 --recursive f.mlw -o f.ml
ocamlfind ocamlopt -package zarith -c -i f.ml
```
Here's the generated OCaml file:
```ml
type t = {
is_p: bool;
n: Z.t;
}
let f (x: t) (pred: t -> (bool)) : Z.t =
if pred x then begin x.n end else begin Z.zero end
let g (_: unit) : Z.t = f ({ is_p = true; n = (Z.of_string "42") }) is_p
```
The `is_p` on the last line should be replaced by `(fun el -> el.is_p)`, otherwise it fails with this error:
```sh
why3 extract -L . -D ocaml64 --recursive f.mlw -o f.ml
ocamlfind ocamlopt -package zarith -c -i f.ml
File "f.ml", line 9, characters 68-72:
Error: Unbound value is_p
make: *** [Makefile:4: extract] Error 2
```The following is allowed by Why3:
```ml
use int.Int
type t = {
is_p: bool;
n: int;
}
let f (x: t) (pred: t -> bool) : int
=
if pred x then x.n else 0
let g () =
f { is_p = true; n = 42 } is_p
```
But then, when extracted using:
```sh
why3 extract -L . -D ocaml64 --recursive f.mlw -o f.ml
ocamlfind ocamlopt -package zarith -c -i f.ml
```
Here's the generated OCaml file:
```ml
type t = {
is_p: bool;
n: Z.t;
}
let f (x: t) (pred: t -> (bool)) : Z.t =
if pred x then begin x.n end else begin Z.zero end
let g (_: unit) : Z.t = f ({ is_p = true; n = (Z.of_string "42") }) is_p
```
The `is_p` on the last line should be replaced by `(fun el -> el.is_p)`, otherwise it fails with this error:
```sh
why3 extract -L . -D ocaml64 --recursive f.mlw -o f.ml
ocamlfind ocamlopt -package zarith -c -i f.ml
File "f.ml", line 9, characters 68-72:
Error: Unbound value is_p
make: *** [Makefile:4: extract] Error 2
```PARREIRA PEREIRA Mário JoséPARREIRA PEREIRA Mário Joséhttps://gitlab.inria.fr/why3/why3/issues/324Let-functions without non-ghost arguments2019-06-25T09:37:00ZRaphaël Rieu-HelftLet-functions without non-ghost argumentsThe following example is miscompiled because `Compile` treats RLnone and RLls differently.
```
use int.Int
let function f (ghost x:int) = 42
let main () =
let y = f 26 in
y + 2
```The following example is miscompiled because `Compile` treats RLnone and RLls differently.
```
use int.Int
let function f (ghost x:int) = 42
let main () =
let y = f 26 in
y + 2
```1.3.0Raphaël Rieu-HelftRaphaël Rieu-Helfthttps://gitlab.inria.fr/why3/why3/issues/323Allow Coq proof using why3prove only2019-10-25T14:22:29ZDAILLER SylvainAllow Coq proof using why3prove onlyIt could be useful to allow doing Coq proof from the command line with Why3prove in the following way:
```
why3prove -P coq foo.mlw -o bar
coqide -R path_to_why3 Why3 bar/*.mlw
why3replay foo
```
The only missing piece seems to be that why3prove does not update the session in the first step.It could be useful to allow doing Coq proof from the command line with Why3prove in the following way:
```
why3prove -P coq foo.mlw -o bar
coqide -R path_to_why3 Why3 bar/*.mlw
why3replay foo
```
The only missing piece seems to be that why3prove does not update the session in the first step.https://gitlab.inria.fr/why3/why3/issues/322Error ident renaming2019-12-03T11:08:21ZDAILLER SylvainError ident renamingWhen reloading after a typing error occurs, the error message increments the disambiguation of the ident.
For example, in the following code:
```
module Ex2
use array.Array
use int.Int
use option.Option
val my_set: array (option int) -> int -> option int -> unit
let rec my_fact (mem: array (option int)) (n: int): int
=
match mem[n] with
| None -> let r = n * my_fact mem (n- 1) in
my_set mem n (Some r);
r
| Some n -> n
end
end
```
The error is (after 8 reloads):
` line 154, characters 10-17: The type of this function contains an alias with external variable my_set8`
I think we managed to solve (or mitigate) this problem in the past for typing error of transformations: it is possible that it does not work anymore either.When reloading after a typing error occurs, the error message increments the disambiguation of the ident.
For example, in the following code:
```
module Ex2
use array.Array
use int.Int
use option.Option
val my_set: array (option int) -> int -> option int -> unit
let rec my_fact (mem: array (option int)) (n: int): int
=
match mem[n] with
| None -> let r = n * my_fact mem (n- 1) in
my_set mem n (Some r);
r
| Some n -> n
end
end
```
The error is (after 8 reloads):
` line 154, characters 10-17: The type of this function contains an alias with external variable my_set8`
I think we managed to solve (or mitigate) this problem in the past for typing error of transformations: it is possible that it does not work anymore either.https://gitlab.inria.fr/why3/why3/issues/321"val" differenciation question2019-05-23T06:51:11ZDAILLER Sylvain"val" differenciation questionHello,
This is probably a naive question. In the following simple program, there is a difference of behavior between the two `val` I am using. Is that intentional ? Am I using this wrong ?
The commented version works fine whereas there is an error for the uncommented one.
```
module Ex1
use array.Array
use int.Int
use option.Option
val my_set: array (option int) -> int -> option int -> unit
(* val my_set (m: array (option int)) (i: int) (e: option int) : unit*)
let rec my_fact (mem: array (option int)) (n: int): int
=
match mem[n] with
| None -> let r = n * my_fact mem (n- 1) in
my_set mem n (Some r);
r
| Some n -> n
end
end
```Hello,
This is probably a naive question. In the following simple program, there is a difference of behavior between the two `val` I am using. Is that intentional ? Am I using this wrong ?
The commented version works fine whereas there is an error for the uncommented one.
```
module Ex1
use array.Array
use int.Int
use option.Option
val my_set: array (option int) -> int -> option int -> unit
(* val my_set (m: array (option int)) (i: int) (e: option int) : unit*)
let rec my_fact (mem: array (option int)) (n: int): int
=
match mem[n] with
| None -> let r = n * my_fact mem (n- 1) in
my_set mem n (Some r);
r
| Some n -> n
end
end
```https://gitlab.inria.fr/why3/why3/issues/320Preferences for no jumping around is not recorded2019-05-22T11:23:46ZDAILLER SylvainPreferences for no jumping around is not recordedDAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/issues/317Update library Queue2019-06-06T15:47:12ZMARCHE ClaudeUpdate library Queue1. queue.Queue: use sequences instead of lists for the specs
2. update the OCaml driver
3. update the 6 examples using queue.Queue1. queue.Queue: use sequences instead of lists for the specs
2. update the OCaml driver
3. update the 6 examples using queue.QueueLéo AndrèsLéo Andrèshttps://gitlab.inria.fr/why3/why3/issues/316extraction of references2019-05-27T12:53:51ZMARCHE Claudeextraction of referencesAn update to a reference `x <- e` is extracted (ocaml64) in two
different ways: Without using `--modular`, the result is simply
`x.contents <- e`. But when using `--modular`, the field of the
reference is qualified as `x.Why3__Ref.contents <- e`.
Is the latter intended, and is there a library that defines the module
Why3__Ref? Or does somebody have a pointer where the builtin reference
is substituted in the Why3 codebase?
(I am using the last week’s master branch of Why3.)
```
$ cat test.mlw
module Test
let ref x = ()
let f (y:unit) = x <- y
end
$ why3 extract -D ocaml64 -L . test.Test
let x = ref ()
let f (y: unit) : unit = x.contents <- y
$ why3 extract --modular -D ocaml64 -L . test.Test -o .
$ cat test__Test.ml
let x = ref ()
let f (y: unit) : unit = x.Why3__Ref.contents <- y
```An update to a reference `x <- e` is extracted (ocaml64) in two
different ways: Without using `--modular`, the result is simply
`x.contents <- e`. But when using `--modular`, the field of the
reference is qualified as `x.Why3__Ref.contents <- e`.
Is the latter intended, and is there a library that defines the module
Why3__Ref? Or does somebody have a pointer where the builtin reference
is substituted in the Why3 codebase?
(I am using the last week’s master branch of Why3.)
```
$ cat test.mlw
module Test
let ref x = ()
let f (y:unit) = x <- y
end
$ why3 extract -D ocaml64 -L . test.Test
let x = ref ()
let f (y: unit) : unit = x.contents <- y
$ why3 extract --modular -D ocaml64 -L . test.Test -o .
$ cat test__Test.ml
let x = ref ()
let f (y: unit) : unit = x.Why3__Ref.contents <- y
```1.3.0Raphaël Rieu-HelftRaphaël Rieu-Helfthttps://gitlab.inria.fr/why3/why3/issues/314Spurious "unused at/old" warning in lemma function parameters2019-06-05T14:53:25ZRaphaël Rieu-HelftSpurious "unused at/old" warning in lemma function parametersPassing a lemma function parameter in the form (pure { x at L }) seems to trigger a spurious "unused at/old" warning.
In the example below, the `at` operator at line 9 works as expected, but the following warning is emitted:
```
File "atold.mlw", line 9, characters 17-18:
warning: this `at'/`old' operator is never used
```
```
use int.Int
let lemma l (x:int) requires { x <> 0 } ensures { x * x > 0 } = ()
let f () =
let ref x = any int ensures { result <> 0 } in
label L in
x <- -3;
l (pure { x at L });
assert { (x at L) * (x at L) > 0 };
```Passing a lemma function parameter in the form (pure { x at L }) seems to trigger a spurious "unused at/old" warning.
In the example below, the `at` operator at line 9 works as expected, but the following warning is emitted:
```
File "atold.mlw", line 9, characters 17-18:
warning: this `at'/`old' operator is never used
```
```
use int.Int
let lemma l (x:int) requires { x <> 0 } ensures { x * x > 0 } = ()
let f () =
let ref x = any int ensures { result <> 0 } in
label L in
x <- -3;
l (pure { x at L });
assert { (x at L) * (x at L) > 0 };
```Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/issues/312Missing hypothesis when splitting a formula with if-then-else and by2019-12-09T14:33:06ZGARCHERY QuentinMissing hypothesis when splitting a formula with if-then-else and byConsider the following code :
```
use int.Int
use seq.Seq
let function dirac (a b : int) =
if b = a then 1 else 0
let rec function count (x : int) (seq : seq int)
variant { Seq.length seq }
=
if Seq.length seq = 0
then 0
else dirac x seq[0] + count x seq[1..]
lemma count_case :
forall x h, t : seq int.
(if x = h
then (count x (cons h t) = count x t + 1
by dirac x h = 1)
else (count x (cons h t) = count x t
by dirac x h = 0))
by (cons h t)[1..] == t
```
When trying to prove the generated VCs (after split_vc) corresponding to the if-branches in the lemma,
the hypothesis `(cons h t)[1..] == t` is missing from the context. This makes the solvers fail to prove
the VCs directly (at least on my machine, giving them a reasonable delay).Consider the following code :
```
use int.Int
use seq.Seq
let function dirac (a b : int) =
if b = a then 1 else 0
let rec function count (x : int) (seq : seq int)
variant { Seq.length seq }
=
if Seq.length seq = 0
then 0
else dirac x seq[0] + count x seq[1..]
lemma count_case :
forall x h, t : seq int.
(if x = h
then (count x (cons h t) = count x t + 1
by dirac x h = 1)
else (count x (cons h t) = count x t
by dirac x h = 0))
by (cons h t)[1..] == t
```
When trying to prove the generated VCs (after split_vc) corresponding to the if-branches in the lemma,
the hypothesis `(cons h t)[1..] == t` is missing from the context. This makes the solvers fail to prove
the VCs directly (at least on my machine, giving them a reasonable delay).https://gitlab.inria.fr/why3/why3/issues/311Transformation `destruct` should handle negation too2019-04-25T11:33:35ZMARCHE ClaudeTransformation `destruct` should handle negation tootitle says alltitle says allDAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/issues/310improve the reactivity of the IDE2019-06-05T21:13:40ZLAWALL Juliaimprove the reactivity of the IDEOn a machine with many cores, the goal of producing a backlog of verification conditions seems to cause the IDE to freeze, which is a bit tiresome for the user. It would be good if the IDE could wake up every 0.1 seconds, even if the backlog is still under construction.On a machine with many cores, the goal of producing a backlog of verification conditions seems to cause the IDE to freeze, which is a bit tiresome for the user. It would be good if the IDE could wake up every 0.1 seconds, even if the backlog is still under construction.DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/issues/309Exit status on un-proved goals2019-10-25T14:24:32ZLoïc CorrensonExit status on un-proved goalsWhen `why3 prove` leaves non proven goals, its exit status is `1`.
This is very confusing because this exit code is also used for syntax errors, incorrect command line arguments, etc.
Having an « unknown » goal is a normal outcome, and shall not be meld with syntactic errors!
Although, it can be interesting to known with an exit code whether all goals have been proven or not, and it shall be different from `1`. Better: what about some `-exit-unproved <n>` option on the command line, that would exit with status code `<n>` in this case?
Sincerely yours, L.When `why3 prove` leaves non proven goals, its exit status is `1`.
This is very confusing because this exit code is also used for syntax errors, incorrect command line arguments, etc.
Having an « unknown » goal is a normal outcome, and shall not be meld with syntactic errors!
Although, it can be interesting to known with an exit code whether all goals have been proven or not, and it shall be different from `1`. Better: what about some `-exit-unproved <n>` option on the command line, that would exit with status code `<n>` in this case?
Sincerely yours, L.https://gitlab.inria.fr/why3/why3/issues/307Add `(e at label)` as acceptable ghost code2019-04-20T12:02:23ZFrançois BobotAdd `(e at label)` as acceptable ghost codeThe `at` construction could be generalized from logic expression to ghost code. It would remove some need of `let ghost` construction which have their own restriction.The `at` construction could be generalized from logic expression to ghost code. It would remove some need of `let ghost` construction which have their own restriction.