why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2023-10-09T13:25:17+02:00https://gitlab.inria.fr/why3/why3/-/issues/803`why3 session create` should not apply transform `split_vc` by default2023-10-09T13:25:17+02:00MARCHE Claude`why3 session create` should not apply transform `split_vc` by defaultSince there is option `-a`, there is no reason to apply `split_vc` by default.
Please change the code and the documentation accordinglySince there is option `-a`, there is no reason to apply `split_vc` by default.
Please change the code and the documentation accordinglyMatteo ManighettiMatteo Manighettihttps://gitlab.inria.fr/why3/why3/-/issues/802Why3 goal oriented strategies : Correct some bugs2023-09-26T09:23:02+02:00BONNOT PaulWhy3 goal oriented strategies : Correct some bugsCurrently, the execution of goal oriented strategies from the IDE is not working.Currently, the execution of goal oriented strategies from the IDE is not working.BONNOT PaulBONNOT Paulhttps://gitlab.inria.fr/why3/why3/-/issues/801color highlighting takes too long time in IDE2023-09-25T13:57:21+02:00MARCHE Claudecolor highlighting takes too long time in IDEColor highlighting seems to take a lot of time.
It seems it tries to colorize much too many terms: it should be limited to the local context.
Limiting to the local context may indeed solve the long time issueColor highlighting seems to take a lot of time.
It seems it tries to colorize much too many terms: it should be limited to the local context.
Limiting to the local context may indeed solve the long time issuehttps://gitlab.inria.fr/why3/why3/-/issues/800RAC : Improve the validation of some CEX2023-11-08T11:42:35+01:00BONNOT PaulRAC : Improve the validation of some CEXWe have some examples of counterexamples in TrustInSoft that should be considered as valid but the Z3 and CVCx are unable to verify them.We have some examples of counterexamples in TrustInSoft that should be considered as valid but the Z3 and CVCx are unable to verify them.BONNOT PaulBONNOT Paulhttps://gitlab.inria.fr/why3/why3/-/issues/799Sexp files slow down the IDE2023-09-27T08:31:41+02:00Guillaume CluzelSexp files slow down the IDELoading a session in the IDE that contains sexp files takes a long time. Our sexp files are printed in a single line.
The problem does not exist when the session is replayed with `why3 replay`. Then it's more likely that the problem come...Loading a session in the IDE that contains sexp files takes a long time. Our sexp files are printed in a single line.
The problem does not exist when the session is replayed with `why3 replay`. Then it's more likely that the problem comes from the highlighting or the rendering of the sexp file in the IDE.
If needed, I can provide a reproducer. I'm working with Why3 version based on 7a94acebb.https://gitlab.inria.fr/why3/why3/-/issues/798Loading error when a transformation is present twice2023-09-20T15:54:42+02:00BONNOT PaulLoading error when a transformation is present twiceIn the IDE, it is possible to have the same transformation present twice at one node.
However, when loading a session where this is the case, we get a failure.
The behavior should be consistent, I think allowing the duplication of a tra...In the IDE, it is possible to have the same transformation present twice at one node.
However, when loading a session where this is the case, we get a failure.
The behavior should be consistent, I think allowing the duplication of a transformation on a node is the better choice here.BONNOT PaulBONNOT Paulhttps://gitlab.inria.fr/why3/why3/-/issues/797Add a command "why3 play"2023-09-15T16:37:44+02:00BONNOT PaulAdd a command "why3 play"That command would take a list of mlw files and try to prove them with the specified provers and strategies, saving them to a session.
It should also be able to play sessions by clearing the proof attempts (?), and try to prove all proof...That command would take a list of mlw files and try to prove them with the specified provers and strategies, saving them to a session.
It should also be able to play sessions by clearing the proof attempts (?), and try to prove all proof nodes again.
At the end it should display a short report saying how many proof attempts were successful.BONNOT PaulBONNOT Paulhttps://gitlab.inria.fr/why3/why3/-/issues/796IDE : Some improvements of the command window2023-10-16T16:57:01+02:00BONNOT PaulIDE : Some improvements of the command window- The autocompletion is triggered after we use a command (with Enter), it should not
- When using the arrow keys to look for the previous command, the autocompletion is triggered, it should not
- Add the possibility to use Ctrl+left/righ...- The autocompletion is triggered after we use a command (with Enter), it should not
- When using the arrow keys to look for the previous command, the autocompletion is triggered, it should not
- Add the possibility to use Ctrl+left/right to navigate between words
- When pasting, the newline characters are inserted, we should filter them
- Add the possibility to use left/right arrow keys to open/close a nodeBONNOT PaulBONNOT Paulhttps://gitlab.inria.fr/why3/why3/-/issues/795RAC : List functions and loops that might have a too weak contract2023-10-13T10:11:53+02:00BONNOT PaulRAC : List functions and loops that might have a too weak contractWhen the small step RAC succeeds but the giant step RAC fails, this means we have a weakness in the contract of some previous loop of function that has been executed. We should list the previously called functions/loops as being the pote...When the small step RAC succeeds but the giant step RAC fails, this means we have a weakness in the contract of some previous loop of function that has been executed. We should list the previously called functions/loops as being the potential culprits.
We should filter from this list functions from the standard library as well as whyML builtins (like `ref` for instance), to keep only user-defined functions and loops. A way to do this is to add an attribute `[@stdlib]` on all stdlib functions so that we can distinguish them easily, and an attribute `[@mlw:builtin]` for whyML builtins functions.1.8.0BONNOT PaulBONNOT Paulhttps://gitlab.inria.fr/why3/why3/-/issues/794`why3 session update --add-provers` adds too many proof nodes2023-09-26T11:05:55+02:00MARCHE Claude`why3 session update --add-provers` adds too many proof nodescurrently, adding provers in a session adds proof nodes both on root goals and on subgoals of transformations. This is not expectedcurrently, adding provers in a session adds proof nodes both on root goals and on subgoals of transformations. This is not expectedMatteo ManighettiMatteo Manighettihttps://gitlab.inria.fr/why3/why3/-/issues/793config for version 2.4.3 of Alt-Ergo does not record steps2023-09-06T17:42:12+02:00MARCHE Claudeconfig for version 2.4.3 of Alt-Ergo does not record steps1.7.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/792The session should not be considered systematically obselte when shapes are i...2023-09-06T17:23:37+02:00MARCHE ClaudeThe session should not be considered systematically obselte when shapes are ignoredThe recent option added to ignore shapes as useful, but it seems the result of merge session always reports an obsolete session. There is no reason to consider the session obsolete if all the checksums were matched exactly.The recent option added to ignore shapes as useful, but it seems the result of merge session always reports an obsolete session. There is no reason to consider the session obsolete if all the checksums were matched exactly.1.7.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/791drivers should not be searched in the current directory2023-09-07T17:33:15+02:00MARCHE Claudedrivers should not be searched in the current directoryThe driver files are currently search for in the current directory. This is a misleading feature. The semantics should be:
1. if the driver is given by a name without extension, it should be searched in the Why3 library. This is already ...The driver files are currently search for in the current directory. This is a misleading feature. The semantics should be:
1. if the driver is given by a name without extension, it should be searched in the Why3 library. This is already the case
2. is the driver is given with an extension `.drv`, and possibly with a path, it should be searched in the filesystem with the given path, *relatively* to the configuration file it is written
The case 2 is already done since #743 was solved. There is no reason anymore to search in the current directory1.7.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/790Remove axiom CompatOrderMult from Int theory of CVCx and Z3 drivers.2023-09-07T20:05:04+02:00BONNOT PaulRemove axiom CompatOrderMult from Int theory of CVCx and Z3 drivers.1.7.0BONNOT PaulBONNOT Paulhttps://gitlab.inria.fr/why3/why3/-/issues/789feature wish : goal- or more generally task-oriented proof strategies2023-10-13T10:12:37+02:00MARCHE Claudefeature wish : goal- or more generally task-oriented proof strategiesThis issue suggests a more general form of strategies, which are not blind with respect to the current goal. The idea would be to mimick the current function `Controller_itp.run_strategy on goal`, but instead of passing a quite limited p...This issue suggests a more general form of strategies, which are not blind with respect to the current goal. The idea would be to mimick the current function `Controller_itp.run_strategy on goal`, but instead of passing a quite limited parameter `Strategy.t`, would accept a function of type `task -> strat`. The type strat could be
something like
```
type strat = Do_nothing | Run_prover of prover * time * ... | Apply_trans of Trans.t * strat list
```
In the case `Apply_trans`, it is supposed to apply the given transformation, that should return the same number of subgoals as the given sublist of `strat`, and then each of these sub strat should be in turn applied to the corresponding subtask.
Such a general mechanism should permit to write complex, dedicated proof strategies that operate differently in function of the shape of the goal: e.g., decide to compute things in the goal, apply specific known lemmas for the topmost predicate symbol. A mechanism similar to Frama-C `Qed` should be doable with that mechanism.MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/788Add a meta "remove_def"2023-09-01T18:02:32+02:00BONNOT PaulAdd a meta "remove_def"This meta would allow to remove the definition of a symbol but keeping the declaration.
There already exists a meta `remove_logic` to remove a symbol as well as a meta `remove_syntax_logic` to remove the definition of a symbol by replaci...This meta would allow to remove the definition of a symbol but keeping the declaration.
There already exists a meta `remove_logic` to remove a symbol as well as a meta `remove_syntax_logic` to remove the definition of a symbol by replacing it by one in a printer. We just have to add a new meta `remove_def` that does the same as `remove_syntax_logic` but is not interpreted by the printer.1.7.0BONNOT PaulBONNOT Paulhttps://gitlab.inria.fr/why3/why3/-/issues/787Remove axioms in Z3 and CVC4 drivers2023-09-01T17:47:36+02:00BONNOT PaulRemove axioms in Z3 and CVC4 driversSome axioms should have been removed in !875 but their deletion is commented out.Some axioms should have been removed in !875 but their deletion is commented out.1.7.0BONNOT PaulBONNOT Paulhttps://gitlab.inria.fr/why3/why3/-/issues/786Improving the Why3 CLI for proving2024-01-12T14:56:18+01:00Xavier DenisImproving the Why3 CLI for provingIn the last GT we saw the new changes to `why3 session-create` and the improved `why3 bench`, during that session I proposed that it would be helpful for Why3 to provide a CLI interface of 'equal' power to the IDE, for the users of Why3 ...In the last GT we saw the new changes to `why3 session-create` and the improved `why3 bench`, during that session I proposed that it would be helpful for Why3 to provide a CLI interface of 'equal' power to the IDE, for the users of Why3 that for various reasons cannot or chose not to use the IDE.
In particular, I'm refering to the ability to run _strategies_ on targetted files, potentially creating the session if necessary.
If such a command were added it could be done as a replacement for the current `why3 prove` which is sort of misleadingly named as it does not use the sessions, even if they are available.
I think the requirements for this new / upgraded command would be:
- Load or create a session for the targeted files
- Ability to apply transformations, provers and **strategies** to goals in the file
- Should run all chosen provers and output a clear ok / reject message.
What does everyone think?https://gitlab.inria.fr/why3/why3/-/issues/785Add support for Alt-Ergo 2.4.32023-08-22T10:58:19+02:00BONNOT PaulAdd support for Alt-Ergo 2.4.3BONNOT PaulBONNOT Paulhttps://gitlab.inria.fr/why3/why3/-/issues/784Common options are read twice2023-09-06T16:00:46+02:00MARCHE ClaudeCommon options are read twiceThe common options, as declared in `Whyconf.Args.common_options`, are interpreted twice, once by the main executable (see `src/tools/main.ml`, line 18, `options_list` contains `Args.common_options`) and then again by each subcommands, ty...The common options, as declared in `Whyconf.Args.common_options`, are interpreted twice, once by the main executable (see `src/tools/main.ml`, line 18, `options_list` contains `Args.common_options`) and then again by each subcommands, typically via call to `Whyconf.Args.initialize` (for example, `why3 prove`, in `src/tools/why3prove.ml`, line 203).
Among these common options, only two are say "cumulative": `-L` and `--extra-config`, they can be given several times and they are interpreted as a list.
That means that when one types say `why3 prove -L . <...>`, `.` is added once on the loadpath, but with `why3 -L . prove <...>` it is added twice.
The fact that elements in the loadpath are duplicated is not a problem because when creating the environment, the code uses `Sstr.of_list` (line 43 of `src/core/env.ml`) so duplications are removed.
The fact that extra config files are duplicated is more problematic, though the current code in `src/driver/whyconf.ml` is quite defensive against duplication. The only visible effect I was able to obtain is as follows : first create an extra config file `myextra.conf`
```
[prover]
name = "Z3"
version = "4.8.10"
alternative = "myalt"
shortcut = "z3alt"
driver = "z3_471"
command = "z3-4.8.10 -smt2 -T:%t sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 -st %f"
command_steps = "z3-4.8.10 -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 -st rlimit=%S %f"
```
then run an example say using
```
why3 --extra-config myextra.conf prove examples/isqrt.mlw
```
and one obtains
```
Shortcut z3alt appears twice in the configuration file
```
If I remove the shortcut from the config, everything is fine. I believe this is because the code in `src/driver/whyconf.ml`, function `Rc_load.load_prover` lines 334-382, takes into account the case when a prover is already present. But it does not handle the shortcuts, which are treated elsewhere.
Of course, a workaround would to avoid the error on the duplicated shortcut, but I believe reading twice the options is the original issue there.1.7.0Guillaume MelquiondGuillaume Melquiond