why3 issueshttps://gitlab.inria.fr/why3/why3/issues2019-05-22T17:19:30Zhttps://gitlab.inria.fr/why3/why3/issues/322Error ident renaming2019-05-22T17:19:30ZDAILLER SylvainError ident renamingWhen reloading after a typing error occurs, the error message increments the disambiguation of the ident.
For example, in the following code:
```
module Ex2
use array.Array
use int.Int
use option.Option
val my_set: array (option int) -> int -> option int -> unit
let rec my_fact (mem: array (option int)) (n: int): int
=
match mem[n] with
| None -> let r = n * my_fact mem (n- 1) in
my_set mem n (Some r);
r
| Some n -> n
end
end
```
The error is (after 8 reloads):
` line 154, characters 10-17: The type of this function contains an alias with external variable my_set8`
I think we managed to solve (or mitigate) this problem in the past for typing error of transformations: it is possible that it does not work anymore either.https://gitlab.inria.fr/why3/why3/issues/319Proved state of dependencies2019-05-21T11:56:44ZDAILLER 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.https://gitlab.inria.fr/why3/why3/issues/318List a module's depencies2019-05-21T11:56:45ZDAILLER SylvainList a module's depenciesGive a way to obtain a list of all the modules that a given file or module depends on (see why3-club)https://gitlab.inria.fr/why3/why3/issues/317Update library Queue2019-05-21T09:04:35ZMARCHE ClaudeUpdate library Queue1. queue.Queue: use sequences instead of lists for the specs
2. update the OCaml driver
3. update the 6 examples using queue.QueueJean-Christophe FilliâtreJean-Christophe Filliâtrehttps://gitlab.inria.fr/why3/why3/issues/316extraction of references2019-05-14T15:12:46ZMARCHE Claudeextraction of referencesAn update to a reference `x <- e` is extracted (ocaml64) in two
different ways: Without using `--modular`, the result is simply
`x.contents <- e`. But when using `--modular`, the field of the
reference is qualified as `x.Why3__Ref.contents <- e`.
Is the latter intended, and is there a library that defines the module
Why3__Ref? Or does somebody have a pointer where the builtin reference
is substituted in the Why3 codebase?
(I am using the last week’s master branch of Why3.)
```
$ cat test.mlw
module Test
let ref x = ()
let f (y:unit) = x <- y
end
$ why3 extract -D ocaml64 -L . test.Test
let x = ref ()
let f (y: unit) : unit = x.contents <- y
$ why3 extract --modular -D ocaml64 -L . test.Test -o .
$ cat test__Test.ml
let x = ref ()
let f (y: unit) : unit = x.Why3__Ref.contents <- y
```1.3.0Raphaël Rieu-HelftRaphaël Rieu-Helfthttps://gitlab.inria.fr/why3/why3/issues/315Too much ghostification?2019-05-21T09:15:38ZBECKER BenediktToo 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 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/314Spurious "unused at/old" warning in lemma function parameters2019-05-21T09:16:46ZRaphaël Rieu-HelftSpurious "unused at/old" warning in lemma function parametersPassing a lemma function parameter in the form (pure { x at L }) seems to trigger a spurious "unused at/old" warning.
In the example below, the `at` operator at line 9 works as expected, but the following warning is emitted:
```
File "atold.mlw", line 9, characters 17-18:
warning: this `at'/`old' operator is never used
```
```
use int.Int
let lemma l (x:int) requires { x <> 0 } ensures { x * x > 0 } = ()
let f () =
let ref x = any int ensures { result <> 0 } in
label L in
x <- -3;
l (pure { x at L });
assert { (x at L) * (x at L) > 0 };
```Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/issues/313Why3 API backward compatibility2019-05-10T14:00:48ZFranç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 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/312Missing hypothesis when splitting a formula with if-then-else and by2019-04-26T07:58:03ZGARCHERY QuentinMissing hypothesis when splitting a formula with if-then-else and byConsider the following code :
```
use int.Int
use seq.Seq
let function dirac (a b : int) =
if b = a then 1 else 0
let rec function count (x : int) (seq : seq int)
variant { Seq.length seq }
=
if Seq.length seq = 0
then 0
else dirac x seq[0] + count x seq[1..]
lemma count_case :
forall x h, t : seq int.
(if x = h
then (count x (cons h t) = count x t + 1
by dirac x h = 1)
else (count x (cons h t) = count x t
by dirac x h = 0))
by (cons h t)[1..] == t
```
When trying to prove the generated VCs (after split_vc) corresponding to the if-branches in the lemma,
the hypothesis `(cons h t)[1..] == t` is missing from the context. This makes the solvers fail to prove
the VCs directly (at least on my machine, giving them a reasonable delay).https://gitlab.inria.fr/why3/why3/issues/310improve the reactivity of the IDE2019-05-21T09:57:54ZLAWALL Juliaimprove the reactivity of the IDEOn a machine with many cores, the goal of producing a backlog of verification conditions seems to cause the IDE to freeze, which is a bit tiresome for the user. It would be good if the IDE could wake up every 0.1 seconds, even if the backlog is still under construction.https://gitlab.inria.fr/why3/why3/issues/309Exit status on un-proved goals2019-05-13T16:00:30ZLoïc CorrensonExit status on un-proved goalsWhen `why3 prove` leaves non proven goals, its exit status is `1`.
This is very confusing because this exit code is also used for syntax errors, incorrect command line arguments, etc.
Having an « unknown » goal is a normal outcome, and shall not be meld with syntactic errors!
Although, it can be interesting to known with an exit code whether all goals have been proven or not, and it shall be different from `1`. Better: what about some `-exit-unproved <n>` option on the command line, that would exit with status code `<n>` in this case?
Sincerely yours, L.https://gitlab.inria.fr/why3/why3/issues/308Forall construction in code for ghost binding2019-05-10T14:00:38ZFranç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) }
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/306Add program equality on Boolean type2019-04-20T06:55:02ZMARCHE ClaudeAdd program equality on Boolean typeTheory bool.Bool should provide (=) on Boolean type in programshttps://gitlab.inria.fr/why3/why3/issues/305ensure file synchronization2019-04-15T12:08:46ZLAWALL Juliaensure file synchronizationIt seems that when one modifies a file from within the IDE, it doesn't check whether the disk version is more recent. Changes on the disk are then lost if the file is modified within the IDE before doing a file refresh.1.3.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/issues/304improve ide window resizing2019-04-11T19:47:54ZLAWALL Juliaimprove ide window resizingWhen one resizes the IDE, the pane with the code in the upper right stays the same size, while the panes on the left and at the bottom get bigger. It is the code that one typically wants to see more of, so some effort is repetitively wasted to adjust the size of its pane. It would be fine if all the panes increased in size at the same rate, or if only the pane with the code got larger.https://gitlab.inria.fr/why3/why3/issues/300Add file from IDE is broken2019-04-08T08:19:20ZDAILLER SylvainAdd file from IDE is brokenHello,
When I have two files a.mlw and b.mlw in the same directory in the filesystem and the session for a.mlw in a/why3session.xml as usual. If I try to open why3ide on a.mlw and then add file b.mlw, I get an error in the "Messages" stating (cannot open a/../home/dailler/b.mlw). I think this is a problem with Sysutil.relativize_filename.DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/issues/298Migrate to Zarith2019-05-10T14:04:06ZFranç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 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.François BobotFrançois Bobothttps://gitlab.inria.fr/why3/why3/issues/297smoke detection in ide2019-04-04T13:45:59ZDAILLER 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 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/294Why3 IDE - close a file/tab from the IDE directly2019-04-10T12:51:11ZDEMANGE DelphineWhy3 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, 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/291search in task view2019-04-02T07:45:09ZLAWALL Juliasearch in task viewIt would be nice to be able to search in the task view.