why3 issueshttps://gitlab.inria.fr/why3/why3/issues2018-04-18T06:28:49Zhttps://gitlab.inria.fr/why3/why3/issues/110Unused constant in stdlib/floating_point2018-04-18T06:28:49ZTomohito Yabuji170258@u-fukui.ac.jpUnused constant in stdlib/floating_pointIn `floating_point.SingleFull` module, constant `min_single` is defined but it's unused
(The same is true of `DoubleFull` module) .
I think that it should be the following:
```ocaml
module SingleFull
use export SingleFormat
constant min_single : real = 0x1p-149
clone export GenFloatSpecFull with
type t = single,
constant max = max_single,
constant max_representable_integer = max_int,
constant min = min_single, (* Added by me *)
lemma Bounded_real_no_overflow
end
```https://gitlab.inria.fr/why3/why3/issues/109split_*_wp redundant?2018-04-17T06:54:31ZAndrei Paskevichsplit_*_wp redundant?Now that we have a canonical split-simplify-introduce transformation, can we drop the split_*_wp transformations which are just aliases for split_*_right?https://gitlab.inria.fr/why3/why3/issues/108[@model_trace: <name>] labels redundant?2018-04-17T09:05:59ZAndrei Paskevich[@model_trace: <name>] labels redundant?Is there a reason to have these labels on symbols, in addition to [@model]? It seems that the name they carry always coincides with id_string of the symbol ident. If we need to change the name, e.g. for the SPARK-produced inputs, maybe we can only use [@model_trace: ...] in these cases, but not by default?https://gitlab.inria.fr/why3/why3/issues/105why3 is not compatible with OCaml 4.072018-04-13T15:51:56ZKatewhy3 is not compatible with OCaml 4.07Just reporting here a PR from opam-repository: https://github.com/ocaml/opam-repository/pull/11775
The issue comes from the fact that one of the modules in why3 has been named `Stdlib` which clashes with the new `Stdlib` module packing the standard library since 4.07.
If you want to test things using 4.07, `4.07.0+beta2` is available through opam.Next releasehttps://gitlab.inria.fr/why3/why3/issues/100why3 config for provers with compile-time support2018-03-23T15:12:12ZGuillaume Melquiondwhy3 config for provers with compile-time supportTo use a prover such as Coq, the detected version needs to match the one used to compile the `.vo` (assuming they were even compiled). If this is not the case, the prover is discarded. This is the expected behavior, but `why3 config`'s message is quite confusing for the user:
```
$ why3 config --detect
Found prover Alt-Ergo version 2.0.0, OK.
Found prover Coq version 8.7.2, but Why3 wasn't compiled with support for it
Found prover Coq version 8.7.2, but Why3 wasn't compiled with support for it
Found prover Coq version 8.7.2, but Why3 wasn't compiled with support for it
1 provers detected and 0 provers detected with unsupported version
```
First, the check should be made only once. Second, the final summary should reflect the result of the check.https://gitlab.inria.fr/why3/why3/issues/99Simplification of array initializer for generated Why3 code2018-03-14T11:54:31ZDAILLER SylvainSimplification of array initializer for generated Why3 codeFor array initializer of Why3 automatically generated code, some simplifications can sometimes be done. This ticket is about writing a transformations to simplify these array initialization.
This is relevant to new_ide only (corresponding draft branch is array_initializer).DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/issues/97range types should introduce an injectivity axiom2018-03-08T14:53:55ZMARCHE 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
(1) forall x y:t. t'int x = t'int y -> x = y
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
(2) forall x:t. t'ofInt (t'int x) = x
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/96Release of the new system2018-04-05T09:24:38ZGuillaume MelquiondRelease of the new systemThings to do before releasing `master`:
- [X] Enumerate the changes
- [X] Document the changes of syntax
- [ ] Remove the obsolete parts of documentation
- [X] Update the Coq realizations (especially `seq.Seq`) :arrow_right: `seq.Seq` is no longer realized
- [ ] Update the Isabelle realizations
- [ ] Kill the Coq tactic (still used by about 30 proofs from the gallery)
- [ ] Port the 'prover' example (blocked by issue #87)
- [X] Stabilize `Etry`
- [ ] Solve issue #9
- [ ] Solve issue #6
- [ ] not a regression, but I think it would be preferable to find a solution to the various problems related to the why3.conf file (see issues #55 and #69)
New systemhttps://gitlab.inria.fr/why3/why3/issues/88Improve handling of premises2018-02-20T12:42:37ZGuillaume MelquiondImprove handling of premises1. Add a meta on top of the toplevel goals (`split_theory`? IDE?) for display purpose.
2. Systematically add a transformation node that performs `split` and `intro` on a VC (can be disabled by a configuration option).
3. Modify `split_goal` so that it splits the last labeled disjunction in the context.
4. Remove the implicit `introduce_premises` used for display purpose.Next releasehttps://gitlab.inria.fr/why3/why3/issues/87Cannot use a type variable absent from the function arguments2018-03-07T08:49:21ZMARCHE ClaudeCannot use a type variable absent from the function argumentsThe following is an excerpt of a code that was working in the 'old' system.
It is not well-typed anymore: `Unbound type variable: 'c`
```
function compose (g:'b -> 'c) (f:'a -> 'b) : 'a -> 'c
axiom compose_def : forall g:'b -> 'c,f:'a -> 'b,x:'a.
compose g f x = g (f x)
function const (x: 'b) : 'a -> 'b
axiom const_def : forall x:'b,z:'a. const x z = x
predicate extensionalEqual (f g:'a -> 'b) =
forall x:'a. f x = g x
let lemma const_compose_right (f:'a -> 'b) (x:'a) : unit
ensures { compose f (const x) = (const (f x): 'c -> 'b) }
=
assert { extensionalEqual (const (f x) : 'c -> 'b) (compose f (const x)) }
```New systemAndrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/issues/63Commands request to be reorganized2017-12-22T12:39:21ZDAILLER SylvainCommands request to be reorganizedThis is a reminder issue for reorganization of code of ide and server commands which could be unified (but are currently in two separate worlds). Relevant variables are command_table (server_utils) and ide_command_table (why3ide).MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/issues/57Variants and soundness guarantees2017-12-15T08:03:43ZGuillaume MelquiondVariants and soundness guarantees```
predicate p (x y : unit) = true
let rec function foo (x : unit) : unit
variant { x with p } ensures { false } = foo x
goal g : false
```
As far as I understand it, the rule of thumb has always been that, in absence of `axiom` or `val`, the system should be sound. So either this rule should also exclude the use of custom `variant`, or Why3 should generate a proof obligation for the wellfoundedness of such relations.https://gitlab.inria.fr/why3/why3/issues/56No default order for range types2017-12-14T16:01:19ZGuillaume MelquiondNo default order for range types```
use import mach.int.Int63
let rec foo (x: int63): int63
variant { x }
= foo (x - 1)
```
```
File "foo.mlw", line 4, characters 2-13:
no default order for o
```
It would be good if range types were usable as variants without having to use `of_int`. In fact, the ordering relation is much simpler than in the `int` case, since we do not even have to choose an arbitrary lower bound.
Note also that the error message is rather poor since it mentions an automatically generated binder.New systemhttps://gitlab.inria.fr/why3/why3/issues/55additional manually-written configuration files2018-03-26T08:22:21ZCLOCHARD 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 data loss for unknown causes (this happened for some user strategies).https://gitlab.inria.fr/why3/why3/issues/52warning when cloning module containing only "val"s as abstract symbols2018-03-06T17:47:51ZCLOCHARD 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 symbol; it should be used instead`. However, `A0` does contain an abstract symbol.New systemhttps://gitlab.inria.fr/why3/why3/issues/51Instantiation of mutable type symbol when cloning2017-12-15T08:06:51ZCLOCHARD 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
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/42Invalid_argument('Expr.let_rec") in clone declarations2018-03-06T17:43:36ZRaphaël Rieu-HelftInvalid_argument('Expr.let_rec") in clone declarationsIn a large clone declaration containing `val x = y` where `x` is a `val constant` and y is a `let ghost constant` , I received the error `Invalid_argument("Expr.let_rec")`. My attempts to reproduce on smaller examples were not rejected at all.New systemAndrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/issues/39Tab completion in the command line2017-12-19T16:21:47ZRaphaël Rieu-HelftTab completion in the command lineWhen typing a command in the IDE command line, a list of possible completions appears below, but hitting Tab moves the focus away from the command line (completions can be selected with arrow keys and enter, but it is less intuitive and requires more keypresses).
It would be comfortable if Tab iterated through possible completions instead (or at least if it did not defocus the command line), especially when there is only one such completion.DAILLER SylvainDAILLER Sylvainhttps://gitlab.inria.fr/why3/why3/issues/35Coercions in branching expressions (if and match)2018-03-06T17:49:40ZMARCHE ClaudeCoercions in branching expressions (if and match)Coercions are not attempted when typing branches of if and match, e.g
```
use import int.Int
type byte = < range 0 255 >
meta coercion function byte'int
goal g : (if true then 2 else (3:byte)) = 4
```
should be well-typedNew systemPARREIRA PEREIRA Mário JoséPARREIRA PEREIRA Mário Joséhttps://gitlab.inria.fr/why3/why3/issues/30Refresh does not reload source view, causing loss of work2017-11-10T16:29:20ZRaphaë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 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 Claude