why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2023-08-29T18:22:36+02:00https://gitlab.inria.fr/why3/why3/-/issues/454Update documentation2023-08-29T18:22:36+02:00MARCHE 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`
* ...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
* [x] 7.5.1. Algebraic types
* [x] mutually recursive types and functions
* [ ] 7.6. Standard Library: expand and add more modules there
* [ ] Cursor
* [ ] Seq
* [ ] document termination/variant/etc.
* [ ] 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.8.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/670document possible source of unsoundness when using Why32022-11-16T13:35:09+01:00MARCHE Claudedocument possible source of unsoundness when using Why3See also end of discussion on !717See also end of discussion on !717https://gitlab.inria.fr/why3/why3/-/issues/557Build a glossary of error messages2022-11-04T16:33:12+01:00MARCHE 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 a...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/337Module `Cursor` should be documented2021-09-22T10:42:56+02:00MARCHE 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/570Functions that could be used as let-functions2021-04-16T11:35:50+02:00Loï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 lo...: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/201Document extraction of clonable/cloned modules2021-02-11T10:42:27+01:00MARCHE 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/202Document syntax of clone2018-11-13T19:00:01+01:00DAILLER 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/204Syntax of drivers is not documented2018-10-10T14:28:14+02:00DAILLER 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..