why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2018-08-14T12:24:32Zhttps://gitlab.inria.fr/why3/why3/-/issues/138Remaining TODOs for Range and Float2018-08-14T12:24:32ZFrançois BobotRemaining TODOs for Range and FloatSome todos remain in pretty.ml and theory.ml aboute Range and Float constructorSome todos remain in pretty.ml and theory.ml aboute Range and Float constructor1.0.0DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/137Readd smoke detector2018-06-18T16:11:46ZFrançois BobotReadd smoke detectorReadd the functionnality of smoke detector in why3 replay. Removed in commit 57de2a1485e5d2d29c71d8205a33838ffee6fba3Readd the functionnality of smoke detector in why3 replay. Removed in commit 57de2a1485e5d2d29c71d8205a33838ffee6fba31.0.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/136Make `any ... ensures` less error-prone2018-06-22T09:28:03ZGuillaume MelquiondMake `any ... ensures` less error-proneI didn't know that `any ... ensures` introduces an axiom. And I was not the only developer to get it wrong. We really should limit the number of language constructions that introduce axioms.
There are only three occurrences of this cons...I didn't know that `any ... ensures` introduces an axiom. And I was not the only developer to get it wrong. We really should limit the number of language constructions that introduce axioms.
There are only three occurrences of this construction in the gallery:
- `unraveling_a_card_trick`: `any int ensures { 0 <= result <= n*m }`
- `white_and_black_balls`: `any (x: int, y: int) ensures { 0 <= x && 0 <= y && x + y = 2 && x <= !b && y <= !w }`
- `vstte12_bfs`: `any B.t ensures { !!result = succ v }`
The first two occurrences are actually provable, so I am not sure their authors intended them to generate axioms. The last one is an actual axiom, but it should ideally have been `val`, so that the user could instantiate it to obtain an effective algorithm.
Thus, I suggest that this construction be repurposed so that it generates a verification condition.1.0.0https://gitlab.inria.fr/why3/why3/-/issues/128Transformation `split_vc` and term shapes2018-06-13T14:56:30ZGuillaume MelquiondTransformation `split_vc` and term shapesThe transformation `split_vc` splits the goals, simplifies trivial quantifications, and then introduces premises. Unfortunately, it means that we might end up with several proof tasks that have exactly the same shape as children of a sin...The transformation `split_vc` splits the goals, simplifies trivial quantifications, and then introduces premises. Unfortunately, it means that we might end up with several proof tasks that have exactly the same shape as children of a single node of the proof tree. As a consequence, pairing gets completely confused as soon as the code is modified.
A solution would be to change the shape algorithm so that it also hashes the premises that have been marked by `introduce_premises`. This might considerably increase the size of the shapes, but that will also make the pairing algorithm more reliable.
I mark this issue as blocking, since `split_vc` is the recommended transformation for newcomers.1.0.0Raphaël Rieu-HelftRaphaël Rieu-Helfthttps://gitlab.inria.fr/why3/why3/-/issues/121Check Isabelle realization2018-05-24T14:45:47ZFrançois BobotCheck Isabelle realization1.0.0DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/-/issues/118Failure to compile the error reporting module of the parser2018-10-02T14:43:42ZGuillaume MelquiondFailure to compile the error reporting module of the parser```
Ocamlc src/parser/report.mli
File "src/parser/report.mli", line 2, characters 2-40:
Error: Unbound module Parser.MenhirInterpreter
```
Menhir 20151112 does not seem to provide anything like that.```
Ocamlc src/parser/report.mli
File "src/parser/report.mli", line 2, characters 2-40:
Error: Unbound module Parser.MenhirInterpreter
```
Menhir 20151112 does not seem to provide anything like that.1.0.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/96Release of the new system2018-06-25T07:49:52ZGuillaume MelquiondRelease of the new systemThings to do before releasing `master`:
- [x] Enumerate the changes
- [x] Document the changes of syntax
- [ ] Remove the obsolete parts of documentation
- [x] Update the Coq realizations (especially `seq.Seq`) :arrow_right: `seq.Seq` i...Things to do before releasing `master`:
- [x] Enumerate the changes
- [x] Document the changes of syntax
- [ ] Remove the obsolete parts of documentation
- [x] Update the Coq realizations (especially `seq.Seq`) :arrow_right: `seq.Seq` is no longer realized
- [x] Update the Isabelle 2017 realizations
- [x] Update the Isabelle 2016-1 realizations, or drop them
- [x] Kill the Coq tactic (still used by about 20 proofs from the gallery)
- [x] Port the 'prover' example (blocked by issue #87)
- [x] Stabilize `Etry`
- [x] Solve issue #9
- [x] Solve issue #6
- [x] Solve issue #63 (issue not fully solved but should not be a blocker anymore for the release)
- [ ] Not a regression, but I think it would be preferable to find a solution to the various problems related to the `why3.conf` file (see issues #55 and #69 and !7)
- [x] Solve issue #118
- [x] Solve issue #128
- [x] Solve issue #131
- [x] Solve issue #125
- [x] Fix the gallery, possibly adopting issue #132
- [x] Solve issue #1361.0.0https://gitlab.inria.fr/why3/why3/-/issues/87Cannot use a type variable absent from the function arguments2018-05-23T07:37:59ZMARCHE ClaudeCannot use a type variable absent from the function argumentsThe following is an excerpt of a code that was working in the 'old' system.
It is not well-typed anymore: `Unbound type variable: 'c`
```
function compose (g:'b -> 'c) (f:'a -> 'b) : 'a -> 'c
axiom compose_def : forall g:'b -> 'c,f:'...The following is an excerpt of a code that was working in the 'old' system.
It is not well-typed anymore: `Unbound type variable: 'c`
```
function compose (g:'b -> 'c) (f:'a -> 'b) : 'a -> 'c
axiom compose_def : forall g:'b -> 'c,f:'a -> 'b,x:'a.
compose g f x = g (f x)
function const (x: 'b) : 'a -> 'b
axiom const_def : forall x:'b,z:'a. const x z = x
predicate extensionalEqual (f g:'a -> 'b) =
forall x:'a. f x = g x
let lemma const_compose_right (f:'a -> 'b) (x:'a) : unit
ensures { compose f (const x) = (const (f x): 'c -> 'b) }
=
assert { extensionalEqual (const (f x) : 'c -> 'b) (compose f (const x)) }
```1.0.0Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/76Syntactic construction for infinite loops disappeared2018-03-14T16:54:19ZCLOCHARD MartinSyntactic construction for infinite loops disappearedQuoting from the manual, the construction:
loop invariant* variant? expr end
is supposed to be an infinite loop (modulo escape mechanisms like exceptions).
This construction silently disappeared from the new_system branch
(during commi...Quoting from the manual, the construction:
loop invariant* variant? expr end
is supposed to be an infinite loop (modulo escape mechanisms like exceptions).
This construction silently disappeared from the new_system branch
(during commit d048170536cadb58d315be06a44382e71790fb79).1.0.0https://gitlab.inria.fr/why3/why3/-/issues/72Coercion and Higher-Order2018-03-06T17:32:38ZCLOCHARD MartinCoercion and Higher-OrderCoercions are not applied under implicit higher-order application.
Examples:
```
module Foo1
type t
type u
function f t : u
meta coercion function f
constant g : u -> bool
goal G : forall x:t. g x
end
```
```
module Foo2
...Coercions are not applied under implicit higher-order application.
Examples:
```
module Foo1
type t
type u
function f t : u
meta coercion function f
constant g : u -> bool
goal G : forall x:t. g x
end
```
```
module Foo2
type t
type u
function f t : u -> u
meta coercion function f
goal G : forall x:t,y:u. x y = y
end
```
In both modules, the occurrence of "x" within the goal is not coerced as one would expect, leading to a type error. However, when one explicit the higher-order application (operator (@)), those occurrences are coerced as expected.1.0.0Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/62Merge theories and modules into a single directory2017-12-18T15:23:49ZGuillaume MelquiondMerge theories and modules into a single directory1.0.0Guillaume MelquiondGuillaume Melquiondhttps://gitlab.inria.fr/why3/why3/-/issues/41Poor error message when assigning field of a purified type2017-11-23T14:47:38ZGuillaume MelquiondPoor error message when assigning field of a purified type```
type foo = { mutable a: int }
let update (q: {foo}) = q.a <- 42
```
gives `anomaly: Invalid_argument("Ity.eff_assign")````
type foo = { mutable a: int }
let update (q: {foo}) = q.a <- 42
```
gives `anomaly: Invalid_argument("Ity.eff_assign")`1.0.0Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/29Machine integers and range types2018-02-02T09:52:53ZGuillaume MelquiondMachine integers and range typesNow that range types are available, we should investigate moving away types such as `int31` from abstract types. We should also see whether it helps expressing `for` loops on machine integers (hopefully yes).Now that range types are available, we should investigate moving away types such as `int31` from abstract types. We should also see whether it helps expressing `for` loops on machine integers (hopefully yes).1.0.0Guillaume MelquiondGuillaume Melquiondhttps://gitlab.inria.fr/why3/why3/-/issues/6Error-prone behavior when cloning theories2018-06-15T08:38:42ZGuillaume MelquiondError-prone behavior when cloning theoriesWhen cloning a theory, the behavior is to keep axioms as axioms, unless the user explicitly put a `with lemma foo` clause. This approach is error-prone, as it will cause (possibly inconsistent) facts to never get any proof obligation, du...When cloning a theory, the behavior is to keep axioms as axioms, unless the user explicitly put a `with lemma foo` clause. This approach is error-prone, as it will cause (possibly inconsistent) facts to never get any proof obligation, due to the user forgetting about them at clone time. I suggest that the default behavior be changed so that any cloned axiom produces a proof obligation, unless the user explicitly put a `with axiom foo` clause. For the sake of conciseness, there should be a special syntax (e.g. `with axiom *`) to skip over all the remaining cloned axioms. Another possibility would be to not turn cloned axioms into lemmas if none of their symbols got instantiated at clone time.1.0.0Andrei PaskevichAndrei Paskevich