why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2018-10-16T16:59:45+02:00https://gitlab.inria.fr/why3/why3/-/issues/127missing encoding of polymorphism2018-10-16T16:59:45+02:00Jean-Christophe Filliâtremissing encoding of polymorphismOn the following, a call to a prover requiring polymorphism to be encoded fails:
goal G0: (fun x -> x) 0 = 0
For instance:
```
> why3 prove -P cvc4 test.mlw
This type isn't supported:
'a -> 'a
smtv2: you must encode type poly...On the following, a call to a prover requiring polymorphism to be encoded fails:
goal G0: (fun x -> x) 0 = 0
For instance:
```
> why3 prove -P cvc4 test.mlw
This type isn't supported:
'a -> 'a
smtv2: you must encode type polymorphism
```1.1.0Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/121Check Isabelle realization2018-05-24T16:45:47+02:00François BobotCheck Isabelle realization1.0.0https://gitlab.inria.fr/why3/why3/-/issues/118Failure to compile the error reporting module of the parser2018-10-02T16:43:42+02:00Guillaume 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-25T09:49:52+02:00Guillaume 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-23T09:37:59+02:00MARCHE 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-14T17:54:19+01:00CLOCHARD 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-06T18:32:38+01:00CLOCHARD 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-18T16:23:49+01:00Guillaume MelquiondMerge theories and modules into a single directory1.0.0Guillaume MelquiondGuillaume Melquiondhttps://gitlab.inria.fr/why3/why3/-/issues/42Invalid_argument('Expr.let_rec") in clone declarations2020-03-17T01:18:27+01:00Raphaë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 a...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/41Poor error message when assigning field of a purified type2017-11-23T15:47:38+01:00Guillaume 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-02T10:52:53+01:00Guillaume 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-15T10:38:42+02:00Guillaume 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 Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/839forward_propagation strategy : sin and cos support2024-03-28T15:49:25+01:00BONNOT Paulforward_propagation strategy : sin and cos supportBONNOT PaulBONNOT Paulhttps://gitlab.inria.fr/why3/why3/-/issues/837Document the forward_propagation strategy2024-03-06T12:09:42+01:00BONNOT PaulDocument the forward_propagation strategyBONNOT PaulBONNOT Paulhttps://gitlab.inria.fr/why3/why3/-/issues/835Emacs mode setup is insufficient: opam-share is void2024-02-20T14:04:10+01:00David MENTRÉEmacs mode setup is insufficient: opam-share is voidHello,
When following Why3 documentation to setup Why3 Emacs mode (https://why3.gitlabpages.inria.fr/why3/install.html#emacs), I stumbled on an Emacs error: "`opam-share` variable is void". My understanding is that this variable should ...Hello,
When following Why3 documentation to setup Why3 Emacs mode (https://why3.gitlabpages.inria.fr/why3/install.html#emacs), I stumbled on an Emacs error: "`opam-share` variable is void". My understanding is that this variable should be defined beforehand. I copied/pasted its definition from Merlin documentation. With below changes, I have no error and expected behavior.
```lisp
(let ((opam-share (ignore-errors (car (process-lines "opam" "var" "share")))))
(when (and opam-share (file-directory-p opam-share))
(setq why3-share (if (boundp 'why3-share) why3-share (ignore-errors (car (process-lines "why3" "--print-datadir")))))
(setq why3el
(let ((f (expand-file-name "emacs/why3.elc" why3-share)))
(if (file-readable-p f) f
(let ((f (expand-file-name "emacs/site-lisp/why3.elc" opam-share)))
(if (file-readable-p f) f nil)))))
(when why3el
(require 'why3)
(autoload 'why3-mode why3el "Major mode for Why3." t)
(setq auto-mode-alist (cons '("\\.mlw$" . why3-mode) auto-mode-alist)))
))
```
I think Why3 documentation should be updated with above changes.
Best regards,
davidMARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/833Triggers in SMT output2024-01-29T10:47:47+01:00Johannes KanigTriggers in SMT outputSee this [cvc5 issue](https://github.com/cvc5/cvc5/issues/10303), where we reported some regressions to cvc5 team. According to Andrew Reynolds it was due to this:
> Just for more information, the quantified formulas that are confusing ...See this [cvc5 issue](https://github.com/cvc5/cvc5/issues/10303), where we reported some regressions to cvc5 team. According to Andrew Reynolds it was due to this:
> Just for more information, the quantified formulas that are confusing are of this form:
> > (forall ((x Int)) (forall ((y Int)) (! P :pattern ((f x y))))
> Technically this is say "instantiate x with no guidance, afterwards instantiate y based on the pattern (f x y) for which x you chose. > The clearer definition is:
>> (forall ((x Int) (y Int)) (! P :pattern ((f x y))))
> Which says "instantiate x and y based on the pattern (f x y)".
It seems they are fixing cvc5 to accept both forms, but do we want to change why3 to emit the second form?https://gitlab.inria.fr/why3/why3/-/issues/832Some resources disappeared from why3.org (including some linked from the home...2024-02-12T15:53:58+01:00Matteo ManighettiSome resources disappeared from why3.org (including some linked from the homepage)I had tab open on this file: https://www.why3.org/ssft-16/notes-why3.pdf and now the file is not there anymore. Other links to learning resources are now broken in the homepage:
* http://why3.lri.fr/digicosme-spring-school-2013/
* htt...I had tab open on this file: https://www.why3.org/ssft-16/notes-why3.pdf and now the file is not there anymore. Other links to learning resources are now broken in the homepage:
* http://why3.lri.fr/digicosme-spring-school-2013/
* http://why3.lri.fr/jfla-2012/
Other things are indexed by Google but not accessible anymore: https://www.why3.org/queens/queens.pdf and so onhttps://gitlab.inria.fr/why3/why3/-/issues/831Inefficiency related to "use"2024-02-27T03:26:46+01:00Johannes KanigInefficiency related to "use"Hello,
In SPARK, we try to be very modular and generate many small theories so that we control the proof context. On a customer code we had now the situation where SPARK generates around ~800 modules, with lots of "use" statements (`gre...Hello,
In SPARK, we try to be very modular and generate many small theories so that we control the proof context. On a customer code we had now the situation where SPARK generates around ~800 modules, with lots of "use" statements (`grep "use" gives a count of over 6000).
Currently, why3 seems to be inefficient on such code. As an example, `Task.split_theory` accumulates several seconds on this input file, even though it mostly returns the empty list. This is because in our case, only a single module actually contains lemmas or goals. If I check for the presence of lemmas/goals before doing the work in `Task.split_theory`, we are able to recover this time, but then the code related to "use" in `Typing.ml` still takes a lot of time.
Unfortunately I can't directly share the reproducer as it derives from customer code, but if needed I could possibly prepare something similar. Do you have any idea how to improve the running time?https://gitlab.inria.fr/why3/why3/-/issues/830Forward error propagation strategy : Sum, Exp, Log2024-02-23T13:01:06+01:00BONNOT PaulForward error propagation strategy : Sum, Exp, LogProvide support for propagation of errors of sum, exp and log functions for ufloats.Provide support for propagation of errors of sum, exp and log functions for ufloats.BONNOT PaulBONNOT Paulhttps://gitlab.inria.fr/why3/why3/-/issues/826Improve the parser for models returned by SMT solvers2024-01-23T13:41:46+01:00Matteo ManighettiImprove the parser for models returned by SMT solversThe model parser behaves unexpectedly when encountering values whose name contains parentheses, which may happen for values introduced by the prover (that begin with `@`), such as in:
```plaintext
(define-fun x_vc_constant () (poly_map ...The model parser behaves unexpectedly when encountering values whose name contains parentheses, which may happen for values introduced by the prover (that begin with `@`), such as in:
```plaintext
(define-fun x_vc_constant () (poly_map Int Int) (as @(poly_map Int Int)_0 (poly_map Int Int)))
```
Since the parser also throws away most exceptions, this was both hard to detect and to inspect. The fix for this is simple, but the parser should be strengthened.
In the future we might consider using an external library for this, for example Dolmen.Matteo ManighettiMatteo Manighetti