why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2024-01-18T11:31:15+01:00https://gitlab.inria.fr/why3/why3/-/issues/810Strategy for forward error computation2024-01-18T11:31:15+01:00BONNOT PaulStrategy for forward error computationCreate a new theory for unbounded floats, which are float numbers with no upper bound on the exponent.
Add a goal oriented strategy to automatically compute forward error for float terms if possible.Create a new theory for unbounded floats, which are float numbers with no upper bound on the exponent.
Add a goal oriented strategy to automatically compute forward error for float terms if possible.BONNOT PaulBONNOT Paulhttps://gitlab.inria.fr/why3/why3/-/issues/809Improvements on goal oriented strategies2023-10-23T17:09:47+02:00BONNOT PaulImprovements on goal oriented strategiesExplore a way to have more control on the flow of execution of goal oriented strategies.
One thing that would be interesting would be to choose the next strat to apply based on the result of a strategy, ie. dynamically generate an order ...Explore a way to have more control on the flow of execution of goal oriented strategies.
One thing that would be interesting would be to choose the next strat to apply based on the result of a strategy, ie. dynamically generate an order of execution.
For instance, we could apply a transformation that generates a list of subtasks, and then instead of applying strats to the subtasks in the subtasks creation order, the order is specified by the strategy.BONNOT PaulBONNOT Paulhttps://gitlab.inria.fr/why3/why3/-/issues/808Command completion issues in the IDE2023-10-19T16:57:56+02:00BONNOT PaulCommand completion issues in the IDE#796 introduced some bugs in the command line completion that need to be fixed.#796 introduced some bugs in the command line completion that need to be fixed.BONNOT PaulBONNOT Paulhttps://gitlab.inria.fr/why3/why3/-/issues/807Why3 should allow to compile several engines for invariant inference simultan...2023-10-06T15:34:04+02:00MARCHE ClaudeWhy3 should allow to compile several engines for invariant inference simultaneouslyThe function `Vc.set_infer_invs` allows to record one engine to infer invariants, if one records a second it will replace the former recorded one. We should allow several such engines.The function `Vc.set_infer_invs` allows to record one engine to infer invariants, if one records a second it will replace the former recorded one. We should allow several such engines.MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/806Attribute tags should not be stored in sexp2023-10-02T21:56:34+02:00Matteo ManighettiAttribute tags should not be stored in sexpCurrently tags for attributes are hardcoded in the `sexp` output, resulting in clashes when these are read backCurrently tags for attributes are hardcoded in the `sexp` output, resulting in clashes when these are read back1.7.0Matteo ManighettiMatteo Manighettihttps://gitlab.inria.fr/why3/why3/-/issues/805Error with function literals2023-09-29T11:50:18+02:00Xavier DenisError with function literalsI was trying to use function literals as a way to encode sequence literals, but very quickly hit an issue:
```
use seq.Seq
let boom x : seq int = Seq.create 1 [| x |]
```
The following program fails to load saying `File "../broken.ml...I was trying to use function literals as a way to encode sequence literals, but very quickly hit an issue:
```
use seq.Seq
let boom x : seq int = Seq.create 1 [| x |]
```
The following program fails to load saying `File "../broken.mlw", line 3, characters 28-29: Logical symbol (=) is used in a non-ghost context`
It seems like the desugaring for function literals does not work well in program contexts?https://gitlab.inria.fr/why3/why3/-/issues/804support for Alt-Ergo 2.5.12023-09-29T11:46:32+02:00MARCHE Claudesupport for Alt-Ergo 2.5.1Alt-Ergo 2.5.1 is out since Sep 28. We should support it for Why3 1.7.0.
We could just add support with the native syntax. The support for the SMT-LIB input is more future work, with needed tests for new features in particular bitvector...Alt-Ergo 2.5.1 is out since Sep 28. We should support it for Why3 1.7.0.
We could just add support with the native syntax. The support for the SMT-LIB input is more future work, with needed tests for new features in particular bitvectors and counterexamples.1.7.0MARCHE ClaudeMARCHE Claudehttps://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 Claude