Re: [PG-devel] -quick
Ralf Jung writes: > Ah, that's a good point. I should try that one time. Thanks for the hints! And if you define that procedure (changing to the import all file, doing C-c C-b there) as an emacs macro, then you can start the whole recompilation with just one key stroke. Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] -quick
>> OK, how about creating a emacs macro that does C-c C-b in the >> file that imports everything? You can easily bind this to F9 or >> or any other key - then you get everything with just one >> keystroke! > > That wouldn't be in background though, right? It'd stop interactive > mode in the file I was in. If I understood correctly, you wanted to compile the whole project after finishing some change in one of the files. This is what you get here: You process the require commands in the import-all file, thereby compiling everything in your project that is outdated. Then you wait for the first error in *coq-compile-respone*, when you see one, you can go there to examine the situation. Meanwhile the background compilation will go on as far as possible, possibly producing more errors in *coq-compile-respone*. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] -quick
Ralf Jung writes: >> - you start scripting in file A (for instance to fix a proof) >> while compile-everything is still in progress? Have 2 >> compilations in parallel or abort compile-everything? > > Aborting when the active file is changed sounds fine. I guess that's > what vio2vo also does in background? OK, how about creating a emacs macro that does C-c C-b in the file that imports everything? You can easily bind this to F9 or or any other key - then you get everything with just one keystroke! Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] -quick
Ralf Jung writes: > To follow-up on this: I guess what I am asking for is some command in PG > to say "now please compile everything", that command should be as smart > about compilation as the compilation on import. It should behave just as > if I would step over a file that "Require"s everything in _CoqProject, > including all the magic to be able to jump to where the error was and > everything. OK, lets call this the compile-everything thingy. What do you want when - you start scripting in file A (for instance to fix a proof) while compile-everything is still in progress? Have 2 compilations in parallel or abort compile-everything? - while fixing B you realize you want to change the imports of A? Restart compile-everything automatically after you saved A to disk? - you decide to do a git pull to get the patch that fixed the problem in some file from you colleague? Note that in all these cases you might end up with inconsistent vo files on disk if you just let compile-everything continue. Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] -quick
Ralf Jung writes: > (and from what I see it do), "Keep Going" is about compiling more of the > dependencies of the current file even if other dependencies failed. Right. > What I am looking for is something that compiles more of the current > *project* (i.e., things listed in the _CoqProject), even if everything > that the current file depends on is already compiled. OK, sorry, then I misunderstood. I thought quick-and-vio2vo is what you were looking for. This option at least compiles some files to .vo while you can make some progress in your scripting buffer. What you want - compiling files unrelated to the current scripting buffer - is currently not available. I can only suggest the following workaround: Create a file that imports everything. After a change, do C-c C-b in that file. If quick compilation finds an error, that file is unlocked and you can go there and start fixing it (however, if you start scripting there, the keep going background compilation of the import everything will be aborted). If only vio2vo finds an error, the erroneous file is not unlocked and you need to select an ancestor looking mode that permits you to change the locked region. The assumption behind the current background compilation is that it is explicitly triggered by the user in a state where the file dependencies do not change. It is therefore fine to compute the dependencies only once at the beginning of the compilation. If the user triggers a second compilation after the first one has finished, the dependencies are computed again. If you have a continuously running background compilation process, then this process must be notified when some file changes on the disk because it then has to invalidate this file and everything depending on it. I can imagine that this would be useful for big projects, but it would be a lot of work. (Just imagine you switch git branches while the background compilation is in progress...) > Furthermore (and maybe not entirely related), when using one of the > quick modes, is there a good way to incrementally check that the entire > development compiles before pushing to git? Note that "compiles with Do C-c C-b in a buffer that imports everything with quick-and-vio2vo, this will run vio2vo on all those files that don't have an up-to-date .vo. > * Right before push, I do "make -j4". That will however recompile many > files that PG already created with vio2vo, because the .vo files' > timestamps do not match their dependency order when created by vio2vo. Right, Proof General runs vio2vo usually in the right order (but there are exceptions), but if B depends on A, vio2vo on B might start immediately after starting A and thus finish before A. It would be not too difficult to enforce that in case B depends on A, vio2vo on B only starts when A is finished. The dependency information is there, it is just not used for vio2vo. However, you might always run into the situation where B depends on A and where only the .vo file for A is missing. What do you want in this case? Run vio2vo on B again? > * Right before push, I do "make quick -j4 ; make vio2vo J=4". That will > however always re-check all proofs because vio2vo is not incremental. The make targets that coq_makefile generates are not very sophisticated, but I believe you would need quite a bit of makefile hacking to get the features that you want. Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] -quick
Ralf, your first email got through and thanks for you positive feedback! I have the impression that you have not read any documentation about the quick compilation feature. The CHANGES file is unfortunately not the place to describe a complex feature completely, but it contains a pointer: "See the option `coq-compile-quick' or the subsection "11.3.3 Quick compilation and .vio Files" in the Coq reference manual." May I ask that you follow one of these links? I believe all your questions are answered there and you will also find the documentation about the feature that you are requesting! Best regards, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] -quick
Hi, I opend a PR for comments with a first version of -quick support, see the quick branch on g...@github.com:hendriktews/PG.git. The solution has advantages over using make because the quick options accept an up-to-date .vo file for prerequisites (make insists on producing .vio files for all files). Further, it does not suffer from the consistency issue that make has: Proof General will delete outdated .vo when compiling or relying on a .vio. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] future of coq-seq-compile.el
Pierre Courtieu writes: > I think there are people using it but I suspect it is only by lack of _ > CoqProject file. I don't quite understand, how is a missing _CoqProject file connected with using sequential compilation? > Do we support vio compilation? No, see the other thread. > If we do I guess the parallel and non blocking compilation becomes > much less important. So if you think about removing some part you may I only see a 2-3 fold speed increase with -quick. Compilation times will still be substantial. I really believe we should keep the parallel compilation and discontinue the sequential one. Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] vio compilation options
Hi, Pierre Courtieu writes: > Do we support vio compilation? No. I started to think about it and I would like to hear about your opinion here. I've only done a few experiments so far with -quick, -schedule-vio2vo and -schedule-vio-checking. Therefore, if you made different observations, please tell. For files that don't use Proof using, vio compilation is noticeably slower then vo compilation. Therefore, vio compilation should be optional. It will be quite easy to change background compilation to use -quick, depending on some user option. How do people enable -quick currently? Via putting -quick into _CoqProject? The main question is whether and how Proof General should support vio2vo and vio-checking. Ideally, I would like to have one vio2vo instance, that only uses those cores that are not needed for vio compilation and that dynamically reschedules another module as soon as vio compilation finishes. For instance, consider a project where B depends on A and all of C, D, E and F depend on B. When I compile this on 4 cores, I would like to do vio2vo on 3 cores while I am compiling B. However, when B finishes, I want to be able to tell vio2vo to immediately stop such that I can do coqc -quick for C, D, E and F. As soon as the first of it finishes, vio2vo should commence on 1 core, but now schedule all remaining tasks from A, B and the one that just finished. As far as I understand this is not possible with the current Coq version. Therefore I thought the background compilation should create one vio2vo or vio-checking task for each module when its vio compilation finishes. As long as vio compilation is not finished, these tasks are only started when the number of free cores exceeds a certain threshold. When vio compilation finishes, Proof General should continue with the current scripting buffer and use all the remaining cores for vio2vo or vio-checking. This means errors from vio2vo could show up when Proof General is processing stuff far below the Require that triggered recompilation. Finally, when vio2vo checking finishes there should be a notification such that the user can decide to re-assert the Require lines in order to get proper universe constraint checking. Opinions? Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] future of coq-seq-compile.el
Hi, how long do we want to keep the sequential and blocking compilation implemented in coq-seq-compile.el? Is anybody actually using it? I am asking because I am not really motivated to maintain this code. If you look at the 8.5 changes, many things had to be done twice, in coq-seq-compile and in coq-par-compile. I would therefore propose to delete the sequential compilation soon. There is one feature that is still missing in parallel compilation: compiling outside of emacs with eg. make (see coq-compile-command). Is anybody using this? Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] State button for Coq, needed?
Hi, "Paul A. Steckler" writes: > Well, the current goal should always be shown, unless there's a bug. What if the user deletes the emacs window containing the current goal because he temporarily wants to use that screen space for something else? I used to do this quite often when I needed to look into other files in the middle of the proof. When going back to the proof I would then hit C-c C-p. It should of course be fine if PG just redisplays a cached version of the current goal without talking to Coq when the user hits C-c C-p. The redisplay-goal functionality, however, should IMO be kept together with a button or menu entry. Of course, if you want to put more important stuff in the toolbar, a menu entry and a key binding are sufficient. Bye, Hendrik This email and any attachments thereto may contain private, confidential, and/or privileged material for the sole use of the intended recipient. Any review, copying, or distribution of this email (or any attachments thereto) by others is strictly prohibited. If you are not the intended recipient, please contact the sender immediately and permanently delete the original and any copies of this email and any attachments thereto. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] Proof tree code
Hi, >> 2016-05-12 18:22 GMT+02:00 Paul A. Steckler : >>> The code in generic/proof-tree appears to rely on proof shell modes. >>> >>> Is the `prooftree' tool in common use among Coq users? I used it all the time ;-) For coq, prooftree needs the following: 1) a unique proof goal identifier 2) the full sequent text of additionally generated proof goals 3) information about the instantiation status of existential variables 4) which goals contain which existential variables 5) the updated sequent text once an existential variable got instantiated. The existing implementation does 1 and 3 by modifying the generated output from coq when coq runs under PG. 4 is done with a simple regular expression on the proof goal text. For 2 and 5 I insert additional print commands into the queue of commands. Because you cannot print wrt. an old state, these print commands need to be inserted directly after the command that generates additional subgoals or that instantiate existential variables. > On 2016-05-12 12:33, Pierre Courtieu wrote: >> I don't know. It is a nice peace of code. Maybe we can ask Hendrik to >> port it once you have something working. I agree here. Please go ahead for the moment and ignore proof tree. Unfortunately, I cannot promise that I will be able to update prooftree eventually. It would of course be nice if you keep an eye on the above requirements such that we can plug in prooftree eventually with only little changes. Bye, Hendrik This email and any attachments thereto may contain private, confidential, and/or privileged material for the sole use of the intended recipient. Any review, copying, or distribution of this email (or any attachments thereto) by others is strictly prohibited. If you are not the intended recipient, please contact the sender immediately and permanently delete the original and any copies of this email and any attachments thereto. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] Moving to ELPA!
Hi, I don't have the knowledge to join the discussion about the relative benefits of different emacs package distribution systems. I once made significant contributions on PG and will join whatever the active majority here decides. At some stage I also prepared a PG debian packages - this was significant work, because of some non-standard design decisions in PG. It would certainly be good if we could move to a standard distribution system. Bye, Hendrik This email and any attachments thereto may contain private, confidential, and/or privileged material for the sole use of the intended recipient. Any review, copying, or distribution of this email (or any attachments thereto) by others is strictly prohibited. If you are not the intended recipient, please contact the sender immediately and permanently delete the original and any copies of this email and any attachments thereto. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] Migrating Proof-General to Git
Hi, thanks a lot for taking the initiative! Clément Pit--Claudel writes: > changes (we would need to migrate once and for all). I haven't contributed for a while and I am unsure if I will find time in the future, therefore I don't know if I am eligible to take part in the discussion. However, if I were, I would suggest to give everybody a last chance to commit to cvs until, say, May 11 and move then everything to git and take the cvs repo offline. In the unlikely case that David is not participating in this discussion (and that we therefore cannot take CVS offline), I suggest that we try to reach an agreement among the contributors of the last 2 years. And then somebody with write permission makes a last CVS commit to delete all the files there, except for a README pointing to the git repo. > would be nice to map CVS usernames to proper names and emails; the Some email addresses are in Makefile.devel in the DEVELOPERS variable. weber is Tjark Weber , I believe. > It would be great to get feedback on the history as recorded in I would suggest to move to git even if the history is completely broken, therefore I won't check it. Bye, Hendrik This email and any attachments thereto may contain private, confidential, and/or privileged material for the sole use of the intended recipient. Any review, copying, or distribution of this email (or any attachments thereto) by others is strictly prohibited. If you are not the intended recipient, please contact the sender immediately and permanently delete the original and any copies of this email and any attachments thereto. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] Ticket #467: vernacular command no longer displays timings
Hi, I fixed #467 now such that the menu entries (including "Time commands") do work. If you type "Time" on your own, you have to use customize yourself, see ticket #467. I hope this is sufficient for closing the bug. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] defpacustom project-filename
Hendrik Tews writes: I don't think using defpacustom for project-filename is a good idea. This way it appears in the menu and when you enable it, coq-project-filename is set to t. I fixed the t setting with fixing the :type of coq-project-filename. Now it can stay in the menu (although I would not put it into a menu). Can defpacustom handle string options, such that the user is queried for a string, when he enables the menu entry? Yes, if you use :type 'string Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] defpacustom project-filename
Hi Pierre, I don't think using defpacustom for project-filename is a good idea. This way it appears in the menu and when you enable it, coq-project-filename is set to t. Can defpacustom handle string options, such that the user is queried for a string, when he enables the menu entry? Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] Move to Github
Pierre Courtieu writes: > - similarly for the coq/faq: wouldn't it be better to integrate > this in the user manual and have then a "coq faq" link on the > web page? > I don't understand this one. Do you mean in the coq user manual? No, my suggestion was to integrate coq/faq as section into the Proof General user manual. We could then directly link this FAQ from the Proof General website. It should also be possible to have the FAQ alone somewhere in the Proof General distribution, at least in html format. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] Move to Github
Pierre Courtieu writes: Date: Fri, 5 Jul 2013 16:04:43 +0200 Subject: Re: [PG-devel] Move to Github I don't mind changing the name of coq.el into pg-coq.el. Will it break something? You mean in the Proof General distribution, not in the Coq distribution, right? > Hendrik Tews writes: > > Both Proof General and Coq install coq.el (and some other files > with identical name), which cases trouble, because the feature > name space of Emacs is flat. > > Possible solutions (with decreasing preference for me) are: > > - The defending files are deleted in Coq or are not installed by > the default make install. > > - The files are renamed in the Coq distribution. You don't like these two options? When it comes to renaming, keep in mind, that coq-db.el and coq-syntax.el must be renamed too. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] Move to Github
Hendrik Tews writes: Regarding the 4.3 release: ... I have another issue that I would like to see resolved in 4.3: The feature name conflict with Coq, see http://lists.inf.ed.ac.uk/pipermail/proofgeneral-devel/2012/000241.html Both Proof General and Coq install coq.el (and some other files with identical name), which cases trouble, because the feature name space of Emacs is flat. Possible solutions (with decreasing preference for me) are: - The defending files are deleted in Coq or are not installed by the default make install. - The files are renamed in the Coq distribution. - The files are renamed in Proof General. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] Move to Github
Hi, I am happy to see Pierre you back on this list and back committing to Proof General. Regarding the 4.3 release: There are some indentation bugs in the tracker. Pierre, could you spend some time for them? I intend to fix #467 and have a look at #460. Does anybody else use the new parallel compilation feature? For me it works perfectly and I would make it default (and delete serial compilation before the 4.4 release). I have some comments about recent commits: - the project file feature should IMHO be mentioned in the user manual - similarly for the coq/faq: wouldn't it be better to integrate this in the user manual and have then a "coq faq" link on the web page? - similarly for ML4PG: it certainly deserves a separate subsection in the user manual About Hol Light support: I posted a hint about it on hol-info but got no reaction. It seems that no Hol Light user is interested in having Proof General support. I therefore expect it to stay forever in the current unfinished state. 2013/7/4 David Aspinall > Some time ago I mooted moving from our clunky University-hosted CVS+trac > to Github. I think it would allow people to more easily make modifications A better tracker would certainly be nice. Otherwise I don't care much. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] non-fatal warnings for make compile
David Aspinall writes: This fix was helpful but unfortunately means that developers are more likely to introduce bugs unless they run make clean; make check I agree. But even before the change we had now and then compilation errors in the repository. >From my point of view the compilation errors are not an issue. They are rare and if one is reported on this list it is fixed immediately. I have nevertheless two suggestions: - we could have a nightly compilation and spam pg-devel when errors occur - we could add -include LocalMakefile to Makefile and have a LocalMakefile that makes ``check'' the default compilation target and omit LocalMakefile from the distribution. If you think these compilation errors are an issue, I volunteer to implement one or both suggestions. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] ProofGeneral symlink?
Hi, the Proof General releases do always contain a symlink ProofGeneral --> ProofGeneral-X.Y, which, ahem, is a bit in the way when creating debian packages. What is the reason for having this symlink in the tar archive? Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] non-fatal warnings for make compile
Hi, I spend some time to find a fix for tickets #458. The problem is that special-display-regexps is obsolete in 24.3, while its replacement, display-buffer-alist was only introduced in 24.1 and not fully functional before 24.3. Writing compatible code for emacs 23 and 24 without obsolete warning therefore requires explicit version checks. I therefore suggest that we change to display-buffer-alist when we drop support for Emacs 23. To fix #458, warnings should be non-fatal when users compile Proof General for their local emacs. I just committed the necessary changes in the Makefile. For developers, there is now the new target 'check' that retains the old behavior, i.e., stopping compilation on every byte-compilation warning. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] Re: Ticket #467: vernacular command no longer displays timings
I believe all Proof General versions (including the latest trunk) show the timing in the *goals* buffer when you use them with Coq 8.3pl4 or earlier. If you have more than one subgoal the timing is shown only when coq-hide-additional-subgoals is off. Then the *goals* buffer looks like ## 2 subgoals True subgoal 2 is: True Finished transaction in 0. secs (0.u,0.s) ## When coq-hide-additional-subgoals is on, only the text before "subgoal 2" is copied to the *goals* buffer, and then the timing is obviously only displayed when you have one subgoal. Coq 8.4 displays the dependent evar line under Proof General. Therefore, with Coq 8.4, Proof General only copies the material before the dependent evar line to the *goals* buffer, and the timing is lost. Jason, can you try setting coq-end-goals-regexp-show-subgoals to nil? (M-x customize-variable coq-end-goals-regexp-show-subgoals, Value Menu -> nil; State -> Save for furture sessions; then restart Proof General) Then the goals buffer looks like ## 2 subgoals, subgoal 1 (ID 3) True subgoal 2 (ID 4) is: True (dependent evars:) Finished transaction in 0. secs (0.u,0.s) ## Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] Re: Ticket #467: vernacular command no longer displays timings
I remember how PG used to behave, but I do not recall which version it was. I started using Coq at version 8.3pl2, or there-abouts, so I can try to 8.3pl3 was released in December 2011, so it was probably Proof General 4-2pre111207 or earlier. Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] Ticket #467: vernacular command no longer displays timings
Hi, somebody wrote in the bug tracker: Btw, is it possible to get me added to the cc list for this bug? (jasongross9+PG AT gmail DOT com) I don't know how. I therefore suggest to continue the discussion here at ProofGeneral-devel. I have some suspicions, what caused the timings to disappear. However, before I dig into the issue, I would like to see how Proof General used to behave. I therefore ask for the third time: Do you remember a PG version that had the behavior you expect? Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] urgent message hide errors?
Hi, currently, proof-shell-filter looks for urgent messages before looking for errors. Moreover, if an urgent message is found, it searches for errors only in the output that follows the urgent message. This behavior is responsible for issue #463, where Coq outputs an error before a warning and the error is lost because the warning is recognized as urgent message. What is the problem here? Coq outputting the warning _after_ the error? Or matching the warning as urgent message? Or searching for errors only behind urgent messages? Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] status of support for Proof General
Hi, do we have a support problem for Proof General? I am asking because we have issues in the tracker that are quite old and nobody seems to care... for instance #460 or #463 to which I gave partial answers today. Do we have a lack of developers or do the developers not like to comment on issues in the tracker? Whatever the reason is, if we cannot improve the situation, I would suggest to put an appropriate note on the tracker, saying issue handling may take some time. Letting users find this out themselves is the worst we can do. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] prooftree users?
Hi, is anybody actually using prooftree with the cvs head of Proof General? For supporting bullets, braces and "Grab Existential Variables" I would like to make several commits that break compatibility with the current release of prooftree. A suitable prooftree release will follow within a month. Please drop me a line, if you would be disturbed if compatibility breaks between cvs head of Proof General and prooftree version 0.10. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] make clean deletes backup files
Hi, currently editor backup files are deleted by make clean. I find this unfortunate, because I have to use make clean quite often to remove elc files. If nobody disagrees, I move the removal of *~ to the distclean target. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] overlapping calls to proof-shell-filter
I wrote: here is a patch that solves the problem for me. Any comments? I committed now. I deleted the argument of proof-shell-filter, to make sure, nobody will use it. Reasons are described in the doc comments. Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] overlapping calls to proof-shell-filter
David Aspinall writes: At a quick glance this looks like a reasonable way to fix without messing with the current filter code. Luckily, I don't think the str argument is used. I'm not completely clear on the error case, is the idea just to give up if we hit an error in some call? If proof-shell-filter signals an error, the error is just propagated, only the active flag is reset to enable later calls again. Or do you mean the case where a parallel, overlapping call is detected? In this case the -was-blocked flag is set and the already running instance of the wrapper stays for one more iteration in the while loop, thus calling proof-shell-filter after the previous call finished. This effectively delays Coq until prooftree catches up. This is just what you want, I believe. Under normal circumstances prooftree is much faster than Coq. Because of the experience with PVS, where the proof tree visualizer was often the bottleneck, I made some special optimizations: - tree layout is linear in the tree depth; for PVS it is apparently worse than linear in the number of nodes - tree display is delayed until no display commands are available on input; nevertheless, when asserting large regions, you see the tree growing node by node, indicating that prooftree is faster than Coq Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] overlapping calls to proof-shell-filter
Stefan Monnier writes: I think this deserves an Emacs bug report. see http://debbugs.gnu.org/cgi/bugreport.cgi?bug=13400 There are definitely some documentation problems. process-send-string is not mentioned as function that might trigger a filter call. I think many packages are vulnerable to this problem, although they usually don't suffer from it. The most common case where they do suffer from it is when you try to Edebug the process filter. I believe it would be good to have a process-specific flag that inhibits overlapping parallel calls to the same process filter. Emacs could accept output but buffer it until the previous filter terminates. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] overlapping calls to proof-shell-filter
Hi, here is a patch that solves the problem for me. Any comments? Bye, Hendrik Index: generic/proof-shell.el === RCS file: /disk/cvs/proofgen/ProofGeneral/generic/proof-shell.el,v retrieving revision 12.15 diff -u -r12.15 proof-shell.el --- generic/proof-shell.el 3 Jan 2013 09:33:38 - 12.15 +++ generic/proof-shell.el 9 Jan 2013 20:49:38 - @@ -243,6 +243,13 @@ :type 'boolean :group 'proof-shell) +(defvar proof-shell-filter-active nil + "t when `proof-shell-filter' is running.") + +(defvar proof-shell-filter-was-blocked nil + "t when a recursive call of `proof-shell-filter' was blocked. +In this case `proof-shell-filter' must be called again after it finished.") + (defun proof-shell-set-text-representation () "Adjust representation for current buffer, to match `proof-shell-unicode'." (unless proof-shell-unicode @@ -277,6 +284,7 @@ (interactive) (unless (proof-shell-live-buffer) +(setq proof-shell-filter-active nil) (setq proof-included-files-list nil) ; clear some state (let ((name (buffer-file-name (current-buffer @@ -1288,12 +1296,37 @@ ;; The proof shell process filter ;; +(defun proof-shell-filter-wrapper (str) + "Wrapper for `proof-shell-filter', protecting against recursive calls. +In Emacs a process filter function can be called while the same +filter is currently running for the same process, for instance, +when the filter bocks on I/O. This wrapper protects the main +entry point, `proof-shell-filter' against such recursive calls." + (if proof-shell-filter-active + (progn + (setq proof-shell-filter-was-blocked t)) +(let ((call-proof-shell-filter t)) + (while call-proof-shell-filter + (setq proof-shell-filter-active t + proof-shell-filter-was-blocked nil) + (condition-case err + (progn + (proof-shell-filter str) + (setq proof-shell-filter-active nil)) + ((error quit) + (setq proof-shell-filter-active nil +proof-shell-filter-was-blocked nil) + (signal (car err) (cdr err + (setq call-proof-shell-filter proof-shell-filter-was-blocked) + + (defun proof-shell-filter (str) "Master filter for the proof assistant shell-process. A function for `scomint-output-filter-functions'. -Deal with output STR and issue new input from the queue. This is -an important internal function. +Deal with output STR and issue new input from the queue. This is +an important internal function. Actually, STR is not used, the +output is taken from `proof-shell-buffer'. Handle urgent messages first. As many as possible are processed, using the function `proof-shell-process-urgent-messages'. @@ -1806,7 +1839,7 @@ (setq scomint-output-filter-functions (append (if proof-shell-strip-crs-from-output 'scomint-strip-ctrl-m) -(list 'proof-shell-filter))) +(list 'proof-shell-filter-wrapper))) (setq proof-marker ; follows prompt (make-marker) ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] overlapping calls to proof-shell-filter
David Aspinall writes: Quick thoughts: this sounds like a pretty fundamental problem and surprising if we hadn't come across it before. Do you definitely see this in the ordinary running code, not just when using the debugger? I don't use the debugger, I let certain functions insert start and end messages into a dedicated buffer. There, I see proof-shell-filter starting before the previous instance finished. In principle, the problem can also appear without prooftree. Proof General will block when sending a sufficiently large command. If the proof assistant generates output before completely reading the command, proof-shell-filter might get called a second time. The command has to be really large, because default pipe size is 64K since Linux 2.6.11. If we need to fix it, I suppose we could try to exit the PG filter function early using our own flag to detect nested calls. Yes, using a second flag to remember aborted nested calls, such that proof-shell-filter can call itself recursively if a nested call was aborted. Am I right, that proof-shell-filter does not use its ``str'' argument? Because the problem does only appear when starting prooftree with cold disk caches (which takes more than 1 sec on my laptops), a partial fix would be to block Proof General until prooftree is ready. (Or could you do that just for proof tree?) I don't understand. The problem appears, because it takes more than one second until prooftree is ready and Coq + Proof General generate more than 64K display commands in that time. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] overlapping calls to proof-shell-filter
Hi, sometimes I see prooftree crashes with a cold disk cache (eg after reboot or after "sync; sudo sh -c 'echo 3 > /proc/sys/vm/drop_caches'"). What apparently happens is that at some stage process-send-string blocks because the pipe to prooftree is full. This happens inside proof-shell-filter, because the prooftree display commands are created and sent when output arrives from Coq. When I/O blocks, Emacs automatically accepts output processes. So it calls proof-shell-filter again before the previous call finished. Finally some garbage or truncated messages is written to the pipe and prooftree crashes. It should definitely not happen that proof-shell-filter is called while another instance is still running. Does anybody know a way to ensure this? Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] first version of parallel background compilation for Coq
David Aspinall writes: > I just committed the first version of parallel background > compilation for Coq. It sounds very useful! Are there some Coq users who are testing for you? Not that I know. H. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] Coq menu entries
Pierre Courtieu writes: Since double hit terminator is more or less an alternative to electric terminator, I have put them side by side in coq menu, to see if people OK, I thought "double hit" would modify the behavior of electric terminator. like it, but I did not make it geenric yet. Maybe one entry for both settings with a 3-value setting would be better? >From the user perspective this would certainly be better. But if the implementation is not trivial, we can also keep the two settings. Actually tooltips are so useless and annoying (flickering) in coq mode that I wanted the disabling option to be as immediate as possible. It would probably be better to disable it by default and put the option in the settings menu. Fine with me. By the way is there a "emacs gui recommendations somewhere?" I don't know any. BTW, I just wanted to ask. I don't really have a strong opinion where those items should go. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] first version of parallel background compilation for Coq
Hi, I just committed the first version of parallel background compilation for Coq. It is disabled by default in favor of the old synchronous compilation method. Parallel compilation required one fundamental and one minor change in the general proof shell treatment, see below. If you want to try parallel compilation: - Check menu entry Coq -> Settings -> Compile Parallel In Background - Configure coq-max-background-compilation-jobs to something greater than 1 to actually experience parallel compilation - C-c C-c kills all compilation jobs - you may try M-: (coq-par-emergency-cleanup) in emergencies Information about the implementation is in coq/coq-par-compile.el. THE FUNDAMENTAL PROOF SHELL CHANGE: The Require command and the items that follow it must not be added to proof-action-list before the compilation finishes. Therefore, from now on, proof-action-list does not necessarily contain all items from the queue region. Require commands and items that follow them are stored in some property list of some uninterned symbols that I manage in the background compilation process. If compilation finishes these items are put back into proof-action-list. Typically, proof-action-list gets empty before this happens. Nevertheless, the proof shell lock must not be released and the queue span must stay active in such cases. I therefore added the variable proof-second-action-list-active, which gets set to t if some queue items are stored elsewhere. This variable then modifies the behavior of the proof shell functions at appropriate places. THE MINOR PROOF SHELL CHANGE: I added a new hook proof-shell-signal-interrupt-hook, that is called in proof-interrupt-process and proof-shell-kill-function. With this hook I can kill all background compilation jobs as early as possible. FUTURE PLANS: There are a number of TODO's in coq/coq-par-compile.el. Synchronous and asynchronous compilation are in separate files with the common functionality in coq/coq-compile-common.el. My plan is to leave both coexist for a while. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] Coq menu entries
Hi, I just noticed that there are a view boolean settings in the Coq menu which are not done via defpacustom and which are therefore not in the Settings submenu. Is there a reason, why "Toggle tooltips", "Electric Terminator" and "Double Hit Electric Terminator" are not in the Settings submenu? It might be good to have "Electric Terminator" in the main Coq menu but the other two could go into Settings menu IMHO. [I understand that "Toggle 3 Windows Mode" cannot be inside Settings, as defpacustom cannot handle radio button style submenus.] Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] proof-shell-pre-interrupt-hook ?
Hi, I just came across proof-shell-pre-interrupt-hook. I can't find any location where this hook is run. Am I missing something? Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] pg-finish-tracing-display ?
Hi, I am missing the documentation comment for pg-finish-tracing-display. What is it used for? (As you may have noticed I am implementing parallel background compilation for Coq. It is working already if there is no error in the compilation itself. I am now trying to keep the queue region alive when proof-action-list get empty while a whole bunch of items are waiting at a different place until the background compilation finishes. During this I came across the call to pg-finish-tracing-display close to the end of proof-shell-exec-loop...) Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] Reboot: Release of PG 4.2
Hi, David, is there anything left to do before you can do "make release"? Maybe I or somebody else could help? (My Coq project is now so large that the sequential blocking compilation really sucks. I would really like to start now with rewriting the compilation with parallel background jobs.) Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] Reboot: Release of PG 4.2
Hi, there are no issues left with milestone 4.2. Nobody has committed changes for one week. David, I believe, you can release now. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] Tracker questions
Hi, how can I add my email address (which is different from coquser) to an existing bug report? Having to click all issues, only for checking if somebody has answered, is really not acceptable. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] Reboot: Release of PG 4.2
Hendrik Tews writes: - support for braces and bullets This requires more work than I thought. I have to postpone this to October. Given that only few people use braces/bullets (because they are new) and even fewer use Prooftree, it doesn't make sense to delay the release of Proof General because of this issue. The problem is that with braces and bullets Coq exhibits a state where the old current goal has been finished but it has not yet switched to the next goal. Without braces and bullets you never see such a state and therefore all prooftree code assumes that such a state is not visible. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] Reboot: Release of PG 4.2
In addition to Davids list we should fix the conflict between proof-electric-terminator and coq-colon-self-insert, that I reported yesterday on this list. issue #449 - Proof appears as command in the proof tree issue #450 - support for braces and bullets issue #451 H. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] Reboot: Release of PG 4.2
David Aspinall writes: I'd like to push the button on this soon, so I think we should stop adding new features/hacks to the CVS head for a while... How about Hol light? Would you release 4.2 with the current partial hol light support enabled? Or would you put hol-light into comments in generic/proof-site.el? I would suggest that we agree on some schedule. For instance: - we stop adding new features now - permit 2 weeks for further bug fixes - have another prerelease on 18 September - release 4.2 on 25 September In addition to Davids list we should fix the conflict between proof-electric-terminator and coq-colon-self-insert, that I reported yesterday on this list. I would like to fix some proof-tree problems before the release: - Proof appears as command in the proof tree - support for braces and bullets Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] Howto disable the double hit terminator for Coq?
Pierre Courtieu writes: (define-key coq-mode-map (kbd ".") 'self-insert-command) (define-key coq-mode-map (kbd ";") 'self-insert-command) No, I want the default Proof General electric terminator thing, where one "." asserts up to the last phrase. Sorry for being not clear enough about this. My curiosity: did it jump at you by accident? Hitting ".." quickly is not so common is it? I _do_ look at diffs, when other people commit to the Proof General cvs ;-). But the change in behavior is obvious: Before a single "." asserted the last phrase, now it does nothing. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] Howto disable the double hit terminator for Coq?
Hi, coming back from holiday, I got the new double hit terminator feature on checkout. Being not open-minded about new things, I wanted to disable it. But how to do that? Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] speed up Coq Proof General by processing complete proofs
The main problem with your solution is that for the moment pg coq needs to see the informations that were present in the prompt before a command was issued to know how to back just before this command. Therefore if we want to be able to backtrack inside the chunks we need to read all prompts and link each of them to the corresponding command. If we hide the prompts then backtracking inside chunks will be impossible. Well, there is no backtracking to a position inside a proof once you finished the proof. So if a chunk is a whole proof, you loose nothing. Otherwise, I would say, if you switch on the speedup-option for processing in chunks, then you loose the ability to backtrack inside the chunks. If you want to go there, you have to backtrack the whole chunk and then start asserting again in smaller steps. Similarly to what you have to do now when you want to go into the middle of a proof after finishing it. Dealing with errors, as David said, will be a mess. Indeed. My plan would be the following: Before processing a chunk I remember the chunk start position somewhere. If there is an error inside the chunk I backtrack to the beginning of the chunk. I am pretty sure that this can work out without creating a mess. On the problem of speeding up pgcoq Hendrik please consider waiting for the next big change in Coq kernel: asynchronism. Or at least proof lazy evaluation. I have seen a prototype of that (by Enrico Tassi) and it surely will make pg and any other interface much faster from the user perspective I believe that these changes will speed up the compilation of whole files, i.e. coqc. But I doubt they will speed up my 2000 line files. If Proof General is too slow to feed coqtop such that the latter saturates 1 of my 4 cores, how could I gain from more parallelism? On the contrary, processing bigger chunks, especially whole proofs, would certainly increase the chance to profit from these improvements. These results are indeed surprising. As I don't see why sending commands separately would speed down Coq, I guess pg is slow at interpreting prompts (see below). Maybe I should have a look at my code on this. It might be the case that I see this big speedup, because my tactics are too low level. For the measurement I disabled the parser cache and inserted the following hack into coq-script-parse-cmdend-forward at the end, where it returns 'cmd: (progn (if (save-excursion (forward-line 0) (looking-at " *Proof")) (progn (re-search-forward "Qed\\." limit t) (end-of-line))) 'cmd ) Further I inserted (message "QUEUE EMPTY at %s" (float-time)) inside proof-shell-filter-manage-output in the if where proof-shell-exec-loop returns with true. I processed the buffer with M-x eval-expression (progn (message "START %s" (float-time)) (proof-process-buffer)) The above measurement hack works only if - you first delete all Qed's inside comments - make sure each Qed / Defined is the last command on its line - add ``(* Qed. *)'' after each Defined If you send me a file, which you are interested in, I can easily do the measurements. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] speed up Coq Proof General by processing complete proofs
Hi, I was recently a bit annoyed by the time Proof General needs to process my Coq files. A simple measurement showed that Proof General has only one third or less of the speed of coqc. I therefore tested the following idea: When Proof General processes larger chunks, it can send proof scripts as a whole instead of sending single tactics. The results were rather surprising: sample1 proof file file (200 lines) (2050 lines) (3400 lines) coqc - 7.1 sec 6.5 sec PG standard 4.2 sec 21 sec 29 sec optimized PG processing whole proofs 0.05sec5.4 sec 5.4 sec The comparison with coqc is a bit unfair here, because in Proof General I measured proof-process-buffer after asserting a first comment in the file, thus, in the Proof General measurements, starting coqtop was not included. The optimized measurement is not completely accurate, because Proof General got confused by seeing too much coq prompts and therefore sent the material earlier than it should. There are of course a number of problems to solve before Proof General is really able to process proofs, sections or modules as one chunk. But with the prospective speed improvement I would like to explore this idea further. I believe the first problem to solve is that of multiple prompts: When Proof General sends several statements together, coqtop answers with several prompts instead of one prompt. AFAICT there is no command to change or disable the prompt in coqtop. Pierre, do you think there are changes to get a Set/Unset Prompt command included, which enables/disables prompt printing? Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] ProofGeneral 4.1 byte-compilation fails if image-load-path is not defined
Ulrich Mueller writes: Byte-compilation of ProofGeneral fails if Emacs was configured with option --without-x, because image-load-path is not defined in this case: Which emacs version are you using? Could anybody explain me, why I cannot reproduce the problem? I tried with emacs23-nox from Debian, which has image.el not loaded and where (boundp 'image-load-path) gives nil. Nevertheless, emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/tmp/ProofGeneral-4.1/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego pgshell phox generic lib))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))) (setq byte-compile-error-on-warn t))' -f batch-byte-compile generic/proof-toolbar.el runs without error on proof-toolbar.el version 11.1 Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] Feature name conflict with Coq
Pierre Courtieu writes:
2012/6/6 Stefan Monnier :
>
> Another take on it is that the two teams should join their efforts.
I already asked why this old file is still in coq distribution. The
answer was: some people just want to open coq file for syntax
highlighting. For them starting pg is too slow (+ splash screen).
Is it just about the splash screen? It can be disabled easily
with proof-splash-enable. BTW, who wants to see the splash screen
on any Proof General start anyway? Don't get me wrong: I like the
splash screen and I am happy about its existence. Nevertheless,
the first thing that I configured for Proof General was
proof-splash-enable.
How about disabling the splash screen by default and enabling it
explicitly for those shell scripts that are called by menu items?
I did some measurements about startup times. Proof General needs
about 1.3 seconds until it is idling when starting form the shell
("emacs test.v"). The coq-mode from Coq needs about 0.9 seconds,
this _is_ noticeably faster.
Loading the generic part (proof-site.el) only takes 0.004 s, but
loading the prover specific part ((load-library ,elisp-file) in
the coq-mode stub takes 0.3 seconds. Then after the coq-mode
stubs finished, that is after the real coq-mode has been
finished, it takes another 0.3 seconds until emacs starts idling.
It is not clear to me, what it is doing in these last 0.3
seconds.
Bye,
Hendrik
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] Feature name conflict with Coq
Stefan Monnier writes: > Or by those who designed Emacs with a flat namespace for features and > library files... Ahem! Please don't put .../ProofGeneral/coq in the load-path, and then simply do (require 'coq/coq). Where is this documented? I would even say that the Elisp manual (sect 15.7) If the feature is not present, then `require' loads FILENAME with `load'. If FILENAME is not supplied, then the name of the symbol FEATURE is used as the base file name to load. implies that require 'coq/coq should load "coq\/coq.el" instead of "coq.el" in subdir coq. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] Feature name conflict with Coq
Hendrik Tews writes: This is going to be a problem for those that want to use a manually installed Coq 8.4 with a Debian installation of Proof General. In Debian, manually installed stuff has precedence, so when proof-site requires 'coq, Emacs will actually load coq.el from the Coq installation. I only found out yesterday, that the load-path management is severely broken in Debian (I would say), see bug #676424. So I am not going to change the load-path management of Proof General now and manual installs of Coq 8.4 are going to work as usual. Nevertheless, we should try to solve the feature name conflicts. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] Feature name conflict with Coq
Hi, both Proof General and Coq install and provide Emacs files and features for 'coq, 'coq-db and 'coq-syntax (the latter two are actually old versions from Proof General). This is going to be a problem for those that want to use a manually installed Coq 8.4 with a Debian installation of Proof General. In Debian, manually installed stuff has precedence, so when proof-site requires 'coq, Emacs will actually load coq.el from the Coq installation. Note that the current Proof General package (version 4.2~pre120411-2) does suffer, because it violates the Debian policy, see http://bugs.debian.org/cgi-bin/bugreport.cgi?bug=670339 . But this will change soon. Further, whole distributions (like Debian) where Proof General and Coq are installed from packages are likely to ignore the problem, because in ascii order "coq" appears before "proofgeneral", therefore Proof General appears before Coq in the load path. In such a installation only those who load coq-inferior will have a problem, because the (require 'coq) inside coq-inferior.el will load coq.el from Proof General. One could of course argue that the problem should be solved by those who mix a packaged Proof General with a manual install of Coq. Or by those who designed Emacs with a flat namespace for features and library files... However, I believe it would be better if Coq and Proof General use different feature names. Because I have the impression, the Emacs mode distributed with Coq is rarely used, I would suggest that Coq changes the names of 'coq, 'coq-db and 'coq-syntax. Or supresses the installation of these files with the default "make install". If this is not going to work out, I would suggest that Proof General changes file names (hoping that not more files are copied from Proof General to Coq). Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] bar cursor in *goals* and *response*
I wrote: > I believe setting cursor-in-non-selected-windows to nil (and > leaving cursor-type unchanged) in *goals* and *response* would be > more appropriate. I've committed this change yesterday. David, quite some changes accumulated since Release-4-2pre120430. Do you think you can schedule another prerelease this or next week? Stefan Monnier writes: You might like to check the VCS to see what is the history of that code, but I suspect that those cursor-type settings came before Well, if the :version tag is right, cursor-in-non-selected-windows exists since version 21.1 from 2001. The cursor-type change was first committed 2008. BTW, can you explain, way cursor-in-non-selected-windows is customizable while cursor-type is not? Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] bar cursor in *goals* and *response*
Hi, what is the rationale for overriding the user preference for cursor-type in *goals* and *response* ? I would expect that people who really want different cursors within one frame, set the cursor appearance in their personal configuration, eg via proof-shell-init-hook. I believe setting cursor-in-non-selected-windows to nil (and leaving cursor-type unchanged) in *goals* and *response* would be more appropriate. This way there would be no cursor as long as *goals* and *response* are not selected. But if the user switches to one of these buffers in order to copy some text, then he immediately gets his preferred cursor. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] let proof-retract-buffer only move point when called interactively
Hi, I still don't like the fact that Proof General moves point to the beginning of the buffer, when the buffer is automatically retracted, because I change the current scripting buffer. See also the old discussion at http://lists.inf.ed.ac.uk/pipermail/proofgeneral-devel/2011/000139.html I have now committed a simple fix: proof-retract-buffer only moves point when called interactively. To distinguish interactive calls I use the trick described in section "21.4 Distinguish Interactive Calls" in the Elisp manual. I am prepared to retract this change and search for a different solution, if people don't like this change. Note however, that there are also other cases where point does not follow the locked region (when proof-follow-mode = 'locked). For instance when locking or unlocking ancestors, point does not move. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] kill windows showing response and goals buffers on proof-shell-exit
Hi, my last commit fixes the problem that Proof General was screwing up the displayed buffers when switching the active scripting buffer with Coq. Let me explain: I use the 2-windows mode of Proof General, usually one frame showing the current scripting buffer and either *goals* or *response*. Let's say a.v is the active scripting buffer, but I want to do something in b.v. So I switch buffer to b.v and start scripting there. Before my last commit, the result was that Proof General was finally showing an empty *response* buffer. This was very annoying. Proof General was doing the following: - retract a.v completely, thereby changing the window configuration to show b.v and *response* - kill coqtop, thereby killing *response* and as a result the window configuration changes to show b.v and a.v. For some strange reason b.v is the least recently selected window now. - start coq for the new scripting buffer and start sending the initialization commands - after the first init command, Proof General decides it should show *response*, and finally calls (proof-get-window-for-buffer "*response*"). There, the first if selects the else branch and the next if calls (display-buffer "*response*"). Because b.v is least recently selected, the window configuration changes to show *response* and a.v. - For some reason a.v disappeared during processing other init commands. I thought about a heuristic that avoids to replace the current scripting buffer in proof-get-window-for-buffer. However, I finally decided to kill the *response* window before killing the *response* buffer. Please check that this change does not have some unwanted side effects. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] obsolete coq/coqtags
Hi, if nobody disagrees I am going to remove coq/coqtags because the Coq distribution contains its own coqtags. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] Proof-tree merge
Hi, I just merged the ProofTreeBranch into the main trunk. Hopefully I didn't break anything. If you want to try it you have to install Coq 8.4 beta (from http://coq.inria.fr/coq-84) or a recent development version of Coq and Prooftree (from http://askra.de/software/prooftree/). The Prooftree website provides binary packages for Debian Squeeze i386 and amd64. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] hiding additional subgoals
Hi, for Coq I implemented a setting that dynamically changes proof-shell-end-goals-regexp and thereby either hides or shows additional subgoals (see my commit this morning). If other proof assistants do also want this, we could generalize the change and move the setting into the Proof General menu. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] use vcursor in locked region
Hi, if you would like the virtual cursor of the vcursor package being visible also inside the locked region you can put the following as fix into your .emacs: (defadvice vcursor-move (after vcursor-overlay-set-priority activate) "Set a high priority for the vcursor overlay to make the vcursor visible in looked regions of Proof General." (and vcursor-overlay (overlay-put vcursor-overlay 'priority 1000))) Bye, Hendrik PS. See also http://debbugs.gnu.org/cgi/bugreport.cgi?bug=9663 ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] PG 4.1 released!
David Aspinall writes: I plan to announce a little bit more widely later this week, please let me know asap if there are any hiccups. I haven't seen an announcement of Proof General 4.1 on coq-club. If nobody else wants to do this I'll post something this afternoon. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] [PATCH] coq: Add option to ignore warning from coqdep in auto-compilation mode.
Tom Prince writes: >Some developments don't fully qualify their imports, and so coqdep gives >warning about ambiguous imports. Allow these developments to use >auto-compilation mode anyway. Sorry about the delay, I somehow forgot about the issue. It's now fixed in the repository. The regular expression for detecting coqdep errors can be customized now and the default value is chosen more carefully to only match those cases where a library cannot be found. If you really want to ignore all warnings you can change coq-coqdep-error-regexp such that if will never match anything. But be prepared to hit the assertion in coq-map-module-id-to-obj-file, when you ignore the "library X is required and has not been found" warning for a require command. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] [PATCH] coq: Allow specifying recursive entries in coq-load-path.
That sounds OK, except there shouldn't be quotes in there: Sure, I've committed the change now, please test. Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] A few major bugs about exiting ProofGeneral with current CVS version
> If nobody objects, I'll adopt solution 1 (see #421 for solution 2): Fixed now in cvs, please test. Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] [PATCH] coq: Allow specifying recursive entries in coq-load-path.
Tom Prince writes:
>> Does anybody use -I ... -as ... ?? Does anybody has an opinion
>> about whether Coq Proof General should support -I ... -as ... ??
If somebody needs it later, we can
always add it.
Of course, but I don't want to make an incompatible change, when
we add -I ... -as ... later.
Given that nobody really needs -I ... -as ..., I suggest to have
3 kinds of elements in coq-load-path:
- simple strings for option -I
- lists of the form ('rec "dir" "path") for -R dir -as path,
where path can be omitted for -R dir
- lists of the form ('nonrec "dir" "path") for -I dir -as path,
Finally, for convenience, elements of the form ("dir") and
("dir" "path") are treated as abbreviations of ('rec "dir") and
('rec "dir" "path"), respectively.
Bye,
Hendrik
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] A few major bugs about exiting ProofGeneral with current CVS version
Pierre Courtieu writes: 2011/9/10 Erik Martin-Dorel : > 3. Finally, it seems the function `proof-shell-exit' raises > systematically an unexpected error. > > To reproduce it, run the (Coq) prover, then try: > [M-: (setq debug-on-error t) RET] > [C-c C-x] I have noticed this too. This is recent. I have put this in trac. The problem is coq-switch-buffer-kill-proof-shell and that proof-shell-kill-function does not take into account that a prover might get killed when scripting is deactivated. For more details see #421. If nobody objects, I'll adopt solution 1 (see #421 for solution 2): Inside proof-shell-kill-function set a global variable proof-shell-exit-in-progress. When coq-switch-buffer-kill-proof-shell sees this it refrains from calling proof-shell-exit recursively. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] [PATCH] coq: Add option to ignore warning from coqdep in auto-compilation mode.
Tom Prince writes: Some developments don't fully qualify their imports, and so coqdep gives warning about ambiguous imports. Allow these developments to use auto-compilation mode anyway. Could you describe an example? What is coqdep printing in these cases? -(if (string-match "^\\*\\*\\* Warning" coqdep-output) +(if (and (not coq-auto-compilation-ignore-coqdep-warnings) + (string-match "^\\*\\*\\* Warning" coqdep-output)) I would rather prefer to change the regular expression here, in order to only ignore the warning about ambiguous imports. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] [PATCH] coq: Allow specifying recursive entries in coq-load-path.
Tom Prince writes: On Fri, 09 Sep 2011 11:04:30 +0200, Hendrik Tews wrote: > * With the patch, coq-load-path covers the options -I and > -R ... -as ... With a minor change we will also get -R ... > However, -I ... -as ... would still be unsupported. -R only accepts two options, not a single one. I see blau ~ 4> coqc -help Usage: coqc file... options are: -verbose compile verbosely -image f specify an alternative executable for Coq -tkeep temporary files Coq options are: -I dir -as coqdir map physical dir to logical coqdir -I dir map directory dir to the empty logical path -include dir (idem) -R dir -as coqdir recursively map physical dir to logical coqdir -R dir coqdir (idem) And the reference manual lists only -R dir -as coqdir. > Does anybody use -I ... -as ... ?? Does anybody has an opinion > about whether Coq Proof General should support -I ... -as ... ?? I suspect that it isn't worth it. If there are no subdirectories, -R ... ... and -I ... -as ... have the same effect. Sure, but if there are subdirectories, the effect is different. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] [PATCH] coq: Allow specifying recursive entries in coq-load-path.
I am also in favor of releasing this patch, as it doeas not seem ro break the users old configuration settings using coq-prog-args (does it?). No, as long as coq-compile-before-require is nil. What do you think about -I ... -as ... ? Do people use it? Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] [PATCH] coq: Allow specifying recursive entries in coq-load-path.
Tom Prince writes: Make coq-load-path accept either strings (which are passed "-I" options) or conses of strings (which are passed as "-R" options). Thanks a lot for your patch. This has been on my todo list, however, I never looked at this point, because I don't use -R (yet). Before I commit your patch to the repository, I would like to discuss the following two points: * Proof General 4.1 will be released shortly (hopefully). I don't know if the policy permits commits with new minor features. David, could you comment on this? Probably a fair portion of the Coq users would benefit from the patch. The patch is very small and can be easily tested. Therefore, I would be in favor of committing the patch, although Proof General is already deeply frozen. * With the patch, coq-load-path covers the options -I and -R ... -as ... With a minor change we will also get -R ... However, -I ... -as ... would still be unsupported. Does anybody use -I ... -as ... ?? Does anybody has an opinion about whether Coq Proof General should support -I ... -as ... ?? [The point here is not the implementation, which would be very simple. The point is, if and how to encode -I ... -as ... in coq-load-path.] Note that Tom's patch does not apply cleanly to cvs head any more. When reading the patch I spotted some errors in the documentation strings, which I fixed a few minutes ago. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] ProofGeneral repository view
Hi, the mercurial view of the Proof General cvs repository at http://www4.in.tum.de/~wenzelm/cgi-bin/repos.cgi/ProofGeneral/ seems to be dead. Is there any alternative? If not I would volunteer to set up viewvc and cvshistory, but for that I would need access to the raw *,v rcs files. Of course a loginfo entry that runs, for instance, unison to synchronize the repository with my copy would suffice. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] setting completion-ignored-extensions
Do you want to try that? Watch out for the AUTOMODE-REGEXP optional last column (not currently used but was in the past). Just committed. Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] setting completion-ignored-extensions
Stefan Monnier writes: But admittedly, it also means that it's mostly useless as well: if your Coq file is called ".v" the completion will stop at ".v" in any case, No, it won't, because Coq does also generate ".glob" files. Additionally completion-ignored-extensions are hidden by default in dired buffers. Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] setting completion-ignored-extensions
David Aspinall writes:
Hendrik, do you want to add this for Coq?
Yes, as soon as we agree on how to it best.
I don't think it needs to
be added to generic mechanisms since Coq is the only supported prover
that compiles files at the moment.
You are right. However, completion-ignored-extensions should be
set up _before_ visiting the first Coq file. That is, it must be
initialized when Emacs loads proof-site.el. As far as I can see
the only prover specific stuff, which proof-site.el does, comes
from proof-assistant-table. Therefore I suggested, to extend
proof-assistant-table with one row for ignored extensions. This
is not particularly nice, because Coq will be the only one that
uses this row.
If you don't like changing proof-assistant-table, my suggestion
is the following: In proof-site.el I add a new defcustom
proof-general-completion-ignored-extensions with default value
'(".vo" ".glob"). Additionally, somewhere in proof-site.el the
contents of proof-general-completion-ignored-extensions is added
to completion-ignored-extensions.
Bye,
Hendrik
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] Re: auto coppile hangs emacs
David Aspinall writes: > Yes, but this will not be easy. The problem is the > following: I temporarily have to stop the proof-shell main > loop if the next item in proof-action-list is a Require and > if the corresponding compile job has not been finished. > > Simply calling accept-process-output inside > proof-shell-exec-loop does not help, because emacs does not > process keyboard input during waiting inside > accept-process-output. No, I don't think you want to insert a wait inside proof-shell-exec-loop -- this is called from the process filter function for the prover just to handle the last prover output. I guess the way to do things is to trigger the compilation in *another* asynchronous subprocess (I think you call coqc synchronously at the moment?) and use a filter function or process sentinel to handle the compile output. Yes, I actually meant that the compilation is running in separate asynchronous subprocesses. However, I thought that all asserted commands are put into proof-action-list before proof-assert-until-point completes. Require commands are marked as unfinished when they are inserted into proof-action-list. When the asynchronous compilation process for some required library is finished the corresponding Require command is marked as finished. When proof-shell-exec-loop sees an unfinished Require command it suspends itself without inserting it into the proof shell. This would allow control to return to the ordinary top level. Then the filter function goes back to call the insertion function which sends Require to the prover, if the compile succeeded. The exec loop picks up automatically again. You seem to suggest to keep unfinished Require commands (and all what follows such a command) in a separate list and add them only to proof-action-list when the compilation process is finished. This seems simpler. However, it would be nice, when still unfinished Require commands are colored pink as belonging to the queue region. Where is this pink coloring happening? I searched the subroutines of proof-assert-until-point, but did not find the function that is responsible for the pink color. Anyway, I agree this improvement is probably for v2. We should try to release PG 4.1 in the next couple of weeks (at last). Fine with me. I would suggest that we deal with the following issues before releasing: - fix broken pg cache (http://proofgeneral.inf.ed.ac.uk/trac/ticket/395) - fix defpacustom customization groups (http://lists.inf.ed.ac.uk/pipermail/proofgeneral-devel/2011/000115.html) - decide on completion-ignored-extensions (http://lists.inf.ed.ac.uk/pipermail/proofgeneral-devel/2011/000122.html) Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] Re: auto coppile hangs emacs
Pierre Courtieu writes: > Emacs is locked because I avoided all synchronization trouble and > call coqdep and coqc synchronously. All this happens before the > asserted items are put into proof-action-list. > > This is not optimal, but for a first version it is hopefully ok. It is indeed ok but it may be worth allowing the user to be able to edit unlocked region during this time. This can be a feature of second version :) Yes, but this will not be easy. The problem is the following: I temporarily have to stop the proof-shell main loop if the next item in proof-action-list is a Require and if the corresponding compile job has not been finished. Simply calling accept-process-output inside proof-shell-exec-loop does not help, because emacs does not process keyboard input during waiting inside accept-process-output. There seems to be no way around aborting proof-shell-exec-loop in the middle and restarting it when the compile job has finished. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] proof-follow-mode in invisible buffers
David Aspinall writes: > In order to do some changes in A the user unlocks A, thereby > retracting B. If B is not visible, then the point in B will > be moved to the beginning of the buffer. [ is there a difference between what happens with B invisible and visible? ] Yes, if B is visible in some window then its point is not changed. > Is this behavior really intended? The beginning of the > buffer is not a very useful position. If the user ever > switches back to B, he probably wants to continue at the > position where he left. I agree that's not useful for your suggested use case, although it certainly matches the understanding of "follow the locked region". Do you find "follow the locked region down" more useful? I am going to try that. As an improvement we might set the mark so the user could simply hit C-u C-space to jump back, then C-RET to carry on scripting. Yes, I though about this too. However, there should be a threshold, such that the mark is only set if point moves more than threshold lines. Otherwise simple one-line undo commands will clutter the mark ring. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] Why does proof-retract-until-point call proof-activate-scripting?
David Aspinall writes: > why does proof-retract-until-point make the current buffer > the active scripting buffer? It seems that Proof General > anticipates that the user starts asserting immediately > afterward. Not particularly, this is to enforce the simplifying invariant that there is at most only one buffer which can be partially processed. That in turn is to simplify things for the user and for interaction with the proof assistant. OK, I understand. For Coq however, if you modify an ancestor file, the complete locked ancestor is unlocked at once. So the invariant would not be broken if one does not change the active scripting buffer. In general, Coq's require commands can appear in the middle of a file. Say, for instance b.v requires a.v on line 100. Then, when you start changing a.v, you only have to undo b.v up to line 99. Then b.v could still be the only partially processed file, without breaking the invariant. In most of the Coq code that I saw until now, Require commands appear only at the beginning of the file, before all other material. So letting b.v remain a partially processed active scripting buffer (as described in the previous paragraph), would only be interesting, if the user organizes the Require commands as follows: (* First *) Require Some_big_and_expensive_to_load_and_rarely_changed_library. (* Second *) Require Everything_else. The idea here would be that if you change something in the ancestor hierarchy of Everything_else, the active scripting buffer is _not_ changed and the first line is _not_ undone. Then if you assert the second line again, you avoid loading the big library again. However, even the big libraries are loaded in about 1 second, so implementing this would only make sense if it doesn't require too much changes inside Proof General. > In all these cases it is right to completely retract the > current scripting buffer A, because this ensures that the > changes in B are recompiled and loaded. However, it is not > necessary to kill and restart coqtop. OK -- but the kill and restart is only happening now, because you have added patches to make deactivating a scripting buffer kill the Coq process, right? Well, killing and restarting is the only correct solution for Coq. It will remain until it is possible to undo changes in the load path inside coqtop (which is currently not possible). There is a possible optimization to reuse the same Coq session if the load path and the working directory of the old and new active scripting buffer are identical. But I am unsure if it is worth implementing. Is there a major drawback to killing and restarting in this case? No, I just noticed this behavior and started to wonder... Earlier you said that loading compiled files was so cheap it didn't matter to redo this. Loading compiled files is cheap in comparison to reprocessing them from source. And usually it is even very fast, unless you load one of the big library packages, such as, for instance, the omega library for presburger arithmetic. Then loading takes about 1 second. Is the issue that the UI loses this state (i.e. which files have been processed)? No. I would even say the UI must clean this state. Because, when the user starts asserting again, Proof General must check the complete ancestor hierarchy in order to determine which files must be recompiled. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] Re: auto coppile hangs emacs
Hi, Pierre Courtieu writes: Is there a reason why emacs completely hangs when auto compilation is working? You mean emacs is locked until compilation is finished and all asserted items are in the queue region? Or do you mean something else? Emacs is locked because I avoided all synchronization trouble and call coqdep and coqc synchronously. All this happens before the asserted items are put into proof-action-list. This is not optimal, but for a first version it is hopefully ok. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] proof-follow-mode in invisible buffers
Hi, in its default setting (which is locked) proof-follow-mode ensures that point is at the end of the locked region. Consider the following case: The user switches to buffer A, which is a locked ancestor of the current scripting buffer B. In order to do some changes in A the user unlocks A, thereby retracting B. If B is not visible, then the point in B will be moved to the beginning of the buffer. Is this behavior really intended? The beginning of the buffer is not a very useful position. If the user ever switches back to B, he probably wants to continue at the position where he left. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] Why does proof-retract-until-point call proof-activate-scripting?
Hi, why does proof-retract-until-point make the current buffer the active scripting buffer? It seems that Proof General anticipates that the user starts asserting immediately afterward. However, it might also be the case that the user does only make some very small change and then goes to the previous active scripting buffer (or to some other buffer) and continues processing there. In this case the call to proof-activate-scripting could have been saved. While for most proof assistants the additional call to proof-activate-scripting is probably not noticeable, for Coq it involves killing and restarting the proof assistant. I am posting this because of the following: For Coq (and probably other proof assistants as well) there are a number of small changes that are processed in the following way. While working in A you notice that such a small change is required in B, which is a locked ancestor of A. So you change to B, unlock it, make the small change and _immediately_ go back to A, asserting to the point where you left. Examples for such small changes are: - adding a simple definition - changing an Import into an Export - making an explicit argument implicit or vice versa. In all these cases it is right to completely retract the current scripting buffer A, because this ensures that the changes in B are recompiled and loaded. However, it is not necessary to kill and restart coqtop. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] ChangeLog branch chaos
Hi, after creating the ProofTreeBranch the generated ChangeLog (make ChangeLog) contains the commit messages from the trunk and the branch, which is a bit confusing. The problem is that rcs2log relies on cvs log, which outputs all available information by default. There is no real fix, because cvs log cannot generate all information that belongs to a particular branch. Even Debian gave up on the problem, see http://bugs.debian.org/cgi-bin/bugreport.cgi?bug=216246 There are the following partial fixes. If you want a ChangeLog containing only the messages for the main trunk then you can include the options ``-r -b'' in the rcs2log call in Makefile.devel. For the ProofTreeBranch including the options ``-r -rProofTreeBranch'' generates a ChangeLog with _just_ the commits to ProofTreeBranch. If you also want to see the messages from the main trunk before the branch point of ProofTreeBranch, you have to append them manually. To do this, generate the ChangeLog for the main trunk and copy everything starting with the entry ``2011-04-15 Hendrik Tews''. Alternatively you can use the rcs2log option ``-v''. This generates a ChangeLog containing commit messages from all branches, but includes cvs revision numbers. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] prooftree test release
Hi, I prepared the first release of prooftree, please have a look at http://askra.de/software/prooftree/ Installation is a bit tedious, because you have to manually compile and install Proof General, Coq and prooftree itself. The prooftree-bundle that I am releasing contains a snapshot from the ProofTreeBranch of Proof General. However, if you are using this branch from the cvs repository, then your version of prooftree will probably break when I commit changes for the next version. The general setup is described in generic/proof-tree.el and also at the website. Changes to existing code in Proof General are described in the commit messages. Comments are welcome, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] proof tree visualization -- where to commit?
Hi, inspired by PVS, I started to work on an external visualization of the proof tree. I have now a basic version running, see below. It is implemented in GTK and Ocaml, integrated with Proof General and works with a patched version of Coq. I believe it's time now to share the code with others and I would therefore like to commit the necessary changes to the repository of Proof General. It probably makes sense to commit to a branch first. How about ``ProofTreeBranch''? Bye, Hendrik <>___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] setting completion-ignored-extensions
Pierre Courtieu writes:
I agree with the idea, but should we really modify
completion-ignored-extensions by ourselves?
That's the usual practice. Here emacs -q -no-site-file gives
completion-ignored-extensions is a variable defined in `C source code'.
Its value is
(".o" "~" ".bin" ".lbin" ".so" ".a" ".ln" ".blg" ".bbl"
".elc" ".lof" ".glo" ".idx" ".lot" ".svn/" ".hg/" ".git/"
".bzr/" "CVS/" "_darcs/" "_MTN/" ".fmt" ".tfm" ".class"
".fas" ".lib" ".mem" ".x86f" ".sparcf" ".fasl" ".ufsl" ".fsl"
".dxl" ".pfsl" ".dfsl" ".p64fsl" ".d64fsl" ".dx64fsl" ".lo"
".la" ".gmo" ".mo" ".toc" ".aux" ".cp" ".fn" ".ky" ".pg"
".tp" ".vr" ".cps" ".fns" ".kys" ".pgs" ".tps" ".vrs" ".pyc"
".pyo")
Is it not considered a
user preference? Some people dislike hiding files at all.
Those people must then switch off the effects of
completion-ignored-extensions on a different level, so they won't
even notice if we add another two elements.
Bye,
Hendrik
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] setting completion-ignored-extensions
Hi, AFAICT there is no support for completion-ignored-extensions in Proof General. For coq, setting completion-ignored-extensions would be nice, because the coq compiler clutters the directory with .vo and .glob files. My suggestion would be to extend proof-assistant-table with one row for a list of to-be-ignored file-extension. Then the initialization code in proof-site.el could extend completion-ignored-extensions appropriately. Comments? Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] delete proof-done-advancing-require-function ?
Hi, proof-done-advancing-require-function and proof-shell-require-command-regexp seem to have only been used for coq and they are no longer needed. IMHO it makes sense to delete them. If this is general consensus I would develop a patch and post it here for review. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] coq-auto-compile-vos discontinued
Hi, because nobody answered to my poll on the coq mailing list (https://sympa-roc.inria.fr/wws/arc/coq-club/2011-02/msg00059.html), I suggest to not further support coq-auto-compile-vos. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] Flushing old coq multiple file support
Hi, if nobody disagrees I am going to delete the old multiple file handling code for coq. There was one worthwhile thing in it: the coq-auto-compile-vos option. I'll check how I can keep its functionality. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] defpacustom customization groups
Hi, is it really intended to add defpacustom variables to two customization groups, to proof-assistant-internals-cusgrp and to proof-assistant-setting? Is there a reason why the group proof-assistant-setting is not defined? Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] fix coq proof shell not running after activate-scripting
Hi, for coq there is currently a problem when you switch the active scripting buffer: The first assert command in the new scripting buffer does not assert anything. This happens, because coq mode kills the proof assistant in the deactivation hooks and proof-activate-scripting runs those hooks _after_ proof-shell-ready-prover. Below I append a patch that fixes this problem for me. Please review this patch, because I have not much understanding of what I am changing... There are two points about the patch: - I first experimented with calling proof-shell-ready-prover after the big unless-form in proof-activate-scripting. This was running fine for me, but then I figured it would be better if the proof assistant is restarted before the activation hooks run. Now proof-shell-ready-prover is called in the middle of the unless-form (which has been split into two halves). - When I first tested this patch back in January, it was not sufficient. Back then the patch ensured that the proof assistant was running after proof-activate-scripting, but the first assert in the new scripting buffer was nevertheless lost (because, IMO, proof-shell-exit killed all spans). However, I cannot reproduce this problem any more, not even with old Proof General versions from January. The patch below is working correctly for me ... Bye, Hendrik Index: generic/proof-script.el === RCS file: /disk/cvs/proofgen/ProofGeneral/generic/proof-script.el,v retrieving revision 11.8 diff -u -r11.8 proof-script.el --- generic/proof-script.el 31 Jan 2011 10:35:55 - 11.8 +++ generic/proof-script.el 14 Feb 2011 12:05:54 - @@ -1196,8 +1196,14 @@ (unless (eq proof-buffer-type 'script) (error "Must be running in a script buffer!")) - (proof-shell-ready-prover queuemode) ; fire up/check mode - + ;; Check whether we have a new or changed proof-script-buffer. If + ;; this is the case, a lot of things must be done. We split all + ;; these things into two halves. The first half follows immediately: + ;; it shuts down the old proof-script-buffer and retracts some + ;; files. The second half initializes the new proof-script-buffer. + ;; Because the first half might kill the prover (which is actually + ;; the case for coq), we make sure the proof shell is ready before + ;; we start the second half. (unless (equal (current-buffer) proof-script-buffer) ;; TODO: narrow the scope of this save-excursion. @@ -1228,10 +1234,18 @@ (if proof-script-buffer (proof-deactivate-scripting)) (assert (null proof-script-buffer) - "Bug in proof-activate-scripting: deactivate failed.") + "Bug in proof-activate-scripting: deactivate failed."))) - ;; Set the active scripting buffer, and initialise regions + (proof-shell-ready-prover queuemode) ; fire up/check mode + ;; It now follows the second half of things to do if we have a new + ;; or changed proof-script-buffer. + (unless (equal (current-buffer) proof-script-buffer) + +;; TODO: (copied from above) narrow the scope of this save-excursion. +;; Where is it needed? Maybe hook functions. +(save-excursion + ;; Set the active scripting buffer, and initialise regions (setq proof-script-buffer (current-buffer)) (if (proof-locked-region-empty-p) ;; Clear locked regions, unless buffer is "full". ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] no deactivation-hooks when killing fully asserted active buffer
David Aspinall writes: OK, I committed a patch now (not quite the one I sent you off list) which ensures that the hook function is run. Thanks, we can now close the killing-fully-asserted-active-buffer issue. And I don't get an error! You don't see the error any more, because we have now double security: - first the buffer is retract because of proof-no-fully-processed-buffer - second coqtop is killed on switching the active scripting buffer At the moment proof-no-fully-processed-buffer is therefore not necessary, because killing coqtop retracts everything. Eventually I want coqtop to survive switching the active buffer if the load path' of the new and old buffer are equal. Then proof-no-fully-processed-buffer will again be essential. I just updated the description in that README file, if you want to see the error you have to disable a deactivate-scripting-hook in coq.el. Regarding test case above: the bug mentioned in README is fixed, but the behaviour I described earlier (about Coq process being started at odd time) still happens when I follow the "To provoke an error" When do you see coq being restarted? When I follow the old instructions (that is without disabling the deactivate-scripting-hook), I see: - coq starting when I script the first comment in a.v - coq killed when I script the first comment in b.v - coq started again when I script the first non-comment line in b.v This is precisely as it should be. (Only that I don't understand why I can script the first comment in b.v without coq running.) Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] Inverse of proof-register-possibly-new-processed-file?
Hi, I looked around, but I could not find the inverse of proof-register-possibly-new-processed-file. This inverse should delete a file from proof-included-files-list and unlock its buffer, if it exists. There is proof-unregister-buffer-file-name, but - it only works on buffers - it does not unlock the buffer I also looked at proof-retract-buffer, but it wants to change the active scripting buffer, which is not the right thing to do when unlocking an ancestor. I finally came up with the following (defun coq-unlock-ancestor (ancestor-src) "Unlock ANCESTOR-SRC." (let* ((true-ancestor (file-truename ancestor-src)) (buffer (find-buffer-visiting true-ancestor))) (setq proof-included-files-list (delete true-ancestor proof-included-files-list)) (if buffer (with-current-buffer buffer (proof-set-locked-end (point-min)) (proof-script-delete-spans (point-min) (point-max)) This works in my tests, but I am not sure, if it is the right thing. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] how to unlock ancestors
David Aspinall writes: So I agree that your approach 1 is best. Implemented and seems to work, but see my next post on "Reverse of proof-register-possibly-new-processed-file". > BTW, what is the relation of 'remove-action and > 'span-delete-action? If there is a hook, the remove action > could also be put into the hook. [...] I agree that it looks like these could be combined into a hook, but please be careful with the order of calling if you try that: I suggest to make it a second refactoring step after converting span-delete-action into span-delete-actions. (It may be that we can also address the minor FIXME on line 2140 of proof-script.el here by letting proof-setup-retract-action take a list of functions to append to the hook, and putting on a function to adjust the proof depth counter there, but let's also try that at a later step). There is now span-add-delete-action which adds a function to the 'span-delete-actions property. But it is only used for the action that was previously stored in 'span-delete-action and for coq-unlock-all-ancestors-of-span. I neither touched the remove action nor that FIXME. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
