why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2021-02-02T22:20:07+01:00https://gitlab.inria.fr/why3/why3/-/issues/541The execute button in TryWhy3 no longer works2021-02-02T22:20:07+01:00Guillaume MelquiondThe execute button in TryWhy3 no longer worksWhen pressing the "execute" button, TryWhy3 complains: "No main function found" (even when there is a `main` function), which makes the feature completely uselles. This is a regression with respect to TryWhy3 1.3.When pressing the "execute" button, TryWhy3 complains: "No main function found" (even when there is a `main` function), which makes the feature completely uselles. This is a regression with respect to TryWhy3 1.3.1.4.0https://gitlab.inria.fr/why3/why3/-/issues/540TryWhy3 crashes at startup: "caml_thread_initialize not implemented"2021-02-02T19:47:21+01:00Guillaume MelquiondTryWhy3 crashes at startup: "caml_thread_initialize not implemented"Since the `Unix` module is indirectly reachable from `trywhy3/why_worker.ml`, JavaScript chokes on the initialization code of this module, which includes a call to the unavailable function `caml_thread_initialize`.Since the `Unix` module is indirectly reachable from `trywhy3/why_worker.ml`, JavaScript chokes on the initialization code of this module, which includes a call to the unavailable function `caml_thread_initialize`.1.4.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/536Find a replacement for headache2021-02-01T19:29:07+01:00Guillaume MelquiondFind a replacement for headacheWe are using the `headache` tool to handle the copyright headers of our files. Unfortunately, the binary packaged in Ubuntu 20.04 is broken. Compiling it by hand is not an option either, since it requires an antiquated version of OCaml. ...We are using the `headache` tool to handle the copyright headers of our files. Unfortunately, the binary packaged in Ubuntu 20.04 is broken. Compiling it by hand is not an option either, since it requires an antiquated version of OCaml. So, we need to come up with a better solution.1.4.0https://gitlab.inria.fr/why3/why3/-/issues/473ppx_deriving dependency2021-02-05T17:33:21+01:00Claudio Belo Lourencoppx_deriving dependencyThe compilation of Why3 fails if ppx_deriving is not installed. Maybe the configure script should fail if the library is not installed?The compilation of Why3 fails if ppx_deriving is not installed. Maybe the configure script should fail if the library is not installed?1.4.0Benedikt BeckerBenedikt Beckerhttps://gitlab.inria.fr/why3/why3/-/issues/462Detection of non-progressing transformation is broken2020-03-24T01:35:22+01:00Guillaume MelquiondDetection of non-progressing transformation is brokenThis was presumably caused by e51eff2e0c392bf15f6508b23357a1544bc720fb. CC @paskevycThis was presumably caused by e51eff2e0c392bf15f6508b23357a1544bc720fb. CC @paskevyc1.3.1Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/455'make clean' erases Why3_BV.thy and Why3_Map.thy2020-03-03T13:47:23+01:00Guillaume Melquiond'make clean' erases Why3_BV.thy and Why3_Map.thyAre these files supposed to be part of the git repository?Are these files supposed to be part of the git repository?1.3.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/428Merge unreleased shape formats2020-02-12T00:36:14+01:00Guillaume MelquiondMerge unreleased shape formatsSince the 1.2 release, three new shape formats were introduced (`SV5`, `SV6`, `SV7`). This is pointless and will cause issues in the long run. Features from both `SV6` and `SV7` should be merged into `SV5` before the 1.3 release, to redu...Since the 1.2 release, three new shape formats were introduced (`SV5`, `SV6`, `SV7`). This is pointless and will cause issues in the long run. Features from both `SV6` and `SV7` should be merged into `SV5` before the 1.3 release, to reduce the backward compatibility logic.1.3.0Guillaume MelquiondGuillaume Melquiondhttps://gitlab.inria.fr/why3/why3/-/issues/407Impossible to build Why3 due to `parser/handcrafted.messages`2019-11-04T16:04:04+01:00Guillaume MelquiondImpossible to build Why3 due to `parser/handcrafted.messages````
Ocamlopt src/util/mlmpfr_wrapper.ml
File "src/util/mlmpfr_wrapper.ml", line 1:
Error: Could not find the .cmi file for interface
src/util/mlmpfr_wrapper.mli.
Makefile:2244: recipe for target 'src/util/mlmpfr_wrapper.cmx' faile...```
Ocamlopt src/util/mlmpfr_wrapper.ml
File "src/util/mlmpfr_wrapper.ml", line 1:
Error: Could not find the .cmi file for interface
src/util/mlmpfr_wrapper.mli.
Makefile:2244: recipe for target 'src/util/mlmpfr_wrapper.cmx' failed
```
And this is caused by `parser/handcrafted.messages`!
More precisely, my version of `menhir` produces a slightly different file `parser/handcrafted.messages.temp` (semantically identical, but not byte-to-byte). As a consequence, the generation of `src/parser/parser_messages.ml` fails. But since it fails at dependency generation time, the error is ignored, dependency generation is aborted, and the actual build starts. The build eventually fails because `.dep` files were not properly generated due to the above failure.
So, not only the user is unable to build Why3, but the build error message is completely misleading. (I wasted quite some time trying to understand what was wrong with `mlmpfr_wrapper.ml`.)
@bobot @sdailler If we can't find a solution by 1.3.0, I will again revert this code.1.3.0https://gitlab.inria.fr/why3/why3/-/issues/402`why3 ide` fails to start because of some missing files2019-10-29T08:48:53+01:00Guillaume Melquiond`why3 ide` fails to start because of some missing filesIt seems like `make install` does not install enough files: `language file for 'Why3python' not found in directory /usr/local/share/why3/lang`.
Presumably caused by 5886268a33563de981ea5ff138fd6ba8c9c992b2It seems like `make install` does not install enough files: `language file for 'Why3python' not found in directory /usr/local/share/why3/lang`.
Presumably caused by 5886268a33563de981ea5ff138fd6ba8c9c992b21.3.0Guillaume MelquiondGuillaume Melquiondhttps://gitlab.inria.fr/why3/why3/-/issues/182Unsound termination check2018-10-05T13:56:19+02:00Guillaume MelquiondUnsound termination checkConsider the following snippet:
let rec function f () : unit = f ()
let main () = f ()
According to Why3, this is a terminating function, which gets extracted to a non-terminating one:
let rec f (_: unit) : unit = f ()
...Consider the following snippet:
let rec function f () : unit = f ()
let main () = f ()
According to Why3, this is a terminating function, which gets extracted to a non-terminating one:
let rec f (_: unit) : unit = f ()
let main (_: unit) : unit = f ()1.1.0Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/128Transformation `split_vc` and term shapes2018-06-13T16:56:30+02:00Guillaume MelquiondTransformation `split_vc` and term shapesThe transformation `split_vc` splits the goals, simplifies trivial quantifications, and then introduces premises. Unfortunately, it means that we might end up with several proof tasks that have exactly the same shape as children of a sin...The transformation `split_vc` splits the goals, simplifies trivial quantifications, and then introduces premises. Unfortunately, it means that we might end up with several proof tasks that have exactly the same shape as children of a single node of the proof tree. As a consequence, pairing gets completely confused as soon as the code is modified.
A solution would be to change the shape algorithm so that it also hashes the premises that have been marked by `introduce_premises`. This might considerably increase the size of the shapes, but that will also make the pairing algorithm more reliable.
I mark this issue as blocking, since `split_vc` is the recommended transformation for newcomers.1.0.0Raphaël Rieu-HelftRaphaël Rieu-Helfthttps://gitlab.inria.fr/why3/why3/-/issues/119Obsolete nodes unsoundly reattached after errors2018-05-18T11:26:34+02:00Raphaël Rieu-HelftObsolete nodes unsoundly reattached after errorsHere are reproduction steps for the bug initially reported by @filliatr in lineardecision.mlw
After recovering from an error, the nodes that became detached due to the error are reattached. However, this reattaches some nodes that were ...Here are reproduction steps for the bug initially reported by @filliatr in lineardecision.mlw
After recovering from an error, the nodes that became detached due to the error are reattached. However, this reattaches some nodes that were obsolete before that, which is unsound.
Reproduction steps using the example below:
1. Prove this file
2. Uncomment the precondition of f, reload (the proofs of f,g,h are now obsolete)
3. Prove f, but not g or h (leaving them obsolete)
4. Uncomment the precondition of g, reload (there is an error because "<" is unknown in B)
5. Uncomment the "use import int.Int" in module B, reload
The proof of g is correctly still obsolete, but the proof of h has been reattached but is false (the precondition of f cannot be proved).
```
module A
use import int.Int
let f (x:int) : int
requires { true (* /\ x < 42*) }
ensures { result = 42 }
= 42
end
module B
use A
(* use import int.Int *)
let g (x:int) : int
requires { true (* /\ x < 42 *) }
ensures { result = 42 }
= A.f x
end
module C
use A
let h (x:int) : int
requires { true }
ensures { result = 42 }
= A.f x
end
```Raphaël Rieu-HelftRaphaël Rieu-Helfthttps://gitlab.inria.fr/why3/why3/-/issues/118Failure to compile the error reporting module of the parser2018-10-02T16:43:42+02:00Guillaume MelquiondFailure to compile the error reporting module of the parser```
Ocamlc src/parser/report.mli
File "src/parser/report.mli", line 2, characters 2-40:
Error: Unbound module Parser.MenhirInterpreter
```
Menhir 20151112 does not seem to provide anything like that.```
Ocamlc src/parser/report.mli
File "src/parser/report.mli", line 2, characters 2-40:
Error: Unbound module Parser.MenhirInterpreter
```
Menhir 20151112 does not seem to provide anything like that.1.0.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/96Release of the new system2018-06-25T09:49:52+02:00Guillaume MelquiondRelease of the new systemThings to do before releasing `master`:
- [x] Enumerate the changes
- [x] Document the changes of syntax
- [ ] Remove the obsolete parts of documentation
- [x] Update the Coq realizations (especially `seq.Seq`) :arrow_right: `seq.Seq` i...Things to do before releasing `master`:
- [x] Enumerate the changes
- [x] Document the changes of syntax
- [ ] Remove the obsolete parts of documentation
- [x] Update the Coq realizations (especially `seq.Seq`) :arrow_right: `seq.Seq` is no longer realized
- [x] Update the Isabelle 2017 realizations
- [x] Update the Isabelle 2016-1 realizations, or drop them
- [x] Kill the Coq tactic (still used by about 20 proofs from the gallery)
- [x] Port the 'prover' example (blocked by issue #87)
- [x] Stabilize `Etry`
- [x] Solve issue #9
- [x] Solve issue #6
- [x] Solve issue #63 (issue not fully solved but should not be a blocker anymore for the release)
- [ ] Not a regression, but I think it would be preferable to find a solution to the various problems related to the `why3.conf` file (see issues #55 and #69 and !7)
- [x] Solve issue #118
- [x] Solve issue #128
- [x] Solve issue #131
- [x] Solve issue #125
- [x] Fix the gallery, possibly adopting issue #132
- [x] Solve issue #1361.0.0https://gitlab.inria.fr/why3/why3/-/issues/69why3 config does not update main.loadpath2018-03-26T10:22:21+02:00MARCHE Claudewhy3 config does not update main.loadpathwhen using 'why3 config', if a why3.conf file already exists then the loadpath= fields of the [main]
record are not updated. For example, in the master branch, the path ".../theories" and ".../modules"
should be automatically replaced by...when using 'why3 config', if a why3.conf file already exists then the loadpath= fields of the [main]
record are not updated. For example, in the master branch, the path ".../theories" and ".../modules"
should be automatically replaced by ".../stdlib"MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/61Errors make too many nodes obsolete2017-12-21T15:30:08+01:00Raphaël Rieu-HelftErrors make too many nodes obsoleteReproduction steps:
* Have the IDE open
* In your favorite editor, edit the code of a function but make a syntax or type error
* Reload, the IDE shows the error and a ton of detached nodes
* Fix the error
* Reload
Expected results: obso...Reproduction steps:
* Have the IDE open
* In your favorite editor, edit the code of a function but make a syntax or type error
* Reload, the IDE shows the error and a ton of detached nodes
* Fix the error
* Reload
Expected results: obsolete nodes are the same as if the change was made without error (so the subgoals after the change in the function)
Actual result: every node in the proof is obsolete, even those outside the modified function
This gets old very fast in proofs that take a lot of time to replay.MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/33Reload remove transformations with same name2017-11-16T12:40:35+01:00DAILLER SylvainReload remove transformations with same nameWhen two transformations on the same node have the same name. For example, ``assert (0 = 0)`` and ``assert (1 = 1)``, one of them disappear after reload.When two transformations on the same node have the same name. For example, ``assert (0 = 0)`` and ``assert (1 = 1)``, one of them disappear after reload.https://gitlab.inria.fr/why3/why3/-/issues/26Key shorcut for going from command-line to task-tree2017-11-08T17:30:19+01:00MARCHE ClaudeKey shorcut for going from command-line to task-treeWe need a key shorcut to move the focus from the command-line to the proof tree (i.e. the reverse of Enter)
suggestion: Escape, or Enter when the input is emptyWe need a key shorcut to move the focus from the command-line to the proof tree (i.e. the reverse of Enter)
suggestion: Escape, or Enter when the input is emptyGuillaume MelquiondGuillaume Melquiondhttps://gitlab.inria.fr/why3/why3/-/issues/6Error-prone behavior when cloning theories2018-06-15T10:38:42+02:00Guillaume MelquiondError-prone behavior when cloning theoriesWhen cloning a theory, the behavior is to keep axioms as axioms, unless the user explicitly put a `with lemma foo` clause. This approach is error-prone, as it will cause (possibly inconsistent) facts to never get any proof obligation, du...When cloning a theory, the behavior is to keep axioms as axioms, unless the user explicitly put a `with lemma foo` clause. This approach is error-prone, as it will cause (possibly inconsistent) facts to never get any proof obligation, due to the user forgetting about them at clone time. I suggest that the default behavior be changed so that any cloned axiom produces a proof obligation, unless the user explicitly put a `with axiom foo` clause. For the sake of conciseness, there should be a special syntax (e.g. `with axiom *`) to skip over all the remaining cloned axioms. Another possibility would be to not turn cloned axioms into lemmas if none of their symbols got instantiated at clone time.1.0.0Andrei PaskevichAndrei Paskevich