why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2019-05-21T11:36:47+02:00https://gitlab.inria.fr/why3/why3/-/issues/8Allow undo after removing node in task tree2019-05-21T11:36:47+02:00MARCHE ClaudeAllow undo after removing node in task treeUndo would be more useful.
For the moment, removing a node (using the Delete key) is applied without confirmation, and without
any way to undo this effect. There should be some protection:
- asking for confirmation with a dialog window,...Undo would be more useful.
For the moment, removing a node (using the Delete key) is applied without confirmation, and without
any way to undo this effect. There should be some protection:
- asking for confirmation with a dialog window, as in former IDE ? but could become painful now...
- option: configure whether such a confirmation should be asked in the preferences, as it is done
already for saving session at exit?
- or: implement some "undo" feature: seems really hard with the current implementation of sessions
- or: implement a temporary "trash" directory for recoveringhttps://gitlab.inria.fr/why3/why3/-/issues/27Sequence literals2020-12-17T10:27:16+01:00Guillaume MelquiondSequence literalsCurrently, the only non-singleton data structure for which literal constants can be provided is the `list` type. This is especially limiting, since both interpretation and extraction can easily take advantage of random access data struct...Currently, the only non-singleton data structure for which literal constants can be provided is the `list` type. This is especially limiting, since both interpretation and extraction can easily take advantage of random access data structures. So it would be worth having an input syntax for expressing literals for such structures and propagating these constants as far as possible in the system. A few questions to answer:
1. What is the syntax? The OCaml syntax `[| ... ; ... |]` might be fine.
2. What is the type of such a literal? Should it have a fixed type (e.g. `seq 'a`)? Or should its type depend on the context so that one can use this syntax to input program arrays?
3. How should it be translated to provers that do not support such literals? Using `epsilon s. length s = ... /\ s[0] = ... /\ ...` might be both effective and cheap implementation-wise.https://gitlab.inria.fr/why3/why3/-/issues/30Refresh does not reload source view, causing loss of work2019-10-25T15:12:27+02:00Raphaël Rieu-HelftRefresh does not reload source view, causing loss of workRefreshing the session with Ctrl-R does not reload the source view. I lost work from this with the following steps:
1) Open Why3 ide
2) Edit the source file in your favorite editor
3) Reload (source view does not change)
4) Edit the ...Refreshing the session with Ctrl-R does not reload the source view. I lost work from this with the following steps:
1) Open Why3 ide
2) Edit the source file in your favorite editor
3) Reload (source view does not change)
4) Edit the file from Why3 ide (in my case, inadvertently by pressing tab a few times in the ide), save file
5) You lose the work from 2)MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/51Instantiation of mutable type symbol when cloning2019-01-28T14:35:28+01:00CLOCHARD MartinInstantiation of mutable type symbol when cloningThere are several problems in cloning when dealing with mutable type symbols.
1) One cannot instantiate a private mutable type with a type application:
```
module A0
type t = private mutable {}
end
module A1
use import ref.Ref
cl...There are several problems in cloning when dealing with mutable type symbols.
1) One cannot instantiate a private mutable type with a type application:
```
module A0
type t = private mutable {}
end
module A1
use import ref.Ref
clone A0 with type t = ref int
end
```
fail with error `Illegal instantiation for symbol t`. However, replacing `ref int`
by an alias works. This problem only arises for abstract mutable types.
2) If one instantiate a private mutable type `t` with a non-mutable type in a module
which also contains a `val` taking an element of `t` as argument:
```
module A0
type t = private mutable {}
val g (x:t) : unit
end
module A1
use import list.List
type u = list int
clone A0 with type t = u
end
```
why3 crash with exception `Invalid_argument("Ity.create_region")`.
3) If one attempt to instantiate a non-mutable type with a mutable one, why3 silently
accept the substitution by transforming the mutable type into its snapshot. This lead to
unexpected type errors in other places:
```
module A0
type t
val g (x:t) : unit
end
module A1
use import ref.Ref
type u = ref int
let g (x:u) : unit = x := 0
clone A0 with type t = u, val g = g
end
```
result in an error when instantiating `A0.g` by `A1.g`:
`This application expects a mutable type but receives {ref int}`.https://gitlab.inria.fr/why3/why3/-/issues/52warning when cloning module containing only "val"s as abstract symbols2018-08-29T16:00:53+02:00CLOCHARD Martinwarning when cloning module containing only "val"s as abstract symbolsWhen cloning a module where all abstract symbols are val, like
```
module A0
val f () : unit
end
module A1
let f () = ()
clone A0 with val f = f
end
```
Why3 sends the warning `cloned theory .A0 does not contain any abstract symb...When cloning a module where all abstract symbols are val, like
```
module A0
val f () : unit
end
module A1
let f () = ()
clone A0 with val f = f
end
```
Why3 sends the warning `cloned theory .A0 does not contain any abstract symbol; it should be used instead`. However, `A0` does contain an abstract symbol.https://gitlab.inria.fr/why3/why3/-/issues/55additional manually-written configuration files2021-02-15T16:51:08+01:00CLOCHARD Martinadditional manually-written configuration filesIt would be nice to have some additional configuration files on top of why3.conf, so that configuration is not entirely re-written by Why3 at each run. This would avoid the insertion of the "\n" in the user strategies, and prevent user d...It would be nice to have some additional configuration files on top of why3.conf, so that configuration is not entirely re-written by Why3 at each run. This would avoid the insertion of the "\n" in the user strategies, and prevent user data loss for unknown causes (this happened for some user strategies).François BobotFrançois Bobothttps://gitlab.inria.fr/why3/why3/-/issues/97range types should introduce an injectivity axiom2020-10-28T14:11:17+01:00MARCHE Clauderange types should introduce an injectivity axioma range type declaration
type t = range < a b >
generates a function `t'int` with an axiom
forall x:t. a <= t'int x <= b
but does NOT introduce any injectivity property such as
forall x y:t. t'int x = t'int y -> x = y (*...a range type declaration
type t = range < a b >
generates a function `t'int` with an axiom
forall x:t. a <= t'int x <= b
but does NOT introduce any injectivity property such as
forall x y:t. t'int x = t'int y -> x = y (*1*)
Note that the form (1) is not easy to handle by solver. A potential interesting variant
is introducing a reverse function
function t'ofInt int : t
with axiom
forall x:t. t'ofInt (t'int x) = x (*2*)
This variant has the advantage of avoiding a potential quadratic number of instanciations,
as it is the case for (1)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/156"use" in drivers is done too late2018-07-23T13:59:37+02:00Andrei Paskevich"use" in drivers is done too lateAfter the merge of ComputerEuclideanDivision, we have errors for Alt-Ergo 2.0.0:
goal ..., prover 'Alt-Ergo 2.0.0': internal failure '
Ident infix > is not yet declared'
These happen when Alt-Ergo is called after inline_all, which elim...After the merge of ComputerEuclideanDivision, we have errors for Alt-Ergo 2.0.0:
goal ..., prover 'Alt-Ergo 2.0.0': internal failure '
Ident infix > is not yet declared'
These happen when Alt-Ergo is called after inline_all, which eliminates the declaration of ">".
This particular problem can be fixed by rewriting the imported module avoiding ">" (which is ugly but will work), but the general issue is that anything imported via the driver does not go through the same transformation chain as the rest of the task.
I do not see a good solution for this right away. In fact, "use" in drivers starts to see inherently risky for me. Maybe we should simply rethink the treatment of EuclDiv and CompDiv for each major prover, aiming to have a good and sound translation in each case?François BobotFrançois Bobothttps://gitlab.inria.fr/why3/why3/-/issues/171Extraction of absurd2020-10-23T17:36:51+02:00MARCHE ClaudeExtraction of absurdExtraction of ```absurd``` is currently ```assert false``` which is perfectly fine. Though, during development it happens that ```absurd``` is temporary used on "todo" branches as one uses ``` assert false``` in OCaml. In that case, it w...Extraction of ```absurd``` is currently ```assert false``` which is perfectly fine. Though, during development it happens that ```absurd``` is temporary used on "todo" branches as one uses ``` assert false``` in OCaml. In that case, it would be a very interesting feature if the line number of the original Why3 file be given so that the "Assert_failure" exception raised could point to the proper Why3 file and the proper line. This could be done easily by inserting
```
# <line number> <mlw file name>
```
on the line before ```assert false```PARREIRA PEREIRA Mário JoséPARREIRA PEREIRA Mário Joséhttps://gitlab.inria.fr/why3/why3/-/issues/176Miscellaneous feature wishes for discussion2018-08-31T14:18:20+02:00Benedikt BeckerMiscellaneous feature wishes for discussionHere is a small list of features I missed in Why3 1.0 for discussion:
1. The error message `Error in transformation function: apply: there are N terms missing` would be vastly more useful if it included the names of the `N` missing term...Here is a small list of features I missed in Why3 1.0 for discussion:
1. The error message `Error in transformation function: apply: there are N terms missing` would be vastly more useful if it included the names of the `N` missing terms. Possible?
1. Applying a transformation with superfluous arguments or with missing keys (e.g., `with`) results in the error messages `First arguments were parsed and typed correctly but the last following are useless:`, which is not fully clear. Maybe `The last N arguments are not applicable (or did you miss a keyword?)`?
1. When trying to apply a transformation a second time, the IDE only prints message `Transformation already applied`. The IDE could additionally jump to the corresponding VC as if the transformation was applied for the first time.
1. Reloading (`C-r`) is slow for large files (>1k lines), also when they contain parsing/typing errors. (Errors are detected quickly in large files by `why3 prove`.) Could the IDE check for errors before spending a lot of time on other tasks?
1. After verifying one VC the IDE jumps to the *first* unverified VC in the module. It would be more intuitive if it jumped to the *next* unverified VC (or not at all)
1. The following syntax would be useful `fun (x, y) -> ...`
1. The following syntax would be useful in `inductive`: `let (x, y) = ...` (it currently causes the error `Ill-Formed inductive clause ...` but `let xy = ...` is OK)
1. Propagate small dot-symbol of previously succeeded but outdated proofs to the VC
1. Focus/Unfocus should be under menu View not Tools
1. Keyboard shortcuts to jump between commands and tree
1. A table of content for generated documentation (`why3 doc`) including headings `{N ...}` whould be useful to navigate in large files.https://gitlab.inria.fr/why3/why3/-/issues/193usage of array.Array should not enforce polymorphic VCs2021-02-11T10:42:47+01:00MARCHE Claudeusage of array.Array should not enforce polymorphic VCsIn Why3 0.88, for a program importing `array.Array` but wasn't using any other polymorphic types, the resulting tasks were not polymorphic and were consequently easier to discharge by SMT solvers.
Would it be possible to ignore the pol...In Why3 0.88, for a program importing `array.Array` but wasn't using any other polymorphic types, the resulting tasks were not polymorphic and were consequently easier to discharge by SMT solvers.
Would it be possible to ignore the polymorphism of the new array type in Why3 1.0 ?https://gitlab.inria.fr/why3/why3/-/issues/196Interaction of smt encoding with meta2021-03-13T00:53:06+01:00DAILLER SylvainInteraction of smt encoding with metaHello,
For the support of counterexamples, I am trying to add meta on a polymorphic functions but it seems that the transformation `encoding_smt_if_poly` breaks the meta I introduced when it monomorphizes the function. I would have expe...Hello,
For the support of counterexamples, I am trying to add meta on a polymorphic functions but it seems that the transformation `encoding_smt_if_poly` breaks the meta I introduced when it monomorphizes the function. I would have expected the meta to be adapted (by the transformation) to the generated ident for the monomorphized function.
For example, the following task:
```
function length (array 'a) : int
(* meta my_meta function length *)
```
is translated to:
```
function length ty uni : uni
(* meta my_meta function length1 *)
```
Note that length1 seem to still refer to the first definition whereas it does not appear anymore in the task: its only apparition is in the meta declaration. Is there a way to keep the meta on my monomorphized function or should I find another solution ?Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/201Document extraction of clonable/cloned modules2021-02-11T10:42:27+01:00MARCHE ClaudeDocument extraction of clonable/cloned modulesI'd like to extract to OCaml a WhyML code that clones `appset.Appset`. How is it supposed to work?I'd like to extract to OCaml a WhyML code that clones `appset.Appset`. How is it supposed to work?https://gitlab.inria.fr/why3/why3/-/issues/202Document syntax of clone2018-11-13T19:00:01+01:00DAILLER SylvainDocument syntax of cloneHello,
I did not find explanation of this syntax (and equivalents) in the doc:
`clone export A with axiom .`
Can this be added ?Hello,
I did not find explanation of this syntax (and equivalents) in the doc:
`clone export A with axiom .`
Can this be added ?https://gitlab.inria.fr/why3/why3/-/issues/204Syntax of drivers is not documented2018-10-10T14:28:14+02:00DAILLER SylvainSyntax of drivers is not documentedThe syntax of drivers is not documented. I think it should be. In particular difference between `syntax function` `syntax converter` etc..The syntax of drivers is not documented. I think it should be. In particular difference between `syntax function` `syntax converter` etc..https://gitlab.inria.fr/why3/why3/-/issues/211Questions on labels2018-12-17T11:14:52+01:00DAILLER SylvainQuestions on labelsHello,
It's not quite clear to me what the standard usage of labels is/should be. Here are some questions in comments of an example:
```
module Labels
use int.Int
type r = {mutable f :int}
val z : r
let f1 (x: r) : unit =
...Hello,
It's not quite clear to me what the standard usage of labels is/should be. Here are some questions in comments of an example:
```
module Labels
use int.Int
type r = {mutable f :int}
val z : r
let f1 (x: r) : unit =
z.f <- 5;
label L in
z.f <- 7;
let f2 (x : r) : unit =
x.f <- 8;
(*assert { x at L = x}; (* B1: Should this be: "x not defined at L" ? *)*)
in
f2 x
let f3 (x: r) : unit =
z.f <- 5;
label L in
z.f <- 7;
let f2 (x : r) : unit =
x.f <- 8;
assert { z at L = x} (* B2:Should this be forbidden ? Label is not in the current function *)
in
let f3 (x: r) : unit =
x.f <- 42;
(*assert { z at L1 = x} (* B3: Should this be allowed ? Label is after the definition *)*)
in
label L1 in
f3 x;
f2 x
let f4 (x: r) : unit =
z.f <- 5;
label L in
z.f <- 10;
label L in (* B4: Should there be a warning here because the first label become not accessible ? *)
z.f <- 11;
assert {z at L = z at L}
let f5 (x:r) : unit =
z.f <- 5;
(* assert {z at L = z} (* B5: Should this be allowed ? Label is in another toplevel function *)*)
end
```https://gitlab.inria.fr/why3/why3/-/issues/215Extraction des foncteurs2021-02-11T10:41:17+01:00François BobotExtraction des foncteursLes clones et l'extraction vers les foncteurs sont expérimentales. Pour les utilisateurs expert on pourrait essayer d'ajouter des exemples. On pourrait également réfléchir a ajouter des constructions dans les drivers pour simplifier l'ex...Les clones et l'extraction vers les foncteurs sont expérimentales. Pour les utilisateurs expert on pourrait essayer d'ajouter des exemples. On pourrait également réfléchir a ajouter des constructions dans les drivers pour simplifier l'extraction des modules (juste "module M va vers module N") et foncteurs (juste "c'est un foncteur avec ce mapping des arguments").
- [ ] Ajouter des exemples d'utilisation
- [ ] Ajouter un printer de mli dans l'extraction OCaml
- [ ] Réflexion sur extension des drivershttps://gitlab.inria.fr/why3/why3/-/issues/230Add warning to anonymous function without ensures2018-11-07T09:52:46+01:00DAILLER SylvainAdd warning to anonymous function without ensuresIn the following program, the contract of the intermediate function is not inferred automatically by Why3 (it apparently cannot be in the general case): in particular, the assignment to b is not reflected in the generated tasks. This iss...In the following program, the contract of the intermediate function is not inferred automatically by Why3 (it apparently cannot be in the general case): in particular, the assignment to b is not reflected in the generated tasks. This issue is for generating a warning when such function do not carry a postcondition:
```
use int.Int
use int.MinMax
use ref.Ref
let f3 (a b : ref int) (c d: int)
requires { c < d }
ensures { result = min c d /\ !b = 22 }
=
a :=
(fun () -> if c < d then
(b := 4; c)
else
d) (* Here we should probably add a postcondition *) ();
!a + !b
```Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/233Improve apply2018-11-07T11:08:46+01:00DAILLER SylvainImprove applyIn some cases, we would like apply to perform matching on hypothesis too. Coq can do that in:
```
Goal forall P Q, (forall x y, P x y -> Q) -> P 3 4 -> Q.
intros P Q H H1.
apply H with (1:=H1).
```
We could imagine:
`apply H with_hyp ...In some cases, we would like apply to perform matching on hypothesis too. Coq can do that in:
```
Goal forall P Q, (forall x y, P x y -> Q) -> P 3 4 -> Q.
intros P Q H H1.
apply H with (1:=H1).
```
We could imagine:
`apply H with_hyp H1`
To be investigated.MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/242Division and comparison in SMT and Alt-ergo2021-02-11T10:40:57+01:00François BobotDivision and comparison in SMT and Alt-ergoIt seems that we have no lemmas that relate real division and comparison. It is the case for provers that doesn't have built-in these symbol because `/.` is defined with `inv` and `*.`, and because `*.` is said monotone.It seems that we have no lemmas that relate real division and comparison. It is the case for provers that doesn't have built-in these symbol because `/.` is defined with `inv` and `*.`, and because `*.` is said monotone.https://gitlab.inria.fr/why3/why3/-/issues/246Allow "use ghost Foo"2019-05-21T15:37:41+02:00Guillaume MelquiondAllow "use ghost Foo"It might happen that one wants to use a module for specification and ghost code, but not for actual code (and a fortiori extraction). A good example is `int.Int` which is ubiquitous in WhyML programs but not necessarily in extracted prog...It might happen that one wants to use a module for specification and ghost code, but not for actual code (and a fortiori extraction). A good example is `int.Int` which is ubiquitous in WhyML programs but not necessarily in extracted programs.
It would be good to have a way in the surface language to express and enforce that such a module is not meant to be actually used. Proposed syntax: `use ghost int.Int`. This would also make the extraction a lot less adhoc with respect to these modules.
A possible implementation would be to flag the corresponding scopes as being restricted. Any symbol accessed through such a scope would be forbidden to occur in non-ghost code. The change in `Why3extract.use_fold` would be trivial.
Open questions:
- what if the user do both `use` and `use ghost`?
- what if the user do `use ghost` on a module with toplevel side effects?https://gitlab.inria.fr/why3/why3/-/issues/272CVC4 for smtlib 2.62022-03-22T16:55:27+01:00DAILLER SylvainCVC4 for smtlib 2.6Apparently, the semantics of bvurem changed from smtlib 2.5 to 2.6 quoting Andres Nötzli from cvc-users mailing list:
> Yes, the semantics changed in version 2.6 [0]. `(bvurem s t)` returns `s` if `t` is zero (before, the value was a fr...Apparently, the semantics of bvurem changed from smtlib 2.5 to 2.6 quoting Andres Nötzli from cvc-users mailing list:
> Yes, the semantics changed in version 2.6 [0]. `(bvurem s t)` returns `s` if `t` is zero (before, the value was a fresh constant). CVC4 automatically chooses the semantics that matches the SMT-LIB version. You can manually toggle the behavior with --(no-)bv-div-zero-const (enabling the flag corresponds to the 2.6 version, disabling to earlier versions). If your problems only use QF_BV, you can also improve performance by compiling CVC4 with support for CaDiCaL (run the `contrib/get-cadical` script, then configure with `--cadical`) and then using the flags `--bitblast=eager --bv-sat-solver=cadical` (eager bitblasting and using CaDiCaL as the SAT solver).
Is that possible that we now need to add the option "--(no-)bv-div-zero-const" to the smt-lib provers using 2.6 ? It seems to help SPARK users.
Additional question:
Will there be a problem with the following axiom because urem seems to be linked to bvurem by smt-lib drivers ? (axioms about "mod ?x 0" do not seem to exist so I guess it is ok unless mod is also mapped by a driver?)
```
val function urem (v1 v2 : t) : t
axiom to_uint_urem:
forall v1 v2. to_uint (urem v1 v2) = mod (to_uint v1) (to_uint v2)
```https://gitlab.inria.fr/why3/why3/-/issues/278Parsing on attributes in programs2022-06-24T11:44:12+02:00DAILLER SylvainParsing on attributes in programsHello,
This issue is to keep track of discussions.
The question is the following. On why3 0.88, it was possible to add attributes to the program in order to retrieve them later in goals. This behaviour disappeared: it seems to be neede...Hello,
This issue is to keep track of discussions.
The question is the following. On why3 0.88, it was possible to add attributes to the program in order to retrieve them later in goals. This behaviour disappeared: it seems to be needed by SPARK for tracability of goals (goals A contains stuff that originate from this and that part of the code).
```
module Test
use int.Int
type d = {mutable contents: int; mutable useless: int}
let f c
ensures { c.contents = 1 }
= (*[@vc_sp]*)
c.contents <- 2;
[@This disappears] (c.contents <- 3);
c.contents <- 4
end
```
Copying potentially interested persons: @paskevyc @marche
PS: If you think people from SPARK should be involved, I can ask them to comment on this.MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/285split_all_full raises out of memory on float theory2022-03-22T16:55:27+01:00DAILLER Sylvainsplit_all_full raises out of memory on float theoryHello,
Using split_all_full on goals containing the ieee_float theory can result in out of memory (see attached file [b.mlw](/uploads/777dac8832951acc1eacf6a489be58ba/b.mlw) ). Most likely, on the hypothesis fma_special, the negative mo...Hello,
Using split_all_full on goals containing the ieee_float theory can result in out of memory (see attached file [b.mlw](/uploads/777dac8832951acc1eacf6a489be58ba/b.mlw) ). Most likely, on the hypothesis fma_special, the negative monoid generated by split_core grows exponentially (which eventually eat all available memory).
I encountered this problem when launching the strategy "1" (problem which should be solved by #282).
Is it possible to optimize the generation of monoids during the transformation, stop the splitting done by the transformation when it grows to a critical size, or disallow part of the splitting ?https://gitlab.inria.fr/why3/why3/-/issues/294Why3 IDE - close a file/tab from the IDE directly2020-10-23T17:34:58+02:00Delphine DemangeWhy3 IDE - close a file/tab from the IDE directlySuppose I start a fresh why3 module in file1.mlw.
Then, suppose I want to either read, or reuse some definitions in another previous file, file2.mlw.
So I add file2.mlw to the current session to be able to read it in the IDE.
Now, suppo...Suppose I start a fresh why3 module in file1.mlw.
Then, suppose I want to either read, or reuse some definitions in another previous file, file2.mlw.
So I add file2.mlw to the current session to be able to read it in the IDE.
Now, suppose I'm done consulting file2.mlw, and that I don't want to see it appear in the source tabs,
or that I don't want to bother with the VCs in that file.
Currently, it doesn't seem to be possible to close the tab for file2.mlw from the IDE.
When I try to remove the "module proof node", the IDE tells me :
"Cannot remove attached proof nodes or theories, and proof_attempt that did not yet return"
So, I have to close the IDE, remove the directory corresponding to the session, and relaunch the IDE, and re-start all proofs related to file1.mlw.
Being able to remove a file (file2.mlw) from a session would be more convenient.https://gitlab.inria.fr/why3/why3/-/issues/297smoke detection in ide2022-03-29T16:22:03+02:00DAILLER Sylvainsmoke detection in ideHello,
This issue is to record discussion about smoke detector on why3-club. smoke detector is a transformation that can be launched on any goal: using it may lead to an inconsistent state.
People want to keep usability of this transfo...Hello,
This issue is to record discussion about smoke detector on why3-club. smoke detector is a transformation that can be launched on any goal: using it may lead to an inconsistent state.
People want to keep usability of this transformation in the IDE. Several solutions exist to prevent errors:
- do nothing: the transformation is already described in the IDE
- allow using it only on proof nodes
- raise a warning when this transformation is called
- treat the smoke detector transformation in a specific way in the IDE/session so that smoke detected transformation do not make their parent goal appear proved. Adding an "inconsistent if reachable" value ?
[EDIT: Also make sure that the exact same smoke from why3replay can be used in IDE (or intentionally forbid it)?https://gitlab.inria.fr/why3/why3/-/issues/298Migrate to Zarith2023-09-25T14:19:39+02:00François BobotMigrate to ZarithPreviously we had to keep the num library for the why3 library because we compiled the coq-plugin. Could we now migrate to zarith?
From the [num](https://github.com/ocaml/num) website:
>This is a legacy library. It used to be part of th...Previously we had to keep the num library for the why3 library because we compiled the coq-plugin. Could we now migrate to zarith?
From the [num](https://github.com/ocaml/num) website:
>This is a legacy library. It used to be part of the core OCaml distribution (in otherlibs/num) but is now distributed separately. New applications that need arbitrary-precision arithmetic should use the Zarith library (https://github.com/ocaml/Zarith) instead of the Num library, and older applications that already use Num are encouraged to switch to Zarith. Zarith delivers much better performance than Num and has a nicer API.1.8.0François BobotFrançois Bobothttps://gitlab.inria.fr/why3/why3/-/issues/306Add program equality on Boolean type2023-08-28T16:11:06+02:00MARCHE ClaudeAdd program equality on Boolean typeTheory bool.Bool should provide (=) on Boolean type in programsTheory bool.Bool should provide (=) on Boolean type in programs1.8.0https://gitlab.inria.fr/why3/why3/-/issues/308Forall construction in code for ghost binding2019-05-10T16:00:38+02:00François BobotForall construction in code for ghost bindingSometimes when we want to prove such functions:
```
let f x : result
ensures { forall y. P(x,y) -> Q(x,y) }
```
We need to prove with a ghost variable, for easing the proof
```
let f' x (ghost y) : result
requires { P(x,y) }
ens...Sometimes when we want to prove such functions:
```
let f x : result
ensures { forall y. P(x,y) -> Q(x,y) }
```
We need to prove with a ghost variable, for easing the proof
```
let f' x (ghost y) : result
requires { P(x,y) }
ensures { Q(x,y) }
```
However it is not possible to prove the first function using the second.
We propose to add a new construction which allows it.
```
let f x : result
ensures { forall y. P(x,y) -> Q(x,y) }
=
forall y requires { P(x,y) } in
f' x y
```
The semantic of this function is not completely clear:
* should a VC be generated to check that it exists such `y`
* what if the result contains a ghost
* what if there are ghost effecthttps://gitlab.inria.fr/why3/why3/-/issues/313Why3 API backward compatibility2019-05-10T16:00:48+02:00François BobotWhy3 API backward compatibilityWhich backward compatibility should provide the Why3 API?
Backward compatibility could mean two things:
- User of an old version of the API could use the new
- New user of the API can write code that works with the old and new API
The ...Which backward compatibility should provide the Why3 API?
Backward compatibility could mean two things:
- User of an old version of the API could use the new
- New user of the API can write code that works with the old and new API
The first one implies the second one, but the first one can be defeated just by adding an optional argument.
Recently two little modifications broke the backward compatibility of Why3. The API of Why3 is quite big now, so I think it is hard to not get such cases. What can we try to do to avoid that?
- Do we give no backward compatibility insurance
- Do we add a smaller API which would be backward compatible
- Do we try to check in some ways that all the API is backward compatible with the last why3 version?https://gitlab.inria.fr/why3/why3/-/issues/315Too much ghostification?2022-03-22T16:55:27+01:00Benedikt BeckerToo much ghostification?In the following example, the ghostification that is introduced by line 16, is expanded to line 12, which results in a compilation error.
The example code works fine when `f` is non-recursive, when the `ghost` keyword is removed from li...In the following example, the ghostification that is introduced by line 16, is expanded to line 12, which results in a compilation error.
The example code works fine when `f` is non-recursive, when the `ghost` keyword is removed from line 16, or when an `; ()` is added after line 16.
```
$ cat test.mlw
module Test
use option.Option
let ref x = ()
exception E
type t = A | B
let rec f (t: t) diverges raises { E -> true } =
match t with
| A ->
x <- () (* Line 12 *)
| B ->
try
f t;
ghost () (* Line 16 *)
with E ->
raise E
end
end
end
$ why3 extract --modular -D ocaml64 -L . test.Test -o /tmp
File "./test.mlw", line 12, characters 6-13:
This expression makes a ghost modification in the non-ghost variable x
```Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/319Proved state of dependencies2019-06-05T16:38:27+02:00DAILLER SylvainProved state of dependenciesCreate something that checks that all dependencies of a module/file are proven (see why3-club). Probably better to do #318 first.Create something that checks that all dependencies of a module/file are proven (see why3-club). Probably better to do #318 first.François BobotFrançois Bobothttps://gitlab.inria.fr/why3/why3/-/issues/330Use hypotheses when doing compile_match2020-10-28T14:07:52+01:00PARREIRA PEREIRA Mário JoséUse hypotheses when doing compile_matchFor the following example:
```
use list.List
constant l: list int = Cons 42 Nil
goal G : 42 = match l with Nil -> 0 | Cons x _ -> x end
```
if I want to get a goal of the form `42 = 42`, I must do first `subst_all` and only then `compi...For the following example:
```
use list.List
constant l: list int = Cons 42 Nil
goal G : 42 = match l with Nil -> 0 | Cons x _ -> x end
```
if I want to get a goal of the form `42 = 42`, I must do first `subst_all` and only then `compile_match` is able to give me `42 = 42`.
Would it be possible for `compile_match` to use hypotheses of the form `H: e = e'` to further simplify goals of the form `match e with e' -> ... end` ?https://gitlab.inria.fr/why3/why3/-/issues/333Why3 shell improvements2019-06-07T10:27:45+02:00François BobotWhy3 shell improvementsSome proposed improvements:
[EDITED by SD: for merging my comments in the description. Completion according to !175]
* [x] `why3 shell` prints by default on stdout
* [ ] Add an option to print in a file
* [x] --quiet option to print not...Some proposed improvements:
[EDITED by SD: for merging my comments in the description. Completion according to !175]
* [x] `why3 shell` prints by default on stdout
* [ ] Add an option to print in a file
* [x] --quiet option to print nothing
* [x] restore printing of the proof tree with identifiers
* [ ] allows to put commands on the command line. Not on stdin. --batch mode
* [ ] allows to use command request Add_file to add a file to the session
* [x] Remove the debug messages: use standard Why3 debugging
* [ ] Add any other relevant features in this listFrançois BobotFrançois Bobothttps://gitlab.inria.fr/why3/why3/-/issues/337Module `Cursor` should be documented2021-09-22T10:42:56+02:00MARCHE ClaudeModule `Cursor` should be documentedPlease add documentation as why3doc comments in `stdlib/cursor.mlw`Please add documentation as why3doc comments in `stdlib/cursor.mlw`PARREIRA PEREIRA Mário JoséPARREIRA PEREIRA Mário Joséhttps://gitlab.inria.fr/why3/why3/-/issues/355Counterexamples for labels bug2023-08-28T16:07:03+02:00DAILLER SylvainCounterexamples for labels bugOn the ref_mono.mlw example, the last case (Postcondition of `test_loop`) does not include the value for the variables of "x at L" and "x at M". The invariant should appear in the task so these locations labels should appear too:
```
...On the ref_mono.mlw example, the last case (Postcondition of `test_loop`) does not include the value for the variables of "x at L" and "x at M". The invariant should appear in the task so these locations labels should appear too:
```
label M in
while !x > 0 do
(* x = 0 (0x0) *)
invariant { !x > !x at L + !x at M }
variant { !x }
x := !x - 1
done
```
should be:
```
label M in
while !x > 0 do
(* x = 0 (0x0) *)
invariant { !x > !x at L + !x at M }
(* x = ???, x at L = ???, x at M = ??? *)
variant { !x }
x := !x - 1
done
```1.8.0https://gitlab.inria.fr/why3/why3/-/issues/362overly generic logics declaration causes slowdown of cvc4 proof2023-09-11T14:23:38+02:00Johannes Kanigoverly generic logics declaration causes slowdown of cvc4 proofFlorian had identified a long time ago an issue where cvc4 would take
much longer to prove a given VC if a non-linear arithmetic was specified
compared to a linear one. See this ticket and the example in the ticket:
https://github.com/C...Florian had identified a long time ago an issue where cvc4 would take
much longer to prove a given VC if a non-linear arithmetic was specified
compared to a linear one. See this ticket and the example in the ticket:
https://github.com/CVC4/CVC4/issues/1276
On my machine, there is a factor of 10 (0.6s vs 6s) between UFBVDTLIRA
and UFBVDTNIRA when using cvc4 on the example in the issue.
We were wondering if Why3 could be more precise, e.g. detecting when
only linear operators are used. Given the potentially large speedups it
seems worthwhile. The other idea mentioned in the TN to specify
--inst-when-strict-interleave isn't an option for us.Matteo ManighettiMatteo Manighettihttps://gitlab.inria.fr/why3/why3/-/issues/368Add a Why3 lexer to Rouge2019-07-15T10:28:19+02:00Guillaume MelquiondAdd a Why3 lexer to RougeThat way, Gitlab will automatically perform syntax highlighting for `.mlw` files, as well as allow users to type
```why3
let foo () = ()
```
to get syntax highlighting in issues. Gitlab's syntax highlighting is based on [Ro...That way, Gitlab will automatically perform syntax highlighting for `.mlw` files, as well as allow users to type
```why3
let foo () = ()
```
to get syntax highlighting in issues. Gitlab's syntax highlighting is based on [Rouge](https://github.com/rouge-ruby/rouge).https://gitlab.inria.fr/why3/why3/-/issues/370Session_itp.merge_trans: Not_found2019-07-29T11:03:24+02:00Raphaël Rieu-HelftSession_itp.merge_trans: Not_foundWhile reloading a large proof, I got the error message `[Session_itp.merge_trans] FATAL unexpected exception: anomaly: Not_found` followed by a crash. I did not manage to reproduce.While reloading a large proof, I got the error message `[Session_itp.merge_trans] FATAL unexpected exception: anomaly: Not_found` followed by a crash. I did not manage to reproduce.https://gitlab.inria.fr/why3/why3/-/issues/375Why3 parsing slow2019-08-26T11:26:17+02:00Johannes KanigWhy3 parsing slowThis is an issue that we discovered together with @sdailler. I added the attached patch to why3 to mesure CPU time spent in some parts of the code (here: driver loading).[timing.patch](/uploads/47c75df43d6e56653c3a5ee6543e4d41/timing.pat...This is an issue that we discovered together with @sdailler. I added the attached patch to why3 to mesure CPU time spent in some parts of the code (here: driver loading).[timing.patch](/uploads/47c75df43d6e56653c3a5ee6543e4d41/timing.patch)
With this patch I was able to determine that on some file (I don't think it matters which), if I ask why3 to load e.g. the cvc4 driver:
```
why3 prove -P CVC4 <somefile>
```
loading the driver takes roughly 0.1 seconds. With @sdailler we found that it isn't actually loading drivers that is slow, but the reading of the why3 libs referenced from the driver.
In SPARK we have switched to a mode where we run why3 much more often than before (possibly hundreds of times on large projects) so while 0.1 seconds seems tiny, it does add up to dozens of seconds on such projects. Also, the above 0.1s measures only parts of the why3 library, while in SPARK we also have some support files which are parsed on every invocation of why3, so for us the time is closer to 0.2 or even 0.4s.
I checked the file sizes of the entire why3 stdlib, and of drivers, and everything is very small, so I'm surprised that any measurable time is spent parsing these files. Can this be improved?https://gitlab.inria.fr/why3/why3/-/issues/376handling of smoke detection in sessions2022-03-29T16:22:03+02:00Johannes Kanighandling of smoke detection in sessionsSPARK now has a switch --proof-warnings that enables a number of extra checks via VCs that are of the "smoke detection" type, that is, if they are *proved*, something is wrong (and a warning is issued to the user). I believe why3 testing...SPARK now has a switch --proof-warnings that enables a number of extra checks via VCs that are of the "smoke detection" type, that is, if they are *proved*, something is wrong (and a warning is issued to the user). I believe why3 testing also uses some kind of smoke detection.
In most cases, no smoke is detected, so the VCs remain unproved. However, the unproved goal is still stored in the session. This is not very nice when the user looks into the session, which is now polluted with lots of unproved goals, even though all "real" VCs might be proved. The user can directly see the session via why3ide, or the manual proof feature of SPARK, or even by looking at the session file (a common way of looking at the session file would be via the "diff" feature of the version control system, if the session file is checked in).
It is unclear to me how this situation should best be improved. For example, the various tools (why3ide, SPARK manual proof) could hide by default smoke detection goals. That would require such goals to be marked specially (via an attribute?). Does the Why3 team have an idea how to deal with this, given that you already have a lot of experience with smoke detection?https://gitlab.inria.fr/why3/why3/-/issues/389Add "final" specifier2021-02-11T10:39:53+01:00Raphaël Rieu-HelftAdd "final" specifierIt could be used for private types that we do not want to be refinable.It could be used for private types that we do not want to be refinable.Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/391Refining types by cloning ?2020-03-16T23:04:59+01:00DAILLER SylvainRefining types by cloning ?Hello,
After the GT of last week, I learned that it seemed to be possible to refine types by cloning. And, perhaps this issue is related to the one on "final" (and exactly why people want a final keyword ? I am not sure I understand).
...Hello,
After the GT of last week, I learned that it seemed to be possible to refine types by cloning. And, perhaps this issue is related to the one on "final" (and exactly why people want a final keyword ? I am not sure I understand).
Long story short, I was not satisfied by standard library's hashtbl (for my usage) because I wanted to have a hashtbl in which at most one element corresponds to each key. The hashtbl from standard library are àla Ocaml so they allow several addition for each key.
So, I start to refine the type as follows by adding an invariant to the type `t` stating that only list of length one are allowed:
```
module H
use int.Int
use map.Map
use list.ListRich
type key = int
type t 'a = { ghost mutable contents: map key (list 'a) }
invariant { forall k: key. length (contents k) <= 1 }
by { contents = (fun _ -> Nil) }
clone hashtbl.Hashtbl as H with
type key = key,
type t = t
```
What I would expect now is for the tool to make me prove somehow that this is compliant with the current signature of the hashtbl module ? But, instead, the definition is accepted and the following code can be proven:
```
let f (h: t int) (k: key) : unit
ensures { false }
=
H.add h k 3;
H.add h k 4
let invalid () : unit
ensures { false }
=
f (H.create 42) 1
end
```
I can use the `invalid` function like this:
```
module T
use H
let f (a: int) : int
ensures { result = 3 }
=
H.invalid ();
a
end
```
@paskevyc and others: Do you have any idea of what happens here ? Should I not be allowed to refine type `t`, should we generate new goals on the clone declaration (how?), or any other solution ?
I definitely don't want to be allowed to break the system like this (even if I did something wrong).https://gitlab.inria.fr/why3/why3/-/issues/393type invariant preservation question2019-11-27T13:19:54+01:00DAILLER Sylvaintype invariant preservation questionI have a quite simple question about the behavior of type invariant. In the simple program below, I am asked by the tool to prove a type invariant inside function `g` for variable `e` (after split). I would have expected this invariant t...I have a quite simple question about the behavior of type invariant. In the simple program below, I am asked by the tool to prove a type invariant inside function `g` for variable `e` (after split). I would have expected this invariant to be ensured in the proof for `f`. Is there a way to tell the tool "at this point of program type invariants should hold" ?
```
module Example
type r = { mutable p: int }
invariant { p = 42 }
let f (e: r)
writes {e}
ensures { true }
=
e.p <- 42
let g ()
diverges
=
let e: r = { p = 42 } in
while true do
f (e);
done
end
```https://gitlab.inria.fr/why3/why3/-/issues/394Warning on useless exception catching2019-11-08T09:19:06+01:00DAILLER SylvainWarning on useless exception catchingThis is a feature request and I don't know if it would easily be doable (it seems to be possible as the converse is notified to the user: exceptions that are raised but not caught must appear in the `raises` contract).
In the following,...This is a feature request and I don't know if it would easily be doable (it seems to be possible as the converse is notified to the user: exceptions that are raised but not caught must appear in the `raises` contract).
In the following, I would like a warning on the last line telling me that `TODO` is caught but never raised:
```
use int.Int
use ref.Ref
exception TODO
exception TODO2
let f (a: ref int)
ensures { !a = 3 }
=
try raise TODO2 with
| TODO2 -> a := 3
| TODO -> a := 4 end
```https://gitlab.inria.fr/why3/why3/-/issues/400Improve shape structures2019-10-25T16:55:23+02:00Guillaume MelquiondImprove shape structuresAs explained by @paskevyc in #276, the following could improve the situation with respect to the part of the shapes that is really needed for pairing:
"The idea is that a transformation that produces several tasks that only differ in pr...As explained by @paskevyc in #276, the following could improve the situation with respect to the part of the shapes that is really needed for pairing:
"The idea is that a transformation that produces several tasks that only differ in premises (e.g., destruct or split_vc when the goal is no more splittable) should mark these differing premises, and only them, to be included into the shape."https://gitlab.inria.fr/why3/why3/-/issues/403Localisation of errors during extraction of cloned module2019-10-31T11:25:06+01:00DAILLER SylvainLocalisation of errors during extraction of cloned moduleRecently, I tried to extract some code written in Why3 into OCaml. I did not manage to use modular extraction so I used flat extraction which seemed easier to handle. Something like:
`why3 extract -L . --recursive -D ocaml64 -D driver/o...Recently, I tried to extract some code written in Why3 into OCaml. I did not manage to use modular extraction so I used flat extraction which seemed easier to handle. Something like:
`why3 extract -L . --recursive -D ocaml64 -D driver/ocaml_ext.drv interface.mlw -o extract/all.ml`
In my Why3 code, I cloned the hasthbl.mlw file. So, I need to provide a driver for this cloned module so that I instantiate all axiomatic parts with real OCaml code. My feature wish would be to improve the error that `why3extract` outputs when it cannot find an implementation for a specific ident. I currently typically get:
```
File "$MY_PATH_TO_WHY3/why3/share/stdlib/hashtbl.mlw", line 30, characters 6-9:
Symbol mem1 cannot be extracted
```
I would like to know which chain of clone is used to find this error. For example, in my case, I clone this library two different times (not with the same key type) and in one of the cases I clone the resulting module. So, this gets pretty confusing. I would like something along the lines of:
```
Symbol mem1 cannot be extracted during cloning of Hashtbl at file my_hashtbl.mlw line 15 characters 42
The symbol is originally defined in
File "$MY_PATH_TO_WHY3/why3/share/stdlib/hashtbl.mlw", line 30, characters 6-9:
The chain of cloning is the following:
Hashtbl at file hashtbl.mlw ...
H at file my_hashtbl.mlw ...
Ha at file my_code.mlw ...
```
Looking at the code for extraction, I think that the cloning module can be tracked and the error could be better handled. I can try to look at how this could be done if there is no time ?https://gitlab.inria.fr/why3/why3/-/issues/410add realizations for modules in library fmap2020-10-28T14:05:39+01:00Jean-Christophe Filliâtreadd realizations for modules in library fmaphttps://gitlab.inria.fr/why3/why3/-/issues/417Internal error in Alt-ergo after inline_trivial2023-05-12T15:17:45+02:00Benedikt BeckerInternal error in Alt-ergo after inline_trivialAlt-ergo fails on the VC for `x` in the example below after applying the transformation `inline_trivial`:
Example:
```
use int.Int
use mach.int.Int32
lemma x: 0 < 1
```
Alt-ergo output:
```
internal failure: Ident (>) is not yet declare...Alt-ergo fails on the VC for `x` in the example below after applying the transformation `inline_trivial`:
Example:
```
use int.Int
use mach.int.Int32
lemma x: 0 < 1
```
Alt-ergo output:
```
internal failure: Ident (>) is not yet declared
```
Any ideas where this comes might come from? Too much inlining (losing the definition of `>`) or too little (retaining the use of `>`)? Removing the second line does not change the VC to my understanding but make the error disappear…
(Why3 from last Monday (8f9a5016af8) and Alt-ergo 2.2.0/2.3.0)https://gitlab.inria.fr/why3/why3/-/issues/419ppx_debug_optim step fails on windows2020-10-28T14:04:57+01:00Johannes Kanigppx_debug_optim step fails on windowsOur windows build fails as follows:
```
Ocamlopt src/extract/mlinterp.ml
'src' is not recognized as an internal or external command,
operable program or batch file.
File "src/extract/mlinterp.ml", line 1:
Error: Error while running exter...Our windows build fails as follows:
```
Ocamlopt src/extract/mlinterp.ml
'src' is not recognized as an internal or external command,
operable program or batch file.
File "src/extract/mlinterp.ml", line 1:
Error: Error while running external preprocessor
Command line: src/util/ppx_debug_optim "/it/sbx/wave/x86_64-windows64/why3/tmp/camlppx47c442" "/it/sbx/wave/x86_64-windows64/why3/tmp/camlppxbb7bd3"
```
The command line, using `VERBOSEMAKE=yes`, is
```
ocamlopt.opt -c -w A-4-9-41-44-45-50-52@5@8@48 -safe-string -keep-locs -bin-annot -dtypes -g -I lib/why3 -I C:/tokyo.a/sandbox/x86_64-windows64/opamq/install/opamrep/ocaml-system.4.07.1/lib/re -I C:/tokyo.a/sandbox/x86_64-windows64/opamq/install/opamrep/ocaml-system.4.07.1/lib/zip -I C:/tokyo.a/sandbox/x86_64-windows64/opamq/install/opamrep/ocaml-system.4.07.1/lib/menhirLib -I C:/tokyo.a/sandbox/x86_64-windows64/opamq/install/opamrep/ocaml-system.4.07.1/lib/num -I plugins/parser -I plugins/printer -I plugins/transform -I plugins/tptp -I plugins/python -I plugins/microc -I plugins/ada_terms -I src/util -I src/core -I src/driver -I src/mlw -I src/extract -I src/parser -I src/transform -I src/printer -I src/session -for-pack Why3 -ppx src/util/ppx_debug_optim src/extract/mlinterp.ml
```
This works when I copy the `src/util/ppx_debug_optim` executable to `./` and run the command again with `-ppx ppx_debug_optim`, so it has something to do with the slashes (the error message also matches this guess).
We have ocaml 4.07.1. We have a workaround for this to simply force `enable_ppx` to be false. So it's not critical right now.
Any idea what could be wrong or how to fix it?https://gitlab.inria.fr/why3/why3/-/issues/421Add support for VSCoq as additional editor for Coq2019-12-19T13:13:02+01:00MARCHE ClaudeAdd support for VSCoq as additional editor for Coq@sdailler made some experiment for that, but it seemed there was an issue to pass the option `-R` to VSCoq. To investigate@sdailler made some experiment for that, but it seemed there was an issue to pass the option `-R` to VSCoq. To investigateDIVERIO DiegoDIVERIO Diegohttps://gitlab.inria.fr/why3/why3/-/issues/424Improvement of Python plug-in2023-02-22T11:10:31+01:00MARCHE ClaudeImprovement of Python plug-inSeveral directions to which the python plugin-in could be improved
- [ ] add more cases in the dedicated external printer for terms, e.g. division and remainder operators, application using parentheses i.e. `f(x,y)` instead of `f x y`
...Several directions to which the python plugin-in could be improved
- [ ] add more cases in the dedicated external printer for terms, e.g. division and remainder operators, application using parentheses i.e. `f(x,y)` instead of `f x y`
- [ ] add the corresponding cases in the external parser for transformation arguments
- [x] document the plugin (done and available at http://why3.lri.fr/python/trywhy3_help.html)Benedikt BeckerBenedikt Beckerhttps://gitlab.inria.fr/why3/why3/-/issues/425Improvement of Micro-C plugin2023-02-22T11:10:15+01:00MARCHE ClaudeImprovement of Micro-C pluginSeveral directions to which the micro-C plug-in could be improved
- [ ] add more cases in the dedicated external printer for terms, e.g. division and remainder operators
- [ ] add the corresponding cases in the external parser for tran...Several directions to which the micro-C plug-in could be improved
- [ ] add more cases in the dedicated external printer for terms, e.g. division and remainder operators
- [ ] add the corresponding cases in the external parser for transformation arguments
- [x] document the plug-inBenedikt BeckerBenedikt Beckerhttps://gitlab.inria.fr/why3/why3/-/issues/426Simplify code for JSON handling of ITP server protocol2023-02-21T15:42:33+01:00MARCHE ClaudeSimplify code for JSON handling of ITP server protocolThe JSON layer of the ITP server protocol is currently done by ad-hoc Ocaml code. Adding a new construct in that protocol is currently painful and error-prone because several case must be added by hand. It should be simplified and made m...The JSON layer of the ITP server protocol is currently done by ad-hoc Ocaml code. Adding a new construct in that protocol is currently painful and error-prone because several case must be added by hand. It should be simplified and made more robust by using an existing OCaml library, or some PPX-based thing, for producing JSON and parsing it.https://gitlab.inria.fr/why3/why3/-/issues/429LSP server2020-02-28T14:34:26+01:00MARCHE ClaudeLSP serverThis issue aims at tracking what we would like to add to the current embryo of support of LSP for Why3
- [X] Automatic report of syntax errors and typing errors when saving the source file
- [X] go to the definition of a global symbol
...This issue aims at tracking what we would like to add to the current embryo of support of LSP for Why3
- [X] Automatic report of syntax errors and typing errors when saving the source file
- [X] go to the definition of a global symbol
- [ ] fix: go to a module name : needs to fix why3doc glob tables
- [ ] go to the definition of a local symbol
- needs to fix why3doc glob tables so as they also include local symbols
- [ ] show the type of a symbol
- again, modify the glob so as to store lsymbols, psymbols, etc. instead of idents
- [ ] utiliser user-setup dans opam pour installer le mode why3
- [ ] simple proof mode : run `split VC` then `Auto level 0` and report all VCs not proved, in the proper line of the source (like syntax errors)
- [ ] auto indentation of the current line (maybe create a separate issue)
- [ ] propose completion: show all symbols starting with current identifier, show their types
- [ ] important issue: make things, like go to def, work even on files with syntax errors
(difficult to do, may need many changes in the parser. Investigate how menhir could do
things automatically. Investigate how merlin does for OCaml)
Other secondary issues:
* discuss alternative to allowing passing options to the underlying why3 : the current solution is an extra config file named `.why3_lsp_server.conf` in the directory of the source
See also #430
* PRIORITAIRE add additional support for VScode
* PRIORITAIRE put the code of LSP-why3 directly in Why3 repositoryDIVERIO DiegoDIVERIO Diegohttps://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/432Why3 uses too much memory2020-02-11T10:49:39+01:00Guillaume MelquiondWhy3 uses too much memoryThis is a meta-issue to summarize all the discussions into a single place.
Things to do:
- [X] Do not precompute `Decl.d_sysms`, as they consume about 15% memory.
- [x] Change `split_vc` so that it introduces premises by itself instead ...This is a meta-issue to summarize all the discussions into a single place.
Things to do:
- [X] Do not precompute `Decl.d_sysms`, as they consume about 15% memory.
- [x] Change `split_vc` so that it introduces premises by itself instead of relying on `introduce_premises`. The latter has too little information to share common declarations between subtasks. This should make the memory consumption linear rather than quadratic in the number of proof obligations.
- [ ] Investigate `Decl.known_add_decl`, as its `Mid.union` call seems responsible for about 25% memory consumption.
- [x] Investigate `Termcode.task_v3`, as its `Mid.add` call seems responsible for about 25% memory consumption.
Remark: The `master` branch supports memory profiling, when using a suitable compiler, e.g., the one from the Opam switch `4.07.1+statistical-memprof`. First, configure Why3 with `--enable-statmemprof` and build it. Then, execute `bin/why3ide -L examples/multiprecision examples/multiprecision/toom`. Once the interface is loaded, execute `sturgeon-connect` in Emacs to see the memory consumption. (See Statmemprof's documentation for details about Sturgeon.)https://gitlab.inria.fr/why3/why3/-/issues/437SMT support for solvers which do not support quantifiers2022-11-03T09:48:58+01:00MARCHE ClaudeSMT support for solvers which do not support quantifiersWe should support SMT solvers even if they do not support quantifiers, like Yices 2 and mathsat.
This can be done by applying a transformation that removes quantified hypotheses, like it is done already for Colibri I think (see !112)We should support SMT solvers even if they do not support quantifiers, like Yices 2 and mathsat.
This can be done by applying a transformation that removes quantified hypotheses, like it is done already for Colibri I think (see !112)BONNOT PaulBONNOT Paulhttps://gitlab.inria.fr/why3/why3/-/issues/439Warn about spurious `rec` keyword2022-03-22T16:55:27+01:00MARCHE ClaudeWarn about spurious `rec` keywordUnlike OCaml, Why3 does not warn about useless `rec` keyword, could it do it? It would avoid strange behaviours like in
```
let rec f (x:int) ensures { result > x } = x+1
let rec ghost g (x:int) ensures { result > x } = x+1
let rec gh...Unlike OCaml, Why3 does not warn about useless `rec` keyword, could it do it? It would avoid strange behaviours like in
```
let rec f (x:int) ensures { result > x } = x+1
let rec ghost g (x:int) ensures { result > x } = x+1
let rec ghost h (x:int) variant { 0 } ensures { result > x } = x+1
```
for `f`, there is no warning, for `g` there is an error `This ghost function may not terminate`, but it is OK for `h` of course.Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/440Syntax `(fun x -> ...)` should always denote a lambda-expression, not a program2022-03-22T16:55:27+01:00MARCHE ClaudeSyntax `(fun x -> ...)` should always denote a lambda-expression, not a programIt seems that in the current Why3, the syntax `(fun x -> e)` is interpreted either as a logic function or as a program function, depending on the context. For example in
```
let test () =
let ref f = (fun x -> x+1) in
assert { f 0 = ...It seems that in the current Why3, the syntax `(fun x -> e)` is interpreted either as a logic function or as a program function, depending on the context. For example in
```
let test () =
let ref f = (fun x -> x+1) in
assert { f 0 = 1 };
let g = (fun x -> x+1) in
assert { g 1 = 2 }
```
the first function `f` is a logic function, and as such the first assert is OK, whereas the second function `g` is a program function, and the second assert triggers the error `unbound symbol g`. My arguments against considering `g` as a program function :
* This is error-prone
* The error message above is incomprehensible
* I feel there is no case where one would like to define an anonymous program function since Why3 does not support higher-order programs.https://gitlab.inria.fr/why3/why3/-/issues/443interrupt individual goals2022-05-06T14:29:00+02:00LAWALL Juliainterrupt individual goalsIt would be nice to interrupt individual goals. One may try several solvers and find that one is much faster than another. In that case, one would like to remove the slow one completely. But there seems to be no way to remove somethin...It would be nice to interrupt individual goals. One may try several solvers and find that one is much faster than another. In that case, one would like to remove the slow one completely. But there seems to be no way to remove something that is running, so the only choice seems to be a global interrupt. This then requires restarting everything else.https://gitlab.inria.fr/why3/why3/-/issues/449bisect fails when the prover returns HighFailure2020-10-28T14:53:19+01:00Raphaël Rieu-Helftbisect fails when the prover returns HighFailureWhen a prover call result is HighFailure during bisection, the bisection sometimes seems to get interrupted. It would be better to do as if the prover had not proved anything.When a prover call result is HighFailure during bisection, the bisection sometimes seems to get interrupted. It would be better to do as if the prover had not proved anything.https://gitlab.inria.fr/why3/why3/-/issues/454Update documentation2023-08-29T18:22:36+02:00MARCHE ClaudeUpdate documentationA non-exhaustive list of sections that are not up-to-date.
## High priority (for 1.4.0)
* [x] 9.4. Isabelle/HOL: needs update to isabelle 2019
* [x] 10.6. Proof Strategies: needs update to auto levels 0 to 3
* [x] document `foreach`
* ...A non-exhaustive list of sections that are not up-to-date.
## High priority (for 1.4.0)
* [x] 9.4. Isabelle/HOL: needs update to isabelle 2019
* [x] 10.6. Proof Strategies: needs update to auto levels 0 to 3
* [x] document `foreach`
* [x] document micro-C and micro-python (at least short paragraphs refering to the web pages)
* [x] document old and at (@filliatr )
* [x] document auto-dereference
## Medium priority (as soon as possible)
* [x] 7.5.2. Record types: in particular the differences between abstract/private and such, and the type invariants
* [x] 7.5.6. Module Cloning: to be completed
* [x] 4.11. Infering loop invariants: needs porting from latex to rst (@marche )
* [x] Functor extraction (@mariojppereira )
## Low priority
* [x] 7.5.1. Algebraic types
* [x] mutually recursive types and functions
* [ ] 7.6. Standard Library: expand and add more modules there
* [ ] Cursor
* [ ] Seq
* [ ] document termination/variant/etc.
* [ ] fix undefined labels and multiply-defined labels in Latex version. This seems to be a bug in sphinx, in its modules for formal grammars, which produces labels from non-terminal by replacing the underscore characters by minus, but not always. We can wait Sphinx to be fixed, or stop using underscores in non_terminals (annoying)1.8.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/458Add automated pairing tests2020-03-12T15:23:28+01:00Raphaël Rieu-HelftAdd automated pairing testsPairing bugs such as the one fixed in !342 currently go undetected until users complain. We should add a test directory with obsolete sessions of various shape numbers to check that the pairing succeeds without detached goals.Pairing bugs such as the one fixed in !342 currently go undetected until users complain. We should add a test directory with obsolete sessions of various shape numbers to check that the pairing succeeds without detached goals.https://gitlab.inria.fr/why3/why3/-/issues/472Distinguish usages of explanations2020-04-06T13:17:57+02:00MARCHE ClaudeDistinguish usages of explanationsCurrently the explanations are used by two completely different purposes:
1. Display information in IDE for the user
2. Stored in shapes for helping merging: preventing associated goals that were not of the same kind (pre, post, loop i...Currently the explanations are used by two completely different purposes:
1. Display information in IDE for the user
2. Stored in shapes for helping merging: preventing associated goals that were not of the same kind (pre, post, loop inv init, loop inv preserv, assert, etc.)
For usage 1, it is allowed to have several explanations, possible with different prefixes in the corresponding attributes. For usage 2, it is mandatory to have only one explanations. Usage 2 is potentially broken if a user adds other attributes prefixed with `expl:`.https://gitlab.inria.fr/why3/why3/-/issues/475Extraction of top-level function alias2020-10-23T17:18:56+02:00Mário PereiraExtraction of top-level function aliasConsider the following example:
```
use mach.int.Int63
let f (x y: int63) = x + y
let g = f
let a = g 42 0
```
Extracting this program results in the following ill-typed OCaml code:
```
let f (x y: int) : int = x + y
let a = g 42 0
``...Consider the following example:
```
use mach.int.Int63
let f (x y: int63) = x + y
let g = f
let a = g 42 0
```
Extracting this program results in the following ill-typed OCaml code:
```
let f (x y: int) : int = x + y
let a = g 42 0
```
This problem happens because in `compile.ml` we are simply ignoring `PDlet (LDsym (_, cty))` nodes where `cty.c_node` is not a `Cfun`. For the above example, `c_node = Capp _`.
I thought we could not define any kind of partial application at top-level at all, but it seems that function aliasing is allowed. @paskevyc is it true that we can only have a `c_node = Capp _` at top-level if it is a function aliasing, such as the above `let g = f`? It that is the case, should this be compiled as a partial application, using @rrieuhel !364 merge request?https://gitlab.inria.fr/why3/why3/-/issues/476Strange interaction between `remove module` and extraction to C2020-04-20T13:19:44+02:00Guillaume MelquiondStrange interaction between `remove module` and extraction to CCurrently, when extracting module `fxp.Fxp` to C, the resulting files `fxp.h` and `fxp.c` are basically empty. So, I tried adding `remove module` to the corresponding section of `drivers/c.drv`. Unfortunately, this breaks the extraction ...Currently, when extracting module `fxp.Fxp` to C, the resulting files `fxp.h` and `fxp.c` are basically empty. So, I tried adding `remove module` to the corresponding section of `drivers/c.drv`. Unfortunately, this breaks the extraction of `examples/multiprecision/sqrt.mlw` to C, as variables of type `fxp` are then ignored (silently!).Raphaël Rieu-HelftRaphaël Rieu-Helfthttps://gitlab.inria.fr/why3/why3/-/issues/477Extraction of interface files is too conservative2020-04-14T09:09:04+02:00Guillaume MelquiondExtraction of interface files is too conservativeWhen extracting an interface file, all the modules used by the current module are considered as dependencies. This is correct but leaks implementation details. Ideally, only the modules that define types needed to typecheck the types and...When extracting an interface file, all the modules used by the current module are considered as dependencies. This is correct but leaks implementation details. Ideally, only the modules that define types needed to typecheck the types and function signatures of the current module should be dependencies.https://gitlab.inria.fr/why3/why3/-/issues/482Spurious statements when extracting to C2020-04-29T18:13:47+02:00Guillaume MelquiondSpurious statements when extracting to CWhen extracted to C, file `multiprecision/sqrtrem.mlw` produces spurious statements such as
```c
res = wmpn_rshift(nr, nx, l, UINT64_C(1));
IGNORE2(sp,scratch);
res; // <- HERE
```
This comes from
let ghost r = wmpn_rshift_sep sp s...When extracted to C, file `multiprecision/sqrtrem.mlw` produces spurious statements such as
```c
res = wmpn_rshift(nr, nx, l, UINT64_C(1));
IGNORE2(sp,scratch);
res; // <- HERE
```
This comes from
let ghost r = wmpn_rshift_sep sp scratch l 1 in
This might be caused by an interaction between ghost results and function inlining.Raphaël Rieu-HelftRaphaël Rieu-Helfthttps://gitlab.inria.fr/why3/why3/-/issues/486MLCFG frontend : bugs with the `old` construct2020-06-18T10:59:02+02:00MARCHE ClaudeMLCFG frontend : bugs with the `old` constructThe MLCFG translation scheme does not handle correctly the `old` construct:
* for `old` occuring in the post-condition of the global 'cfg' function, the duplication of that post-condition to the internal functions generated should repla...The MLCFG translation scheme does not handle correctly the `old` construct:
* for `old` occuring in the post-condition of the global 'cfg' function, the duplication of that post-condition to the internal functions generated should replace `old t` with `at t Init` for the appropriate label `Init`.
* for `old` occuring in a code invariant, the same replacement should occur as well
(Note: I distinguish the case of code invariants since for me it is not so clear that the use of `old` should be allowed at all... it is another story)MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/487MLCFG frontend : feature wishes2021-01-26T16:04:34+01:00MARCHE ClaudeMLCFG frontend : feature wishes
* [ ] allow a `mlcfg` file to contain no module at all, like in regular WhyML
* [ ] The new keywords `cfg/var/goto/switch` should be colored in emacs and Why3 ide
* [ ] The use of the `var` section at the beginning of the body seems s...
* [ ] allow a `mlcfg` file to contain no module at all, like in regular WhyML
* [ ] The new keywords `cfg/var/goto/switch` should be colored in emacs and Why3 ide
* [ ] The use of the `var` section at the beginning of the body seems superfluous, it could suffice to allow introduction of `let in` at the beginning
* [ ] the first could have a label too
* [ ] it should not be mandatory to name invariants
* [x] allow the `rec` keyword on MLCFG functions so as to define recursive ones
* [ ] allow a variant of the switch statement were the patterns are integer constants, such as
```
switch (e)
| 1 -> ...
| 2 | 3 -> ...
| 4..7 -> ...
end
```
* [ ] allow scopes to be opened in mlcfg modules. See following code:
```
module B
scope A
let cfg test () : () = { () }
end
end
```https://gitlab.inria.fr/why3/why3/-/issues/488allow using some gtk language style other than classic.xml2020-06-21T09:04:14+02:00LAWALL Juliaallow using some gtk language style other than classic.xml/usr/share/gtksourceview-3.0/styles/classic.xml is fine for a light background, but many of the bindings result in text that is unreadable on a dark background, particularly the red and blue colors. It would be good it if the definition.../usr/share/gtksourceview-3.0/styles/classic.xml is fine for a light background, but many of the bindings result in text that is unreadable on a dark background, particularly the red and blue colors. It would be good it if the definitions considered were customizable.
I don't know gtk well enough to know whether this is a why3 specific problem.https://gitlab.inria.fr/why3/why3/-/issues/490Function symbol not found in a block of mutually recursive definitions2020-06-23T18:50:33+02:00Mário PereiraFunction symbol not found in a block of mutually recursive definitionsConsider the following example:
```
let rec function f (x: int)
ensures { result = g x }
=
g x
with function g (x: int) =
f x
```
Why3 complains with an unbound function error for the postcondition of `f`. Is this the expected beh...Consider the following example:
```
let rec function f (x: int)
ensures { result = g x }
=
g x
with function g (x: int) =
f x
```
Why3 complains with an unbound function error for the postcondition of `f`. Is this the expected behavior? Since `g` is defined using `with function`, I supposed it would be bound also for the contract of `f`.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/500Simplify bitvector module `Bv`2023-09-06T13:47:44+02:00Benedikt BeckerSimplify bitvector module `Bv`The module `Bv` for bitvectors, specifically its axiomatization, should be simplified using recent features of Why3, see
https://gitlab.inria.fr/why3/why3/-/merge_requests/393#note_378246,
https://gitlab.inria.fr/why3/why3/-/merge_reque...The module `Bv` for bitvectors, specifically its axiomatization, should be simplified using recent features of Why3, see
https://gitlab.inria.fr/why3/why3/-/merge_requests/393#note_378246,
https://gitlab.inria.fr/why3/why3/-/merge_requests/393#note_3782471.8.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/504list functions to move from "function" to "let function"2020-10-23T17:17:08+02:00Jean-Christophe Filliâtrelist functions to move from "function" to "let function"Functions in modules `list.Map`, `list.FoldLeft`, and `list.FoldRight` are currently defined as `function` but could be `let function` (to be used in non-ghost programs).Functions in modules `list.Map`, `list.FoldLeft`, and `list.FoldRight` are currently defined as `function` but could be `let function` (to be used in non-ghost programs).https://gitlab.inria.fr/why3/why3/-/issues/508Detection of rsymbol that corresponds to a constant2023-06-22T16:46:36+02:00MARCHE ClaudeDetection of rsymbol that corresponds to a constantCurrently a declaration of the form
```
val constant x : int
```
is transformed into
```
let constant x : int { ensures result = x } = fun -> any int
```
This particular encoding should be taken into account both in extraction and execut...Currently a declaration of the form
```
val constant x : int
```
is transformed into
```
let constant x : int { ensures result = x } = fun -> any int
```
This particular encoding should be taken into account both in extraction and execution.
Feature wish : provide a new OCaml function that, given a rsymbol `rs`, and possibly the environment to access to its declaration, tells whether this rsymbol is a regular function or an encoding of a constant.Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/511Smt-lib2 counterexample syntax extension2023-02-22T11:03:16+01:00Albin CoquereauSmt-lib2 counterexample syntax extensionDear Why3 dev team,
We propose an extension of the smt-lib2 model format that can handle both assertions and declaration of constants. Our proposition is to use the *new* keywords declare-const and assert to declare fresh constants and ...Dear Why3 dev team,
We propose an extension of the smt-lib2 model format that can handle both assertions and declaration of constants. Our proposition is to use the *new* keywords declare-const and assert to declare fresh constants and to express assertions, respectively.
```
(declare-const <name> <type>)
(assert <expression>)
```
The main motivation for our request is to adapt the smt-lib2 format to the (richer) counterexamples (CE) produced by our SMT solver Alt-Ergo (AE).
We recently instrumented AE to produce CE in the smt-lib2 format. However, AE can output models implying intervals (like `x in [0;100]`) or linear constraints (like `x = y + 1`) that cannot be expressed in the (too restricted) format of smt-lib2 . Now, by combining assert, declare-const, AE could produce models for such CE .
For instance, to express that a variable x is in the interval [0;100], AE could output the following model:
```
(declare-const c_x Int)
(assert (and (<= c_x 100) (>= c_x 0)))
(define-fun x () Int c_x)
```
or even simpler:
```
(declare-const x Int)
(assert (and (< x 100) (> x 0)))
```
Our proposition could also be very useful to output expressive models for other datatypes.
For instance, suppose a CE contains a record x with two labels `a` and `b` of type Int, and that `x.a in [0;100]` and `x.b = 42`. Such a model could be expressed as follows:
```
(declare-datatype t (mk (a Int) (b Int)))
(declare-const c_a Int)
(assert (and (< c_a 100)(>= c_a 0)))
(define-fun x () t (mk c_a 42))
```
As another example, suppose a CE contains an enumeration datatype `type u = A | B | C | D` and a variable i of type u which is known to be only A or B.
Such a model could be expressed as follows:
```
(declare-datatype u (A B C D))
(declare-const c_i u)
(assert (or (= c_i A) (= c_i B)))
(define-fun i () u c_i)
```
Best regards,
Alt-Ergo dev. teamhttps://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 GThttps://gitlab.inria.fr/why3/why3/-/issues/519When clauses2021-01-29T07:27:18+01:00Xavier DenisWhen clausesI promised Jean-Christophe I'd write this long ago.. 🙈.
----
In functional languages it's a common feature to be able to perform matches on constants. Since why3 doesn't support constant patterns, it complicates translations from langu...I promised Jean-Christophe I'd write this long ago.. 🙈.
----
In functional languages it's a common feature to be able to perform matches on constants. Since why3 doesn't support constant patterns, it complicates translations from languages with support for this functionality.
The challenge with adding this functionality to why3 is that patterns are desugared quite late in the compilation pipeline. Since we would like to desugar a constant pattern into an equality test, this is problematic as we must correctly resolve `=` for the type of the matched constant.
An alternative approach which is also more general would be to introduce `when` clauses. In this approach, match arms could be annotated with any boolean valued function. This function would have access to any binders created by the match arm's patterns. As this function would get typechecked with the rest of the AST, by the time we get to case-desugaring we should have no difficulty transforming it into a boolean test.
---
During a GT a few weeks ago we discussed this and several challenges and alternative solutions were proposed, unfortunately I didn't take notes at time and I no longer recall them.https://gitlab.inria.fr/why3/why3/-/issues/522why3 configuration2022-06-01T14:53:30+02:00François Bobotwhy3 configurationThe why3 configuration as never been satisfying, but the current state create even more problems.
To recall:
- before: after each update of Why3, the user needed to run `rm ~/.why3.conf && why3 config`
- now, it is not needed anymore bu...The why3 configuration as never been satisfying, but the current state create even more problems.
To recall:
- before: after each update of Why3, the user needed to run `rm ~/.why3.conf && why3 config`
- now, it is not needed anymore but the system became too complicated to be correct
This issue propose to summarize which feature we want for why3 configuration (which one to keep, which one to remove) and to details solutions.
Possible features:
1. why3 knows which solvers the user wants to consider
2. why3 knows which shortcut are available
3. why3 knows which strategy are available
4. why3 knows which editor to use
5. works with different `opam switch` at the same time
6. keep configuration for new version of why3
7. IDE configuration
8. ability to add new configuration locally
9. ability to add new solvers
10. ability to add new strategy
Features kept:
Issues on the topic: #489, #518, #469
This description will be updated with the discussion.https://gitlab.inria.fr/why3/why3/-/issues/526Private types are exposed in server communication2021-01-18T10:47:49+01:00Xavier DenisPrivate types are exposed in server communicationIn Why3, IDEs are constructed using a server-client model, in which the IDE UI sends `request` to Why3 which then responds using `notification`. There is plenty of existing infrastructure that can be used to define a new IDE interface, h...In Why3, IDEs are constructed using a server-client model, in which the IDE UI sends `request` to Why3 which then responds using `notification`. There is plenty of existing infrastructure that can be used to define a new IDE interface, however, if you wish to serialize these requests and notifications, you can encounter problems. In my case I am using (`ppx_deriving_yojson` / `ocaml-rpc`) but these problems are independent of the tool used.
Specifically, the `notification` includes the `proof_attempt_status` type indirectly through `update_info`. This type has two problems when attmepting to derive serialization structurally, one minor and one more serious:
1. The `InternalFailure` constructor has an `exn` type field which should not / cannot be serialized.
2. The `Done` constructor includes the the `model` type through `Call_provers.prover_result`, `model` is opaque, and it's uncledar how it should be properly serialized as a result.
Since `notification` is part of the IDE api boundary I feel like it should be possible to roundtrip notifications, or at least _fully_ serialize them.
The most immediate solution that occurs to me would be to use serialization friendly representations. This seems easy for the `InternalFailure` case but less clear for the `model` case.https://gitlab.inria.fr/why3/why3/-/issues/531Add a deriving framework for WhyML2021-02-11T10:36:18+01:00François BobotAdd a deriving framework for WhyMLFollow #306 and Guillaume proposition:
> generate equality for enumeration type.
Should we go too `[@ deriving eq]` ?Follow #306 and Guillaume proposition:
> generate equality for enumeration type.
Should we go too `[@ deriving eq]` ?https://gitlab.inria.fr/why3/why3/-/issues/546Inductive proofs on inductives2021-02-11T10:35:12+01:00Loïc CorrensonInductive proofs on inductivesThis is a proposal feature allowing inductive proofs over inductive predicates in why3.
Consider an inductive predicate `P` as follows:
```
inductive p xs = A: forall ys. hs -> p es | ...
```
The idea is to automatically generate the ...This is a proposal feature allowing inductive proofs over inductive predicates in why3.
Consider an inductive predicate `P` as follows:
```
inductive p xs = A: forall ys. hs -> p es | ...
```
The idea is to automatically generate the following items:
- `type p'witness = A ys | ...` witnessing the universally quantified variables obtained to build a proof of `p` with each constructor
- `val ghost function p'proof xs : p'witness` returns, under precondition `p xs`, a witness of its (minimal) proof.
- `val ghost function p'induction xs : int` returns a (decreasing) variant over the proof of `p xs`.
The post condition of `p'proof xs` introduces, for each witness constructor `A ys` the hypotheses `hs` and the associated unifications of `es` and `xs`, together with strictly decreasing variants of `p'induction` for any sub-proofs of `p` in `hs`.
A complete example of how this can be used in practice is provided here:
- [ind.mlw](/uploads/a336611a3844c6a68dcbc8debfa44960/ind.mlw): full example of use of the generated symbols
(including also why3/why3#547 although it is not necessary…).
- [ind_gen.mlw](/uploads/d42763ecbdab345676b472d7d8fecdb6/ind_gen.mlw): the full exemple together with the (axiomatized) generated symbols, that makes the lemma proof automatically discharged easily.
- [ind.v](/uploads/042c16623daa356c4ef5ef0b792d3e06/ind.v): a Coq realization of the generated symbols of the example using destruction of the inductive predicate in `Type` (we can not realize modules... yet, although it shall look like this).
- [ind_fol.mlw](/uploads/dbf0d183aa20786db2437064782ba440/ind_fol.mlw): a fully proven Why-3 reference implementation (without inductives) for all the generated symbols of the example.https://gitlab.inria.fr/why3/why3/-/issues/547Syntactic sugar for lemma functions2021-04-09T08:27:17+02:00Loïc CorrensonSyntactic sugar for lemma functionsThe following syntactic sugar for automatically introduce proof-based lemma functions:
```
lemma a: forall xs. hs -> p [variant { v }] [do t done] [with …]
```
This automatically generates:
```
let [rec] lemma a'apply xs requires { hs...The following syntactic sugar for automatically introduce proof-based lemma functions:
```
lemma a: forall xs. hs -> p [variant { v }] [do t done] [with …]
```
This automatically generates:
```
let [rec] lemma a'apply xs requires { hs } ensures { p } [variant {v}] = begin t end
[with …]
```https://gitlab.inria.fr/why3/why3/-/issues/552RFC: binders for tuple components in function prototype2021-02-11T10:43:19+01:00Jean-Christophe FilliâtreRFC: binders for tuple components in function prototypeIt would be useful if we could name tuple components in function prototypes e.g.
```
val f (x: int, y: int) : (r: int)
requires { x < 0 && y > 0 }
ensures { r = x + y }
```
Currently, we have to bind the tuple and then decompose it ...It would be useful if we could name tuple components in function prototypes e.g.
```
val f (x: int, y: int) : (r: int)
requires { x < 0 && y > 0 }
ensures { r = x + y }
```
Currently, we have to bind the tuple and then decompose it in every clause of the contract:
```
val f (p: (int, int)) : (r: int)
requires { let x, y = p in x < 0 && y > 0 }
ensures { let x, y = p in r = x + y }
```https://gitlab.inria.fr/why3/why3/-/issues/557Build a glossary of error messages2022-11-04T16:33:12+01:00MARCHE ClaudeBuild a glossary of error messagesThere are quite a lot of possible error messages from Why3, in particular from typing. It would help beginners, and indeed all users, if all these messages where explained in the manual, hopefully with examples.
Note: there should be a...There are quite a lot of possible error messages from Why3, in particular from typing. It would help beginners, and indeed all users, if all these messages where explained in the manual, hopefully with examples.
Note: there should be at least one example exhibiting each error message anyway, in `bench/typing/bad'https://gitlab.inria.fr/why3/why3/-/issues/567wish: provide monomorphic, clonable modules for references and arrays2024-02-13T17:09:15+01:00MARCHE Claudewish: provide monomorphic, clonable modules for references and arraysPolymorphism is raising several issues. Currently the encoding from Spark to Why3 carefully avoids to produce any polymorphism in the WhyML generated, because provers CVC4 and Z3 are better when tasks have no polymorphism. The counterexa...Polymorphism is raising several issues. Currently the encoding from Spark to Why3 carefully avoids to produce any polymorphism in the WhyML generated, because provers CVC4 and Z3 are better when tasks have no polymorphism. The counterexample features are essentially broken in presence of polymorphism. In the current implementation of "jessie3" in collaboration with TIS, I had to suggest to avoid producing WhyML code involving polymorphism, both for proving efficiency and counterexamples. Recently, Quentin came up with the following trivial example
```
use int.Int
use array.Array
let update a i (v:int)
requires { 0 <= i < length a }
ensures { a[i] = v }
= a[i] <- v
```
which is easily solved by Alt-Ergo, but not by CVC4 nor Z3.
I suggest:
- to provide monomorphic clonable versions of ref.Ref and array.Array in the stdlib, which would allow to program without polymorphism unless needed elsewhere
- to review to current support of polymorphism in Why3: are the drivers appropriate? it seems that in Why3 0.xx, using modules ref.Ref or array.Array was *not* enforcing polymorphism in the generated tasks, but since Why3 1.0 tasks generated are always polymorphic because of type `ref'mk 'a` or `array'mk 'a`https://gitlab.inria.fr/why3/why3/-/issues/568unused variables2021-04-01T13:44:23+02:00Jean-Christophe Filliâtreunused variablesWhen function parameters are not used in spec/code, Why3 emits a warning, which is useful.
But it does not for unused variables in the function result.
For instance
```
val f (x: int) : (y:int, z: int)
ensures { true }
```
emits a warn...When function parameters are not used in spec/code, Why3 emits a warning, which is useful.
But it does not for unused variables in the function result.
For instance
```
val f (x: int) : (y:int, z: int)
ensures { true }
```
emits a warning about `x` being unused, but does not complain about `y` and `z` being ununsed.https://gitlab.inria.fr/why3/why3/-/issues/569Use lemma function like « by » operator2021-04-09T08:37:35+02:00Loïc CorrensonUse lemma function like « by » operatorIn addition to #547, it would be very useful to call a lemma function for writing a formula (_aka_, its ensures) along with its proof (_aka_, its requires).
Hence, the semantics of `f a…` where `f` is a lemma function would be similar t...In addition to #547, it would be very useful to call a lemma function for writing a formula (_aka_, its ensures) along with its proof (_aka_, its requires).
Hence, the semantics of `f a…` where `f` is a lemma function would be similar to `(E a…) by (R a…)`, where `E` and `R` are the ensures & requires of `f`, although there is no need for side condition `(R a… -> E a…)` since the lemma has been already established.
The manual description would be (Cf. § 7.3.4):
« An occurrence of `f a...` where `f` is a lemma function generates no side condition, since the lemma has already been established. When `f a...` occurs as a premise, it is reduced to the conjunction of `E a...` for all ensures `E` of `f` (the conclusion of the lemma are exhibited). When `f a...` occurs as a goal, it is reduced to the conjunction of `R a...` (the premisses of the lemma are verified). »https://gitlab.inria.fr/why3/why3/-/issues/570Functions that could be used as let-functions2021-04-16T11:35:50+02:00Loïc CorrensonFunctions that could be used as let-functions:warning: **Disclaimer** this report is _wrong_ : a let-function without a contract actually exposes its definition to callers.
**Original Report** (wrong)
A frequent pattern we face when writing why3 code for extraction, is a pure lo...:warning: **Disclaimer** this report is _wrong_ : a let-function without a contract actually exposes its definition to callers.
**Original Report** (wrong)
A frequent pattern we face when writing why3 code for extraction, is a pure logical function that _only makes use of extractible expressions_. We then have to write the following code, with full duplication of core function definition:
```
function f x… : r = e
let rec function f x… : r ensures { result = e } = e
```
For large definition `e` with pattern matching or mutual-recursion, this is annoying !
This is the dual situation of a `let function f … = e`, where `f` can be used in both code & logic except that (among others):
1. the definition `e` of `let function f … = e` is _not_ available to provers
2. when writing `function f … = e` there is _no_ preconditions to `f`, hence `f x = e` always holds
3. pure logic function `f` must be structurally recursive so `let function f` needs no variant
**Proposal:**
Add a keyword to `function` definitions in order to have the associated `let rec function ...` for free.
Alternatively, detect that function definition only contains extractible terms and allow to use it like a `let function` in code.https://gitlab.inria.fr/why3/why3/-/issues/573Opening scopes at top level2021-04-30T10:06:00+02:00Xavier DenisOpening scopes at top levelWhen targetting WhyML from other languages, we would like to use `scopes` to help manage the namespaces for the produced code. In particular, it is desirable to produce a forest of nested scopes which contain modules or other declaration...When targetting WhyML from other languages, we would like to use `scopes` to help manage the namespaces for the produced code. In particular, it is desirable to produce a forest of nested scopes which contain modules or other declarations at the leaves. Currently, this is not possible as `module`s must be the top-level constructs of a WhyML file (implicit or explicit).
This restriction which prevents scopes from being at the top-level and thus containing modules seems unnecessary.
As a concrete example of what I would like to do:
```
scope MyScope
module Mod1
type t
end
scope OtherScope
(* optional, allow implicit modules inside scopes *)
let x () : bool = body
end
end
```
This code currently raises an error stating "Trying to open a module inside a module" due to the _implicit_ module opened by Why3.https://gitlab.inria.fr/why3/why3/-/issues/574Record transformation time2021-05-05T18:01:13+02:00Quentin GarcheryRecord transformation timeWhen developping in Why3, one might want to quickly know which part of the replay of a file takes time.
To this end, I think it would be useful if the transformations also recorded the time they spend. It could be stored in the `why3ses...When developping in Why3, one might want to quickly know which part of the replay of a file takes time.
To this end, I think it would be useful if the transformations also recorded the time they spend. It could be stored in the `why3session.xml` with another attribute to the transformation, which would give something like `<transf name="split_vc" time="0.01" >`. It probably should be disabled by default, although it would mean that we should be able to handle session files that differ in this way.
As for prover calls, it could also be shown in the IDE. To not clutter the IDE, it could only be shown if the time goes beyond X seconds.
Would it even make sense to do this ? Is the time spent by transformations too volatile ?https://gitlab.inria.fr/why3/why3/-/issues/579Extend sets with filter and cartesian product2021-06-27T18:44:04+02:00Quentin GarcheryExtend sets with filter and cartesian productLooking at the modules inside `set.mlw`, I'm wondering whether or not it is possible to extend some of them.
For the `filter` function defined in module `Fset`, can we also have it in `SetApp` ?
What about `Set` ? I understand that thes...Looking at the modules inside `set.mlw`, I'm wondering whether or not it is possible to extend some of them.
For the `filter` function defined in module `Fset`, can we also have it in `SetApp` ?
What about `Set` ? I understand that these are potentially infinite sets, is it an issue ?
Another operator on sets that I think would be nice to have is the cartesian product.
For the finite sets, this can be added by:
```
let rec ghost function cartesian_product (s1 : fset 'a) (s2 : fset 'b)
variant { cardinal s1 }
ensures { forall x y. mem (x, y) result <-> mem x s1 /\ mem y s2 }
=
if is_empty s1 then empty
else let x1 = pick s1 in
union (map (fun y -> (x1, y)) s2)
(cartesian_product (remove x1 s1) s2)
```
Could we also add a cartesian product for all kinds of sets ?Quentin GarcheryQuentin Garcheryhttps://gitlab.inria.fr/why3/why3/-/issues/581Mlw printer incorrect for Eoptexn2023-09-06T13:47:31+02:00MARCHE ClaudeMlw printer incorrect for EoptexnThe `Eoptexn` constructor of `Ptree.expr` is for special local exceptions involved in `break`, `continue` and `return`.
Since there is no concrete syntax for those, they should be printed as
declaration of a local exception with an exp...The `Eoptexn` constructor of `Ptree.expr` is for special local exceptions involved in `break`, `continue` and `return`.
Since there is no concrete syntax for those, they should be printed as
declaration of a local exception with an explicit `try ... with ... -> () end` around. The current printing is not parseable.1.8.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/585New function for conversion from real to float2023-11-13T14:56:16+01:00Guillaume CluzelNew function for conversion from real to floatIt would be useful to have in the `ieee_float.Float_Gen` theory a function `of_real mode real : t` that correctly rounds a real to a float `t` according to the rounding mode given.It would be useful to have in the `ieee_float.Float_Gen` theory a function `of_real mode real : t` that correctly rounds a real to a float `t` according to the rounding mode given.1.8.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/588Coercion with type variables2021-09-09T14:34:28+02:00François BobotCoercion with type variablesIt is currently not possible to add the following coercion
```
type t 'a = {
t_a : 'a;
}
meta coercion function t_a
```
Currently only from one type constructor to another is allowed. It seems that allows to compute the transitive c...It is currently not possible to add the following coercion
```
type t 'a = {
t_a : 'a;
}
meta coercion function t_a
```
Currently only from one type constructor to another is allowed. It seems that allows to compute the transitive closure when inserting new coercion and not during type checking. What would be the complexity to add that? Does it become similar to type-class inference?
EDIT: It could also help if one could define
```
function t_a_foo: (x:t foo) : foo = x.t_a
meta coercion function t_a_foo
function t_a_bar: (x:t bar) : bar = x.t_a
meta coercion function t_a_bar
```https://gitlab.inria.fr/why3/why3/-/issues/591Misleading "unbound function" error message2021-09-27T14:23:59+02:00Xavier DenisMisleading "unbound function" error messageI was recently caught by the error message:
`unbound function or predicate symbol 'UInt64.of_int'`
It took me a second to realize that the reason was being raised was that `of_int` is a `val` and not a `function` or `predicate`. I feel...I was recently caught by the error message:
`unbound function or predicate symbol 'UInt64.of_int'`
It took me a second to realize that the reason was being raised was that `of_int` is a `val` and not a `function` or `predicate`. I feel like the message could be improved when a program symbol with the same name appears, something like:
```
unbound function or predicate symbol 'UInt64.of_int', but a program symbol with the same name was found
```
Even this marginal improvement would make the error much more clear (imo).https://gitlab.inria.fr/why3/why3/-/issues/599Usage of `Map.const` triggers polymorphism2023-11-13T14:55:16+01:00MARCHE ClaudeUsage of `Map.const` triggers polymorphismThe SMT-LIB driver allows one to use higher-order and `map.Map`, both of them being mapped to SMT-LIB expressions without polymorphism.
It would be better to also map the `map.Const.const` to something not requiring the encoding of poly...The SMT-LIB driver allows one to use higher-order and `map.Map`, both of them being mapped to SMT-LIB expressions without polymorphism.
It would be better to also map the `map.Const.const` to something not requiring the encoding of polymorphism. Note that writing `(fun _ -> c)` instead of `const c` does *not* trigger encoding, so it must be doable.1.8.0MARCHE ClaudeMARCHE Claude