why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2021-03-12T17:45:52Zhttps://gitlab.inria.fr/why3/why3/-/issues/387Cloning: please improve syntax and error messages2021-03-12T17:45:52ZMARCHE ClaudeCloning: please improve syntax and error messagesSee the following example file.
1. in the first case, the error message should be much more explicit on why the instantiation is illegal
2. in the second case: the syntax `val function` seems not supported though it should be natural
3. in the third case it works but: one would expect that only the program symbol would be substituted. the goal afterwards is proved (e.g by Alt-Ergo) and so the logic symbol is also substituted, which is just unexpected
```
module M
type t
val function f t : t
end
module N
use int.Int
function g (x:int) : int = x+1
(* give `Illegal instantiation for symbol f`
clone M
with type t = int, function f = g
*)
let function h (x:int) : int = x+1
(* give ` syntax error` (on lexeme `function`)
clone M
with type t = int, val function f = h
*)
clone M
with type t = int, val f = h
goal test: g 41 = 42
end
```See the following example file.
1. in the first case, the error message should be much more explicit on why the instantiation is illegal
2. in the second case: the syntax `val function` seems not supported though it should be natural
3. in the third case it works but: one would expect that only the program symbol would be substituted. the goal afterwards is proved (e.g by Alt-Ergo) and so the logic symbol is also substituted, which is just unexpected
```
module M
type t
val function f t : t
end
module N
use int.Int
function g (x:int) : int = x+1
(* give `Illegal instantiation for symbol f`
clone M
with type t = int, function f = g
*)
let function h (x:int) : int = x+1
(* give ` syntax error` (on lexeme `function`)
clone M
with type t = int, val function f = h
*)
clone M
with type t = int, val f = h
goal test: g 41 = 42
end
```1.4.0Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/392Allow changing foreground color in source on error2021-02-15T15:54:26ZDAILLER SylvainAllow changing foreground color in source on errorCurrently, its not possible to do this change AFAIK. And, the gconfig.error_color parameter is used both for the error message (bottom right corner) and for the source coloring.Currently, its not possible to do this change AFAIK. And, the gconfig.error_color parameter is used both for the error message (bottom right corner) and for the source coloring.1.3.0DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/325Extraction of partial applications2020-06-02T08:57:16ZRaphaël Rieu-HelftExtraction of partial applicationsExtraction of partial applications fails at least in the following case
```
let f (ghost x1 : int) (x2:int) (x3:int) = 53
let main () =
let g = f 1 in
let h = g 2 in
h 3
```
We should also add constructors to Mltree to differentiate between total and partial application.Extraction of partial applications fails at least in the following case
```
let f (ghost x1 : int) (x2:int) (x3:int) = 53
let main () =
let g = f 1 in
let h = g 2 in
h 3
```
We should also add constructors to Mltree to differentiate between total and partial application.Raphaël Rieu-HelftRaphaël Rieu-Helfthttps://gitlab.inria.fr/why3/why3/-/issues/42Invalid_argument('Expr.let_rec") in clone declarations2020-03-17T00:18:27ZRaphaël Rieu-HelftInvalid_argument('Expr.let_rec") in clone declarationsIn a large clone declaration containing `val x = y` where `x` is a `val constant` and y is a `let ghost constant` , I received the error `Invalid_argument("Expr.let_rec")`. My attempts to reproduce on smaller examples were not rejected at all.In a large clone declaration containing `val x = y` where `x` is a `val constant` and y is a `let ghost constant` , I received the error `Invalid_argument("Expr.let_rec")`. My attempts to reproduce on smaller examples were not rejected at all.1.3.0Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/168Cloning function with bad ghost status raises Invalid_argument("Expr.let_rec")2020-03-17T00:18:26ZPARREIRA PEREIRA Mário JoséCloning function with bad ghost status raises Invalid_argument("Expr.let_rec")The following fails with anomaly: Invalid_argument("Expr.let_rec")
```
module A
type t
val f (ghost x: t) : t
let rec ff (ghost x: t) = f x
end
module B
let f (x: int) = 42
clone A with val f, type t = int
end
```
The error message points to the `clone` line. Removing the `rec` keyword from the definition of `ff`, or stating the argument `x`, of function `f` in module B, as ghost removes the problem.
The error message is a little cryptic, and I don't fully understand why this only happens when we call `f` inside a `let rec` definition.The following fails with anomaly: Invalid_argument("Expr.let_rec")
```
module A
type t
val f (ghost x: t) : t
let rec ff (ghost x: t) = f x
end
module B
let f (x: int) = 42
clone A with val f, type t = int
end
```
The error message points to the `clone` line. Removing the `rec` keyword from the definition of `ff`, or stating the argument `x`, of function `f` in module B, as ghost removes the problem.
The error message is a little cryptic, and I don't fully understand why this only happens when we call `f` inside a `let rec` definition.1.3.0Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/420The behavior of Ctrl-Down is not user-friendly2020-03-06T12:22:18ZRaphaël Rieu-HelftThe behavior of Ctrl-Down is not user-friendlyOn the following file, apply `split_vc` on main and on subgoal 0, and prove subgoal 1 by calling a prover.
```
use int.Int
let f () : unit requires { 1 + 1 = 2 /\ 2 + 2 = 4 } = ()
let main () = f(); f(); f()
```
Assume that we want to save the proof of subgoal 0 for later. The navigation between goals with Ctrl-Up/Down becomes very painful. We can observe two issues:
- When selecting a subgoal of goal 0, pressing Ctrl-Down only cycles between subgoals 0.0 and 0.1, never reaching subgoal 2.
- When selecting subgoal 1, pressing Ctrl-Down jumps back up to 0.0 instead of going to 2.On the following file, apply `split_vc` on main and on subgoal 0, and prove subgoal 1 by calling a prover.
```
use int.Int
let f () : unit requires { 1 + 1 = 2 /\ 2 + 2 = 4 } = ()
let main () = f(); f(); f()
```
Assume that we want to save the proof of subgoal 0 for later. The navigation between goals with Ctrl-Up/Down becomes very painful. We can observe two issues:
- When selecting a subgoal of goal 0, pressing Ctrl-Down only cycles between subgoals 0.0 and 0.1, never reaching subgoal 2.
- When selecting subgoal 1, pressing Ctrl-Down jumps back up to 0.0 instead of going to 2.Raphaël Rieu-HelftRaphaël Rieu-Helfthttps://gitlab.inria.fr/why3/why3/-/issues/452Update gallery2020-03-04T15:56:19ZGuillaume MelquiondUpdate gallerySee at the bottom of `misc/release.md` for instructions about gallery generation.
:warning: Never commit all the modified files of the generated gallery. Only commit the few examples that you have just added to `examples.rc`.
Examples that are not yet part of the gallery:
- [x] `array_most_frequent`
- [x] `bignum` (too simple)
- [x] `coincidence_count_list`
- [x] `cubic_root`
- [x] `cursor_examples`
- [x] `equality_up_to_spaces`
- [x] `huffman_with_two_queues`
- [x] (Claude) `isqrt_von_neumann`
- [x] `leftist_heap`
- [x] `list_removal`
- [x] `min_max`
- [x] (Claude) `nistonacci`
- [x] `pairing_heap`
- [x] `pairing_heap_bin`
- [x] `queue_two_lists`
- [x] `simple_queue` (renamed `ring_buffer`)
- [x] `string_base64_encoding`
- [x] `string_hex_encoding`
- [x] `string_search` (to be completed first)
- [x] `subsequence`
- [x] (Claude) `sumrange`
- [x] `white_and_black_balls`
- [x] `word_common_factor`
Multi-file examples that are not yet part of the gallery:
- [x] (outdated) `bitvectors`
- [x] (outdated) `foveoos11-cm`
Multi-file examples that need updating:
- [x] `multiprecision`
Multi-file examples that seem up-to-date but use an antediluvian documentation:
- [x] (Claude) `double_wp`
- [x] (Claude) `verifythis_2016_matrix_multiplication`See at the bottom of `misc/release.md` for instructions about gallery generation.
:warning: Never commit all the modified files of the generated gallery. Only commit the few examples that you have just added to `examples.rc`.
Examples that are not yet part of the gallery:
- [x] `array_most_frequent`
- [x] `bignum` (too simple)
- [x] `coincidence_count_list`
- [x] `cubic_root`
- [x] `cursor_examples`
- [x] `equality_up_to_spaces`
- [x] `huffman_with_two_queues`
- [x] (Claude) `isqrt_von_neumann`
- [x] `leftist_heap`
- [x] `list_removal`
- [x] `min_max`
- [x] (Claude) `nistonacci`
- [x] `pairing_heap`
- [x] `pairing_heap_bin`
- [x] `queue_two_lists`
- [x] `simple_queue` (renamed `ring_buffer`)
- [x] `string_base64_encoding`
- [x] `string_hex_encoding`
- [x] `string_search` (to be completed first)
- [x] `subsequence`
- [x] (Claude) `sumrange`
- [x] `white_and_black_balls`
- [x] `word_common_factor`
Multi-file examples that are not yet part of the gallery:
- [x] (outdated) `bitvectors`
- [x] (outdated) `foveoos11-cm`
Multi-file examples that need updating:
- [x] `multiprecision`
Multi-file examples that seem up-to-date but use an antediluvian documentation:
- [x] (Claude) `double_wp`
- [x] (Claude) `verifythis_2016_matrix_multiplication`1.3.0Jean-Christophe FilliâtreJean-Christophe Filliâtrehttps://gitlab.inria.fr/why3/why3/-/issues/450Wrong smtlib file generation for ieee_float.FloatXX.in_range (at least) for CVC42020-03-04T09:36:51ZGhost UserWrong smtlib file generation for ieee_float.FloatXX.in_range (at least) for CVC4On the following example:
```why3
module Cvc4Bug
use ieee_float.Float32
goal G: in_range 0.0
end
```
The following command fails:
```
$ why3 prove cvc4_bug.mlw -P cvc4
cvc4_bug.mlw Cvc4Bug G: HighFailure (0.03s, 36 steps)
Prover exit status: exited with status 1
Prover output:
(error "expecting an integer subterm")
...
```
Apparently, `in_range` is transformed into `abs 0.0` which requires an int. Note that on Why3 1.2.1, the file contains a definition `abs1` for real numbers, but the generated goal uses `abs` (leading to the same error). If `in_range` is used in a lemma or an axiom, the same bug happens.On the following example:
```why3
module Cvc4Bug
use ieee_float.Float32
goal G: in_range 0.0
end
```
The following command fails:
```
$ why3 prove cvc4_bug.mlw -P cvc4
cvc4_bug.mlw Cvc4Bug G: HighFailure (0.03s, 36 steps)
Prover exit status: exited with status 1
Prover output:
(error "expecting an integer subterm")
...
```
Apparently, `in_range` is transformed into `abs 0.0` which requires an int. Note that on Why3 1.2.1, the file contains a definition `abs1` for real numbers, but the generated goal uses `abs` (leading to the same error). If `in_range` is used in a lemma or an axiom, the same bug happens.1.3.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/401set logic to ALL_SUPPORTED for CVC42020-02-13T11:00:44ZMARCHE 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/374eliminate_if transformation explodes2019-12-10T11:59:00ZJohannes Kanigeliminate_if transformation explodes[lexer__read_token.mlw](/uploads/1401f6eea89f1d461211f6cb8e6b6e8e/lexer__read_token.mlw)
On the attached file, eliminate_if creates a huge formula (20M nodes??) starting from a very small one (less than 200 nodes).
This should reproduce on master using this command: `why3 prove lexer__read_token.mlw -P alt-ergo`[lexer__read_token.mlw](/uploads/1401f6eea89f1d461211f6cb8e6b6e8e/lexer__read_token.mlw)
On the attached file, eliminate_if creates a huge formula (20M nodes??) starting from a very small one (less than 200 nodes).
This should reproduce on master using this command: `why3 prove lexer__read_token.mlw -P alt-ergo`Quentin GarcheryQuentin Garcheryhttps://gitlab.inria.fr/why3/why3/-/issues/300Add file from IDE is broken2019-11-20T07:57:04ZDAILLER SylvainAdd file from IDE is brokenHello,
When I have two files a.mlw and b.mlw in the same directory in the filesystem and the session for a.mlw in a/why3session.xml as usual. If I try to open why3ide on a.mlw and then add file b.mlw, I get an error in the "Messages" stating (cannot open a/../home/dailler/b.mlw). I think this is a problem with Sysutil.relativize_filename.Hello,
When I have two files a.mlw and b.mlw in the same directory in the filesystem and the session for a.mlw in a/why3session.xml as usual. If I try to open why3ide on a.mlw and then add file b.mlw, I get an error in the "Messages" stating (cannot open a/../home/dailler/b.mlw). I think this is a problem with Sysutil.relativize_filename.MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/381Make sure that Str is not used in places that trywhy3 uses2019-11-14T11:31:49ZRaphaël Rieu-HelftMake sure that Str is not used in places that trywhy3 uses`js_of_ocaml` does not support `Str`, which is used in Why3 in several places. We should:
- check that `Str` is still not used in places that `trywhy3` actually uses
- try to find a way to prevent future misuses of `Str`, ideally at compile time or as part of the CI process.`js_of_ocaml` does not support `Str`, which is used in Why3 in several places. We should:
- check that `Str` is still not used in places that `trywhy3` actually uses
- try to find a way to prevent future misuses of `Str`, ideally at compile time or as part of the CI process.Guillaume MelquiondGuillaume Melquiondhttps://gitlab.inria.fr/why3/why3/-/issues/222syntax function in extraction drivers2019-11-13T10:06:25ZJean-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.Benedikt BeckerBenedikt Beckerhttps://gitlab.inria.fr/why3/why3/-/issues/283module appmap.AppMap should propose *finite domain* maps2019-11-12T14:06:51ZMARCHE Claudemodule appmap.AppMap should propose *finite domain* mapsthe module appmap.AppMap is an interface for maps without domain. It should be an interface for maps of finite domain only.
Moreover, it should take the equality on the type of keys as parameterthe module appmap.AppMap is an interface for maps without domain. It should be an interface for maps of finite domain only.
Moreover, it should take the equality on the type of keys as parameter1.3.0Jean-Christophe FilliâtreJean-Christophe Filliâtrehttps://gitlab.inria.fr/why3/why3/-/issues/384Named results shadow parameter names2019-11-12T13:27:22ZRaphaël Rieu-HelftNamed results shadow parameter namesIf the result of a function is named with the same name as a parameter of the function, it becomes impossible to refer to this parameter in the ensures. I think it should be forbidden to give the result the same name as a parameter.
```
let samename (x:uint64) : (x:uint64)
requires { x = 1 }
ensures { x = 3 }
= 3
```If the result of a function is named with the same name as a parameter of the function, it becomes impossible to refer to this parameter in the ensures. I think it should be forbidden to give the result the same name as a parameter.
```
let samename (x:uint64) : (x:uint64)
requires { x = 1 }
ensures { x = 3 }
= 3
```DIVERIO DiegoDIVERIO Diegohttps://gitlab.inria.fr/why3/why3/-/issues/406avoid jumping after deleting a detached subgoal2019-11-12T08:33:44ZLAWALL 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/397Allow modifying colors directly in IDE2019-11-10T15:41:34ZGuillaume MelquiondAllow modifying colors directly in IDEDAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/385Choice of MLMPFR2019-11-08T19:39:04ZFrançois BobotChoice of MLMPFRIs there a specific reason why the binding mlmpfr has been chosen? mlgmpidl is better configured (it links `-lmpfr` automatically). Other binding exists and mlmpfr could be of course fixed.
https://github.com/thvnx/mlmpfr/issues/5Is there a specific reason why the binding mlmpfr has been chosen? mlgmpidl is better configured (it links `-lmpfr` automatically). Other binding exists and mlmpfr could be of course fixed.
https://github.com/thvnx/mlmpfr/issues/5MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/388Rename `axiom` into `hypothesis` in task printing2019-11-08T18:07:28ZMARCHE ClaudeRename `axiom` into `hypothesis` in task printingI wanted to suggest that for a very long time. The question asked by Burkhart at the seminar this morning shows clearly that it must be doneI wanted to suggest that for a very long time. The question asked by Burkhart at the seminar this morning shows clearly that it must be done1.3.0DIVERIO DiegoDIVERIO Diegohttps://gitlab.inria.fr/why3/why3/-/issues/398Modifying source in IDE should remove error marks2019-11-08T13:54:28ZGuillaume MelquiondModifying source in IDE should remove error marks1.3.0DAILLER SylvainDAILLER Sylvain