why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2023-08-28T16:01:32+02:00https://gitlab.inria.fr/why3/why3/-/issues/651More options for `why3 replay`2023-08-28T16:01:32+02:00MARCHE ClaudeMore options for `why3 replay`Several wishes:
- [ ] `why3 replay --merging-only` should have different exit codes depending whether there are obsolete goals and detached goals. Should exit 0 only if no detached and no obsolete
- [ ] an option to ensures that `why3 re...Several wishes:
- [ ] `why3 replay --merging-only` should have different exit codes depending whether there are obsolete goals and detached goals. Should exit 0 only if no detached and no obsolete
- [ ] an option to ensures that `why3 replay` will never change the session, unlike the current behavior that changes the file when are were obsolete files and replay was successful. A kind of converse of `--force`
- [ ] document all options and return codes, including `--merging-only` which is currently not documented1.8.0https://gitlab.inria.fr/why3/why3/-/issues/706Issues with error locations2023-01-11T13:58:50+01:00Guillaume MelquiondIssues with error locationsPrompted by !760, I have tried to understand better how tools are supposed to report error locations.
Here are Emacs' expectations:
1. The first character of a line is at position 1 (even if Emacs itself counts column starting from zer...Prompted by !760, I have tried to understand better how tools are supposed to report error locations.
Here are Emacs' expectations:
1. The first character of a line is at position 1 (even if Emacs itself counts column starting from zero). A buffer setting makes it so that they are at position 0.
2. Tabulation characters count for as many positions as needed to reach the next multiple of eight. A buffer setting makes it so that they count for one.
3. Unicode characters count for one position.
Here are Vim's expectations:
1. The first character of a line is at position 1.
2. Tabulation characters count either for one position, or for as many positions as needed to reach the next multiple of eight, depending on the error format.
3. Unicode characters count for one position.
Here are Gedit's expectations (`+l:c` on command line):
1. The first character of a line is at position 1.
2. Tabulations characters count for one position.
3. Unicode characters count for one position.
Here are Why3 IDE's current expectations:
1. The first character of a line is at position 0. (Trivial to change.)
2. Tabulations characters count for one. (Moderately easy to change.)
3. Unicode characters count for one position. (Almost impossible to change.)
Here is a small example that exhibits the three cases:
```
let f ()
ensures { result = 0 }
(* next is a tab *) ensures { result = 0 }
(* éééé *) ensures { [@ ééé ] result = 0 }
= 0
```
Just select the goal in the IDE and see whether the postconditions are correctly highlighted. If you want to experiment with error messages instead, just change `result` into `risult`.
As it stands (!763, !766), Why3 accommodates these expectations as follows:
1. Not satisfied for Vim (and Gedit, but that is less relevant).
2. Satisfied.
3. Almost satisfied, e.g., in the absence of combining marks.
For completeness, here is GCC's behavior:
1. The first character of a line is at position 1.
2. Tabulation characters count for as many positions as needed to reach the next multiple of eight.
3. Unicode characters count for one.
Here is Clang's behavior:
1. The first character of a line is at position 1.
2. Tabulation characters count for one position for column. They count for multiple positions for caret.
3. Unicode characters count for their number of bytes for column. They count for one position for caret.
Here is OCaml's behavior:
1. The first character of a line is at position 0.
2. Tabulation characters count for one. (Hence a broken caret.)
3. Unicode characters count for their number of bytes. (Hence a broken caret.)
Here is the LSP protocol's specification:
1. The first character of a line is at position 0.
2. Tabulation characters count for one.
3. Unicode characters count for the number of words needed to represent them in UTF-16. (Since May 2022, client and server can negotiate to count in bytes or in unicode.)https://gitlab.inria.fr/why3/why3/-/issues/673Warning: [add_registered_transformation] FATAL transformation already present2022-11-16T13:33:15+01:00Xavier DenisWarning: [add_registered_transformation] FATAL transformation already presentI feel like it's a misnomer for a warning to be fatal ;)
I wasn't able to reduce this session for obvious reasons (why3 won't open at all).
[Archive.zip](/uploads/66a9081078b64a47c358f5309b2caa97/Archive.zip)I feel like it's a misnomer for a warning to be fatal ;)
I wasn't able to reduce this session for obvious reasons (why3 won't open at all).
[Archive.zip](/uploads/66a9081078b64a47c358f5309b2caa97/Archive.zip)https://gitlab.inria.fr/why3/why3/-/issues/693Location warning due to overly long argument due to proof bisection2022-10-03T10:23:29+02:00Guillaume MelquiondLocation warning due to overly long argument due to proof bisectionProof bisection introduces a "remove" transformation in the proof session. It has an argument that lists all the useless symbols. This list can contain hundreds of symbols and thus exceeds 4096 characters. In turn, this causes Why3 to sp...Proof bisection introduces a "remove" transformation in the proof session. It has an argument that lists all the useless symbols. This list can contain hundreds of symbols and thus exceeds 4096 characters. In turn, this causes Why3 to spew warnings in the IDE or when replaying sessions, e.g.,
```console
$ bin/why3 replay --merging-only -L examples/multiprecision/ examples/multiprecision/mpz_set_str
Warning: Loc.user_position: end char number `4098` overflows on next line
```
We should not warn about things that are out of the control of the user.https://gitlab.inria.fr/why3/why3/-/issues/430Local config file common to all Why3 commands2022-03-22T16:55:26+01:00MARCHE ClaudeLocal config file common to all Why3 commandsSuggestion: if a file with a fixed name, for example `.why3`, is present in the directory of a loaded file (source or session) then do as if it was given as a `--extra-config`. It would be a nice alternative to systematically passing `-L...Suggestion: if a file with a fixed name, for example `.why3`, is present in the directory of a loaded file (source or session) then do as if it was given as a `--extra-config`. It would be a nice alternative to systematically passing `-L .` on the command-line for example.https://gitlab.inria.fr/why3/why3/-/issues/135why3 does not support symbolic links2022-03-11T19:34:31+01:00Guillaume Melquiondwhy3 does not support symbolic links```
ln -s /tmp foo
touch bar.mlw
why3 ide foo bar.mlw
why3 ide foo
```
`anomaly: Sys_error("foo/../bar.mlw: No such file or directory")````
ln -s /tmp foo
touch bar.mlw
why3 ide foo bar.mlw
why3 ide foo
```
`anomaly: Sys_error("foo/../bar.mlw: No such file or directory")`https://gitlab.inria.fr/why3/why3/-/issues/494Bogomips2021-02-11T10:37:52+01:00Guillaume MelquiondBogomipsWhen replaying a proof, Why3 multiplies the previous running time by 2 when setting the time limit. This allows for some variance in the execution of provers or in the load of the computer. Unfortunately, this is too large a variance whe...When replaying a proof, Why3 multiplies the previous running time by 2 when setting the time limit. This allows for some variance in the execution of provers or in the load of the computer. Unfortunately, this is too large a variance when replaying a proof on the same computer, and this is too small when replaying on a computer with vastly different specifications. Moreover, for provers that use the time limit to guide their heuristics, this can completely change their behavior.
Suggestion: Run a bogomips-like test at `why3 config` time and store the result into `why3.conf`. Store the value inside proof sessions. Compare the session-stored and configuration-stored values when replaying a session to better choose the allowed variance in running time.https://gitlab.inria.fr/why3/why3/-/issues/513Why3dep ?2020-11-18T11:40:30+01:00François BobotWhy3dep ?For writing rules for a build system it would be interesting to have a way to compute the dependencies of an `.mlw`
More precisely for the extraction we want to know all the file that will be used by why3:
- because of clone the depen...For writing rules for a build system it would be interesting to have a way to compute the dependencies of an `.mlw`
More precisely for the extraction we want to know all the file that will be used by why3:
- because of clone the dependencies must be recursive
- it still be nice to be able to choose recursive or not for perhaps avoiding parsing many times the same dependency.
Note de GT