why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2024-03-28T09:36:21+01:00https://gitlab.inria.fr/why3/why3/-/issues/842why3 execute type inference problem2024-03-28T09:36:21+01:00Delphine Demangewhy3 execute type inference problemI came across a surprising behavior of the `why3 execute` command (why3 plateform 1.6.0).
Here's a shrinked example, to help reproducing the error.
```
module Issue
use bintree.Tree
use bintree.Inorder
use list.List
let issue ...I came across a surprising behavior of the `why3 execute` command (why3 plateform 1.6.0).
Here's a shrinked example, to help reproducing the error.
```
module Issue
use bintree.Tree
use bintree.Inorder
use list.List
let issue () =
let l = inorder Empty in
assert { l = Nil }
end
```
With `why3 ide`, it behaves as excepted : one VC is generated, and the assertion is easily discharged automatically.
With `why3 execute`, I get the following error message :
```
$ why3 execute issue.mlw --use=Issue 'issue ()'
Type mismatch between bintree.Tree.tree 'a and bintree.Tree.tree 'xi
```
Is this a known issue for version 1.6.0 of why3 ?
I have tried to provide more guidance to type inference using type annotations, but this doesn't solve the problem.
Thanks1.7.2MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/841using `model_projection` on alias types should be forbidden2024-03-28T15:51:27+01:00MARCHE Claudeusing `model_projection` on alias types should be forbiddenthe meta `model_projection` has the following form
```
meta "model_projection" function f
```
where `f` is a unary function say from some type `t`. It allows to obtain values in counterexamples say when `t` is an abstract type. It can al...the meta `model_projection` has the following form
```
meta "model_projection" function f
```
where `f` is a unary function say from some type `t`. It allows to obtain values in counterexamples say when `t` is an abstract type. It can also be used when `t` is not abstract. Yet, when `t` is an alias type then the current implementation produces some unexpected behavior, and indeed it is unclear what should be done in such a case. It is thus preferable that Why3 simply signals an error when `t` is an alias type.1.7.2MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/840spurious debug messages when using `why3 session create`2024-03-26T11:03:17+01:00MARCHE Claudespurious debug messages when using `why3 session create`executing `why3 session create` displays spurious debug messages regarding the directory and the session file created. They should be visible only when some debug flag is setexecuting `why3 session create` displays spurious debug messages regarding the directory and the session file created. They should be visible only when some debug flag is set1.7.2Matteo ManighettiMatteo Manighettihttps://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/838Problem with instantiation of interfaces2024-03-19T14:29:57+01:00Mário PereiraProblem with instantiation of interfacesConsider the following piece of WhyML code:
```
module M
type t 'a = 'a -> int
end
module N : M
end
```
Let us assume this is the contents of a `foo.mlw` file. If we use `why3 prove foo.mlw`, then Why3 replies with the error
```...Consider the following piece of WhyML code:
```
module M
type t 'a = 'a -> int
end
module N : M
end
```
Let us assume this is the contents of a `foo.mlw` file. If we use `why3 prove foo.mlw`, then Why3 replies with the error
```
Symbol t not found in implementation
```
However, if we change module N into
```
module N : M
type t 'a = 'a -> int
end
```
then we get the error
```
Cannot instantiate a defined symbol t
```Benjamin Terra-JorgeBenjamin Terra-Jorgehttps://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/836Use clone for ufloat theory2024-02-23T11:20:11+01:00BONNOT PaulUse clone for ufloat theoryProvide a generic theory parametrized by `eps` and `eta`, and clone it for single and double precision.
Also separate ufloat theorems in an other module.Provide a generic theory parametrized by `eps` and `eta`, and clone it for single and double precision.
Also separate ufloat theorems in an other module.BONNOT 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/834Case insensitive filter prover2024-02-12T15:45:51+01:00François BobotCase insensitive filter proverRemove the generation of shortcut from the section header of prover-data-conf and make the filtering of prover case insensitive.
TODO: check that for all prover it will not change the shortcut or add an explicit one
FYI @x-ABlancRemove the generation of shortcut from the section header of prover-data-conf and make the filtering of prover case insensitive.
TODO: check that for all prover it will not change the shortcut or add an explicit one
FYI @x-ABlancFrançois BobotFrançois Bobothttps://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/829Fix the generation of proof taks by the RAC2024-01-16T13:55:34+01:00MARCHE ClaudeFix the generation of proof taks by the RACThe RAC generates proof tasks for checking assertion. This task generation is implemented by some ad-hoc
cloning of the module from which the executed function comes from. This cloning is incorrect in general, as shown by various error m...The RAC generates proof tasks for checking assertion. This task generation is implemented by some ad-hoc
cloning of the module from which the executed function comes from. This cloning is incorrect in general, as shown by various error messages that appear in the check-ce bench after the MR !992 is merged.1.8.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/828No syntax highlighting for mlw files in IDE2024-01-16T17:07:59+01:00MONTAGU BenoitNo syntax highlighting for mlw files in IDESince version 1.7.0, the mlw files loaded in the IDE are all black and white: no syntax highlighting anymore.
Syntax highlighting is working fine in the "Task" tab, however.Since version 1.7.0, the mlw files loaded in the IDE are all black and white: no syntax highlighting anymore.
Syntax highlighting is working fine in the "Task" tab, however.1.7.1MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/827Export sessions as zip file failure2024-01-16T17:41:05+01:00MONTAGU BenoitExport sessions as zip file failureThe command available in the IDE "File > Export session as zip file" does not work when there is a parenthesis in the name of the parent folder.
For example, with a file `test.mlw` in the directory `folder(1)`, I get the two following e...The command available in the IDE "File > Export session as zip file" does not work when there is a parenthesis in the name of the parent folder.
For example, with a file `test.mlw` in the directory `folder(1)`, I get the two following error messages:
- `cannot produce archive test.zip` in the "Messages" tab of the IDE
- `sh: 1: Syntax error: "(" unexpected` in the terminal
This looks like an error in the shell command, where enclosing `"` might be missing.
This error happens frequently in practice: students tend to download several times the same files (or files with the same names, that originate from different courses) in the same home folder. This results in `foo.zip`, `foo(1).zip`, etc. in their home folder. The latter zip file is extracted in a new folder named `foo(1)`.1.7.1MARCHE ClaudeMARCHE Claudehttps://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 Manighettihttps://gitlab.inria.fr/why3/why3/-/issues/825Alt-Ergo 2.5.x should be made used by auto strategies2024-01-08T23:29:38+01:00MARCHE ClaudeAlt-Ergo 2.5.x should be made used by auto strategiesThe Alt-Ergo 2.5.x section of `prover-detection-data.conf` is missing a line `use_at_auto_level` to make it used by auto strategiesThe Alt-Ergo 2.5.x section of `prover-detection-data.conf` is missing a line `use_at_auto_level` to make it used by auto strategies1.7.1MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/824"undone" proofs read in as failed proofs2024-01-09T09:06:10+01:00Johannes Kanig"undone" proofs read in as failed proofsIn the `session_itp` API, the `proof_attempt_node` type has an *optional* result field `proof_state`. This field can be `None`, which represents the fact that the prover hasn't finished yet, or absence of result for another reason. Such ...In the `session_itp` API, the `proof_attempt_node` type has an *optional* result field `proof_state`. This field can be `None`, which represents the fact that the prover hasn't finished yet, or absence of result for another reason. Such a state can occur for example when hitting Ctrl-C while why3 is running.
When such a session is read from a session file, the `None` state is replaced by a default `error` result. This makes it impossible to distinguish between such unfinished states, and actually failed proof attempts.
I will propose a fix.Johannes KanigJohannes Kanighttps://gitlab.inria.fr/why3/why3/-/issues/823Unexpected inconsistency with (<>)2024-01-04T09:26:46+01:00Xavier DenisUnexpected inconsistency with (<>)I stumbled across the following unexpected inconsistency in why3's handling of `<>`.
The following program compiles:
```
type option 'a = Some 'a | None
let rec ghost function f (x y : option int) = x <> y
```
However, this one does ...I stumbled across the following unexpected inconsistency in why3's handling of `<>`.
The following program compiles:
```
type option 'a = Some 'a | None
let rec ghost function f (x y : option int) = x <> y
```
However, this one does not:
```
use int.Int
type option 'a = Some 'a | None
let rec ghost function f (x y : option int) = x <> y
```
Stating,
```
File "test.mlw", line 5, characters 46-47:
This expression has type Top.option int, but is expected to have type int
```
I believe this is due to how `<>` is treated _literally_ as `not (a = b)` and since `int.Int` furnishes a `=` symbol this is used in the expansion, however its strange that if that module is _not_ imported then we get the polymorphic mathematical equality instead.