why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2021-04-16T09:35:50Zhttps://gitlab.inria.fr/why3/why3/-/issues/570Functions that could be used as let-functions2021-04-16T09:35:50ZLoïc CorrensonFunctions that could be used as let-functions:warning: **Disclaimer** this report is _wrong_ : a let-function without a contract actually exposes its definition to callers.
**Original Report** (wrong)
A frequent pattern we face when writing why3 code for extraction, is a pure logical function that _only makes use of extractible expressions_. We then have to write the following code, with full duplication of core function definition:
```
function f x… : r = e
let rec function f x… : r ensures { result = e } = e
```
For large definition `e` with pattern matching or mutual-recursion, this is annoying !
This is the dual situation of a `let function f … = e`, where `f` can be used in both code & logic except that (among others):
1. the definition `e` of `let function f … = e` is _not_ available to provers
2. when writing `function f … = e` there is _no_ preconditions to `f`, hence `f x = e` always holds
3. pure logic function `f` must be structurally recursive so `let function f` needs no variant
**Proposal:**
Add a keyword to `function` definitions in order to have the associated `let rec function ...` for free.
Alternatively, detect that function definition only contains extractible terms and allow to use it like a `let function` in code.:warning: **Disclaimer** this report is _wrong_ : a let-function without a contract actually exposes its definition to callers.
**Original Report** (wrong)
A frequent pattern we face when writing why3 code for extraction, is a pure logical function that _only makes use of extractible expressions_. We then have to write the following code, with full duplication of core function definition:
```
function f x… : r = e
let rec function f x… : r ensures { result = e } = e
```
For large definition `e` with pattern matching or mutual-recursion, this is annoying !
This is the dual situation of a `let function f … = e`, where `f` can be used in both code & logic except that (among others):
1. the definition `e` of `let function f … = e` is _not_ available to provers
2. when writing `function f … = e` there is _no_ preconditions to `f`, hence `f x = e` always holds
3. pure logic function `f` must be structurally recursive so `let function f` needs no variant
**Proposal:**
Add a keyword to `function` definitions in order to have the associated `let rec function ...` for free.
Alternatively, detect that function definition only contains extractible terms and allow to use it like a `let function` in code.https://gitlab.inria.fr/why3/why3/-/issues/557Build a glossary of error messages2021-03-01T07:38:31ZMARCHE ClaudeBuild a glossary of error messagesThere are quite a lot of possible error messages from Why3, in particular from typing. It would help beginners, and indeed all users, if all these messages where explained in the manual, hopefully with examples.
Note: there should be at least one example exhibiting each error message anyway, in `bench/typing/bad'There are quite a lot of possible error messages from Why3, in particular from typing. It would help beginners, and indeed all users, if all these messages where explained in the manual, hopefully with examples.
Note: there should be at least one example exhibiting each error message anyway, in `bench/typing/bad'https://gitlab.inria.fr/why3/why3/-/issues/520Update documentation of the Why3 API2021-01-29T06:26:37ZGuillaume CluzelUpdate documentation of the Why3 APIHello,
I use the Why3 directly in OCaml. In particular I use the `Ptree` module. Unfortunately the documentation is very succinct.
For example, I cannot understand what the `Eoptexn` constructor does. Is it the declaration of a local exception? Is this local exception caught at the end of the block?
It would be a great improvement if all constructors have their own documentation and it would significantly help the Why3 users.Hello,
I use the Why3 directly in OCaml. In particular I use the `Ptree` module. Unfortunately the documentation is very succinct.
For example, I cannot understand what the `Eoptexn` constructor does. Is it the declaration of a local exception? Is this local exception caught at the end of the block?
It would be a great improvement if all constructors have their own documentation and it would significantly help the Why3 users.https://gitlab.inria.fr/why3/why3/-/issues/454Update documentation2021-02-05T13:15:02ZMARCHE ClaudeUpdate documentationA non-exhaustive list of sections that are not up-to-date.
## High priority (for 1.4.0)
* [x] 9.4. Isabelle/HOL: needs update to isabelle 2019
* [x] 10.6. Proof Strategies: needs update to auto levels 0 to 3
* [x] document `foreach`
* [x] document micro-C and micro-python (at least short paragraphs refering to the web pages)
* [x] document old and at (@filliatr )
* [x] document auto-dereference
## Medium priority (as soon as possible)
* [x] 7.5.2. Record types: in particular the differences between abstract/private and such, and the type invariants
* [x] 7.5.6. Module Cloning: to be completed
* [x] 4.11. Infering loop invariants: needs porting from latex to rst (@marche )
* [x] Functor extraction (@mariojppereira )
## Low priority
* [ ] 7.5.1. Algebraic types
* [ ] 7.6. Standard Library: expand and add more modules there
* [ ] Cursor
* [ ] Seq
* [ ] fix undefined labels and multiply-defined labels in Latex version. This seems to be a bug in sphinx, in its modules for formal grammars, which produces labels from non-terminal by replacing the underscore characters by minus, but not always. We can wait Sphinx to be fixed, or stop using underscores in non_terminals (annoying)A non-exhaustive list of sections that are not up-to-date.
## High priority (for 1.4.0)
* [x] 9.4. Isabelle/HOL: needs update to isabelle 2019
* [x] 10.6. Proof Strategies: needs update to auto levels 0 to 3
* [x] document `foreach`
* [x] document micro-C and micro-python (at least short paragraphs refering to the web pages)
* [x] document old and at (@filliatr )
* [x] document auto-dereference
## Medium priority (as soon as possible)
* [x] 7.5.2. Record types: in particular the differences between abstract/private and such, and the type invariants
* [x] 7.5.6. Module Cloning: to be completed
* [x] 4.11. Infering loop invariants: needs porting from latex to rst (@marche )
* [x] Functor extraction (@mariojppereira )
## Low priority
* [ ] 7.5.1. Algebraic types
* [ ] 7.6. Standard Library: expand and add more modules there
* [ ] Cursor
* [ ] Seq
* [ ] fix undefined labels and multiply-defined labels in Latex version. This seems to be a bug in sphinx, in its modules for formal grammars, which produces labels from non-terminal by replacing the underscore characters by minus, but not always. We can wait Sphinx to be fixed, or stop using underscores in non_terminals (annoying)1.5.0https://gitlab.inria.fr/why3/why3/-/issues/337Module `Cursor` should be documented2021-09-22T08:42:56ZMARCHE ClaudeModule `Cursor` should be documentedPlease add documentation as why3doc comments in `stdlib/cursor.mlw`Please add documentation as why3doc comments in `stdlib/cursor.mlw`PARREIRA PEREIRA Mário JoséPARREIRA PEREIRA Mário Joséhttps://gitlab.inria.fr/why3/why3/-/issues/204Syntax of drivers is not documented2018-10-10T12:28:14ZDAILLER SylvainSyntax of drivers is not documentedThe syntax of drivers is not documented. I think it should be. In particular difference between `syntax function` `syntax converter` etc..The syntax of drivers is not documented. I think it should be. In particular difference between `syntax function` `syntax converter` etc..https://gitlab.inria.fr/why3/why3/-/issues/202Document syntax of clone2018-11-13T18:00:01ZDAILLER SylvainDocument syntax of cloneHello,
I did not find explanation of this syntax (and equivalents) in the doc:
`clone export A with axiom .`
Can this be added ?Hello,
I did not find explanation of this syntax (and equivalents) in the doc:
`clone export A with axiom .`
Can this be added ?https://gitlab.inria.fr/why3/why3/-/issues/201Document extraction of clonable/cloned modules2021-02-11T09:42:27ZMARCHE ClaudeDocument extraction of clonable/cloned modulesI'd like to extract to OCaml a WhyML code that clones `appset.Appset`. How is it supposed to work?I'd like to extract to OCaml a WhyML code that clones `appset.Appset`. How is it supposed to work?https://gitlab.inria.fr/why3/why3/-/issues/560document mutually recursive types2021-03-13T06:47:05ZJean-Christophe Filliâtredocument mutually recursive typesQuoting Frank Pfenning's mail to `why3-club` on March 2, 2021:
> Is there a way to define mutually recursive types in WhyML? I couldn't find
> one in the documentation.Quoting Frank Pfenning's mail to `why3-club` on March 2, 2021:
> Is there a way to define mutually recursive types in WhyML? I couldn't find
> one in the documentation.1.5.0