Dear Jean-Jacques,
very late and very partial answer:
On Wed, 10 Apr 2019 at 17:38, Jean-Jacques Levy <jean-jacques.l...@inria.fr>
wrote:
> 1- ide: stop pop-up menus. No reason for them, or make them optional. It
> makes a shaky behaviour. When thinking on a proof, it’s very bad to see
> sparkling menus. Furthermore, the macOS X-window handles them strangely
> when on border of a window.
>
Do you mean contextual menus that appear upon the right mouse click? Or do
you mean error/warning messages that appear in popup windows?
> 2- ide: stop fancy moves. Jumping to next unproved goal is very confusing,
> when you prove goals in non sequential order. Same to jump to a new Emacs
> window when choosing Coq as prover.
>
There is a recenly added option (in the master branch) that makes this
behaviour optional. In the IDE, menu "File", line "Preferences", tab
"General", option "jump to the next unproved goal".
> 3- ide: I loved the display of times on goals. This feature vanished at
> top level !!
>
It is still there, the third column in the session tree window. However, if
the second column "Theory/Goal" becomes too large, it pushes the third
column "Time" too far right, out of visibility.
> 7- I still have difficulties with the new treatment of ghost variables.
> This end with strange text as the sketchy one which follows:
> -------------------------------
> type vertex
> let ghost function (!) (s: S.t) = s.contents
> val (=) (x y: vertex) : bool ensures { result <-> x = y }
>
> clone import appmap.Appmap as M with type key = vertex
> clone import appset.Appset as S with type elt = vertex
>
> val constant vertices: S.t
>
> type env = {ghost black: set vertex; ghost gray: set vertex;
> stack: list vertex; sccs: set (set vertex); sn: int; num: M.t int}
>
> let rec dfs1 x e =
> requires {mem x !vertices}
> ...
> with dfs roots e =
> requires {subset !roots !vertices}
> returns {(_, e') -> subset !roots (union e'.black e'.gray)}
>
> if S.is_empty roots then (infty(), e) else
> let x = S.choose roots in
> let roots' = S.remove x roots in
> let (n1, e1) =
> if e.num[x] <> -1 then (e.num[x], e) else dfs1 x e in
> let (n2, e2) = dfs roots' e1 in (min n1 n2, e2)
> ------------------------------
> I thanks Andreij for giving me hints about equality but I dislike my (!),
> which could conflict later with references !! Maybe there is smarter way
> for distinguishing test-for-emptyness or others in program text ? Maybe
> another analysis of ghost variables is feasible ?
>
Sorry, I don't understand the example or the question. What do you mean by
"distinguishing test-for-emptyness"?
Best,
Andrei
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
