why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2022-04-25T14:28:25+02:00https://gitlab.inria.fr/why3/why3/-/issues/560document mutually recursive types2022-04-25T14:28:25+02:00Jean-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.0https://gitlab.inria.fr/why3/why3/-/issues/554Document the modulo `io`, document printing capabilities2021-09-23T16:25:05+02:00MARCHE ClaudeDocument the modulo `io`, document printing capabilitiesDocument, and export it to [Stdlib online doc](http://why3.lri.fr/stdlib/)
Also, document how to print in the manualDocument, and export it to [Stdlib online doc](http://why3.lri.fr/stdlib/)
Also, document how to print in the manual1.5.0https://gitlab.inria.fr/why3/why3/-/issues/539List changes for 1.4.02021-03-13T11:06:11+01:00Guillaume MelquiondList changes for 1.4.0Things related to `CHANGES.md`, to be done before the release:
- [x] Remove the sentence about MLCFG. (It is new, so listing changes is pointless.)
- [ ] Check that all the newly supported provers are mentioned. (at least CVC4 1.8 missi...Things related to `CHANGES.md`, to be done before the release:
- [x] Remove the sentence about MLCFG. (It is new, so listing changes is pointless.)
- [ ] Check that all the newly supported provers are mentioned. (at least CVC4 1.8 missing)
And obviously, add all the new features!
Tick your name below when you are done with your own changes :
- [ ] @paskevyc
- [x] @bbecker
- [x] @marche
- [ ] @bobot
- [x] @melquion
- [x] @filliatr
- [x] @xdenis
- [x] @rrieuhel -> @melquion
- [x] @cbelodas -> @marche (infer loop, strings)
- [x] @sdailler -> @marche
- [x] @qgarcher -> @marche1.4.0https://gitlab.inria.fr/why3/why3/-/issues/474document the emacs mode for Why32021-02-04T18:47:32+01:00MARCHE Claudedocument the emacs mode for Why3explain where `why3.el` is installed, what to add in the user's `.emacs`explain where `why3.el` is installed, what to add in the user's `.emacs`1.4.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/470Doc: document the any construct2021-01-27T17:03:19+01:00MARCHE ClaudeDoc: document the any constructDocument any, and also local val (emphasize the differences)
Add them in the indexDocument any, and also local val (emphasize the differences)
Add them in the index1.4.0MARCHE ClaudeMARCHE Claudehttps://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/329Missing lots of standard modules in the documentation2019-06-05T22:37:51+02:00Guillaume MelquiondMissing lots of standard modules in the documentationThe following WhyML modules are not documented (see the `stdlibdoc` target in [Makefile.in](Makefile.in)):
- `cursor`, `debug`, `exn`, `for_drivers`, `function`, `io`, `null`, `ocaml`, `regexp`, `tptp`, `tree`
- `mach/`: `bv`, `c`, `flo...The following WhyML modules are not documented (see the `stdlibdoc` target in [Makefile.in](Makefile.in)):
- `cursor`, `debug`, `exn`, `for_drivers`, `function`, `io`, `null`, `ocaml`, `regexp`, `tptp`, `tree`
- `mach/`: `bv`, `c`, `float`, `fxp`, `tagset`
Some of them are presumably not documented on purpose (e.g., `for_drivers`) and they should be explicitly marked as such. The other ones are in need of documentation.1.3.0MARCHE ClaudeMARCHE Claudehttps://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/749Why3doc is too fragile in presence of multiple files2023-04-04T09:43:26+02:00Guillaume MelquiondWhy3doc is too fragile in presence of multiple filesConsider a command line `why3 doc -L . ./foo.mlw ./bar.mlw` and assume that `bar.mlw` depends on a theory `foo.Foo` (hence the need for `-L .`). Why3 first reads `./foo.mlw` in isolation; that is fine. Then it reads `./bar.mlw`, which de...Consider a command line `why3 doc -L . ./foo.mlw ./bar.mlw` and assume that `bar.mlw` depends on a theory `foo.Foo` (hence the need for `-L .`). Why3 first reads `./foo.mlw` in isolation; that is fine. Then it reads `./bar.mlw`, which depends on `./foo.mlw` (and it is exactly `./foo.mlw` due to `-L .`). So, Why3 also loads `foo` as a library. But it has already registered tons of definitions in `./foo.mlw`, so all the definition of `foo.Foo` are dropped. As a consequence, any use of a symbol of `foo.Foo` in `bar.mlw` will be assumed to be from the current file, since that is what `foo.mlw` was at the time it was first parsed. All the corresponding links are thus broken.
There are two potential workarounds:
1. Make sure the files are in syntactically different locations, e.g., `why3 doc -L . foo.mlw bar.mlw`.
2. Make sure the files are documented after they have been already used once, e.g., `why3 doc -L . ./bar.mlw ./foo.mlw`.
This breaks hundreds of links in the documentation of Why3's standard library. Workaround 1 will be used there. But this still needs to be fixed properly.https://gitlab.inria.fr/why3/why3/-/issues/713misalignment of documentation with parser (python)2022-11-17T18:03:48+01:00Yannick Chevaliermisalignment of documentation with parser (python)Hi everyone,
in Section 9.2.1, Syntax of micro-Python, of the manual (https://why3.lri.fr/doc/input_formats.html#syntax-of-micro-python) the logic declaration of a function is defined as:
logic_declaration ::= "#@" "function" iden...Hi everyone,
in Section 9.2.1, Syntax of micro-Python, of the manual (https://why3.lri.fr/doc/input_formats.html#syntax-of-micro-python) the logic declaration of a function is defined as:
logic_declaration ::= "#@" "function" identifier "(" params ")" return_type? ("variant" "{" term "}")? ("=" term)? NEWLINE
However, in the parser (file why3/plugins/python/py_parser.mly on gitlab), the corresponding rule for fp_variant is (line 155):
LEFTBR VARIANT v=term RIGHTBR { v }
i.e., the documentation says to write it variant { n } and the parser awaits { variant n }.
Bests,
YannickJean-Christophe FilliâtreJean-Christophe Filliâtrehttps://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/627Document [@vc:xxx] attributes2022-07-06T10:29:27+02:00MARCHE ClaudeDocument [@vc:xxx] attributesThe current documentation (say http://why3.lri.fr/doc/vcgen.html) lists the possible attributes for altering VC generation: `[@vc:divergent]`, `[@vc:annotation]`, `[@vc:sp]`, `[@vc:wp]`, `[@vc:white_box]`, `[@vc:keep_precondition]`.
Onl...The current documentation (say http://why3.lri.fr/doc/vcgen.html) lists the possible attributes for altering VC generation: `[@vc:divergent]`, `[@vc:annotation]`, `[@vc:sp]`, `[@vc:wp]`, `[@vc:white_box]`, `[@vc:keep_precondition]`.
Only the `[@vc:divergent]` is lightly documented with the sentence "disables generation of VC for termination".
It is desirable to document more. In particular, it should be said *where* these attributes should be put to have an effect. For example, `[@vc:divergent]` has an effect when given as attribute to the body of a function. Is it the only place it has an effect?
Other cases include `[@vc:white_box]` and `[@vc:keep_precondition]` : where should these attributes be put to have an effect? And what effect exactly? For example, is it possible to put an attribute like `[@vc:keep_precondition]` on a *function contract* to tell that precondition should be kept for *all calls* to this function? Or should it be put on individual function calls?
An example for each of these attributes would be welcome.
Side question: is the attribute `[vc:white_box]` able to answer the question on the Zulip about inlining a function call in a VC computation ?
(@paskevyc and @melquion any thoughts?)MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/577TryWhy3 - Symlink of alt-ergo-worker.js instead of the real file2021-05-21T11:48:07+02:00PATAULT PaulTryWhy3 - Symlink of alt-ergo-worker.js instead of the real fileThe `README.md` located in `src/trywhy3` tells to run `mv alt-ergo-worker.js ..` but it is a symlink of the file `_build/default/src/bin/js/worker_js.bc.js`. This implies that the file will not be found by javascript when the engine is l...The `README.md` located in `src/trywhy3` tells to run `mv alt-ergo-worker.js ..` but it is a symlink of the file `_build/default/src/bin/js/worker_js.bc.js`. This implies that the file will not be found by javascript when the engine is launched.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/566Missing instruction in manual for installation of why3 ide2021-03-30T09:20:41+02:00David DeharbeMissing instruction in manual for installation of why3 ideIn section "5.1.1 Installation via Opam" of the manual, it would be nice to include the installation instructions to enable the `ide` command, e.g.:
```
opam install why3-ide
```In section "5.1.1 Installation via Opam" of the manual, it would be nice to include the installation instructions to enable the `ide` command, e.g.:
```
opam install why3-ide
```https://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/529Broken dependency graphs in the documentation2021-01-23T14:46:00+01:00Guillaume MelquiondBroken dependency graphs in the documentationSomething is going terribly wrong with the dependency graphs of the documentation: https://why3.gitlabpages.inria.fr/why3/syntaxref.html#library-int-mathematical-integersSomething is going terribly wrong with the dependency graphs of the documentation: https://why3.gitlabpages.inria.fr/why3/syntaxref.html#library-int-mathematical-integershttps://gitlab.inria.fr/why3/why3/-/issues/520Update documentation of the Why3 API2022-07-20T19:11:22+02:00Guillaume 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 ex...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.MARCHE ClaudeMARCHE Claudehttps://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/237Update counterexample doc2019-02-11T11:38:08+01:00DAILLER SylvainUpdate counterexample docUpdate the counterexamples doc (which is apparently outdated).
This should include API description and how to run counterexamples for tools using Why3 (Spark etc).Update the counterexamples doc (which is apparently outdated).
This should include API description and how to run counterexamples for tools using Why3 (Spark etc).