Re: [Why3-club] dark theme
On Sun, 6 Dec 2020, Laurent Thery wrote: > > > > Is there any hope for getting a better solution? I upgraded my server, > > and seem to have lost whatever I had done. > > > > Note that you can put your change locally in > > ~/.local/share/gtksourceview-3.0/styles/ Thanks for the suggestion. By doing that, my changes seem to have a predictable impact, which wasn't the case when I was editing the global file. > A better solution would be great though ;-) Yes :) julia > > -- > Laurent > ___ > Why3-club mailing list > Why3-club@lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/why3-club > ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
[Why3-club] dark theme
Hello, Our discussion about colors in why3 over the summer ended with the following suggestion from Andrei: --- As a quick and ugly measure I would probably just hack /usr/share/gtksourceview-3.0/styles/classic.xml, which seems to be the default. --- Is there any hope for getting a better solution? I upgraded my server, and seem to have lost whatever I had done. If I use gedit on the server there are other styles available. Classic seems to be particularly unsuitable for a dark background. julia ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
[Why3-club] coloring for type invariants
Previously there was a discussion about what terms should be colored for the case of a VC that is associated with re-establishing a type invariant at the end of a function. It seems that if the function ends with a sequence of ifs, then for a tpye invariant the whole if is colored. On the other hand, for a postcondition, only the relevant branch of the if is colored. Could the same thing be done for type invariants? thanks, julia ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] dark theme
On Tue, 16 Jun 2020, Andrei Paskevich wrote: > Hi Julia, > > if I understand correctly the problem, you may want to look at the file > share/lang/why3.lang — it contains the description of WhyML grammar, and the >
Re: [Why3-club] dark theme
On Fri, 12 Jun 2020, Benoit Rognier wrote: > the doc is here > https://gitlab.inria.fr/why3/why3/-/blob/master/src/ide/gconfig.ml;) I haven't made much progress with this. Probably the problem is that the colors are not suitable at the theme level. For example, I have the same unreadable blue in emacs in some cases as in why3, but in emacs it is used for things that I don't need to read. Is there some way to figure out how words like ensures, requires, variant, invariant, and old are being reported to GTK? And likewise let, for, in, forall, and exists. If these words are considered to be in some categories, perhaps I could figure out how to globally change the colors associated with these categories. thanks, julia > > On Fri, Jun 12, 2020 at 6:15 PM Julia Lawall wrote: > > > On Fri, 12 Jun 2020, Benoit Rognier wrote: > > > Hi Julia, > > here is the ide section in my .why3.conf config file. > > > > [ide] > > allow_source_editing = true > > current_tab = 0 > > error_color = "red" > > error_color_bg = "yellow" > > error_line_color = "yellow" > > font_size = 14 > > goal_color = "#6698C8" > > iconset = "flaticons" > > max_boxes = 16 > > neg_premise_color = "dark magenta" > > premise_color = "#2F3E4D" > > print_attributes = false > > print_coercions = true > > print_locs = false > > print_time_limit = true > > saving_policy = 1 > > show_full_context = false > > task_height = 633 > > tree_width = 519 > > verbose = 0 > > window_height = 896 > > window_width = 1339 > > Thanks! I was just looking at what can be configured in the GUI, but I > see that there are more options. > > julia > > > > > hope this helps, > > regards > > Benoit > > > > On Fri, Jun 12, 2020 at 3:59 PM Julia Lawall > wrote: > > > > > > On Fri, 12 Jun 2020, Benoit Rognier wrote: > > > > > Hello > > > yes because it uses gtk(2?) technology. so you need to install > > a dark gtk > > > theme. > > > which os are you using? if not Linux, it can be a bit bumpy to > > configure. > > > I did so on macos last year and it took some external libs to > > install the > > > gtk theme switcher (via brew I guess) > > > > OK, I've now got the theme I want, but the red and blue keywords > > and the > > magenta numbers are fairly unreadable. Is it possible to change > > them? > > There is a green that is very readable. I would be fine with > > everything > > that is colored having that green color. > > > > thanks, > > julia > > > > > > > > >___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] dark theme
On Fri, 12 Jun 2020, Benoit Rognier wrote: > Hi Julia, > here is the ide section in my .why3.conf config file. > > [ide] > allow_source_editing = true > current_tab = 0 > error_color = "red" > error_color_bg = "yellow" > error_line_color = "yellow" > font_size = 14 > goal_color = "#6698C8" > iconset = "flaticons" > max_boxes = 16 > neg_premise_color = "dark magenta" > premise_color = "#2F3E4D" > print_attributes = false > print_coercions = true > print_locs = false > print_time_limit = true > saving_policy = 1 > show_full_context = false > task_height = 633 > tree_width = 519 > verbose = 0 > window_height = 896 > window_width = 1339 Thanks! I was just looking at what can be configured in the GUI, but I see that there are more options. julia > > hope this helps, > regards > Benoit > > On Fri, Jun 12, 2020 at 3:59 PM Julia Lawall wrote: > > > On Fri, 12 Jun 2020, Benoit Rognier wrote: > > > Hello > > yes because it uses gtk(2?) technology. so you need to install > a dark gtk > > theme. > > which os are you using? if not Linux, it can be a bit bumpy to > configure. > > I did so on macos last year and it took some external libs to > install the > > gtk theme switcher (via brew I guess) > > OK, I've now got the theme I want, but the red and blue keywords > and the > magenta numbers are fairly unreadable. Is it possible to change > them? > There is a green that is very readable. I would be fine with > everything > that is colored having that green color. > > thanks, > julia > > >___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] dark theme
On Fri, 12 Jun 2020, Benoit Rognier wrote: > Hello > yes because it uses gtk(2?) technology. so you need to install a dark gtk > theme. > which os are you using? if not Linux, it can be a bit bumpy to configure. > I did so on macos last year and it took some external libs to install the > gtk theme switcher (via brew I guess) OK, I've now got the theme I want, but the red and blue keywords and the magenta numbers are fairly unreadable. Is it possible to change them? There is a green that is very readable. I would be fine with everything that is colored having that green color. thanks, julia___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] dark theme
On Fri, 12 Jun 2020, Benoit Rognier wrote: > Hello > yes because it uses gtk(2?) technology. so you need to install a dark gtk > theme. > which os are you using? if not Linux, it can be a bit bumpy to configure. > I did so on macos last year and it took some external libs to install the > gtk theme switcher (via brew I guess) Hmm, I'm running why3 on a remote server. It has some form of Ubuntu. I'll see how I can change its theme. thanks, julia > > regards, > Benoit > > > > On Fri, Jun 12, 2020 at 1:43 PM Julia Lawall wrote: > Is there a dark theme for the IDE? > > thanks, > julia > ___ > Why3-club mailing list > Why3-club@lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/why3-club > > >___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
[Why3-club] dark theme
Is there a dark theme for the IDE? thanks, julia ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
[Why3-club] rematching proofs on reload
Recently I was told that there was a regression in the code for matching proofs to VCs on reloading a file. I did a pull and things seemed to work much better. But now I have the impression that things are not working so well again. For example, I have a goal that is just true, and it is associated to a proof that starts with inline. Has something changed again with respect to this issue, or is it just bad luck due to some other changes made on my side? thanks, julia ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
[Why3-club] anomaly
Hello,
I receiced the following message. It says to report it, so I am reporting
it. But I wouldn't know how to reproduce it.
exception 'anomaly:
Why3.Controller_itp.Make(S).TransAlreadyExists("split_vc", "")' was raised
in a LablGtk callback.
This should not happen. Please report.
julia
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] saving preferences
On Sat, 28 Mar 2020, Guillaume Melquiond wrote: > Le 28/03/2020 à 11:16, Julia Lawall a écrit : > > Does saving preferences impact the .why3.config file? I change the editor > > for cvc4 and click on save, but when I leave why3 and restart it, > > the value that I saved is gone and it is back to the default. > > Indeed, it seems broken. If you have not created your why3.conf file > using "why3 config --full-config", Why3 has nowhere to store the editor > preferences and they get lost, I guess. OK, I will make an issue. julia___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] too many asserts
On Thu, 26 Mar 2020, Guillaume Melquiond wrote: > Le 26/03/2020 à 13:08, Julia Lawall a écrit : > > > Are there any other possibilities, or other ways to solve the problem of > > finding useless asserts? > > I don't have any good solution. But here are a few ideas that might make > it easier for you. > > Rather than removing the assertions, make them trivial (e.g., "false -> > ..."). That way, you can reuse your old session without much trouble, as > the proof tree should then be mostly the same as before. (It mostly > depends on the transformations you have applied to the assertions > themselves. If none, it should be identical.) > > I also suggest that you delete why3shapes.gz before running why3replay > or why3ide on your new sources to force a trivial reassociation. > > A completely different approach would be to run a bisection in why3ide > on some goals you consider heavily dependent on assertions. Then take a > look at the hypotheses Why3 has flagged as useless. It should give some > clues on which assertions can be safely removed. Thanks! Bisect is indeed something that I have not yet tried. julia___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
[Why3-club] too many asserts
Hello, I suspect that my proofs have too many asserts. However, I'm not courageous enough to comment them out by hand one by one to find the ones that are not necessary. I tried making a tool to generate a copy of the file with each assert removed, and to copy the session and update the name of the file (using sed, since the session update command doesn't seem very practical). But I can't figure out a way to rerun the proofs and get a reliable answer that the proofs have succeeded. For example, replay will fail if the session contains a timeout and the actual proof succeeds. It seems that having a top-level goal disappear will cause a failure as well. Concretely, if I duplicate an assert, create a session, and then replay the same session with the duplicate removed I end up with a "replay failed, with some merge miss" error. I tried also putting various strings of -a on the command line with why3 prove, but that doesn't work well either, because I don't know a list of transformations that will work for everything, and that also seems to accept only one prover. There is also no parallelism, making it quite time consuming. Denis provided an ml file for using strategies with why3 prove, but it is for an old version of why3, and it's not clear how to update it in a correct way. Are there any other possibilities, or other ways to solve the problem of finding useless asserts? thanks, julia ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
[Why3-club] syntax errors in the ide
Hello, I am using 54b1573501a388c3d9d22c225b7c0857a139bc12. It seems that in the ide, the line numbers on error messages hve disappeared? I still see the line number with why3 prove. thanks, julia ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
[Why3-club] session update
It's not clear to me how why3 session update works. I have a file called system.mlw, and thus a session directory called system. I tried why3 session update -rename-file system xxx and I obtain no file containing xxx in its name and grep -r xxx turns up nothing. I did why3 session update -rename-file system xxx && echo ok and it printed ok, so I guess that it did not actually fail. I would actually like to copy an existing .mlw file and get a new copy of the session as well (ie system should still exist and xxx should be created referring to xxx.mlw). The documentation suggests that why3 session update -rename-file does a mv and not a cp, which is less convenient, but which I could live with. thanks, julia ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] New release Why3 1.3.1
On Wed, 25 Mar 2020, Claude Marche wrote: > > > Le 24/03/2020 à 21:47, Guillaume Melquiond a écrit : > > Le 24/03/2020 à 21:42, Julia Lawall a écrit : > > > >>>* fixed conflicting symbols for CVC4 1.7 > >> > >> I'm not sure what this change is, but after doing a pull of the latest > >> version, I still have to remove the --strings-exp option to get cvc4 to > >> work. > > > > Yes, this is a different issue. The one that was fixed is that CVC4 1.7 > > has a lot of new predefined symbols, so Why3 has to rename user > > identifiers so that they do not confuse CVC4. > > > > The issue with --strings-exp still needs to be investigated. > > The problem was not that CVC4 1.7 has "a lot of new predefined symbols", > it was that we switched from > > (set-logic "AUFDTNIRA") > > to > > (set-logic "ALL_SUPPORTED") > > which by side effect seems to "activate" a lot more predefined symbols > in CVC4. > > So far I assumed that the problem with -strings-exp was the same. If it > isn't then I need a reproducer. Please consider creating a ticket. OK, I'll try to make something small. For me, everything I do with cvc4 crashes almost immediately. julia___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
[Why3-club] why3 prove
I see the option --apply-transform to apply a specific transform, but is it possible to apply a strategy, as defined in the .why3.conf file? thanks, julia ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] let lemma
On Sun, 22 Mar 2020, Andrei Paskevich wrote: > Hi Julia, > > when you call a let-lemma in your code, it behaves in exactly the same way > as a normal function call: you must supply the parameters and prove the > instantiated preconditions. These preconditions do not stay in the context > for the subsequent proof obligations and, normally, there should be no need > to purify the parameters to call the let-lemma. > > Could you please share an example that shows your issue? I don't think I could make it into anything that is digestible. My assumption was that since there is the row of [precondition]s in the list of proof obligations, that that information was remaining available for subsequent proofs. But if it is notm then no problem. The problem is probably just that since things are different somehow than before when I added the uses of the let lemmas, the subsequent proofs come out in a different way. thanks, julia ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
[Why3-club] let lemma
Hello,
I have the impression that when using a let lemma as code, one gets asked
to prove all the preconditions, that then clutter up the space of known
things, making other things harder to prove. In my case, I have to add a
lot of let x = pure { y } declarations to be able to use the let lemma. I
don't know if this is an issue.
Is there a way to write or use a let lemma such that its preconditions
will somehow be local to the use of the lemma and disappear when proving
other things?
Or have I completely misunderstood the issue.
thanks,
julia
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] New release Why3 1.3.0
On Wed, 18 Mar 2020, Guillaume Melquiond wrote: > Le 18/03/2020 à 22:14, Julia Lawall a écrit : > > >> As far as I know, the strategies have not changed since they were > >> renamed, so I have no idea why you are experiencing a change of behavior > >> in "Auto level 3". > > > > Where are the strategies defined? I found strategies.conf, but that seems > > to have only level 0 and level 1. Previously, the auto strategies were > > in the why.conf file, but that doesn't seem to be the case any more. > > I believe that strategies.conf is an obsolete file that should have been > removed years ago. > > Strategies are predefined in src/driver/autodetection.ml. In previous > releases of Why3, "why3 config" called this code and then copied the > generated definition into why3.conf. Starting with Why3 1.3, most of > why3.conf is implicitly generated each time Why3 is executed. In other > words, the code of src/driver/autodetection.ml is now invoked at each > startup rather than once and for all. > > This applies only to predefined strategies. If you have custom > strategies, they still appear in why3.conf. > > You can use "why3 config --full-config" to force Why3 to generate a > fully static why3.conf. In particular, predefined strategies will be > written in why3.conf, as in previous releases of Why3. I have the impression that the problem is that split_vc always succeeds, whether it does anything or not. So Auto level 3 would always be an infinite loop. I just see a cascade of split_vc, and when I look at the alt-ergo code from one to the next, it is identical. julia___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] New release Why3 1.3.0
On Wed, 18 Mar 2020, Guillaume Melquiond wrote: > Le 18/03/2020 à 22:14, Julia Lawall a écrit : > > >> As far as I know, the strategies have not changed since they were > >> renamed, so I have no idea why you are experiencing a change of behavior > >> in "Auto level 3". > > > > Where are the strategies defined? I found strategies.conf, but that seems > > to have only level 0 and level 1. Previously, the auto strategies were > > in the why.conf file, but that doesn't seem to be the case any more. > > I believe that strategies.conf is an obsolete file that should have been > removed years ago. > > Strategies are predefined in src/driver/autodetection.ml. In previous > releases of Why3, "why3 config" called this code and then copied the > generated definition into why3.conf. Starting with Why3 1.3, most of > why3.conf is implicitly generated each time Why3 is executed. In other > words, the code of src/driver/autodetection.ml is now invoked at each > startup rather than once and for all. > > This applies only to predefined strategies. If you have custom > strategies, they still appear in why3.conf. > > You can use "why3 config --full-config" to force Why3 to generate a > fully static why3.conf. In particular, predefined strategies will be > written in why3.conf, as in previous releases of Why3. OK, thanks. julia___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] New release Why3 1.3.0
> * default proof strategies "Auto level 1" and "Auto level 2" > have been respectively renamed "Auto level 2" and "Auto level 3"; > "Auto level 1" now behaves similarly to "Auto level 0" but with a longer > time limit; more details in the manual, Section 10.6 "Proof Strategies" > :x: This means that there is no more of the old Auto Level 3? julia ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] cvc4
There remains the problem that Auto Level 3 goes into an infinite loop, at least when the goal is a predicate. julia ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] cvc4
On Wed, 18 Mar 2020, Claude Marche wrote: > > > Le 18/03/2020 à 14:39, Julia Lawall a écrit : > > The problem seems ot be the --strings-exp option. If I remove that, cvc4 > > seems to work fine. > > Thanks for the feedback. We will do our best to fix this problem in Why3 > development (and probably a soon upcoming 1.3.1 release...) > > Hopefully you can continue your work with Why3 now? Yes, it seems ok. Thanks. julia___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] cvc4
The problem seems ot be the --strings-exp option. If I remove that, cvc4 seems to work fine. julia diff --git a/share/provers-detection-data.conf b/share/provers-detection-data.conf index a85e609e4..eac39d396 100644 --- a/share/provers-detection-data.conf +++ b/share/provers-detection-data.conf @@ -75,8 +75,8 @@ version_ok = "1.7" driver = "cvc4_17" # --random-seed=42 is not needed as soon as --random-freq=0.0 by default # to try: --inst-when=full-last-call -command = "%e --stats --tlimit=%t000 --lang=smt2 --strings-exp %f" -command_steps = "%e --stats --rlimit=%S --lang=smt2 --strings-exp %f" +command = "%e --stats --tlimit=%t000 --lang=smt2 %f" +command_steps = "%e --stats --rlimit=%S --lang=smt2 %f" use_at_auto_level = 1 # CVC4 version 1.6 ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] cvc4
On Wed, 18 Mar 2020, Claude Marche wrote: > > Hello, > > Le 18/03/2020 à 12:31, Julia Lawall a écrit : > >>> But the unconditional (get-info :reason-unknown) doesn't look ideal. > >> > >> Agreed. Unfortunately, to make it conditional, Why3 would have to > >> interact with the SMT solvers, that is, write on stdin, read on stdout, > >> write on stdin, read on stdout, and so on. That is completely different > >> from Why3's current architecture, which gives an input file to the SMT > >> solver, wait for termination, then read stdout. > > > > OK, but then could it be removed? It wasn't there in some previous > > version (concretely, Why3 platform, version 1.2.0+git) > > I agree this is not ideal, but it is the best we were able to do. And > this is harmless. I mean, the bugs you face are not related to that. OK, when I applied all of the suggestions, the problem went away. So I am trying to figure out what exactly causes the issue. julia___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] cvc4
On Wed, 18 Mar 2020, Guillaume Melquiond wrote: > Le 18/03/2020 à 12:28, Julia Lawall a écrit : > > > What should I do to get why3 to use the right file? I tried rerunning > > make, but it didn't do anything. Do I need to change my configuration > > file somehow? > > The file that is located the "drivers" directory contained in a > directory that is either given by the WHY3DATA environment variable or > by the "datadir" symbol in file src/util/config.ml. > > I guess you could also use strace: > > strace -e file why3 ide foo.mlw |& grep cvc4_17 OK, it seems that it is necessary to do a make install after making such a change. julia___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] cvc4
On Wed, 18 Mar 2020, Guillaume Melquiond wrote: > Le 18/03/2020 à 10:48, Julia Lawall a écrit : > > When I run cvc4 on the command line, it ends with > > > > (error "Can't get-info :reason-unknown when the last result wasn't > > unknown!") > > > > If I remove (get-info :reason-unknown) it ends with unsat (which is not > > what I hoped for, but perhaps I am somehow not running it properly). > > If your goal in Why3 is valid, then its negation is expected to be unsat > on the SMT side. So, unless your goal was meant to be unprovable, this > is fine. > > > But the unconditional (get-info :reason-unknown) doesn't look ideal. > > Agreed. Unfortunately, to make it conditional, Why3 would have to > interact with the SMT solvers, that is, write on stdin, read on stdout, > write on stdin, read on stdout, and so on. That is completely different > from Why3's current architecture, which gives an input file to the SMT > solver, wait for termination, then read stdout. OK, but then could it be removed? It wasn't there in some previous version (concretely, Why3 platform, version 1.2.0+git) On the other hand, I don't know if it is really there when I am running within the IDE. julia___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] cvc4
On Wed, 18 Mar 2020, Guillaume Melquiond wrote: > Le 18/03/2020 à 09:21, Julia Lawall a écrit : > > > I have the impression that it is using drivers/cvc4-realize.drv. I made > > the change you suggested, but if I edit the cvc4 proof, it shows > > ALL_SUPPORTED. Or is drivers/cvc4-realize.drv what is used when editing? > > No, cvc4-realize.drv is never used, unless you explicitly request it > through --extra-config or similar. > > I suppose Why3 is not using the cvc4_17.drv file you modified but one > installed at an earlier time. What should I do to get why3 to use the right file? I tried rerunning make, but it didn't do anything. Do I need to change my configuration file somehow? julia___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] cvc4
On Wed, 18 Mar 2020, Guillaume Melquiond wrote: > Le 18/03/2020 à 08:45, Julia Lawall a écrit : > > Could the generated code be bigger than before? I tried cvc4 on a proof > > that is simple and has few dependencies and it was fine. > > Among the things that changed recently regarding CVC4, here are a few > things you could try: > > - In share/prover-detection-data.conf, in the block for CVC4 1.7 (plain > "cvc4", not "cvc4-ce"), remove the "--strings-exp" command-line option. > > - Similarly, remove the "--stats" option. > > - In drivers/cvc4_17.drv, replace "ALL_SUPPORTED" by "AUFBVFPDTSNIRA". I compared with the file generated by an older installation of why3 where I have CVC4 1.6 installed. The only difference I see besides what you suggested is the code generated by the current version ends with (get-info :reason-unknown). julia___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] New release Why3 1.3.0
J'ai aussi l'impression d'avoir une boucle infinie sur un auto level 3. Il fait des split_vc infiniement, mais a chaque etape le but est un predicate, et il n'y a rien a splitter. julia ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] New release Why3 1.3.0
cvc4 1.7 a l'air de me donner systematiquement un seg fault: CVC4 suffered a segfault. Offending address is 0x7fff8 expr::ExprManager::AND, 736 expr::ExprManager::APPLY_UF, 4555 expr::ExprManager::BOUND_VARIABLE:Boolean type, 11 expr::ExprManager::BOUND_VARIABLE:integer type, 663 expr::ExprManager::BOUND_VAR_LIST, 956 expr::ExprManager::EQUAL, 930 expr::ExprManager::EXISTS, 39 expr::ExprManager::FORALL, 917 expr::ExprManager::IMPLIES, 933 expr::ExprManager::INST_PATTERN, 85 expr::ExprManager::INST_PATTERN_LIST, 75 expr::ExprManager::ITE, 12 expr::ExprManager::LEQ, 320 expr::ExprManager::LT, 239 ... julia ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
[Why3-club] reloading proofs
Hello, I wonder if there is some easy room for improvement in the process of reloading a session when things have changed. For example, I have at least the illusion that when I remove a lemma at the end of a large module and then reload it, the proofs don't all end up in the right places. For example, I may get a "index in array bounds" associated with an inline_goal or a formula where the main operator is /\ that is put with an inline_goal, when it is actually only provable with a split. Are proofs at least associated with the kind of goal they are being used for? It's unlikely that a formula would switch from being eg a precondition to a postcondition. thanks, julia ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] error message color
On Mon, 14 Oct 2019, Sylvain Dailler wrote: > Le 14/10/2019 à 14:31, Guillaume Melquiond a écrit : > > Le 14/10/2019 à 07:59, Julia Lawall a écrit : > >> My configuration file contains: > >> > >> error_color = "red" > >> error_color_bg = "yellow" > >> error_line_color = "yellow" > >> > >> This would suggest that bad code would be written in red letters on a > >> yellow background, but actually I get black letters on a red background, > >> which is quite unreadable. Is it possible to change both the letter color > >> and the background color or only the background color? > >> > >> I am using why3 from git, commit e4e2a2a416ff2e98f6247cdf23f068e5369e7f0e > >> (September 2). > > I cannot reproduce your issue, but the code looks a bit dubious. Could > > you try replacing > > > > `BACKGROUND gconfig.error_color > > > > with > > > > `FOREGROUND gconfig.error_color > > > > in src/ide/why3ide.ml at line 270 and see if it makes a difference? > > > Indeed, the error_color field is used both for the foreground color in > the error message (bottom right corner) and as background color in the > source. We may want to separate these two parameters. I think you cannot > yet change the foreground color of the source code on error: I'll open > an issue. Thanks. I think that it would be hard to find a color that works well for both. julia > > Best regards, > > Sylvain Dailler > > ___ > Why3-club mailing list > Why3-club@lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/why3-club >___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] lemma usage
On Thu, 3 Oct 2019, Raphael Rieu-Helft wrote:
> Suppose you want to call the lemma on (old x). When the value of x that
> you are interested in is current (e.g. at the start of the function),
> you can take a snapshot of it using "pure" :
>
> "let ghost ox = pure { x } in ..." You may then call your let lemma on
> ox at a later point.
OK, thanks.
julia
>
> Raphaël
>
> On 03/10/2019 11:30, Julia Lawall wrote:
> > It seems that I cannot use (old ...) in calling my let lemma? Is there a
> > way around this?
> >
> > julia
> > ___
> > Why3-club mailing list
> > Why3-club@lists.gforge.inria.fr
> > https://lists.gforge.inria.fr/mailman/listinfo/why3-club
> ___
> Why3-club mailing list
> Why3-club@lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] lemma usage
It seems that I cannot use (old ...) in calling my let lemma? Is there a way around this? julia ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] lemma usage
On Thu, 3 Oct 2019, Claude Marche wrote:
>
>
> Le 03/10/2019 à 09:06, Julia Lawall a écrit :
> > lemma valid_cont_remove_from_current : forall oldcrs crs:cores, core
> > co:int, t:thread, c:cont.
> > valid_core oldcrs core -> valid_cont oldcrs core c -> core <> co ->
> > cont_thread c <> Some t ->
> > amem t oldcrs.current co ->
> > good_move_from_astate oldcrs.current crs.current co t ->
> > others_in_cores_unchanged_current oldcrs crs ->
> > valid_cont crs core c
> >
> > I didn't pick the ideal ordering of the parameters, but core and c are not
> > known at the place where I use the lemma.
>
> you may consider changing the parameter order if it helps the proof...
>
> I would write
>
> let ghost valid_cont_remove_from_current (oldcrs crs:cores)
> (co:int) (t:thread) : unit
> requires { amem t oldcrs.current co }
> requires { good_move_from_astate oldcrs.current crs.current co t }
> requires { others_in_cores_unchanged_current oldcrs crs }
> ensures { forall core, c:cont.
> valid_core oldcrs core ->
> valid_cont oldcrs core c ->
> core <> co ->
> cont_thread c <> Some t ->
> valid_cont crs core c }
>
> (sorry if I made a copy/paste mistake, but I hope you got the idea)
> and then call
>
> valid_cont_remove_from_current oldcrs crs co t;
>
> at the place of the code I know the lemma is needed, with the appropriate
> values for those arguments.
I'll try that, thanks!
julia___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] lemma usage
On Thu, 3 Oct 2019, Claude Marche wrote: > > > Le 03/10/2019 à 09:02, Julia Lawall a écrit : > > > > > > On Thu, 3 Oct 2019, Claude Marche wrote: > > > > > > > > Notice that if your initial goal is to apply the lemma at the right > > > place with the right instantiation, then a "let lemma" is not necessary, > > > a "let ghost" is enough. > > > > > > An important difference is that with a "let ghost", your lemma will > > > *not* be present in the context for the rest of the code, which can make > > > easier the proof with SMT solver when they don't need that lemma. > > > > > > So use a "let ghost" instead of a "let lemma" if you want to control the > > > location where the lemma should be used > > > > I don't follow this at all. My lemma is in a different file than the > > place where I want to use it. So I guess that the name space is polluted > > anyway? > > You are talking about the name space of the input source, and yes, the name > `l` will be present in that name space in any case. > > I'm talking about the proof context, that is the set of premises of the proof > tasks: a `lemma l` or a `let lemma l` would be in the context of all VCs, > whereas with a `let ghost` it will not. Better to have a smaller proof context > for SMT solvers if they don't need that lemma. Sorry, but I still don't understand. Where do I put this let ghost? julia___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] lemma usage
On Thu, 3 Oct 2019, Claude Marche wrote: > > > Le 03/10/2019 à 08:57, Julia Lawall a écrit : > > >> If the quantified variables are always the same, you can move them from > >> the arguments to the postcondition of the lemma function. > > > > So take the foralls and all of the requires and put them into a big > > implication in the ensures? > > A priori I would say it is a bad idea. Can you give your use case in > more details ? lemma valid_cont_remove_from_current : forall oldcrs crs:cores, core co:int, t:thread, c:cont. valid_core oldcrs core -> valid_cont oldcrs core c -> core <> co -> cont_thread c <> Some t -> amem t oldcrs.current co -> good_move_from_astate oldcrs.current crs.current co t -> others_in_cores_unchanged_current oldcrs crs -> valid_cont crs core c I didn't pick the ideal ordering of the parameters, but core and c are not known at the place where I use the lemma. The lemma is needed to match up with a precondition of another function where the precondition is a forall over these variables. julia___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] lemma usage
On Thu, 3 Oct 2019, Claude Marche wrote:
>
> Notice that if your initial goal is to apply the lemma at the right
> place with the right instantiation, then a "let lemma" is not necessary,
> a "let ghost" is enough.
>
> An important difference is that with a "let ghost", your lemma will
> *not* be present in the context for the rest of the code, which can make
> easier the proof with SMT solver when they don't need that lemma.
>
> So use a "let ghost" instead of a "let lemma" if you want to control the
> location where the lemma should be used
I don't follow this at all. My lemma is in a different file than the
place where I want to use it. So I guess that the name space is polluted
anyway?
julia
>
> - Claude
>
> Le 02/10/2019 à 10:00, Guillaume Melquiond a écrit :
> > Le 01/10/2019 à 17:52, Julia Lawall a écrit :
> >> Hello,
> >>
> >> I have to resort to some explicit applys. When I then change my .mlw
> >> file, it seems that the why3 proof realignment rarely puts the existing
> >> applys in the right place. At some times I have thought that they are
> >> backwards, but I haven't studied that in detail.
> >>
> >> Is there any way to put the application of a lemma in a .mlw file, so that
> >> the right lemma will be applied in the right place more reliably?
> >
> > If your lemma happens to be a "lemma function", then you can call it
> > from your code as any kind of ghost function. There are multiple
> > examples in the gallery; here is a small dumb one:
> >
> > use real.Real
> >
> > let lemma foo (x:real)
> >requires { x <> 0. }
> >ensures { x * (1./x) = 1. }
> > = ()
> >
> > let bar (y:real)
> >ensures { y <> 0. -> result * y = 1. }
> > = if y <> 0. then foo y;
> >1. / y
> >
> > Best regards,
> >
> > Guillaume
> > ___
> > Why3-club mailing list
> > Why3-club@lists.gforge.inria.fr
> > https://lists.gforge.inria.fr/mailman/listinfo/why3-club
> >
> ___
> Why3-club mailing list
> Why3-club@lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] lemma usage
Hmm, in looking further, I have the impression that I can't make a let lemma because the lemma needs to be universally quantified over some variables. julia ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] lemma usage
On Wed, 2 Oct 2019, Guillaume Melquiond wrote:
> Le 01/10/2019 à 17:52, Julia Lawall a écrit :
> > Hello,
> >
> > I have to resort to some explicit applys. When I then change my .mlw
> > file, it seems that the why3 proof realignment rarely puts the existing
> > applys in the right place. At some times I have thought that they are
> > backwards, but I haven't studied that in detail.
> >
> > Is there any way to put the application of a lemma in a .mlw file, so that
> > the right lemma will be applied in the right place more reliably?
>
> If your lemma happens to be a "lemma function", then you can call it
> from your code as any kind of ghost function. There are multiple
> examples in the gallery; here is a small dumb one:
Thanks.
Is there any advantage to not making a lemma a lemma function?
julia
>
> use real.Real
>
> let lemma foo (x:real)
> requires { x <> 0. }
> ensures { x * (1./x) = 1. }
> = ()
>
> let bar (y:real)
> ensures { y <> 0. -> result * y = 1. }
> = if y <> 0. then foo y;
> 1. / y
>
> Best regards,
>
> Guillaume
> ___
> Why3-club mailing list
> Why3-club@lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
[Why3-club] lemma usage
Hello, I have to resort to some explicit applys. When I then change my .mlw file, it seems that the why3 proof realignment rarely puts the existing applys in the right place. At some times I have thought that they are backwards, but I have't studied that in detail. Is there any way to put the application of a lemma in a .mlw file, so that the right lemma will be applied in the right place more reliably? thanks, julia ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] build from sources
On Tue, 3 Sep 2019, Claude Marche wrote: > > Hello, > > For the record, if others have the same issue: > > rm lib/why3/why3extract.cmi > > should solve the problem Works. Thanks! julia > > - Claude > > Le 03/09/2019 à 08:07, Guillaume Melquiond a écrit : > > Le 03/09/2019 à 07:54, Julia Lawall a écrit : > >> With commit e4e2a2a416ff2e98f6247cdf23f068e5369e7f0e, I gate the > >> following: > >> > >> File "src/tools/why3extract.ml", line 1: > >> Error: The implementation src/tools/why3extract.ml > >> does not match the interface lib/why3/why3extract.cmi: > >> The module `Why3__Matrix' is required but not provided > >> The module `Why3__Array' is required but not provided > >> The module `Why3__IntAux' is required but not provided > >> The module `Why3__BigInt' is required but not provided > >> The module `Why3__BigInt_compat' is required but not provided > >> Makefile:2177: recipe for target 'src/tools/why3extract.cmx' failed > >> > >> I've tried rerunning autoconf, automake, configure, and make clean, all > >> with no impact. > > > > It seems like you have some leftover .cmi files from an older commit. > > Unfortunately, "make clean" only removes .cmi files it knows about, > > i.e., the ones built from your current commit. You need a much stronger > > cleanup, e.g., "git clean -fxd", to fix your issue. Make sure to run > > "git clean -nfd" first to check whether any file important to you will > > be removed. > > > > Best regards, > > > > Guillaume > > ___ > > Why3-club mailing list > > Why3-club@lists.gforge.inria.fr > > https://lists.gforge.inria.fr/mailman/listinfo/why3-club > ___ > Why3-club mailing list > Why3-club@lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/why3-club >___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] build from sources
> On 3 Sep 2019, at 08:07, Guillaume Melquiond > wrote: > >> Le 03/09/2019 à 07:54, Julia Lawall a écrit : >> With commit e4e2a2a416ff2e98f6247cdf23f068e5369e7f0e, I gate the >> following: >> File "src/tools/why3extract.ml", line 1: >> Error: The implementation src/tools/why3extract.ml >>does not match the interface lib/why3/why3extract.cmi: >>The module `Why3__Matrix' is required but not provided >>The module `Why3__Array' is required but not provided >>The module `Why3__IntAux' is required but not provided >>The module `Why3__BigInt' is required but not provided >>The module `Why3__BigInt_compat' is required but not provided >> Makefile:2177: recipe for target 'src/tools/why3extract.cmx' failed >> I've tried rerunning autoconf, automake, configure, and make clean, all >> with no impact. > > It seems like you have some leftover .cmi files from an older commit. > Unfortunately, "make clean" only removes .cmi files it knows about, i.e., the > ones built from your current commit. You need a much stronger cleanup, e.g., > "git clean -fxd", to fix your issue. Make sure to run "git clean -nfd" first > to check whether any file important to you will be removed. Thanks! Julia > Best regards, > > Guillaume > ___ > Why3-club mailing list > Why3-club@lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/why3-club ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
[Why3-club] build from sources
With commit e4e2a2a416ff2e98f6247cdf23f068e5369e7f0e, I gate the following: File "src/tools/why3extract.ml", line 1: Error: The implementation src/tools/why3extract.ml does not match the interface lib/why3/why3extract.cmi: The module `Why3__Matrix' is required but not provided The module `Why3__Array' is required but not provided The module `Why3__IntAux' is required but not provided The module `Why3__BigInt' is required but not provided The module `Why3__BigInt_compat' is required but not provided Makefile:2177: recipe for target 'src/tools/why3extract.cmx' failed I've tried rerunning autoconf, automake, configure, and make clean, all with no impact. thanks, julia ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
[Why3-club] [@inline:trivial]
[@inline:trivial] on the definition of a predicate is useful because it allows proofs to directly use the definition of the predicate. But it seems to also make it hard to prove that a use of a predicate follows from itself. Eg if pred has this annotation, then having pred a b c d as a hypothesis does not make it easy to prove pred a b c d as a goal. Would it make sense to have [@inline:trivial] keep two copies of pred a b c d as hypotheses, one inlined and one not? thanks, julia ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] applying a lemma
On Sat, 13 Jul 2019, Jean-Christophe Filliatre wrote: > Hi Julia, > > Indeed it is. The syntax is > > apply Lemma with term1,term2,...,termk > > For instance, in the following situation > > lemma L: forall x y z. p x -> p z -> p y > goal G: p 42 > > you can do > > apply L with 21,21 > > Then the value for "y" (42) is inferred when matching the goal and the > lemma's conclusion, and you are thus providing values for "x" and "z", > in that order. Actually, I get: apply valid_cont_remove_from_current with (old p.cores),p.cores,core,i,dst,t,c Transformation failed. On argument: (old p.cores),p.cores,core,i,dst,t,c Parsing error: `at' and `old' can only be used in program annotations julia > > Hope this helps, > -- > Jean-Christophe > > On 7/13/19 9:12 AM, Julia Lawall wrote: > > I guess the apply transformation is a way to force a lemma to be used at a > > particular place in a proof? How does one specify the list of arguments, > > ie a value of list term type? > > > > thanks, > > julia > > ___ > > Why3-club mailing list > > Why3-club@lists.gforge.inria.fr > > https://lists.gforge.inria.fr/mailman/listinfo/why3-club > > > ___ > Why3-club mailing list > Why3-club@lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/why3-club > ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] applying a lemma
On Sat, 13 Jul 2019, Jean-Christophe Filliatre wrote: > Hi Julia, > > Indeed it is. The syntax is > > apply Lemma with term1,term2,...,termk > > For instance, in the following situation > > lemma L: forall x y z. p x -> p z -> p y > goal G: p 42 > > you can do > > apply L with 21,21 > > Then the value for "y" (42) is inferred when matching the goal and the > lemma's conclusion, and you are thus providing values for "x" and "z", > in that order. > > Hope this helps, Thanks! julia > -- > Jean-Christophe > > On 7/13/19 9:12 AM, Julia Lawall wrote: > > I guess the apply transformation is a way to force a lemma to be used at a > > particular place in a proof? How does one specify the list of arguments, > > ie a value of list term type? > > > > thanks, > > julia > > ___ > > Why3-club mailing list > > Why3-club@lists.gforge.inria.fr > > https://lists.gforge.inria.fr/mailman/listinfo/why3-club > > > ___ > Why3-club mailing list > Why3-club@lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/why3-club > ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
[Why3-club] applying a lemma
I guess the apply transformation is a way to force a lemma to be used at a particular place in a proof? How does one specify the list of arguments, ie a value of list term type? thanks, julia ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
[Why3-club] crash
I obtained the following with the master from the why3 gitlab: warning: [Session_itp.merge_trans] FATAL unexpected exception: anomaly: Not_found This came after commenting some code in the IDE, and then I think save and refresh. After restarting why3, all is fine, so I don't especially care about this problem, but I thought it could be worth reporting. julia ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
[Why3-club] regression testing
Is there an easy way to take a single mlw file and be sure that all of the modules that it relies on have been fully proved? Is there an easy way to obtain a list of all of the modules that a given file or module relies on? thanks, julia ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] concurrency
Indeed, regardless of the multiplier, I never see more than around 20 alt-ergo processes running, even though I asked for 40. So I guess that most of the time is used on generating the verification conditions. julia ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] concurrency
On Sat, 20 Apr 2019, Andrei Paskevich wrote: > Sorry, I meant each 0.1 sec, of course. > > The 3x factor is, if I remember correctly, the upper bound on the backlog > size: Why3 stops preparing tasks once it has 3x#cores tasks ready to go. I > don't think lowering it is a good solution long-term: what we probably > should do is to schedule interruptions at regular intervals then go back to > filling the backlog until the upper bound is reached. Agreed. Shall I make an issue? > > The actual value of 3 is set in src/ide/why3ide.ml:143 for the GUI, and in > src/tools/unix_scheduler.ml:17 for why3replay, IIUC. OK, thanks. julia ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] concurrency
On Sat, 20 Apr 2019, Andrei Paskevich wrote: > Indeed, with as many as 47 cores ready to run external provers, Why3 is sure > busy to fill the working queue with prepared proof tasks. I am not sure what > is the right approach here: set some real-time bounds and go back to UI, > say, each tenth second, even if the backlog is still being filled? Even 10 seconds is a long time. How about every 1 second? The waiting leads to a lot of mental context switching - one doesn't want to stare at a frozen window for a minute or more, so one does something else - and makes the whole process very tiring. Especially since one then has to go back and click on the new goals afterwards, that one could have been doing during the waiting time. Where is the multiplication by 3 found in the code? I could easily try putting a smaller number to see what the impact is. julia ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] concurrency
On Sat, 20 Apr 2019, Guillaume Melquiond wrote: > Le 19/04/2019 à 13:41, Julia Lawall a écrit : > > >> I'm not sure how to help, but I wonder: how many provers you asked Why3 > >> to run in parallel? I suggest you should not use 48, because you will > >> have no remaining cores for the main Why3 process, and other processes > >> of your system. > > > > I asked for 47. > > > > But even if there are only eg 10 things to prove, I still see a > > smaller but noticible delay. > > Keep in mind that Why3 is inherently mono-core. So, Why3 will be > unusable until the 10 corresponding proof obligations have been > generated and sent to external provers. > > More generally, the more cores you computer has, the more proof > obligations Why3 needs to generate to feed all the external provers, the > less usable the user interface becomes. I looked around a bit. In controller_itp.ml there is a function called run_timeout_handler. I printed the difference between the time when this function is called and when timeout_handler runs. run_timeout_handler is only called once in my test. timeout_handler is first run after 0.4 seconds. The next run is after 25 more seconds, when it calls read_answers. The delays after that are 6-7 seconds. Is this expected? julia___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] concurrency
On Fri, 19 Apr 2019, Claude Marche wrote: > > Hello Julia, > > I'm not sure how to help, but I wonder: how many provers you asked Why3 > to run in parallel? I suggest you should not use 48, because you will > have no remaining cores for the main Why3 process, and other processes > of your system. I asked for 47. But even if there are only eg 10 things to prove, I still see a smaller but noticible delay. But if there is nothing obvious, I will try to look into it later. thanks, julia > > - Claude > > Le 18/04/2019 à 11:35, Julia Lawall a écrit : > > Hello, > > > > I wonder if there is a concurrency problem that could be easily solved? I > > use why3 on a 48 core server. When I start up why3, when I refresh, or > > run obsolete proofs, there is a long time (maybe one minute) where the ide > > is not responsive. When I use top, I see the solvers running. But it > > would be nice if the GUI could continue to be usable, particularly for > > running obsolete proofs. Often 90% of the proofs are rerunnable, but > > there are some new ones, and it would be nice to work on them immediately, > > rather than wait for most everything else to finish. > > > > thanks, > > julia > > ___ > > Why3-club mailing list > > Why3-club@lists.gforge.inria.fr > > https://lists.gforge.inria.fr/mailman/listinfo/why3-club > > > ___ > Why3-club mailing list > Why3-club@lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/why3-club >___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] returned value for ensures
On Mon, 15 Apr 2019, Jean-Christophe Filliatre wrote: > Hi Julia, > > > Couldn't the extraction just leave undefined things as undefined? > > You can use the --modular option of Why3's extraction for this purpose. > > Move your undefined function(s) to a separate module, say module X in > file a.mlw, and then extract whatever other file/modules using A, say > b.mlw, with something like > > why3 extract -D ocaml64 --modular b.mlw -o . > > You'll get OCaml files such as b__M.ml with references to some OCaml > module A__X. Now you are free to provide such a module A__X by any means. That sounds fine. Thanks! julia > > Hope this helps, > -- > Jean-Christophe > > >> Le 14/04/19 à 18:51, Julia Lawall a écrit : > >> > >> > >> On Sun, 14 Apr 2019, Mario Pereira wrote: > >> > >> Hi Julia, > >> > >> Can you please check if last commit (62c99f) fixes your extraction problem? > >> > >> I think it is ok. It doesn't actually work, because I have a function > >> random_int that has no definition, but it doesn't give the error I was > >> getting previously. > >> > >> julia > >> > >> Thank you in advance. > >> > >> Best regards > >> -- > >> Mário > >> > >> Le 12/04/19 à 22:34, Julia Lawall a écrit : > >> > >> > >> On Fri, 12 Apr 2019, Jean-Christophe Filliatre wrote: > >> > >> I think I managed to reproduce Julia's problem with a small input file: > >> > >> -- > >> use int.Int > >> > >> let f (x: int) : (ghost a: int, ghost b: int) = > >> x+1, x+2 > >> > >> let g (x: int) = > >> let a, b = f x in > >> () > >> -- > >> > >> It fails on the same assertion. > >> > >> Thanks. My code has ghost on the let variables as well, but probbaly that > >> is not necessary. > >> > >> julia > >> > >> -- > >> Jean-Christophe > >> > >> On 4/12/19 6:24 PM, Mario Pereira wrote: > >> > >> Do you have any suggestions of what to look for? > >> > >> It would maybe be helpful for me to debug the problem to know if this > >> comes from pattern or type extraction. > >> > >> When you are calling the extraction engine, could you please add to your > >> command line the following: "--debug stack_trace". We might be able to > >> track down which function is calling the [visible_of_mask] function. > >> > >> Bests > >> -- > >> Mário > >> > >> > >> ___ > >> Why3-club mailing list > >> Why3-club@lists.gforge.inria.fr > >> https://lists.gforge.inria.fr/mailman/listinfo/why3-club > >> > >> ___ > >> Why3-club mailing list > >> Why3-club@lists.gforge.inria.fr > >> https://lists.gforge.inria.fr/mailman/listinfo/why3-club > >> > >> ___ > >> Why3-club mailing list > >> Why3-club@lists.gforge.inria.fr > >> https://lists.gforge.inria.fr/mailman/listinfo/why3-club > >> > >> > >>> > >> > >> ___ > >> Why3-club mailing list > >> Why3-club@lists.gforge.inria.fr > >> https://lists.gforge.inria.fr/mailman/listinfo/why3-club > >> > >> > >> > > > > > > ___ > > Why3-club mailing list > > Why3-club@lists.gforge.inria.fr > > https://lists.gforge.inria.fr/mailman/listinfo/why3-club > > > ___ > Why3-club mailing list > Why3-club@lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/why3-club >___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] returned value for ensures
On Sun, 14 Apr 2019, Mario Pereira wrote:
>
> Hi,
>
> In that case, I believe you need a custom driver to map your [random_int]
> function to some OCaml code. In the case of function [random_int63] from the
> Why3 standard library, we have the following line in the ocaml64 driver:
>
> syntax val random_int63 "Random.int %1"
>
> This makes every ocurrence of [random_int63 x] to be mapped to [Random.int
> x] in the final extracted code.
>
> On the other hand, why not using one of the [random_int] functions from the
> Why3 standard library? You would benefit from the existing extraction
> drivers.
I followed the documentations, which encourages one to write one's own:
This easiest way to get random numbers (of random values of any type) is
to take advantage of the non-determinism of Hoare triples. Simply
declaring a function
[val random_int: unit -> {} int {}]
is typically enough.
I could try Random, which seems simple enough. But I also need a random
value of one of my own types.
Couldn't the extraction just leave undefined things as undefined?
julia
>
> Best regards
> --
> Mário
>
> Le 14/04/19 à 18:51, Julia Lawall a écrit :
>
>
> On Sun, 14 Apr 2019, Mario Pereira wrote:
>
> Hi Julia,
>
> Can you please check if last commit (62c99f) fixes your extraction problem?
>
> I think it is ok. It doesn't actually work, because I have a function
> random_int that has no definition, but it doesn't give the error I was
> getting previously.
>
> julia
>
> Thank you in advance.
>
> Best regards
> --
> Mário
>
> Le 12/04/19 à 22:34, Julia Lawall a écrit :
>
>
> On Fri, 12 Apr 2019, Jean-Christophe Filliatre wrote:
>
> I think I managed to reproduce Julia's problem with a small input file:
>
> --
> use int.Int
>
> let f (x: int) : (ghost a: int, ghost b: int) =
> x+1, x+2
>
> let g (x: int) =
> let a, b = f x in
> ()
> --
>
> It fails on the same assertion.
>
> Thanks. My code has ghost on the let variables as well, but probbaly that
> is not necessary.
>
> julia
>
> --
> Jean-Christophe
>
> On 4/12/19 6:24 PM, Mario Pereira wrote:
>
> Do you have any suggestions of what to look for?
>
> It would maybe be helpful for me to debug the problem to know if this
> comes from pattern or type extraction.
>
> When you are calling the extraction engine, could you please add to your
> command line the following: "--debug stack_trace". We might be able to
> track down which function is calling the [visible_of_mask] function.
>
> Bests
> --
> Mário
>
>
> ___
> Why3-club mailing list
> Why3-club@lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>
> ___
> Why3-club mailing list
> Why3-club@lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>
> ___
> Why3-club mailing list
> Why3-club@lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>
>
> >
>
> ___
> Why3-club mailing list
> Why3-club@lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>
>
>___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] returned value for ensures
On Sun, 14 Apr 2019, Mario Pereira wrote: > > Hi Julia, > > Can you please check if last commit (62c99f) fixes your extraction problem? I think it is ok. It doesn't actually work, because I have a function random_int that has no definition, but it doesn't give the error I was getting previously. julia > > Thank you in advance. > > Best regards > -- > Mário > > Le 12/04/19 à 22:34, Julia Lawall a écrit : > > > On Fri, 12 Apr 2019, Jean-Christophe Filliatre wrote: > > I think I managed to reproduce Julia's problem with a small input file: > > -- > use int.Int > > let f (x: int) : (ghost a: int, ghost b: int) = > x+1, x+2 > > let g (x: int) = > let a, b = f x in > () > -- > > It fails on the same assertion. > > Thanks. My code has ghost on the let variables as well, but probbaly that > is not necessary. > > julia > > -- > Jean-Christophe > > On 4/12/19 6:24 PM, Mario Pereira wrote: > > Do you have any suggestions of what to look for? > > It would maybe be helpful for me to debug the problem to know if this > comes from pattern or type extraction. > > When you are calling the extraction engine, could you please add to your > command line the following: "--debug stack_trace". We might be able to > track down which function is calling the [visible_of_mask] function. > > Bests > -- > Mário > > > ___ > Why3-club mailing list > Why3-club@lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/why3-club > > ___ > Why3-club mailing list > Why3-club@lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/why3-club > > > > > ___ > Why3-club mailing list > Why3-club@lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/why3-club > > >___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] returned value for ensures
On Fri, 12 Apr 2019, Mario Pereira wrote: > > Do you have any suggestions of what to look for? > > It would maybe be helpful for me to debug the problem to know if this comes > from pattern or type extraction. > > When you are calling the extraction engine, could you please add to your > command line the following: "--debug stack_trace". We might be able to track > down which function is calling the [visible_of_mask] function. Here is the top of the trace: Raised at file "src/mlw/compile.ml", line 63, characters 22-34 Called from file "src/mlw/compile.ml", line 110, characters 17-37 Called from file "src/mlw/compile.ml", line 466, characters 10-17 Called from file "list.ml", line 82, characters 20-23 Called from file "src/mlw/compile.ml", line 442, characters 27-63 Called from file "src/mlw/compile.ml", line 287, characters 20-44 Called from file "src/mlw/compile.ml", line 410, characters 17-39 Called from file "src/mlw/compile.ml", line 287, characters 20-44 Called from file "src/mlw/compile.ml", line 421, characters 19-50 Called from file "src/mlw/compile.ml", line 287, characters 20-44 Called from file "src/mlw/compile.ml", line 287, characters 20-44 Called from file "src/mlw/compile.ml", line 566, characters 16-45 The command line was: why3 extract -L . -D ocaml64 --debug stack_trace file.mlw julia > > Bests > -- > Mário > > >___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] returned value for ensures
why3 extract is tripping on the assert in the following code (MaskGhost case): (* remove ghost components from tuple, using mask *) (* TODO : completely remove this function *) let visible_of_mask m sl = match m with | MaskGhost-> assert false (* FIXME ? *) | MaskVisible -> sl | MaskTuple ml -> let add_ity acc m ity = if mask_ghost m then acc else ity :: acc in if List.length sl < List.length ml then sl (* FIXME ? much likely... *) else List.rev (List.fold_left2 add_ity [] ml sl) I haven't made any effort yet to debug the problem, but any suggestions would be appreciated. thanks, julia ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] returned value for ensures
On Sun, 7 Apr 2019, Mario Pereira wrote:
> Hello,
>
> I believe you can resort to *ghost results* in order to solve this
> issue. In Why3, a function can return multiple results, some of them
> marked as ghost.
>
> For instance:
>
> let f (x: int) : (r: int, ghost rg: int)
> ensures { r = rg + 1 /\ rg = x }
> = (x+1, x)
>
> Generally speaking, whenever you need to quantify existentially in a
> postcondition you might consider return a witness, in the form of a
> ghost result.
So the call site just receives an integer, and not a pair of an integer
and a ghost integer?
It seems that I can put an ensures at the end of the function as well, and
it can refer to a variable that is let bound in the first line. But I
haven't checked whether that ensures is available to the call site.
julia___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] strategy parse error
On Sun, 7 Apr 2019, Jean-Christophe Filliatre wrote: > Hi Julia, > > You cannot use %t and %f in your strategy code. These have to be integer > values instead, e.g. > > c Alt-Ergo,2.3.0 10 4000 > > But it makes a nice feature wish! OK, thanks. I'll add it to the issue tracker as a suggestion. julia > > Best regards, > -- > Jean-Christophe > > On 4/6/19 8:38 AM, Julia Lawall wrote: > > Hello, > > > > I tried to make the following strategy: > > > > [strategy] > > code = "start: > > t inline_goal afterinline > > afterinline: > > t split_vc aftersplit > > aftersplit: > > c Alt-Ergo,2.3.0 %t %f > > " > > desc = "Inline@ then@ split" > > name = "InlineSplit" > > > > It gives a parse error on the c at the beginning of the last line. What > > is wrong? > > > > thanks, > > julia > > ___ > > Why3-club mailing list > > Why3-club@lists.gforge.inria.fr > > https://lists.gforge.inria.fr/mailman/listinfo/why3-club > > > ___ > Why3-club mailing list > Why3-club@lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/why3-club > ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] Different types of function declaration
On Sat, 6 Apr 2019, Andrei Paskevich wrote: > Hi Julia, > > On Sat, 6 Apr 2019 at 17:03, Julia Lawall wrote: > > I am somewhat lost at different types of functions in Why3. I > > understand that there are pure logical functions and program > > functions, but I am confused by different types of > declarations. Here > > are my questions. > > > > What is the difference between val and let? Is it true that > val is > > used for declaring functions without a body and let for > defining > > function with a body? Can they be used for pure and program > functions? > > To my understanding, val and let with function are for the > program side. > val is the not defined ones that you may provide in a subsequent > clone, > and let is for the ones you define. > > > Correct. > > You can also use val and let with lemma. For let, you will > provide a > proof and for val you will not. Not ever. If you want to be > asked to > provide a proof when you clone the module, you should use axiom > rather > than val lemma. > > > Correct, though we might require "val lemmas" to be instantiated when cloned > in the future. It would make the case for lemmas and for functions more parallel. > > > What do keywords function, predicate and lemma (?) mean in > function > > definitions/declarations? What is the difference between > "function f", > > "let function f" and "let f", and similarly for "val"? > > I'm not sure to understand the first sentence. let function > gives you > something that you can use in both code and formulas. > Predicates are > usable in formulas only. > > > I would say "let function and let predicate gives you something that you can > use in both code and formulas. Functions and predicates are usable in > logical formulas and in the ghost code, but not in the code intended for > execution." > > I wonder if there is a difference between a predicate and a > function that returns bool? > > > There is no fundamental difference between the two and the SMT standard > actually does not make one at all. However, the traditional formulations of > the first-order logic (upon which most automated provers are based) > distinguish predicates from Boolean functions, and WhyML retains this > distinction. OK, thanks. julia___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] Different types of function declaration
On Sat, 6 Apr 2019, Евгений Макаров wrote: > Hello, > > I am somewhat lost at different types of functions in Why3. I > understand that there are pure logical functions and program > functions, but I am confused by different types of declarations. Here > are my questions. > > What is the difference between val and let? Is it true that val is > used for declaring functions without a body and let for defining > function with a body? Can they be used for pure and program functions? To my understanding, val and let with function are for the program side. val is the not defined ones that you may provide in a subsequent clone, and let is for the ones you define. You can also use val and let with lemma. For let, you will provide a proof and for val you will not. Not ever. If you want to be asked to provide a proof when you clone the module, you should use axiom rather than val lemma. > > What do keywords function, predicate and lemma (?) mean in function > definitions/declarations? What is the difference between "function f", > "let function f" and "let f", and similarly for "val"? I'm not sure to understand the first sentence. let function gives you something that you can use in both code and formulas. Predicates are usable in formulas only. I wonder if there is a difference between a predicate and a function that returns bool? That's the end of my knowledge :) julia > How can one find out which functions from the standard library have > implementation (can be executed) and which don't? For example, both > function add from Impset and ([]<-) from Array are declared as val. > Can I run them both using "why3 execute"? > > Also, executing functions from Fset, for example, add 3 empty, results > in the message "anomaly: File "src/mlw/pinterp.ml", line 204, > characters 12-18: Assertion failed". > > I apologize if these questions are basic. I spend a lot of time > reading and searching through different parts of the manual, but the > clear picture is still not there, and I feel it takes too much time to > research this on my own. Please direct me to the relevant parts of the > documentation if necessary. > > Evgeny > ___ > Why3-club mailing list > Why3-club@lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/why3-club >___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
[Why3-club] strategy parse error
Hello, I tried to make the following strategy: [strategy] code = "start: t inline_goal afterinline afterinline: t split_vc aftersplit aftersplit: c Alt-Ergo,2.3.0 %t %f " desc = "Inline@ then@ split" name = "InlineSplit" It gives a parse error on the c at the beginning of the last line. What is wrong? thanks, julia ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] smoke detector
On Thu, 4 Apr 2019, Sylvain Dailler wrote: > On 03/04/2019 20:35, Julia Lawall wrote: > > > >The smoke detector is parallel > > > > to the splint in each case, and times out in each case. When I replay > > > > this file with the smoke detector option, I get warnings. > > > Can you tell us what are the warnings you get ? > > Warnings indicating problems. Like: > > > > goal 'move_ready_current_preserves.0.9.0', prover 'Alt-Ergo 2.3.0': result > > is: Valid (0.37s, 556 steps) -> Smoke detected! > > This warning means that the smoke detector detected that the context of this > goal is self contradicting. > > From what I understand, your remark is that the smoke detection from the > why3replay does not result in the same session as the one from the IDE. Yes, > it is the case. Smoke detection was never thought to be launched from the IDE > (even if, to some extent, it can). We'll see if it is possible to harmonize > these two usage in the future. Thanks. I'm ok with the overall usage of the smoke detector at the moment, and it has been very helpful in practice. julia ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
[Why3-club] smoke and unreachable code
The why3 manual says that the smoke detector can give false positives in the case of unreachable code. Is there any way to avoid this? I have an unreachable match case. I tried putting absurd in the code, but I still get a smoke detected report. thanks, julia ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] smoke detector
On Wed, 3 Apr 2019, Sylvain Dailler wrote: > Sorry for the delay. > > On 03/04/2019 11:53, Julia Lawall wrote: > > OK, sorry, I don't know. I tried it again just now, and it sent alt-ergo > > to both subgoals, the children of the split and the children of thesmoke > > detector. Perhaps I misinterpreted what it was doing previously. > > > > Still running smoke detector on the whole project doesn't seem to send the > > smoke detector effect to the same place as one gets when doing why3 > > replay. I've included a small screenshot. > > It is not joint to your mail. Sorry, should be there now. > > > The smoke detector is parallel > > to the splint in each case, and times out in each case. When I replay > > this file with the smoke detector option, I get warnings. > > Can you tell us what are the warnings you get ? Warnings indicating problems. Like: goal 'move_ready_current_preserves.0.9.0', prover 'Alt-Ergo 2.3.0': result is: Valid (0.37s, 556 steps) -> Smoke detected! julia___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] smoke detector
On Wed, 3 Apr 2019, Sylvain Dailler wrote: > On 03/04/2019 10:31, François Bobot wrote: > > So perhaps you both agree that we should hide the smoke detector > > transformation but we should not > > hide the smoke detector functionnality in the IDE. > > Ideally, I would tend to agree with this, I am not sure what it implies in > practice for the tool. I'll open an issue for this in particular with > suggested solutions. > > > As mentioned in my other response, this doesn't work properly when there > > is a split. Perhaps the source of the problem is that typing > > smoke-detector into the command line box doesn't do the same thing as when > > the smoke detector is run on the real command line with replay. > > I don't understand the problem. Do you have an example ? OK, sorry, I don't know. I tried it again just now, and it sent alt-ergo to both subgoals, the children of the split and the children of thesmoke detector. Perhaps I misinterpreted what it was doing previously. Still running smoke detector on the whole project doesn't seem to send the smoke detector effect to the same place as one gets when doing why3 replay. I've included a small screenshot. The smoke detector is parallel to the splint in each case, and times out in each case. When I replay this file with the smoke detector option, I get warnings. This is with top. I have tried deep a few times but haven't seen differences, but anyway, I want to understand the top warnings first. The screen shot results from putting the cursor where you see it on Ule, then typing smoke_detector_top in the command line box, then selecting alt-ergo on the Ule node. julia > > By smoke detector, do you mean smoke_detector_deep, smoke_detector_top or some > other ? It's possible that I don't understand well enough what's changed > during smoke detection. > > smoke_detector_* is a transformation in the IDE. > > When a transformation/prover is launched the behavior should be as follows > (depending on what node is selected in the proof tree): > > - A proof node/goal is selected: execute only on this goal/proof node, > - A transformation node/file/theory is selected: execute on the lowest level > goal nodes, > - A proof attempt (cvc4/z3/altergo..) is selected: execute on the parent goal. > >___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] smoke detector
On Wed, 3 Apr 2019, François Bobot wrote: > Le 03/04/2019 à 10:22, Julia Lawall a écrit : > > On Wed, 3 Apr 2019, Sylvain Dailler wrote: > >> > >> Perhaps, we should hide this kind of transformations from the IDE ? > >>> Is > >>> there a way to click once and get them all to be proved at once? > >> > >> After a transformation is completed, if you want to use a command on all > >> its > >> subnodes, you can first click the transformation node and then use the > >> command > >> as normal. By default, this will execute your command on all the subgoals. > >> Alternatively, you can right click on the transformation node and launch > >> your > >> command from there. > > > > As mentioned in my other response, this doesn't work properly when there > > is a split. Perhaps the source of the problem is that typing > > smoke-detector into the command line box doesn't do the same thing as when > > the smoke detector is run on the real command line with replay. > > > > So perhaps you both agree that we should hide the smoke detector > transformation but we should not > hide the smoke detector functionnality in the IDE. Sorry, I don't know what you mean by "hide the smoke detector transformation". Perhaps there could just be a warning message if the smoke detector is applied to an unproved goal or to a goal that already has a split? julia > The difficulty is too change the way the consolidation of the tree is done by > adding an > "inconsistent if reachable" value. > > -- > François >___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] smoke detector
On Wed, 3 Apr 2019, François Bobot wrote: > Le 02/04/2019 à 14:15, Julia Lawall a écrit : > > Having discovered the commandline, I also found the command smoke > > detector. Running that command makes a lot of proof obligations. Is > > there a way to click once and get them all to be proved at once? > > > > About which commandline are you talking about? > > Is it `why3 replay --smoke-detector deep` ? No, the command line in the why3 ide. It seems that the problem comes if there exists a proof that involves a split. The smoke detector goal comes under the split, and then a call to a prover at the top will just work on the first goal it finds at the lowest level, ie the split, rather than the smoke detector. The problem goes away if I get rid of the splits, but the resulting smoke detection goal is very high level, and may be not provable for that reason. So far I have gotten better results by using replay, and then going into the ide and using the smoke transformation on the specific goal that was highlighted during the replay. This seems like an ok solution. thanks, julia > > Best, > > -- > François > ___ > Why3-club mailing list > Why3-club@lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/why3-club >___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
[Why3-club] smoke detector
Having discovered the commandline, I also found the command smoke detector. Running that command makes a lot of proof obligations. Is there a way to click once and get them all to be proved at once? thanks, julia ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] Questions about the why3 ide
On Fri, 29 Mar 2019, Claude Marche wrote: > > > Le 29/03/2019 à 09:39, Julia Lawall a écrit : > > > > >>> The editor recently introduced in Why3 provides a great improvement to > >>> the user experience. Thanks a lot. > >> > >> Thanks for your positive feedback! > > > > I use this a lot as well. > > > > I miss the ability to search, particularly in the task view. > > > > julia > > I agree this is a missing feature. > > Generally speaking, do not hesitate to put feature wishes in the gitlab > tracker : > > https://gitlab.inria.fr/why3/why3/issues > > and then click on 'new issue' Done, thanks. julia___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] Questions about the why3 ide
On Fri, 29 Mar 2019, Claude Marche wrote: > > Hello, > > Le 28/03/2019 à 16:38, Delphine Demange a écrit : > > Hi, > > > > The editor recently introduced in Why3 provides a great improvement to > > the user experience. Thanks a lot. > > Thanks for your positive feedback! I use this a lot as well. I miss the ability to search, particularly in the task view. julia > > I'm running the Why3 platform, version 1.1.0. > > > > I'd like to know whether it is possible to : > > - configure the IDE so that the tab showed by default would be the > > "Source view", instead of the "Task view" > > It is not configurable, but we could make it configurable of course > > > - close a file from the IDE directly > > What do you mean by "closing"? removing the tab? > > > - reset the session from the IDE > > What do you mean by "reset"? abandon all changes? That is what you can > achieve by exiting without saving and reloading? > > > Perhaps these features were already introduced in a version more recent > > than mine. > > No they aren't, but we are willing to add them if you think it is useful. > > - Claude > ___ > Why3-club mailing list > Why3-club@lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/why3-club >___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] predicates
On Mon, 25 Mar 2019, Andrei Paskevich wrote: > Commited in 5e93e6d7 in master. You can put the attribute [@inline:trivial] > over the predicate symbol (right after the name) or over its definition > (right before the formula). The symbol will be inlined automatically for the > majority > of the automated provers via their drivers. Alternatively, you can call apply > "inline_trivial" in the IDE to force the inlining during the interactive > phase. Great! Thanks so much for taking care of it quickly. julia > > Best, > Andrei > > On Mon, 25 Mar 2019 at 10:43, Julia Lawall wrote: > On Mon, 25 Mar 2019, Andrei Paskevich wrote: > > > The change in the master branch I can do today, if you are okay with > using a development version. > > That would be wonderful. I would be much better than rewriting all of > my > predicates :) > > Thanks very much. > julia > > > > > Best, > > Andrei > > > > On Mon, 25 Mar 2019 at 10:35, Julia Lawall > wrote: > > > > > > On Mon, 25 Mar 2019, Andrei Paskevich wrote: > > > > > Hi Julia, > > > > > > would it help to label such predicates explicitly in order to > always inline them when passing the task to a prover (as you suggested in an > earlier mail)? I am inclined to add this functionality to the > "inline_trivial" > > transformation. > > > One downside of this is that the predicate is not inlined > while you are in the interactive phase, so, for example, "split_goal" will > not work on it, unless you call inline on it. > > > > I would be completely happy to label the predicates with > inline. I know > > up front that they only exist to collect information and reduce > code size. > > The split_goal limitation is not a problem. > > > > Could this be done quickly, or would it have to wait for the > next release? > > > > Thanks, > > julia > > > > > > > > Best, > > > Andrei > > > > > > On Mon, 25 Mar 2019 at 08:57, Julia Lawall > wrote: > > > My natural inclination is to make predicates that > combine other > > > predicates, in order to avoid massive code duplication. > But it seems that > > > doing so makes it very hard for why3 to find the > information it needs. So > > > to get the proof to go through, I have to manually > inline the predicates, > > > which clutters the code and is quite unsatisfying. > > > > > > These predicates are not in the goal, but rather in the > hypotheses, eg in > > > the ensures of a function I am calling. Inline goal is > thus of no use, > > > and Inline all inlines far too much, and seems to make > it impossible to > > > get the proof to go through for other reasons. > > > > > > Is there some intuition about when it is possible to > define predicates > > > that wrap other predicates and when it is not? Is > there some level of > > > nesting that one should not exceed, or is there a > distinction between > > > predicates defined in the current module or some other > module? > > > > > > I have tried meta rewrite_def predicate XXX but it > doesn't seem to give > > > much benefit. > > > > > > thanks, > > > julia > > > ___ > > > Why3-club mailing list > > > Why3-club@lists.gforge.inria.fr > > > https://lists.gforge.inria.fr/mailman/listinfo/why3-club > > > > > > > > > > > > > > > > > >___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] predicates
On Mon, 25 Mar 2019, Andrei Paskevich wrote: > Hi Julia, > > would it help to label such predicates explicitly in order to always inline > them when passing the task to a prover (as you suggested in an earlier mail)? > I am inclined to add this functionality to the "inline_trivial" > transformation. > One downside of this is that the predicate is not inlined while you are in > the interactive phase, so, for example, "split_goal" will not work on it, > unless you call inline on it. I would be completely happy to label the predicates with inline. I know up front that they only exist to collect information and reduce code size. The split_goal limitation is not a problem. Could this be done quickly, or would it have to wait for the next release? Thanks, julia > > Best, > Andrei > > On Mon, 25 Mar 2019 at 08:57, Julia Lawall wrote: > My natural inclination is to make predicates that combine other > predicates, in order to avoid massive code duplication. But it seems > that > doing so makes it very hard for why3 to find the information it needs. > So > to get the proof to go through, I have to manually inline the > predicates, > which clutters the code and is quite unsatisfying. > > These predicates are not in the goal, but rather in the hypotheses, eg > in > the ensures of a function I am calling. Inline goal is thus of no use, > and Inline all inlines far too much, and seems to make it impossible to > get the proof to go through for other reasons. > > Is there some intuition about when it is possible to define predicates > that wrap other predicates and when it is not? Is there some level of > nesting that one should not exceed, or is there a distinction between > predicates defined in the current module or some other module? > > I have tried meta rewrite_def predicate XXX but it doesn't seem to give > much benefit. > > thanks, > julia > ___ > Why3-club mailing list > Why3-club@lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/why3-club > > >___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
[Why3-club] predicates
My natural inclination is to make predicates that combine other predicates, in order to avoid massive code duplication. But it seems that doing so makes it very hard for why3 to find the information it needs. So to get the proof to go through, I have to manually inline the predicates, which clutters the code and is quite unsatisfying. These predicates are not in the goal, but rather in the hypotheses, eg in the ensures of a function I am calling. Inline goal is thus of no use, and Inline all inlines far too much, and seems to make it impossible to get the proof to go through for other reasons. Is there some intuition about when it is possible to define predicates that wrap other predicates and when it is not? Is there some level of nesting that one should not exceed, or is there a distinction between predicates defined in the current module or some other module? I have tried meta rewrite_def predicate XXX but it doesn't seem to give much benefit. thanks, julia ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] constants
On Wed, 20 Mar 2019, Mario Pereira wrote:
> Hi,
>
> Would it help if you attach a postcondition to your constants definition?
>
> let constant realtime = 0
> ensures { result = 0 }
> let constant timeshare = 1
> ensures { result = 1 }
I'll try that. Thanks!
julia
>
> Best regards
> --
> Mário
>
> Le 20/03/19 à 10:49, Julia Lawall a écrit :
> >
> > On Wed, 20 Mar 2019, Jean-Christophe Filliatre wrote:
> >
> >> Dear Julia,
> >>
> >> With a goal as simple as
> >>
> >>let constant realtime = 0
> >>let constant timeshare = 1
> >>goal G: realtime <> timeshare
> >>
> >> I get an SMT input file (e.g. for CVC4) which is
> >>
> >>(assert
> >>;; G
> >> ;; File "test.mlw", line 3, characters 5-6
> >> (not (not (= 0 1
> >>
> >> and (obviously) proved with no difficulty. I get the same SMT input file
> >> with a program VC such as
> >>
> >>let f () ensures { realtime <> timeshare } = ()
> >>
> >> for instance. So I guess you are referring to a more complex situation.
> >> Could you please tell us in which situation you have trouble knowing
> >> that realtime and timeshare have different values?
> > OK, I think it woud be hard to cut down my code to something
> > understandable that would show the problem. I was hoping that constants
> > would be just inlined away, like for a #define in C. But perhaps there
> > are good reasons for not doing that.
> >
> > thanks,
> > julia
> >
> >
> >> Best regards,
> >> --
> >> Jean-Christophe
> >>
> >> On 3/19/19 10:36 PM, Julia Lawall wrote:
> >>> I have some definitions:
> >>>
> >>> let constant realtime = 0
> >>> let constant timeshare = 1
> >>>
> >>> However, subsequently why3 seems to have trouble proving things involving
> >>> these values, particularly things that involve knowing that realtime and
> >>> timeshare don't have the same value. Inlining the values makes the proofs
> >>> work out, but is not great for readability. In the end, I put
> >>>
> >>> 0(*realtime*)
> >>> 1(*timeshare*)
> >>>
> >>> at all the usage sites. Is there a way to cause uses of realtime and
> >>> timeshare to behave exactly like uses of 0 and 1?
> >>>
> >>> thanks,
> >>> julia
> >>> ___
> >>> Why3-club mailing list
> >>> Why3-club@lists.gforge.inria.fr
> >>> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
> >>>
> >> ___
> >> Why3-club mailing list
> >> Why3-club@lists.gforge.inria.fr
> >> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
> >>
> > ___
> > Why3-club mailing list
> > Why3-club@lists.gforge.inria.fr
> > https://lists.gforge.inria.fr/mailman/listinfo/why3-club
> ___
> Why3-club mailing list
> Why3-club@lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] constants
On Wed, 20 Mar 2019, Jean-Christophe Filliatre wrote:
> Dear Julia,
>
> With a goal as simple as
>
> let constant realtime = 0
> let constant timeshare = 1
> goal G: realtime <> timeshare
>
> I get an SMT input file (e.g. for CVC4) which is
>
> (assert
> ;; G
>;; File "test.mlw", line 3, characters 5-6
> (not (not (= 0 1
>
> and (obviously) proved with no difficulty. I get the same SMT input file
> with a program VC such as
>
> let f () ensures { realtime <> timeshare } = ()
>
> for instance. So I guess you are referring to a more complex situation.
> Could you please tell us in which situation you have trouble knowing
> that realtime and timeshare have different values?
OK, I think it woud be hard to cut down my code to something
understandable that would show the problem. I was hoping that constants
would be just inlined away, like for a #define in C. But perhaps there
are good reasons for not doing that.
thanks,
julia
>
> Best regards,
> --
> Jean-Christophe
>
> On 3/19/19 10:36 PM, Julia Lawall wrote:
> > I have some definitions:
> >
> > let constant realtime = 0
> > let constant timeshare = 1
> >
> > However, subsequently why3 seems to have trouble proving things involving
> > these values, particularly things that involve knowing that realtime and
> > timeshare don't have the same value. Inlining the values makes the proofs
> > work out, but is not great for readability. In the end, I put
> >
> > 0(*realtime*)
> > 1(*timeshare*)
> >
> > at all the usage sites. Is there a way to cause uses of realtime and
> > timeshare to behave exactly like uses of 0 and 1?
> >
> > thanks,
> > julia
> > ___
> > Why3-club mailing list
> > Why3-club@lists.gforge.inria.fr
> > https://lists.gforge.inria.fr/mailman/listinfo/why3-club
> >
> ___
> Why3-club mailing list
> Why3-club@lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
[Why3-club] constants
I have some definitions: let constant realtime = 0 let constant timeshare = 1 However, subsequently why3 seems to have trouble proving things involving these values, particularly things that involve knowing that realtime and timeshare don't have the same value. Inlining the values makes the proofs work out, but is not great for readability. In the end, I put 0(*realtime*) 1(*timeshare*) at all the usage sites. Is there a way to cause uses of realtime and timeshare to behave exactly like uses of 0 and 1? thanks, julia ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] strategy definitions in the config file
On Mon, 18 Mar 2019, Claude Marche wrote: > > Sorry for the late answer. > > Please look at the manual http://why3.lri.fr/doc/technical.html#sec137 > for a description of the language of proof strategies. > > As shown by Mario's answer, the "t" instruction requires both a > transformation name and a label. You did not give any label. The > newlines are not significant so in your case the "c" on the next line is > taken as the label, and then the next token "Alt-Ergo,2.0" is not > understood as a command, which can be only c, p, t or a label. Thanks for the explanation and the pointer to the relevant section of the manual. julia > > - Claude > > Le 16/03/2019 à 09:17, Julia Lawall a écrit : > > Often I do split_vc and the alt-ergo. How would I define such a strategy > > in the configuration file? > > > > I tried: > > > > [strategy] > > code = "start: > > t split_all_full > > c Alt-Ergo,2.0 40 1 > > > > But it says "Fatal: loading strategy 'Auto_level_1' failed: syntax error > > on character 'A' at position 26" > > > > I see examples with Eprover where the value in the name keyval pair is > > used to name the prover. Alt-Ergo has Alt-Ergo in this line, but it > > doesn't work. > > > > thanks, > > julia > > ___ > > Why3-club mailing list > > Why3-club@lists.gforge.inria.fr > > https://lists.gforge.inria.fr/mailman/listinfo/why3-club > > > ___ > Why3-club mailing list > Why3-club@lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/why3-club >___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
[Why3-club] strategy definitions in the config file
Often I do split_vc and the alt-ergo. How would I define such a strategy in the configuration file? I tried: [strategy] code = "start: t split_all_full c Alt-Ergo,2.0 40 1 But it says "Fatal: loading strategy 'Auto_level_1' failed: syntax error on character 'A' at position 26" I see examples with Eprover where the value in the name keyval pair is used to name the prover. Alt-Ergo has Alt-Ergo in this line, but it doesn't work. thanks, julia ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] lemma visibility
On Tue, 8 Jan 2019, Claude Marché wrote: > > Hello, > > The easiest way to achieve this is to add, at the end of the module that needs > a lemma "L" only internally, the declaration > > See attached file for example > > meta remove_prop lemma L I never got this to work. Actually my lemma is declared with let rec lemma. Why3 says that it is not a proposition. julia > > Hope this helps, > > Le 04/01/2019 à 16:48, Julia Lawall a écrit : > > Is it possible to make a lemma only visible within a module, but not > > visible to other modules that may import the module? It seems that the > > presence or absence of some irrelevant lemmas can have a big impact on > > whether at least Alt-Ergo can succeed in doing some proofs in a reasonable > > amount of time. > > > > thanks, > > julia > > ___ > > Why3-club mailing list > > Why3-club@lists.gforge.inria.fr > > https://lists.gforge.inria.fr/mailman/listinfo/why3-club > > >___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] always inline a predicate
On Thu, 7 Mar 2019, Jean-Christophe Filliatre wrote: > Dear Julia, > > There is a meta "inline:no" which can be used to indicate that a > function/predicate *must not* be inlined (by inline_all or inline_goal). > Use it like this > > meta "inline:no" predicate foo > > Unless I'm mistaken, there is no way to indicate the opposite i.e. that > a symbol must always be inlined. OK, I've been sprinkling meta "rewrite_def" proposition foo But I'm not sure if it really has an impact... julia > > Best regards, > -- > Jean-Christophe > > On 3/3/19 8:18 AM, Julia Lawall wrote: > > Hello, > > > > Is there an annotation that can be put in a .mlw to cause a predicate > > always to be inlined? Currently, I have to guess when inline_goal or > > inline_all would be useful, and neither is really satisfactory, because I > > don't want to inline everything, but just this one predicate. > > > > thanks, > > julia > > ___ > > Why3-club mailing list > > Why3-club@lists.gforge.inria.fr > > https://lists.gforge.inria.fr/mailman/listinfo/why3-club > > > ___ > Why3-club mailing list > Why3-club@lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/why3-club > ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
[Why3-club] always inline a predicate
Hello, Is there an annotation that can be put in a .mlw to cause a predicate always to be inlined? Currently, I have to guess when inline_goal or inline_all would be useful, and neither is really satisfactory, because I don't want to inline everything, but just this one predicate. thanks, julia ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] how to prove a type is inhabited?
On Thu, 21 Feb 2019, Jean-Jacques Levy wrote:
> I use ‘by’.. it’s good for a very local lemma or assertion. -JJ-
I'll look into that, thanks.
julia
>
> > Le 21 févr. 2019 à 16:46, Julia Lawall a écrit :
> >
> >
> >
> > On Thu, 21 Feb 2019, Raphael Rieu-Helft wrote:
> >
> >>
> >> Hello,
> >>
> >> Use the keyword `by`:
> >>
> >> type t = { x = array int } invariant { length x > 0 /\ x[0] > 0 } by { x =
> >> Array.make 1 1 }
> >
> > Is by useful for anything else? Sometimes I know that a particular lemma
> > should be useful for proving something, and from the English meaning of
> > "by" it would be nice to be able to say by useful_lemma. But that doesn't
> > work.
> >
> > julia
> >
> >>
> >> Raphaël
> >>
> >> On 21/02/2019 15:47, Alan Schmitt wrote:
> >> Hello,
> >>
> >> I have this very simple specification that creates a type and
> >> states an
> >> invariant for it.
> >>
> >> module Test
> >>
> >> use int.Int
> >> use array.Array
> >>
> >> type t = { x : array int }
> >> invariant { length x > 0 /\ x[0] > 0 }
> >>
> >> end
> >>
> >> When I load this in why3, I'm asked to check that the type is
> >> inhabited.
> >> Is there a way to provide a witness, as why3 is unable to guess
> >> it?
> >>
> >> Thanks,
> >>
> >> Alan
> >>
> >> ___
> >> Why3-club mailing list
> >> Why3-club@lists.gforge.inria.fr
> >> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
> >>
> >>
> > ___
> > Why3-club mailing list
> > Why3-club@lists.gforge.inria.fr
> > https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>
>___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] how to prove a type is inhabited?
On Thu, 21 Feb 2019, Raphael Rieu-Helft wrote:
>
> Hello,
>
> Use the keyword `by`:
>
> type t = { x = array int } invariant { length x > 0 /\ x[0] > 0 } by { x =
> Array.make 1 1 }
Is by useful for anything else? Sometimes I know that a particular lemma
should be useful for proving something, and from the English meaning of
"by" it would be nice to be able to say by useful_lemma. But that doesn't
work.
julia
>
> Raphaël
>
> On 21/02/2019 15:47, Alan Schmitt wrote:
> Hello,
>
> I have this very simple specification that creates a type and
> states an
> invariant for it.
>
> module Test
>
> use int.Int
> use array.Array
>
> type t = { x : array int }
> invariant { length x > 0 /\ x[0] > 0 }
>
> end
>
> When I load this in why3, I'm asked to check that the type is
> inhabited.
> Is there a way to provide a witness, as why3 is unable to guess
> it?
>
> Thanks,
>
> Alan
>
> ___
> Why3-club mailing list
> Why3-club@lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
>
>
>___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] inlining functions or explicit predicates
On Mon, 18 Feb 2019, Jean-Jacques Levy wrote:
> Dear Jean-Christophe and Friends,
> thanks for your answer. So you avoid inconsistent use of equality for records
> with ghost fields by preventing its usage in regular code. (I have still to
> understand the meaning of the ‘pure’ attribute). But in my case, ‘set_1000'
> was
> used in regular code, with mappings on an abstract type, which I thnk you do
> not like too !! (since that abstract type could be a record with ghost
> fields).
>
> Therefore :
>
> 1- I should use mappings on concrete scalar types (int, bool) [btw I have
> also a strange error - see below with bool]
>
> 2- I cannot use the ’set’ function of the mappings library when my ‘set_1000’
> is used in regular code :-( !
>
> Cheers, -JJ-
>
> ps/ similar problem with equality in why3.1.2.0 ?
>
> module BBB
>
> use int.Int
> use list.List
>
> type abc = bool
>
> let rec split (x : abc) (s: list abc) : (list abc, list abc) =
> variant {s}
> match s with
> | Nil -> (Nil, Nil)
> | Cons y s' -> if x = y then (Cons x Nil, s') else
> let (s1', s2) = split x s' in
> ((Cons y s1'), s2)
> end
>
> end
>
> hos $ why3 execute bbb.mlw
> File "bbb.mlw", line 12, characters 20-21:
> This expression has type bool, but is expected to have type int
In code, = is only defined on int. So you would need:
val (=) (x y : abc) : bool ensures { result <-> x=y }
julia
>
>
> Le 18 févr. 2019 à 08:21, Jean-Christophe Filliatre
> a écrit :
>
> Dear Jean-Jacques,
>
> You are making use of a ghost function to define set_1000, namely
> function ([<-]) from library map.Map. Consequently, your function
> set_1000 must be declared ghost. You can do this by inserting the
> "ghost" keyword immediately after "let rec":
>
> let rec ghost set_1000 (s : list 'a)(f : map 'a int) : map 'a int =
> ...
>
> Now why3 is going to complain that you must prove termination of
> function set_1000, as ghost code must terminate. Here, this is easy, as
> parameter "s" decreases:
>
> let rec ghost set_1000 (s : list 'a)(f : map 'a int) : map 'a int =
> variant { s }
> ...
>
> The definition is now accepted.
>
> You may wonder why function ([<-]) was declared ghost in the first
> place. This is because polymorphic equality is hidden behind this
> function. Function ([<-]) is actually syntactic sugar for this function
>
> let ghost function set (f: map 'a 'b) (x: 'a) (v: 'b) : map 'a 'b =
> fun y -> if pure {y = x} then v else f y
>
> where you can see that polymorphic equality is used to compare y and x.
> Since we don't know how to provide a polymorphic equality in programs
> (think of the comparison of records with possible ghost fields that
> would be erased at runtime), we have no other choice than forbidding its
> use in regular (i.e. non-ghost) code.
>
> As for your question "where to insert the ghost keyword", you can find
> the answer on page 87 in the PDF manual, Fig. 6.5.
> http://why3.lri.fr/manual.pdf
>
> Cheers
> --
> Jean-Christophe
>
> On 2/15/19 9:51 PM, Jean-Jacques Levy wrote:
> Dear Claude,
>
> thanks for your answer. So I upgraded (with opam) why3 to release 1.1.1.
> (couldn’t find opam upgrade to 1.2.0!)
>
> Now I’m facing a new problem with strange ‘ghost’ error.
> -
> module AAA
>
> use list.List
> use map.Map
>
> let rec set_1000 (s : list 'a)(f : map 'a int) =
> match s with
> | Nil -> f
> | Cons x s' -> (set_1000 s' f)[x <- 1000]
> end
>
> end
> -
> why3 execute aaa.mlw
> File "aaa.mlw", line 6, characters 8-16:
> Function set_1000 must be explicitly marked ghost
> -
> So why that message + where to insert the ghost keyword (couldn’t
> find!) ??
>
> Cheers, -JJ-
>
> Le 15 févr. 2019 à 17:08, Claude Marche > a écrit :
>
>
> Dear JJ,
>
> As you remark, Why3 0.88 is now quite outdated and my answer may
> not
> be very accurate. As far as I remember, the former "Inline"
> button was
> applying the transformation "inline_goal" which has the effect of
> inlining the defined function symbols appearing in an outermost
> position in the goal.
>
> The doc for the transformations are obtained when typing `why3
> --list-transforms', and some of them are documented in a bit more
> details in the manual : "inline_*" are documented at the
> beginning of
> http://why3.lri.fr/doc/technical.html#sec128
>
> In Why3 1.x, the user interface for applying transformations is
> much
> more powerful, in your case you would probably want to type
> "unfold
> foo" where "foo" is your
Re: [Why3-club] (no subject)
On Wed, 30 Jan 2019, François Bobot wrote: > Le 30/01/2019 à 13:36, Julia Lawall a écrit : > > I have the following orgnization of modules: > > > > A parameterized by f > > > > B uses A > > > > C uses A and B and is parameterized by g > > > > D uses A, B and C and provides a definition for f and for g > > The definition for g relies on things defined in A and B. > > > > How can I set this up? In D, I cannot just clone C, because I can't make > > the definition of g without having A and B. If I clone B, then define g, > > then clone C providing the definitions of both f and g, I get a type > > mismatch related to a type defined in B. > > > > In a similar example, I was able to move the problematic type definition out > of all these modules by > making it polymorphic. > > Then you can more easily instantiate functions repeatedly in all the modules. > > Does that work in your case? I don't think so. There are many types involved, but the one it is actually complaining about is a data structure containing arrays and matrices on which there are invariants. thanks, julia___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
[Why3-club] (no subject)
Hello, I have the following orgnization of modules: A parameterized by f B uses A C uses A and B and is parameterized by g D uses A, B and C and provides a definition for f and for g The definition for g relies on things defined in A and B. How can I set this up? In D, I cannot just clone C, because I can't make the definition of g without having A and B. If I clone B, then define g, then clone C providing the definitions of both f and g, I get a type mismatch related to a type defined in B. Is there some way that I can parameterize C by B and then pass B in as a parameter when I clone C? thanks, julia ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] lemma visibility
In the following:
val ([]<-) (a: array 'a) (i: int) (v: 'a) : unit writes {a}
requires { [@expl:index in array bounds] 0 <= i < length a }
ensures { a.elts = Map.set (old a).elts i v }
ensures { a = (old a)[i <- v] }
a = (old a)[i <- v] implies a.elts = Map.set (old a).elts i v
So is it necessary to have both of them? In other cases, I have found
that duplicating lemmas can increase the running time, but I don't have an
example where that is a problem here.
julia
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
[Why3-club] typo
why3.1.1.1/src/driver/call_provers.ml: | OutOfMemory -> fprintf fmt "Ouf Of Memory" ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] lemma visibility
On Thu, 24 Jan 2019, Mohamed Iguernlala wrote: > On 24/01/2019 14:37, Julia Lawall wrote: > > Are there some particular arguments that why3 provides to alt-ergo? Now I > > am just running a proof in altgr-ergo, and it has been running for more > > than 5 minutes with no result - it looks like an infinite loop. But from > > within why3, the lemma is accepted in around 30 seconds. > In Why3 IDE settings, change the default editor of Alt-Ergo > from "AltGr-Ergo" to "Default Editor". I missed this step in my > previous message :-/ OK, actually I tried to change it to emacs, but it stayed being altgr-ergo, so I decided to try it out. julia ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] lemma visibility
Are there some particular arguments that why3 provides to alt-ergo? Now I am just running a proof in altgr-ergo, and it has been running for more than 5 minutes with no result - it looks like an infinite loop. But from within why3, the lemma is accepted in around 30 seconds. julia ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] lemma visibility
On Thu, 24 Jan 2019, Mohamed Iguernlala wrote: > > On 24/01/2019 13:50, Julia Lawall wrote: > > > > On Thu, 24 Jan 2019, Mohamed Iguernlala wrote: > > > > > Hello, > > > > > > You can use "alt-ergo -profiling N " to display some > > > profiling information on standard output every "N" > > > seconds (you'll probably need a big screen or to put a smaller > > > font size for the terminal's text). There are 5 different views, > > > and you are probably interested in the last one. To cycle through > > > different views, use "Ctrl+C" (and "Ctrl+AltGr+\" to kill Alt-Ergo). > > > > > > Alternatively, you can activate debug option "-dmatching 1" to > > > display some information about axioms instantiation activity. > > > > > > To finish, you can use "-save-used-context" to save the names of > > > axioms used by Alt-Ergo during a proof (this will generate a > > > .used file), and "-replay-used-context" to filter out the axioms > > > that do not appear in the .used file corresponding to the input > > > file. > > Does this work from why3? I tried adding the -verbose option in the why3 > > configuration file, and I have the impression that why3 wrote over it. I > > don't know whay information why3 feeds to alt-ergo, so I don't know how to > > run alt-ergo directly. > I don't know if one could pass options to Alt-Ergo via > Why3 (without edition the why3.conf file). This is a question for > Why3 team. > > What I usually do is the following: > > - From Why3 IDE, you should be able to go to "Setting" and change > them to edit files that are not proved by Alt-Ergo with, for > instance, Emacs editor. > > - Then, If a VC is not proved by Alt-Ergo, you should be able > to "edit" the file that contains it. You can save this file on > disk and try Alt-Ergo on it with the options I gave previously > from a terminal. > > (I hope this workflow still works with Why3 1.x ...) It looks like it works. Thanks very much! julia ___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] lemma visibility
On Thu, 24 Jan 2019, Mohamed Iguernlala wrote: > > Hello, > > You can use "alt-ergo -profiling N " to display some > profiling information on standard output every "N" > seconds (you'll probably need a big screen or to put a smaller > font size for the terminal's text). There are 5 different views, > and you are probably interested in the last one. To cycle through > different views, use "Ctrl+C" (and "Ctrl+AltGr+\" to kill Alt-Ergo). > > Alternatively, you can activate debug option "-dmatching 1" to > display some information about axioms instantiation activity. > > To finish, you can use "-save-used-context" to save the names of > axioms used by Alt-Ergo during a proof (this will generate a > .used file), and "-replay-used-context" to filter out the axioms > that do not appear in the .used file corresponding to the input > file. Does this work from why3? I tried adding the -verbose option in the why3 configuration file, and I have the impression that why3 wrote over it. I don't know whay information why3 feeds to alt-ergo, so I don't know how to run alt-ergo directly. thanks, julia > > Hope this helps > > Regards, > > - Mohamed. > > > On 24/01/2019 12:15, Julia Lawall wrote: > > > On Tue, 8 Jan 2019, Claude Marché wrote: > > > Hello, > > The easiest way to achieve this is to add, at the > end of the module that needs > a lemma "L" only internally, the declaration > > > Is there any way to find out what lemmas alt-ergo is trying to > use? This > could be helpful to figure out what to exclude. > > thanks, > julia > > ___ > Why3-club mailing list > Why3-club@lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/why3-club > > >___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
Re: [Why3-club] lemma visibility
On Tue, 8 Jan 2019, Claude Marché wrote: Hello, The easiest way to achieve this is to add, at the end of the module that needs a lemma "L" only internally, the declaration Is there any way to find out what lemmas alt-ergo is trying to use? This could be helpful to figure out what to exclude. thanks, julia___ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
