why3 issueshttps://gitlab.inria.fr/why3/why3/issues2018-05-24T14:45:47Zhttps://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` 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 #136Things 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:'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)) }
```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 commit d048170536cadb58d315be06a44382e71790fb79).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
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.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, 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.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 Paskevichhttps://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/405Hide does not work2019-11-04T12:43:00ZDAILLER SylvainHide does not workOn the following simple goal, `hide t 1` does not work. It should be investigated.
```
axiom h: 1 = 3
goal G: forall x. x = 1
```On the following simple goal, `hide t 1` does not work. It should be investigated.
```
axiom h: 1 = 3
goal G: forall x. x = 1
```DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/issues/399`apply with` and `rewrite with` should give more details (e.g., quantifier na...2019-10-28T11:38:53ZGuillaume Melquiond`apply with` and `rewrite with` should give more details (e.g., quantifier names) when the number of arguments do not matchDAILLER SylvainDAILLER Sylvainhttps://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/395Extraction using a driver on the extracted file2019-10-17T14:27:59ZDAILLER SylvainExtraction using a driver on the extracted fileI am trying to use `why3extract` and a custom driver to extract a Why3 module that would partly depends on an OCaml implementation. I cannot manage to use the driver to change the extraction of this module with the driver.
My file `a.mlw` is as follows:
```
module A
type a
val eq_elt (e1 e2: a) : bool
ensures { e1 = e2 <-> result}
end
```
I took the driver `ocaml64.drv` which I copied (into `driver/ocaml_ext.drv` and added the following at the end:
```
module a.A
syntax val eq_elt "TODO"
end
```
I tried to extract with the following command:
`why3 extract --modular -D driver/ocaml_ext.drv a.mlw -o todo1`
I first get:
`Library file not found: a`
So, I added the option "-L ." to workaround this problem then the driver is read with no problems but, during printing, I get:
`Symbol eq_elt cannot be extracted`
I looked in more details and it seems that in this case, the extraction reads the file `a.mlw` twice: once as a library which is used to fill the syntax map during the driver parsing; and once during the printing of the file `a.mlw`. This leads to the element `eq_elt` being generated twice and the extraction using the second one instead of the first when trying to query the syntax map.
I have a solution which would ensures that this cannot happen by calling both the file and the libraries with the same memoized call (`Env.read_library`) but I am not sure this is how the code was intended.
So, is there currently a way to do what I tried ? If not, is it something that should be allowed ? If yes, a solution is to read all files with read_library (seems to register its result) instead of read_file (seems not to register its result). Does this look like a good enough solution ?
PS: I looked at 1-2 examples that use why3 extract but they do not seem to need this kind of extraction.I am trying to use `why3extract` and a custom driver to extract a Why3 module that would partly depends on an OCaml implementation. I cannot manage to use the driver to change the extraction of this module with the driver.
My file `a.mlw` is as follows:
```
module A
type a
val eq_elt (e1 e2: a) : bool
ensures { e1 = e2 <-> result}
end
```
I took the driver `ocaml64.drv` which I copied (into `driver/ocaml_ext.drv` and added the following at the end:
```
module a.A
syntax val eq_elt "TODO"
end
```
I tried to extract with the following command:
`why3 extract --modular -D driver/ocaml_ext.drv a.mlw -o todo1`
I first get:
`Library file not found: a`
So, I added the option "-L ." to workaround this problem then the driver is read with no problems but, during printing, I get:
`Symbol eq_elt cannot be extracted`
I looked in more details and it seems that in this case, the extraction reads the file `a.mlw` twice: once as a library which is used to fill the syntax map during the driver parsing; and once during the printing of the file `a.mlw`. This leads to the element `eq_elt` being generated twice and the extraction using the second one instead of the first when trying to query the syntax map.
I have a solution which would ensures that this cannot happen by calling both the file and the libraries with the same memoized call (`Env.read_library`) but I am not sure this is how the code was intended.
So, is there currently a way to do what I tried ? If not, is it something that should be allowed ? If yes, a solution is to read all files with read_library (seems to register its result) instead of read_file (seems not to register its result). Does this look like a good enough solution ?
PS: I looked at 1-2 examples that use why3 extract but they do not seem to need this kind of extraction.https://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/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/382Why3 is incompatible with OCaml ≥ 4.092019-10-02T13:20:39ZANGELETTI FlorianWhy3 is incompatible with OCaml ≥ 4.09Compiler plugins have been removed from the OCaml compiler starting from version 4.09 .
This leads to a build failure in why3 on the recent OCaml 4.09 beta due to the `Debug_util` plugin.
Surprisingly, this plugin seems to implement a parsetree transformation that could be implemented as a ppx. So it seems that compatibility could be restored either by disabling this plugin at configuration time for Ocaml versions outside of the [4.05, 4.08] interval or by translating this plugin to a ppx.Compiler plugins have been removed from the OCaml compiler starting from version 4.09 .
This leads to a build failure in why3 on the recent OCaml 4.09 beta due to the `Debug_util` plugin.
Surprisingly, this plugin seems to implement a parsetree transformation that could be implemented as a ppx. So it seems that compatibility could be restored either by disabling this plugin at configuration time for Ocaml versions outside of the [4.05, 4.08] interval or by translating this plugin to a ppx.https://gitlab.inria.fr/why3/why3/issues/379IDE source view is not updated on parsing/typing error2019-09-02T11:33:27ZRaphaë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? @sdaillerDAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/issues/378On session reload, proved goals without any transformation are not marked as ...2019-09-02T08:56:27ZMá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 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.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.DAILLER SylvainDAILLER Sylvain