why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2022-11-14T15:01:48+01:00https://gitlab.inria.fr/why3/why3/-/issues/411Rare GTK idle_expand_row crash2022-11-14T15:01:48+01:00Raphaël Rieu-HelftRare GTK idle_expand_row crashSomewhat regularly, `why3ide` crashes with the following error message followed by an abort.
`ERROR:/build/gtk+2.0-1aCJs4/gtk+2.0-2.24.31/modules/other/gail/gailtreeview.c:2314:idle_expand_row: code should not be reached`
This tends to ...Somewhat regularly, `why3ide` crashes with the following error message followed by an abort.
`ERROR:/build/gtk+2.0-1aCJs4/gtk+2.0-2.24.31/modules/other/gail/gailtreeview.c:2314:idle_expand_row: code should not be reached`
This tends to happen only with large sessions when why3ide has been running for a long time. Is this a Why3 bug or a GTK bug?https://gitlab.inria.fr/why3/why3/-/issues/251Emit a warning when "old" does nothing in a specification2021-07-13T16:40:01+02:00Raphaë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 for...```
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.1.4.0Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/445why3 commands not recognized on Cygwin+MinGW installation2020-02-25T11:36:40+01:00Ghost Userwhy3 commands not recognized on Cygwin+MinGW installationI installed fdopen's [OCaml for Windows](https://fdopen.github.io/opam-repository-mingw/installation/), which currently installs a `4.09.0+mingw64c` opam repository, and then installed the `why3` package. Installation went fine, but when...I installed fdopen's [OCaml for Windows](https://fdopen.github.io/opam-repository-mingw/installation/), which currently installs a `4.09.0+mingw64c` opam repository, and then installed the `why3` package. Installation went fine, but when I run `why3` with any command, it either does nothing, or does something weird. For instance:
```
$ why3 shell
$ why3 shell
Welcome to Why3 shell. Type 'help' for help.
$
```
The first time, it does nothing, and subsequently, it prints the message but opens no shell.
Trying any command with `--help` outputs the *general* usage message (i.e. the same as `why3 --help`, as if the `config` were not there):
```
$ why3 config --help
Usage: why3 [options]
... (rest omitted)
```
On Linux, the same command outputs the *specific* usage message for the `config` command:
```
Usage: why3 config [options]
... (rest omitted)
```
I cannot, for instance, configure why3, since `why3 config --detect` does nothing other than print the same usage message.
I tried adding `--debug-all`, but it prints nothing other than timing information at the end.
Is there a way to try debugging the issue on Cygwin+MinGW? Anything that could help obtain more details about what is going wrong would be useful (e.g. setting an environment variable, looking for specific binaries...).
I tried both why3 1.2.1 and why3 1.2.0, on switches `4.06.1+mingw64c`, `4.07.0+mingw64c`, and `4.09.0+mingw64c`, and in all cases I have the same issue.
I'm aware the problem may be related to the Windows-based opam repository, but if you could provide some basic information to help debugging, e.g. some sanity checks, it would be very helpful.1.3.0https://gitlab.inria.fr/why3/why3/-/issues/276Shape pairing is not stable2019-10-25T16:56:02+02:00Guillaume MelquiondShape pairing is not stableWhen several tasks have the same shape, the pairing algorithm is unable to properly associate old and new tasks. At the very least, it should preserve the original order of tasks.
(I tried to replace `List.sort` with `List.stable_sort` ...When several tasks have the same shape, the pairing algorithm is unable to properly associate old and new tasks. At the very least, it should preserve the original order of tasks.
(I tried to replace `List.sort` with `List.stable_sort` in `termcode.ml`. That didn't help.)1.3.0https://gitlab.inria.fr/why3/why3/-/issues/282Strategies should use split_vc instead of split_all_full2019-04-09T18:36:17+02:00MARCHE ClaudeStrategies should use split_vc instead of split_all_fullThis is a feature wish from Andrei
The strategies that split should split using ``split_vc`` instead of ``split_all_full``This is a feature wish from Andrei
The strategies that split should split using ``split_vc`` instead of ``split_all_full``1.3.0https://gitlab.inria.fr/why3/why3/-/issues/117transformation split_intros_goal_wp always produces a new subgoal2018-08-29T15:46:22+02:00Jean-Christophe Filliâtretransformation split_intros_goal_wp always produces a new subgoalTransformation split_intros_goal_wp always produces a new subgoal, even when it should instead report an absence of progrss.
As a consequence, strategy 1 loops forever on unprovable goals, repeatedly applying split_intros_goal_wp succes...Transformation split_intros_goal_wp always produces a new subgoal, even when it should instead report an absence of progrss.
As a consequence, strategy 1 loops forever on unprovable goals, repeatedly applying split_intros_goal_wp successfully then provers unsuccessfully.
To reproduce the issue, use an input file limited to "goal G: false" and launch strategy 1 from why3 ide.
Note: strategy "2", on the contrary, terminates. But it uses split_all_full instead.MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/9Uninstalled prover policies2018-05-28T15:39:15+02:00MARCHE ClaudeUninstalled prover policiesDuring a replay with "why3 replay", or in the GUI, the existing policies for uninstalled provers are applied as expected. however, when a prover without policy is met, the dialog for selecting a new policy appears as in former interface,...During a replay with "why3 replay", or in the GUI, the existing policies for uninstalled provers are applied as expected. however, when a prover without policy is met, the dialog for selecting a new policy appears as in former interface, but the selected policy is not taken into account immediately, but only after saving preferences and restarting
Implementing this is more complex than in former IDE because of the ITP server mechanism. We need a new query type to modify server config (Set_config_param only applies on the [main] record, too bad)MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/120simplify_trivial_quantification kills some goals2018-05-22T16:47:51+02:00Raphaël Rieu-Helftsimplify_trivial_quantification kills some goalsOn the following program, after using split_vc twice (once on the function and once on the assertion), the subgoal `not true` is generated by simplify_trivial_quantification. My understanding is that the goal `not z = y` is used to repla...On the following program, after using split_vc twice (once on the function and once on the assertion), the subgoal `not true` is generated by simplify_trivial_quantification. My understanding is that the goal `not z = y` is used to replace `z` with `y` when attempting to eliminate the quantified variable `z`, but I hope I am wrong.
```
let f (l: list int) (y:int)
= assert { match l with Cons z _ -> not z = y | Nil -> false end }
```
I'm marking this as high priority because `split_vc` is intended as a default strategy for most users.https://gitlab.inria.fr/why3/why3/-/issues/64Reloading in the IDE does not reload library modules2018-02-16T09:56:08+01:00Raphaël Rieu-HelftReloading in the IDE does not reload library modulesWith the IDE open, I made a change in a theory from stdlib that I was importing (adding an axiom). When reloading from within the IDE, this was not taken into account. Closing and reopening the IDE fixed the problem.With the IDE open, I made a change in a theory from stdlib that I was importing (adding an axiom). When reloading from within the IDE, this was not taken into account. Closing and reopening the IDE fixed the problem.MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/71Incorrect ident parsing in transformations2018-02-02T10:49:53+01:00Raphaël Rieu-HelftIncorrect ident parsing in transformationsIn each of the following examples, the output of `print (+)` is `function (+) real real: real` and (in M1) `cut (0 + 0 = 0)` fails with a typing error, when (+) should be the integer addition :
```
module M1
use import real.RealInfix
...In each of the following examples, the output of `print (+)` is `function (+) real real: real` and (in M1) `cut (0 + 0 = 0)` fails with a typing error, when (+) should be the integer addition :
```
module M1
use import real.RealInfix
use import int.Int
constant x: int = 0 + 0
(* constant y: real = 0.0 + 0.0 typing error*)
goal g: True
end
module M2
use import real.RealInfix
(* constant y: real = 0.0 + 0.0 typing error*)
goal g: True
end
```
Maybe the `use import real.Real` declaration in `RealInfix` is treated as a `use export` ?https://gitlab.inria.fr/why3/why3/-/issues/32Warnings not shown anymore in IDE2018-01-19T10:49:19+01:00MARCHE ClaudeWarnings not shown anymore in IDEThe warnings are not shown anywhere when loading/reloading sources in the IDEThe warnings are not shown anywhere when loading/reloading sources in the IDEMARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/37Conflict between strategies with the same shortcut2017-11-24T17:26:00+01:00Raphaël Rieu-HelftConflict between strategies with the same shortcutWhen several strategies have the same shortcut (including the empty string), attempting to use one of them always calls the topmost one in why3.conf.
Omitting the shortcut line in the conf file is equivalent to setting shortcut="", so th...When several strategies have the same shortcut (including the empty string), attempting to use one of them always calls the topmost one in why3.conf.
Omitting the shortcut line in the conf file is equivalent to setting shortcut="", so this forces users to set unique shortcuts for all strategies even if they do not want to use these shortcuts.MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/19Apply with x2017-11-16T12:40:35+01:00DAILLER SylvainApply with xIt should be possible to give hint terms to apply (or rewrite). For example:
"apply h with x,y"
For example, it should allow to directly apply a lemma on transitivity:
"H : forall x y z, x < y -> y < z -> x < z
Goal: 0 < 2"
"apply H...It should be possible to give hint terms to apply (or rewrite). For example:
"apply h with x,y"
For example, it should allow to directly apply a lemma on transitivity:
"H : forall x y z, x < y -> y < z -> x < z
Goal: 0 < 2"
"apply H with 1" generates two new goals "0 < 1" and "1 < 2"2017-11-15https://gitlab.inria.fr/why3/why3/-/issues/15destruct_alg improvement2017-11-15T16:25:17+01:00DAILLER Sylvaindestruct_alg improvementCurrently, "destruct_alg x" does not work on some cases: it should introduce the new destructed part at the right position in the task. When destructed components are used before their definition, the transformation fails.
Also, rewriti...Currently, "destruct_alg x" does not work on some cases: it should introduce the new destructed part at the right position in the task. When destructed components are used before their definition, the transformation fails.
Also, rewriting after applying this transformation should not be necessary. Add a boolean (or a new transformation name) so that subst is done right after destruct_alg.