why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2019-11-14T12:31:49+01:00https://gitlab.inria.fr/why3/why3/-/issues/381Make sure that Str is not used in places that trywhy3 uses2019-11-14T12:31:49+01:00Raphaë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 comp...`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/380List transformation with arguments and documentation2019-11-22T16:21:38+01:00DAILLER SylvainList transformation with arguments and documentationDocument transformations with arguments with examples.
Investigate the possibility to have a more flexible parsing of list arguments in general (remove space constraint in particular `a, b, c`).Document transformations with arguments with examples.
Investigate the possibility to have a more flexible parsing of list arguments in general (remove space constraint in particular `a, b, c`).https://gitlab.inria.fr/why3/why3/-/issues/379IDE source view is not updated on parsing/typing error2019-09-02T13:33:27+02:00Raphaël Rieu-HelftIDE source view is not updated on parsing/typing errorWhen the parsing or typing fails on reload, the IDE highlights the location of the error, but the source view is not updated.
This makes the highlight nonsensical in many cases. Possibly related to the fix of #371? @sdaillerWhen the parsing or typing fails on reload, the IDE highlights the location of the error, but the source view is not updated.
This makes the highlight nonsensical in many cases. Possibly related to the fix of #371? @sdaillerhttps://gitlab.inria.fr/why3/why3/-/issues/378On session reload, proved goals without any transformation are not marked as ...2019-09-02T10:56:27+02:00Mário PereiraOn session reload, proved goals without any transformation are not marked as obsoleteConsider the following example:
```
module M
goal G : true
end
```
We normally prove the VC for goal G by directly calling Alt-Ergo, without any transformation. Now, we save and quit the session.
Next, we change the very same file a...Consider the following example:
```
module M
goal G : true
end
```
We normally prove the VC for goal G by directly calling Alt-Ergo, without any transformation. Now, we save and quit the session.
Next, we change the very same file as follows:
```
module M
goal G : false
end
```
When we reload the session, goal G is still marked as proved and not as obsolete (I would expect the latter to happen).
We do not observe this behavior if some transformation is used. Consider the following example:
```
module M
use int.Int
goal G : 1 + 1 = 2 /\ true
end
```
We call `split_vc` and then call Alt-Ergo on the generated goal. We save and quit the session. We do the following change:
```
module M
use int.Int
goal G : 1 + 1 = 2 /\ false
end
```
When we reload the session, now the proof attempt is marked as obsolete.https://gitlab.inria.fr/why3/why3/-/issues/377Why3 should not introduce spaces in identifiers2019-08-23T14:47:34+02:00DAILLER SylvainWhy3 should not introduce spaces in identifiersSpaces are introduced in identifiers in some cases. This makes it impossible for the user to use these identifiers in arguments of transformations.
An example with records is the following:
```
use int.Int
type r = {a : int; b : int}
...Spaces are introduced in identifiers in some cases. This makes it impossible for the user to use these identifiers in arguments of transformations.
An example with records is the following:
```
use int.Int
type r = {a : int; b : int}
let f (x y: r): bool
ensures {x.a = y.a}
=
true
```
To explicitly show the problem use the following transformations:
`introduce_premises`
`destruct_term x`
`assert (x2 = mk r x1 x)`
@marche suggest to use tick `'` instead of space because the user would still not be able to define those in .mlw file but they would be able to use them. Here, the result would be something along the lines of `r'mk`.
Note that spaces also appear in the names of goals: they could be removed in favor of `'` too. For example: `f'VC`.
On this issue, I will try to make a MR with the simple replacement of `mk ` with `'mk` to see if it could work. Note that I also expect to change accordingly any code that would recognize a record by looking if its name begins with `mk `.https://gitlab.inria.fr/why3/why3/-/issues/376handling of smoke detection in sessions2022-03-29T16:22:03+02:00Johannes Kanighandling of smoke detection in sessionsSPARK now has a switch --proof-warnings that enables a number of extra checks via VCs that are of the "smoke detection" type, that is, if they are *proved*, something is wrong (and a warning is issued to the user). I believe why3 testing...SPARK now has a switch --proof-warnings that enables a number of extra checks via VCs that are of the "smoke detection" type, that is, if they are *proved*, something is wrong (and a warning is issued to the user). I believe why3 testing also uses some kind of smoke detection.
In most cases, no smoke is detected, so the VCs remain unproved. However, the unproved goal is still stored in the session. This is not very nice when the user looks into the session, which is now polluted with lots of unproved goals, even though all "real" VCs might be proved. The user can directly see the session via why3ide, or the manual proof feature of SPARK, or even by looking at the session file (a common way of looking at the session file would be via the "diff" feature of the version control system, if the session file is checked in).
It is unclear to me how this situation should best be improved. For example, the various tools (why3ide, SPARK manual proof) could hide by default smoke detection goals. That would require such goals to be marked specially (via an attribute?). Does the Why3 team have an idea how to deal with this, given that you already have a lot of experience with smoke detection?https://gitlab.inria.fr/why3/why3/-/issues/375Why3 parsing slow2019-08-26T11:26:17+02:00Johannes KanigWhy3 parsing slowThis is an issue that we discovered together with @sdailler. I added the attached patch to why3 to mesure CPU time spent in some parts of the code (here: driver loading).[timing.patch](/uploads/47c75df43d6e56653c3a5ee6543e4d41/timing.pat...This is an issue that we discovered together with @sdailler. I added the attached patch to why3 to mesure CPU time spent in some parts of the code (here: driver loading).[timing.patch](/uploads/47c75df43d6e56653c3a5ee6543e4d41/timing.patch)
With this patch I was able to determine that on some file (I don't think it matters which), if I ask why3 to load e.g. the cvc4 driver:
```
why3 prove -P CVC4 <somefile>
```
loading the driver takes roughly 0.1 seconds. With @sdailler we found that it isn't actually loading drivers that is slow, but the reading of the why3 libs referenced from the driver.
In SPARK we have switched to a mode where we run why3 much more often than before (possibly hundreds of times on large projects) so while 0.1 seconds seems tiny, it does add up to dozens of seconds on such projects. Also, the above 0.1s measures only parts of the why3 library, while in SPARK we also have some support files which are parsed on every invocation of why3, so for us the time is closer to 0.2 or even 0.4s.
I checked the file sizes of the entire why3 stdlib, and of drivers, and everything is very small, so I'm surprised that any measurable time is spent parsing these files. Can this be improved?https://gitlab.inria.fr/why3/why3/-/issues/374eliminate_if transformation explodes2019-12-10T12:59:00+01:00Johannes 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...[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/373Simplify extraction of C for loops2019-09-06T12:36:33+02:00Raphaël Rieu-HelftSimplify extraction of C for loopsSee discussion on !214.See discussion on !214.Raphaël Rieu-HelftRaphaël Rieu-Helfthttps://gitlab.inria.fr/why3/why3/-/issues/372Extraction is too eager to inline temporary binders in for-loops2019-09-06T12:36:34+02:00Guillaume MelquiondExtraction is too eager to inline temporary binders in for-loopsExtracting the following code to C causes the `costly` function to be called at each loop iteration.
```
use mach.int.UInt64
let costly () = 1000:uint64
let f () = for i = 0 to costly () do done
```
```c
uint64_t costly() {
return UIN...Extracting the following code to C causes the `costly` function to be called at each loop iteration.
```
use mach.int.UInt64
let costly () = 1000:uint64
let f () = for i = 0 to costly () do done
```
```c
uint64_t costly() {
return UINT64_C(1000);
}
void f() {
uint64_t i;
for (i = UINT64_C(0); ; ++i) {
if (i == costly()) {
break;
}
}
}
```Raphaël Rieu-HelftRaphaël Rieu-Helfthttps://gitlab.inria.fr/why3/why3/-/issues/371IDE reload is slow when there are syntax errors2019-08-30T13:09:42+02:00Raphaël Rieu-HelftIDE reload is slow when there are syntax errorsWhen editing a large file and making a syntax error, a failed reload of the IDE takes about half as much time as a successful reload (with no syntax error), while `why3 prove` almost instantly fails. It's significant enough to make me us...When editing a large file and making a syntax error, a failed reload of the IDE takes about half as much time as a successful reload (with no syntax error), while `why3 prove` almost instantly fails. It's significant enough to make me use `why3 prove` as a syntax checker before each reload. It would be nice if the reload failed earlier in case of a syntax error.https://gitlab.inria.fr/why3/why3/-/issues/370Session_itp.merge_trans: Not_found2019-07-29T11:03:24+02:00Raphaël Rieu-HelftSession_itp.merge_trans: Not_foundWhile reloading a large proof, I got the error message `[Session_itp.merge_trans] FATAL unexpected exception: anomaly: Not_found` followed by a crash. I did not manage to reproduce.While reloading a large proof, I got the error message `[Session_itp.merge_trans] FATAL unexpected exception: anomaly: Not_found` followed by a crash. I did not manage to reproduce.https://gitlab.inria.fr/why3/why3/-/issues/369Pattern matching gives confusing error messages2019-12-04T13:10:23+01:00Guillaume MelquiondPattern matching gives confusing error messagesWhile investigating #213, I found the following testcase:
```
type foo = { bar: int } invariant { true }
let baz (v: foo): int = match v with { bar = b } -> b end
```
```
File "foo.mlw", line 2, characters 37-48:
Function mk foo is not...While investigating #213, I found the following testcase:
```
type foo = { bar: int } invariant { true }
let baz (v: foo): int = match v with { bar = b } -> b end
```
```
File "foo.mlw", line 2, characters 37-48:
Function mk foo is not a constructor
```
Either removing the invariant from `foo` or using `v.bar` in `baz` avoid the issue.https://gitlab.inria.fr/why3/why3/-/issues/368Add a Why3 lexer to Rouge2019-07-15T10:28:19+02:00Guillaume MelquiondAdd a Why3 lexer to RougeThat way, Gitlab will automatically perform syntax highlighting for `.mlw` files, as well as allow users to type
```why3
let foo () = ()
```
to get syntax highlighting in issues. Gitlab's syntax highlighting is based on [Ro...That way, Gitlab will automatically perform syntax highlighting for `.mlw` files, as well as allow users to type
```why3
let foo () = ()
```
to get syntax highlighting in issues. Gitlab's syntax highlighting is based on [Rouge](https://github.com/rouge-ruby/rouge).https://gitlab.inria.fr/why3/why3/-/issues/367Trivial goals are not user-friendly2019-12-04T13:24:11+01:00Guillaume MelquiondTrivial goals are not user-friendlyWhen doing `split_vc` on the weakest precondition of `bar`
```
let foo () requires { true } = ()
let bar () = foo (); foo ()
```
we get two subgoals `true` marked as unknown. At this point, the user can either apply `split_vc` or launc...When doing `split_vc` on the weakest precondition of `bar`
```
let foo () requires { true } = ()
let bar () = foo (); foo ()
```
we get two subgoals `true` marked as unknown. At this point, the user can either apply `split_vc` or launch a prover, on each subgoal. In both cases, this is a waste of user time and processor cycles. This becomes especially noticeable after !207, as the number of trivial goals greatly increases.
Two possible solutions:
1. Automatically mark `true` goals as proved.
2. Prevent `split_vc` from generating them.https://gitlab.inria.fr/why3/why3/-/issues/366Incorrect goal location after splitting.2019-07-16T15:01:08+02:00Guillaume MelquiondIncorrect goal location after splitting.Testcase:
```
val bar (x:int): unit requires { x <> 0 }
let foo (x:int) : unit = bar x; bar x
```
When clicking the initially unique goal in the IDE, both calls `bar x` are properly highlighted as being the preconditions to prove. After...Testcase:
```
val bar (x:int): unit requires { x <> 0 }
let foo (x:int) : unit = bar x; bar x
```
When clicking the initially unique goal in the IDE, both calls `bar x` are properly highlighted as being the preconditions to prove. After splitting the goal, both goals cause the IDE to highlight the first call `bar x`, while the second goal is meant to be the precondition of the second call.
Note that this happens quite often in practice. For example, the fast exponentiation algorithm (or its variant, the ancient Egyptian multiplication) contains both divisions and modulos, which all have the same precondition, so all the goals point to the same location of the code.https://gitlab.inria.fr/why3/why3/-/issues/365Should why3config --add-prover only add one prover ?2021-02-15T16:55:23+01:00DAILLER SylvainShould why3config --add-prover only add one prover ?Hello,
It seems that the current behavior of `why3config --add-prover` is to first detect all the provers and then to add the prover given. I would like to add a prover without changing the rest of the configuration. Was it the intended...Hello,
It seems that the current behavior of `why3config --add-prover` is to first detect all the provers and then to add the prover given. I would like to add a prover without changing the rest of the configuration. Was it the intended behavior or could I add a new option such add `--only-add-prover` ?
It's possible that my question make sense only in the SPARK context where we merge configuration files and want to avoid the visibility of some provers in the configuration that we add.https://gitlab.inria.fr/why3/why3/-/issues/364the attribute [@inline:trivial] should be documented2019-12-03T17:07:18+01:00MARCHE Claudethe attribute [@inline:trivial] should be documenteddocumented for example in section 9.5.1, and listed in the `CHANGES.md`documented for example in section 9.5.1, and listed in the `CHANGES.md`Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/363IDE: jump to start of a module2019-07-05T15:48:04+02:00Raphaël Rieu-HelftIDE: jump to start of a moduleWhen clicking a function in the proof tree, the source view jumps to the top of the function definition. It would be nice to have the same for modules.When clicking a function in the proof tree, the source view jumps to the top of the function definition. It would be nice to have the same for modules.https://gitlab.inria.fr/why3/why3/-/issues/362overly generic logics declaration causes slowdown of cvc4 proof2023-09-11T14:23:38+02:00Johannes Kanigoverly generic logics declaration causes slowdown of cvc4 proofFlorian had identified a long time ago an issue where cvc4 would take
much longer to prove a given VC if a non-linear arithmetic was specified
compared to a linear one. See this ticket and the example in the ticket:
https://github.com/C...Florian had identified a long time ago an issue where cvc4 would take
much longer to prove a given VC if a non-linear arithmetic was specified
compared to a linear one. See this ticket and the example in the ticket:
https://github.com/CVC4/CVC4/issues/1276
On my machine, there is a factor of 10 (0.6s vs 6s) between UFBVDTLIRA
and UFBVDTNIRA when using cvc4 on the example in the issue.
We were wondering if Why3 could be more precise, e.g. detecting when
only linear operators are used. Given the potentially large speedups it
seems worthwhile. The other idea mentioned in the TN to specify
--inst-when-strict-interleave isn't an option for us.Matteo ManighettiMatteo Manighetti