why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2018-06-22T14:27:03+02:00https://gitlab.inria.fr/why3/why3/-/issues/145Doc: ticket system ref2018-06-22T14:27:03+02:00DAILLER SylvainDoc: ticket system refHello,
In the doc, the old bug tracking system is advertized:
"There is a public mailing list for users’ discussions: http://lists.gforge.inria.fr/
mailman/listinfo/why3-club.
Report any bug to the Why3 Bug Tracking System: https://gfor...Hello,
In the doc, the old bug tracking system is advertized:
"There is a public mailing list for users’ discussions: http://lists.gforge.inria.fr/
mailman/listinfo/why3-club.
Report any bug to the Why3 Bug Tracking System: https://gforge.inria.fr/
tracker/?atid=10293&group_id=2990&func=browse."
Is this still usable ?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).https://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/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/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/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/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/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/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/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/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/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/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/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/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/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 Claude