[PG-devel] PG 4.0
Dear PG developers I'd like to release PG 4.0 by the end of this month. Please try to get the code into a ready state and test as much as you can. This release marks a big change in the code base (removal of X-Symbol and XEmacs compatibility) and is a good chance to clean things up and remove backward compatibility for old prover versions. - David ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] Improvement of pg-protected-undo
Dear Erik, I replied off-list, but see you have subscribed here too. For other developers: this welcome improvement has been added to PG CVS head now. Please feel free to send any more improvements/fixes for PG 4.0, which should at last be released this summer. - David ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
[PG-devel] Proof General 4.0 - release candidate
Dear PG users and developers, With help from a few special people over the past few months, we have ironed out many issues with the CVS version of Proof General and I think it is good enough to make into an official release --- the first in over two years. In the hope of nipping the last few problems, I'd be grateful for users and developers to try out the current pre-release, through *this week*: http://proofgeneral.inf.ed.ac.uk/devel and report any problems in the usual place http://proofgeneral.inf.ed.ac.uk/trac/ I'm aiming to make the release a week from today. Many thanks in advance, - David ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] multiple file scripting for coq
Hi Hendrik Thanks for looking at this! Pierre and I had investigated a few ideas, you can still see some code remains in coq.el from some old attempts that partly worked (auto-compile-vos), but it seemed that Coq users were never hugely interested in the feature. There is some code to take action after a require has been processed, but, as you say, maybe something should be done just before as well to check compiled files are up to date. I'm not sure whether the file save/load hooks would be more appropriate than a hook run when command is queued, or whether connecting to standard Emacs make mechanisms would be sensible. For your way, maybe the standard proof-shell-insert-hook would work? This runs when a command is actually sent to the process, versus when it is queued. Anyway, would be very happy to get this working with latest Coq and accept a patch. Maybe discussing further on our Trac would be best, there is this ticket here: http://proofgeneral.inf.ed.ac.uk/trac/ticket/363 Best wishes, - David On 06/12/10 12:13, Hendrik Tews wrote: After looking a bit at the code, I believe it is best to install a new hook, say proof-enqueue-item-hook, that is called in proof-add-to-queue just before the queueitems are appended to the proof-action-list. The hook would be called for every item in queueitems. coq-mode can then install a function in the hook that looks for require commands and takes appropriate actions. The hook variable itself should be buffer local, to avoid that the coq-require-filter function is called in an Isabelle session. Any comments? Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] multiple file scripting for coq
Hi Hendrik I looked at proof-shell-insert-hook. Is there a way to send a command to the prover, capture the output and retract this one command from within proof-shell-insert-hook? The documentation says that additional prompts will confuse proofgeneral. So is there a way to interact with the prover from within proof-shell-insert-hook without confusing proofgeneral? Yes, the insert hook is intended to munge the string sent to the prover rather than insert extra commands at that point. You could add them to the queue, but that would be at the wrong moment. The background is that coq has its own load path for libraries (where a library is a compiled .v file). To find out which file needs to be checked for recompilation it would be easiest to ask coq with the Locate Library command. But this would require a synchronous communication with coq from within proof-shell-insert-hook when an Require command is detected. Or... you could do this at another time instead, for example, when the queue of commands is built, or when the file is loaded/saved using standard emacs hooks. I think the file-load/save is a quite natural time to do this since it may interrupt the developer anyway and we try not to query the developer when sending commands in the background (so they can be looking at other parts of the script). You'd lose when the user tries to process a Require command they've just typed but not saved the file, but you could issue a warning about this (or perhaps the require will fail anyway, in which case the user hits save-file and tries again). Using Locate Library would have the advantage that proofgeneral does not need to model coq's library finding functionality. That's *definitely* a good idea. (We tried to use coqdep for the auto-compile-vos option). - D. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] multiple file scripting for coq
[forgot to copy to the list, in case anyone else is listening] And another PS on this: I just suggested file load/save hooks, there is also PG's own file protocol which is activate/deactivate scripting, which also have hooks. These might be nicer to use, but the user ought not to change require commands after activating scripting (again you could spot that and give a warning). This protocol was the simple design that Makarius and I came up with to solve these multiple file issues cleanly in Isabelle, to attempt to have consistent views in the editor and the file system. He is going on to grander sub-file schemes now... - D. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] multiple file scripting for coq
On 08/12/10 16:47, Pierre Courtieu wrote: Hi, I answer Hendrik's message here because i did not recieve it. Can you subscribe to the list Pierre? As a key developer it should be obligatory!! 8-) I'll send the earlier message to you which answers your last question to me below, sorry forgot to CC you! - D. 2010/12/8 David Aspinall: Quick followup to your second message: - good idea to separate the two things, you can set up a customizable command using % substitutions easily - have you looked at the existing (surely broken, but not irreparable) code for calling coqdep? - D. On 08/12/10 15:33, Hendrik Tews wrote: Hi, I would like to separate the following issues: 1. Detecting library loads inside ProofGeneral and finding out what file actually is meant 2. Deciding whether the library is up-to-date and performing the actions to make it up-to-date. OK, I am getting your point. For issue 2 the simplest solution is to provide a user option for an external command to be called. The command will contain some keys that get substituted with file and directory. The default would be something like "make -C %d %f.vo" resulting in "make -C some/dir foo.vo" if library foo in directory some/dir is required. ProofGeneral should always provide this simplest solution, because it scales to arbitrary projects with arbitrary dependencies. I would however also be interested to built some simple dependency analysis into ProofGeneral, based on calling coqdep on some .v files, analyzing the results and then possibly calling coqc on some files. This would relieve simple projects from providing a makefile. However, in the emails before I only discussed issue 1. The problem is that if library foo is required then you need to look at coq's library path, in order to find out which files foo.v and foo.vo are actually meant. It might be that there is foo.vo in the current directory, but coq loads foo.vo from some other directory or even complains that it cannot find foo.vo! To solve issue 1 one can either model coq's library-finding functionality inside ProofGeneral or ask coq with Locate Library. The latter is simpler, but requires that one can synchronously talk to coq without disturbing the rest of ProofGeneral. OK. I get your point completely now. The idea is the following if I understand well. A command "Require f" is about to be sent to coq, but *before that* we want to perform the following: 1) send "Locate Library f" 2) wait for the answer of coq: "path/to/f" . 3) send "make -C ... path/to/f.vo" 4) wait until make finished its job 5) finally send the "Require f" to coq if everything went well (error otherwise). Tell me if I am wrong. David, I am not sure coq-shell-insert-hook is the good entry point for this kind of things. Is it? Cheers, Pierre ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] multiple file scripting for coq
On 09/12/10 14:19, Hendrik Tews wrote: David Aspinall writes: I think the file-load/save is a quite natural time to do this since it may interrupt the developer anyway and we try not to query the developer when sending commands in the background (so they can be looking at other parts of the script). I am not so concerned any more about asking the user when sending commands in the background. The reason is that it doesn't make much sense to decide about recompilation on a per-file basis. I expect that most users will either disable recompilation from ProofGeneral or set it to "automatic" mode, where ProofGeneral recompiles without asking back. The "confirmation" mode, where ProofGeneral is asking for confirmation before recompiling is probably only useful for new users, to give them an impression about what is going on. Did you consider the scripting time option, file activated for scripting? This is the place that saves of potential-ancestor files is triggered (with idea that prover may read them from file system). So it seems to fit this usage with caveats I mentioned before. - D. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] multiple file scripting for coq
So your answer is no? One cannot communicate with the prover from inside proof-shell-insert-hook? No, do not do that. There might be some misunderstanding: I want to use "Locate Library" only to map a library names to a file path. This mapping depends on coq's LoadPath, which can be changed with command line switches or with the various LoadPath commands at runtime. I think I understood, roughly, but thanks for clarifying, I think the coqdep stuff was just a failed attempt to do this (maybe before Locate Library was available). - D. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] multiple file scripting for coq
On 10/12/10 11:43, Hendrik Tews wrote: David Aspinall writes: Did you consider the scripting time option, file activated for scripting? This is the place that saves of potential-ancestor files What precisely do you mean? Do you mean ProofGeneral's concept of the active scripting buffer and proof-activate-scripting-hook? Yes. I don't want a solution based on proof-activate-scripting-hook, because I want to update files outside of emacs (eg by cvs update) while I am scripting in some buffer. But that's OK: the point of the "active" scripting buffer is to isolate the one buffer that you are editing in the editor that *shouldn't* be simultaneously changed outside your control in the file system. Emacs's own hooks will check file-system consistency for you, with usual warning messages and options to reload the buffer, etc. But you don't expect/want this to happen when you've sent half of it Coq. When a new buffer becomes active, it is a chance to check that ancestor files are compiled to their latest versions. For files that are compiled, you might lock them inside PG to indicate this and that the user should not edit them to become confused. If they do edit some file, then dependent files will be unlocked automatically to indicate to the user that they need recompiling to use updated ancestors. See proof-included-files-list, doc here: http://bit.ly/dTItNV I think this could work nicely with Coq and compiled files. If you can try out Isabelle, the trivial test cases include in etc/isar/multiple will demonstrate how it works. Also look at the messages in the *isabelle* buffer. I'm assuming it's not possible to invoke coqc from within coqtop? Instead, you could use a cunning perl wrapper to multiplex the compile/proof commands and use the existing PG configuration mechanisms. Your wrapper could even spot "Require" commands and invoke "coqc" itself as you first thought of doing with PG, then the messages issued could work with the existing protocol. But that's maybe too kludgy, you would need to buffer commands, etc. - D. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] multiple file scripting for coq
On 10/12/10 14:43, Pierre Courtieu wrote: I agree with Hendrik, activate-scripting is not the right trigger because dependencies may change *after* scripting is activated. Each time the user adds "Require Import foo." and scripts it, proofgeneral should try to compile foo.v if it is not up-to-date. This is actually pretty similar to what happens in Isabelle, it is just that Isabelle reports the dependencies to Proof General after it has processed the equivalent of Require (and of course, it reads the file in on the heap at that point rather than compiling). So, if you don't want to parse the file first you can still use a new hook (or the kludgy wrapper idea, or a modified coqtop top level...) to issue the compile commands exactly when you process Requires, but the rest of the active scripting mechanism could join up well. (Note: when you undo a Require you should unlock the corresponding buffer too.) It would be great to get this working, but I am remembering why it wasn't so easy... - D. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] multiple file scripting for coq
Yes but files on which it depends may have changed by cvs (typically you cvs update an external library to its current version). When will this be detected? It would be tedious to have to deactivate/reactivate scripting to detect this. Going back to the require and forward should be enough. This is confusing... I think you're asking for something that neither mechanism we've talked about is trying to do. I don't mean that you turn on/off scripting every time you type a Require command, although we could argue about how bad that really would be (aren't Require commands almost always collected at the top of the file?). I'm suggesting Hendrik uses the existing included files mechanism *and* the coqc/LoadPaths triggers, to give better user feedback on the status of files up-to-date/not in the interface. This was the point of the original included files design. So files which have been compiled are considered up-to-date and are locked. The locking happens when the Require is processed, which is what you want, and up-to-date checks could be made here (IIRC the locking is simplistic: it locks an already visited buffer, and arranges that if that file is visited in future it will be locked). You can always subvert the interface locking if you want to, explicitly with the options, or behind the scenes by being naughty. The point is to have a simple mechanism that gives the user some useful hints in most cases. Personally, I would think that running a big cvs update in the middle of scripting a complex file that depends on the libraries you're updating is not a sensible idea!! Moreover as I said before: the set of ancestors may change during edition as user types its Require. This feature is definitely what we want but it is an error to consider that dependecies are fixed, and that requred files are fixed. This is straightforward, you need to tell PG the dependencies but you can do this from seeing the Require (exact single dependency), or from the output it produces (recursively included files as well). Same as in Isabelle, you should really take a look at it... - D. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] multiple file scripting for coq
Hi Hendrik, Quick reply to your second message: useful hints in most cases. Personally, I would think that running a big cvs update in the middle of scripting a complex file that depends on the libraries you're updating is not a sensible idea!! With PVS I do this now and then for validating proof scripts in the background. For instance, when working in B I notice that I have to change something in A, where B depends on A. So I change A, ... Changing files in the background also happens when working at home: When finished at home I copy the sources to work and hibernate the computer at home with the running proof assistant. At work I continue and later I start the computer at home and copy the changes from work. Thanks a lot for explaining these use cases. I think it's a good way to think about the scenarios that should be supported, or, at least, not prevented. If the developer believes (or the system knows) that the proofs are not going to be broken by changed statements or missing definitions, etc, then continuing scripting while there are updates in ancestors is OK, of course. If the changes are made by someone else you might want to be more careful! The simple-minded file-level locking/decoration is supposed to give a little bit of information so that the developer has some interaction to point out these dependencies and finds out about changes. If you're closely aware of the dependencies (e.g. through writing Makefiles and running compiler on command line), it probably doesn't matter much. I think that was the conclusion Pierre persuaded me of last time I raised the multiple file support with him. Maybe once people get used to automatic compilation it would seem useful. I'll think about your second message in a bit more detail and respond in a while. Meanwhile, I encourage you to develop a patch which supports the uses you're most interested in! Best wishes, - David ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] first multiple coq files patch
Dear Hendrik, Many thanks for the patch! I hope some users will test it but there aren't many on this list, you might like to advertise your web page on the Coq mailing list, perhaps? I'll try to take a look myself soon. I hope to release PG 4.1 shortly to coincide with the Isabelle release and had hoped your patch would be ready by then, but maybe not. - David On 11/01/11 15:07, Hendrik Tews wrote: Hi, below is a first patch against ProofGeneral version 4.0, that adds support for multiple files for coq. The patch is not complete yet, I would not expect an inclusion in the development version of ProofGeneral at this time. I post the patch to give you something to experiment with and to get some feedback. The patch adds a hook to proof-extend-queue such that I can search for Require commands just before they are added to the queue. If I find a require I immediately check dependencies and recompile if necessary. Checking and recompilation is either done in a rather straightforward recursive function (coq-make-lib-up-to-date) or through an external command, configured with coq-recompile-command. For mapping module names to files I use an emacs hash table that models the LoadPath. It gets initialized in proof-shell-init-hook. The patch also adds an option proof-no-fully-processed-buffer, through which coq-mode does now require to fully retract even those buffers that have been completely asserted. There is lots to be done, see http://askra.de/software/multiple-coq/ for known problems. In particular I have not (yet) done any integration with the multiple file support that was there before. I abandoned the following two ideas: - Query coq to map module names to files There is apparently no reliable way to do this. - Do checking/recompilation from inside the process loop The main argument for this approach is that Add LoadPath commands have been processed before starting the dependency analysis. However, nobody is using Add LoadPath, and the argument is therefore a bit weak. On the contrary, error reporting is very complicated ... (I checked all coq user contributions, they only contain "Add LoadPath ".." twice for some examples in a subdirectory.) Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] multiple coq files: error reporting
How to report those coqc errors? I believe I need a refactorization of proof-shell-handle-error-or-interrupt where I can pass the error message as a string argument. Looking at what you've done so far, I suggest simply not sending the commands to the theorem prover process if the auto compilation fails. Your own error reporting brings up a helpful buffer which shows the result of the coqc command, and adjusting the proof-shell patch as below prevents the queue being left in a bad state. - D. *** generic/proof-shell.el 10 Oct 2010 22:57:05 - 11.0 --- generic/proof-shell.el 12 Jan 2011 13:17:27 - *** *** 924,932 --- 924,938 for processing a region from (buffer-queue-or-locked-end) to END. The queue mode is set to 'advancing" (proof-set-queue-endpoints (proof-unprocessed-begin) end) + (condition-case err + (run-hooks 'proof-shell-extend-queue-hook) + (error + (proof-detach-queue) + (signal (car err) (cdr err (proof-add-to-queue queueitems 'advancing)) ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] Automatically retract effects of proof-activate-scripting-hook?
> I expected, that when changing the buffer and retracting the old > scripting buffer, all those Add LoadPath commands are retracted as > well. However, this is not the case! Commands sent via > proof-shell-invisible-command from inside > proof-activate-scripting-hook are not retracted when scripting is > deactivated. proof-shell-invisible-command is designed for sending diagnostic and control commands which are not scripting commands and not part of the undo model of the prover. You only get undo behaviour for commands which appear in the buffer text. So, yes, you may need to adjust the load path manually with the scriting activate/deactivate hooks. - D. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] Automatically retract effects of proof-activate-scripting-hook?
> Undoing those Add LoadPath commands with Remove LoadPath commands > would be rather difficult. If one adds a directory which is > already in the LoadPath, coq reorders the LoadPath, a subsequent > remove will not yield the starting state. In that case I'm not sure how you can achieve what you need, unless there is SetLoadPath. > proof-shell-invisible-command is designed for sending > diagnostic and control commands which are not scripting > > OK, is there an alternative that I could use from inside > proof-activate-scripting-hook in order to get undo behaviour? No, invisible command is the only thing open to you. In any case, Proof General is nowadays (intentionally) quite stupid about undo commands and just points Coq at particular states in its internal history based on counting script commands sent. Maybe Pierre can advise (or has already advised) on whether the load path is part of the state that Coq manages internally in its history. If it isn't then you're not going to get something automatic. To manage things manually, you could add special properties to the spans in the buffer to record the loadpath before an adjustment is made, then alter Coq's undo calculation to issue commands to restore the value when those regions get retracted. Sounds doable, but tedious. How often is AddLoadPath used in scripts? - D. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] Automatically retract effects of proof-activate-scripting-hook?
For getting correct multiple file scripting for coq I would first try to restart coqtop on every new scripting buffer. What would be the best way to achieve this? Put proof-shell-exit into proof-deactivate-scripting-hook? I suppose but this does seem pretty crude, there is some cost to setting up/tearing down process and associated buffers, etc. Doesn't something like Reset Intial work (restart button's command)? > will be sufficient. The -I arguments can be derived from > coq-load-path and coqtop is default. > > That would be nice. For this we can ask David to allow prog-args to be a function instead of a list. In proof-shell near line 239. This way we can define coq-prog-args as the function that build the -I list from coq-load-path. I would leave prog-args as it is now. I view coq-prog-args as the place for options different form -I and -R like -is or -impredicative-set. I suppose Pierre means that you need a way to influence the command line calculation as you wanted, perhaps with yet another control function/hook or variable for prog-args (already several added for Coq..). I suggest refactoring the setting of prog-command-line in proof-shell-start into a new function which does this, so (proof-shell-prog-command-line) returns the command line you want. That would clear up the beginning of proof-shell-start a bit. - D. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] Automatically retract effects of proof-activate-scripting-hook?
> This is, however, not the expected simplification. I decided for > this simple change, because it keeps the functionality of other > proof assistants without that I have to touch their code. This sounds wise, and what Pierre originally suggested, although if I've followed it seems as if that's not compatible with his convention of setting coq-prog-args in file local variables. - D. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] Automatically retract effects of proof-activate-scripting-hook?
> This sounds wise, and what Pierre originally suggested, although if I've > followed it seems as if > that's not compatible with his convention of setting coq-prog-args in file > local variables. I looked again, I see you suggested coq-load-path for this already, not prog-args. Great. - D. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] Re: Multiple files: coq-process-require-command
> However, I am not satisfied with what happens when I switch to > one of these looked ancestors. What currently happens is that > when I start typing there, I am forced to completely retract the > current buffer. IMO this is too much for coq. Yes, it seems that you're actually wanting the opposite situation from Isabelle, where we suppose retracting an ancestor file is potentially expensive operation, so in general we might want to protect ancestor files against accidental retraction more enthusiastically than protecting the current script. > The situation is slightly better than I described, because one > can permit typing by setting proof-strict-read-only to nil. > However, this is a global setting which also affects the current > scripting buffer. Yes. And note that changing it is not dynamic in the sense that it does not affect spans which have been previously constructed. It is tempting to improve that in the function proof-span-read-only by always using a function (i.e. added by span-write-warning) rather than using standard read-only property. Let me understand *exactly* what you're wanting. Currently p-s-ro allows t : prevent editing without retracting manually, give read only error 'retract : automatic retraction before edits (essentially UI convenience). nil : edit freely, don't remove the span colouring or retract In nil case, the interface keeps cues about how much has been processed, but the buffer loses sync with the actual text that was processed in the sense that there is no visual indication that the text has been edited. (Remark: PGIP uses the "outdated" state I mentioned before for this condition, so an edited ancestor file would change from blue to a grey colour and cause all its children to do so also). Instead of what you suggested, could we add an additional option to p-s-ro that would give you what you want? Pro: it seems a bit smoother than your suggestion; Con: it introduces yet another user-visible choice. Something like 'edit-others, meaning nil behaviour for non-current scripting buffers. It's an easy test in the span hook function to see if we are editing in the current active scripting buffer or not. - D. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] Re: Multiple files: coq-process-require-command
P.S. correction to what I said: p-s-ro changes *are* dynamic in that there is a special function which changes the spans following changes in that setting. That's the function that has the same name as the variable, proof-strict-read-only, it's called by the proof-set-value hook in defcustom for the variable. A bit clunky.___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] no deactivation-hooks when killing fully asserted active buffer
Hi Hendrik Yes, it looks like a bad path, probably not noticeable before since we've used the hook for functions that only are useful when the shell is live. Do you want to repair by adding a test for fully processed buffer? [Or I can do, but not until much later today] - D. On 21 Jan 2011, at 07:42, Hendrik Tews wrote: > Hi, > > when you kill the currently active scripting buffer, then the > hooks in proof-deactivate-scripting-hook are not run when the > buffer was fully asserted. I believe this is a bug. > > What happens is that > > - kill-buffer-hook calls proof-script-kill-buffer-fn, > - which calls proof-deactivate-scripting-auto > - which calls (proof-deactivate-scripting 'process) > - which calls (proof-protected-process-or-retract 'process) > - which calls proof-process-buffer > - which calls (proof-assert-until-point-interactive) > - which calls proof-assert-until-point > - which throws > (error >"At end of the locked region, nothing to do to!")) > - this error unwinds until the ignore-errors in > proof-deactivate-scripting-auto, thereby skipping the call to > the hooks in proof-deactivate-scripting > > Bye, > > Hendrik > ___ > ProofGeneral-devel mailing list > ProofGeneral-devel@inf.ed.ac.uk > http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel > ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] no deactivation-hooks when killing fully asserted active buffer
I've committed a patch to proof-protected-process-or-retract now which fixes this problem and I think your test case works. But there may be some further issues (try the coq autotest script) because the coq process is killed and restarted at unusual places in the code now, probably breaking some assumptions. I don't quite understand the places where this happens: it would seem cleanest if the process was started/exited with the activate/deactivate action, but I'm seeing it being started after switching buffers and beginning scripting somewhere else, e.g. on the first non-comment element of the file. - D. On 21 Jan 2011, at 10:06, Hendrik Tews wrote: > David Aspinall writes: > > Do you want to repair by adding a test for fully processed > buffer? > > I reused an existing test case, see the description in > coq/ex/test-cases/retract-completely-asserted/README. > > I would like to leave the work on the fix to you. > > Hendrik > ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] how to unlock ancestors
I think the natural place to do this is actually in the prover-specific retraction function, coq-find-and-forget. But this would also require computing the list of spans in the retracted region, which is avoided in the Coq code now by using span properties to store pointers passed back to Coq. So I agree that your approach 1 is best. > 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. The remove-action was a private action for the script management --- I think only used to delete a region of text for the undo with delete function -- note that it is given the span end points as an argument and called after the span is deleted. The delete action is for other stuff called before the span deletion. In particular, the auxiliary spans for decoration, tooltips, etc use the second one to update the internal maps of auxiliary spans. 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). - D. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] Re: Multiple files: coq-process-require-command
> I only thought about a coq-specific solution that leaves the > other proof assistants untouched. Thinking about it, the feature > might also be interesting for other provers. Maybe -- but I prefer to avoid proliferating user options even further unless there's a desire (ideally from more than one user...). Also, we should avoid making the code overly complicated (and the automatic functionality difficult to guess) if the use case you are addressing could be managed just by the user very easily hitting another key press (e.g. C-c C-r) that becomes part of their work flow. I had in mind us adding one additional option for p-s-ro, not turning it from three settings into 8, so let's think about it... > 1. Make scripting in ancestor ready. This is for the case that I > want to continue with scripting in the ancestor. Proof General > should retract up to the point where I can start scripting in > the ancestor without being another question asked. For coq > this means to completely retract the current active scripting > buffer. OK, so this is current 'retract setting, right? > 2. Make editing in ancestor possible. This is for the case that I > only want to edit the ancestor and continue afterwards with > scripting in the current active buffer. Moreover, I want to > maintain consistency of my buffers and the prove assistant. > For coq this means that the current scripting buffer must > retract up to the appropriate Require command. When I change > my mind and start scripting in the ancestor, then I am asked > again, whether I would like to change the current scripting > buffer. If I understand right, I think the main new use case you're allowing here is for the user to make an edit in an ancestor file, and have that file automatically recompiled (not scripted) by re-processing the Require line in the child buffer and without nuisance of having switched active scripting buffer, etc. Before making that an automatic option for p-s-ro it could be implemented as a user-level command perhaps, and if you want the precise (retract to line of Require) behaviour, for Coq only. > 3. Permit editing in the locked ancestor. This is for the case > that I want to edit the ancestor without changing my current > state in the active buffer. Thereby I accept the inconsistency > between the buffer content and prover. For coq this means that > only the span in the ancestor must be changed to read/write. > When I switch to a different ancestor I want to have a new > choice. Hmm. This sounds like something for consenting adults only, and something that C-c C-z, proof-frob-locked-end should allow. Have you used that command? > For coq there is usually only a tiny difference between option 1 > and 2, because Require commands are usually at the beginning of > the file. Therefore, I would be satisfied with a choice between 2 > and 3 with the following optimisation for option 2: Proof General > must retract at least up to the Require that caused ancestor to > be locked. If there are only comments and Require commands above > this point then the current scripting should be retracted > completely. This optimisation becomes desirable because we have the situation with the implementation that the control over ancestor files is fine-grained (i.e. during scripting the file rather than at the start by parsing "imports" which the included files behaviour assumed). I think you made this decision for implementation ease as well as accuracy, but if you want now to automatically retract things further than target region in certain cases, that definitely looks like a Coq-specific function. > Alternatively a choice between 1 and 3 would be fine, if there is > the following change for coq: If there is substantial material > above the Require that caused ancestor to be locked, then Proof > General should only retract up to this Require, but not the > material before it. Yes, I agree for Coq. Although I notice again it's just one key/button press for the user, C-c C-r. > So in summary, I would like to see the following changes: > > 1. an additional option 'ask for proof-strict-read-only, which > asks whether to retract or to permit modifications in the > locked region. This seems to be an additional dialogue that's not really necessary (the user can manually retract with C-c C-RET when p-s-ro is strict). Perhaps you mean to change the buffer local behaviour temporarily for just the current buffer. Would a buffer-local override to allow edits temporarily meet this? (alternative to C-c C-z, edit, C-c C-z) > 2. splitting proof-strict-read-only into two variables, where one > applies to the active buffer and the other applies to all > other buffers. Not sure about this, and it might be messy in the code. Easier would be a buffer local value for proof-strict-read-only which can be modified from the default, but I'm not sure how smoothly that would work in the c
Re: [PG-devel] Re: Multiple files: coq-process-require-command
Thinking again on this: > This optimisation becomes desirable because we have the situation with the > implementation that the control over ancestor files is fine-grained (i.e. > during scripting the file rather than at the start by parsing "imports" which > the included files behaviour assumed). I think you made this decision for > implementation ease as well as accuracy, but if you want now to > automatically retract things further than target region in certain cases, > that definitely looks like a Coq-specific function. Actually, I realised that we do have the retraction behaviour you described for Isabelle already... If the current Coq mechanism is using proof-register-possibly-new-processed-file, we could make the retraction operation you want generic, but we'd need to implement the span based mechanism (i.e. recording the included files in the Require-like span) in the generic code too. It doesn't seem worth doing this generically because, at least for Isabelle, we had already decided to put the dependency management in the prover. Isabelle issues messages like "Proof General, you can unlock file XXX.thy" that are obeyed dumbly by PG. So the span based mechanism would conflict/overlap with that. Another way to get the behaviour for Coq might have been to implement a wrapper around coqtop that spits out these messages at appropriate points, and hope that the Coq code could be patched at some point. - D. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] no deactivation-hooks when killing fully asserted active buffer
is there viewvc and cvshistory running on the Proof General cvs? There's a handy view via Mercurial here courtesy of Markarius Wenzel (hopefully he won't mind me advertising) http://www4.in.tum.de/~wenzelm/cgi-bin/repos.cgi/ProofGeneral/ I've committed a patch to proof-protected-process-or-retract now which fixes this problem and I think your test case works. I don't see this. Here, coqtop still survives when I kill a completely asserted active scripting buffer. The reason seems to be that the unless now causes proof-protected-process-or-retract to return nil and then the progn in proof-deactivate-scripting-auto, which contains the deactivation hooks, is skipped. OK, let me take a look, I probably missed that the return value was being used. I saw the killing but maybe it was happening at the wrong moment which prompted my question below... But there may be some further issues (try the coq autotest script) OK, I do "make test.coq" and then I see some flickering and finally emacs hangs. What is the proposed way to use the autotest? Just as you did, Emacs shouldn't hang! But that might be a bug in the test as I tried to put in a multiple file test. You can set debug-on-signal to interrupt and get a backtrace. coqtop is killed via proof-shell-exit inside proof-deactivate-scripting-hook, that's inside the deactivation action, isn't it? but I'm seeing it being started after switching buffers and beginning scripting somewhere else, e.g. on the first non-comment element of the file. Yes, that's the desired behavior: You can freely switch buffers, but as soon as you start scripting in a buffer different from the active scripting buffer, then the coptop process is killed. OK, "as soon as you start scripting" includes comments, i.e. on making the buffer active for scripting? That's what I expected (and maybe what you intended!). Cheers - D. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] no deactivation-hooks when killing fully asserted active buffer
I don't see this. Here, coqtop still survives when I kill a completely asserted active scripting buffer. OK confirmed, what happens is that the hook functions are not run because the call is in a path in the code where it is assumed that we haven't changed the state of the buffer after all. Previously that could only happen because the user refused to completely process or retract in a partly completed buffer, but now it can happen because you want to sometimes run this function when the buffer is already completely processed or retracted. proof-script-deactivate scripting is by now quite garbled with the accumulated logic and your new flag which tells it to sometimes ignore the old logic! Could you try making a separate path/function for your desired behaviour first? Then we can combine back and clean up this function. i.e., duplicate some of the code in the body of proof-deactivate-scripting in a new function. OK, I do "make test.coq" and then I see some flickering and finally emacs hangs. What is the proposed way to use the autotest? The hangs seems to be a deadlock in proof-shell-wait that happens with the new way Coq is started with multiple files. I'm not sure why, perhaps because it gets called before the shell has been completely initialised. I removed that line from the tests for now, it works without the wait. - D. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] how to unlock ancestors
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. Looks good, thanks. - D. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] no deactivation-hooks when killing fully asserted active buffer
On 21/01/11 10:06, Hendrik Tews wrote: David Aspinall writes: Do you want to repair by adding a test for fully processed buffer? I reused an existing test case, see the description in coq/ex/test-cases/retract-completely-asserted/README. OK, I committed a patch now (not quite the one I sent you off list) which ensures that the hook function is run. 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" instructions. And I don't get an error! - D. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] no deactivation-hooks when killing fully asserted active buffer
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 Great! BTW, I think the retraction is a bit clunky in the UI because it makes the pointer leap to the top of the 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. OK, understood. 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.) Yes, I see the same and it is the last point that I was querying. I suspect what is happening is that you are killing the process at a place in the code that is not expecting this to happen (i.e., deactivating scripting). Whenever a command is sent to the prover, it is cranked up automatically if it is not running already. But comments are skipped in the interface, hence the behaviour above. This is a concern because it's probably assumed elsewhere in the code that the process is running whenever we have an active script buffer. So we should make sure that the process is cranked up in the script activation code too. Looking at the code, this is supposed to be done already by proof-shell-ready-prover in proof-activate-scripting. Maybe some state isn't being cleared which makes this function think it has nothing to do. I'll investigate (later...) Possibly related to this, I see some odd messages in the log from the Coq autotest examples, where the code is trying to find a process connected to a script buffer rather than the *coq* buffer. Run "make test.coq" (see error "Buffer f.v has no process") - D. PS I'd prefer to move this discussion to the trac rather than mailing list. It's a good way of recording the open issues, any way. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] Flushing old coq multiple file support
Nor me -- but notice that the CVS server has been having problems lately and is offline at the moment. I hope they will fixed it by tomorrow. - David On 15/02/11 16:07, Pierre Courtieu wrote: No problem for me. P. 2011/2/14 Hendrik Tews mailto:t...@os.inf.tu-dresden.de>> 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 -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] Inverse of proof-register-possibly-new-processed-file?
[ Hendrik - you asked me to follow up on this, below is the message I sent before to you 25/1, not sent to the list. ] When this is driven by messages from the prover, this function in proof-shell.el does the job: proof-shell-process-urgent-message-retract It uses proof-restart-buffers which you might want to reuse, does a bit more cleanup than your version. - D. On 25/01/11 14:47, Hendrik Tews wrote: 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 ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] proof tree visualization -- where to commit?
Looks impressive! I agree, use a branch for now until we can release PG 4.1 and then merge back in. - D. On 13 Apr 2011, at 08:29, Hendrik Tews wrote: > 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 ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] ChangeLog branch chaos
> 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. I think this is a fine solution. We haven't used branches much (partly because they are a mess in CVS), and the idea is that they contain experimental developments before being merged back in, the history on the main trunk should be what's most relevant to most users/developers. Makarius's Mercurial mirror provides a nicer way to browse changes anyway. I am keen to use a more modern distributed system but it probably means choosing an external provider rather than trying to get the University to provide yet another semi-supported tool that works at the beginning and then rusts. Sourceforge is the most likely candidate. - David ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] ChangeLog branch chaos
I'd recommend Savannah (either as a GNU or a non-GNU project). interesting idea, good choice of VC systems there, not just bzr Which reminds me: it would be nice to include PG into the GNU ELPA (a package archive from which Elisp packages can be installed conveniently via package.el). If you agree this is a desirable goal, then we'd need to track down all the non-trivial contributors to get them to sign some copyright assignment. I agree it would be nice and I wrote a package.el target a while ago (untested though). It would also be a good exercise to clean up/assign copyrights clearly -- although I'm not keen to do that myself, 8-(. - D. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] ChangeLog branch chaos
I would not expect a paragraph that starts with "modern" end with "Sourceforge". They added some half-harted support for Mercurial, Bazaar, Git some years ago, and people rightly complained that it was "too late and too little". There are several reasons to suggest sf. One is the provision of trac. I'm very keen on having a good issue tracker and haven't been impressed by what I've seen in Google code or Github when I last looked. This is way more important to me than support for multiple forked repositories managed in a social way --- although I agree that doing this for proofs would be pretty interesting. I've heard bitbucket.org is nice for Mercurial although I'm not sure if it's tracker is/will become Jira (Atlassian's well respected commercial tracker tool). - D. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] Why does proof-retract-until-point call proof-activate-scripting?
> 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. (As an aside: the PA side of the contract is the important one: the idea behind PGIP was to turn this into a uniform protocol which could enable richer, generic, user interfaces that *appear* to enable more elaborate interaction in the UI but using the more restricted protocol behind the scenes with the prover) > 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. Yes, of course, the use cases that you describe are very common and a common complaint about working with PG -- partly because it forces this low-level view of what is happening with the prover state abstraction directly in the UI. > 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? Is there a major drawback to killing and restarting in this case? Earlier you said that loading compiled files was so cheap it didn't matter to redo this. Is the issue that the UI loses this state (i.e. which files have been processed)? Perhaps we need to cache the list of processed files and arrange for them to be automatically required again (and locked in PG) on restart? - D. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] proof-follow-mode in invisible buffers
> 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? ] > 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? 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. - D. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] Re: auto coppile hangs emacs
> 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. 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. > There seems to be no way around aborting proof-shell-exec-loop in > the middle and restarting it when the compile job has finished. No, but that seems OK: this should just appear as if the prover is busy, so preventing undo, etc. (You may need to take extra action on interrupts) 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). - D. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] setting completion-ignored-extensions
To come back on this:
I agree that it would be sensible to set completion-ignored-extensions
for Coq, given that one does not usually want to open .vo, .glob files
in the editor.
Hendrik, do you want to add this for Coq? 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.
Cheers,
- David
On 29/03/11 12:08, Pierre Courtieu wrote:
OK then.
Cheers,
P.C.
2011/3/29 Hendrik Tews:
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
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
Re: [PG-devel] setting completion-ignored-extensions
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. I suppose you are right, it should be set early and it makes sense to put in proof-assistant-table because that configures the main file name extensions. Do you want to try that? Watch out for the AUTOMODE-REGEXP optional last column (not currently used but was in the past). - D. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] setting completion-ignored-extensions
As Emacs maintainer I recommend package maintainers to setup their "foo-site.el" such that it is (mostly if not completely) auto-generated by something like update-directory-autoloads. In such a situation a simple ;;;###autoload (add-to-list 'completion-ignored-extensions ".vo") in coq.el will do the trick. Much neater idea... although at the moment our autoloads are only generated for the generic code and one might hope that e.g. using Isabelle doesn't automatically make .vo files unreadable -- in case Isabelle would use that extension for something else (it probably doesn't, but). - D. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] defpacustom customization groups
Thanks for pointing this out. At one point it seemed useful to also have a separate group for things managed automatically by sending commands to the prover (i.e. proof-assistant-setting). I've simplified it now to instead use the proof assistant group directly since the defpacustom settings are not really internal either. Things declared with defpgcustom will be put into the internal group (e.g. Coq-config). For follow up issues, please see http://proofgeneral.inf.ed.ac.uk/trac/ticket/402 - D. On 14/02/11 14:22, Hendrik Tews wrote: 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 ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] Small patch for Coq ProofGeneral bindings
On 03/06/11 12:27, Pierre Courtieu wrote: OK for me. Thanks for taking the time to submit this. If there is no objection I will commit this. P.C. Please go ahead P.C.! Thanks - D. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
[PG-devel] 4.1RC2 available
Dear All, I've made a second release candidate for PG 4.1 which should fix recent Coq parsing issues. Could I persuade people to try it out, to iron out any final problems before release? See main download page, http://proofgeneral.inf.ed.ac.uk/download. Thanks a lot, - David ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] A few major bugs about exiting ProofGeneral with current CVS version
Hi Hendrik Thanks for the discussion on this: > 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. I followed up on Trac. I guess solution 2 would be better, but I don't object if you prefer to implement solution 1. Best wishes, - David -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ___ 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 release ever?
I am sure it will happen *eventually*. It would be nice to precede/coincide with Isabelle's next release. There is a new release candidate available now (RC5) which contains the recent (mainly Coq-related) fixes. I hope this will be the last RC and not contain show stoppers! - David On 11/09/11 14:41, Makarius wrote: Since we are approaching the next official Isabelle release (probably October 2011), this is the same procedure as everytime. Is there any serious release schedule for PG 4.1? Just before Isabelle2011 it was planned to happen within a few days before our release, then new features came it. Now we are 8 months later ... ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] PG 4.1 release ever?
> BTW, http://proofgeneral.inf.ed.ac.uk/download still shows RC4. Oops, committing web page failed -- will fix tomorrow, thanks for note. > +(if (and window-system (fboundp 'tool-bar-mode)) (tool-bar-mode t)) OK, this is likely to be contentious for Emacs experts who prefer the toolbar off and want some way to switch it off, or whoever made the odd decision in that Mac port to turn it off by default, but I'm not going to argue with you putting it in the Isar startup. It certainly is helpful for beginners. > diff -r ProofGeneral-4.1pre101216/generic/proof-useropts.el > ProofGeneral-4.1pre101216-p1/generic/proof-useropts.el > 121c121 > < (defcustom proof-strict-read-only 'retract > --- >> (defcustom proof-strict-read-only t > 345c345 > < (defcustom proof-full-annotation t > --- >> (defcustom proof-full-annotation nil > > My tendency is to ignore the latter and ship PG 4.1 final as is. The first default should be robust now (a race condition was fixed in Trac #403). I've committed the second change. I've had other power users object to the mouse hovers and having trouble finding out how to switch them off, although it is in the user options menu. And given the assumptions made (still?) in Isabelle about trying things asynchronously when quiet mode is disabled we might as well have the speedier default. Besides, people will think that this kind of capability is only possible in jEdit then, 8-). - D. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] PG 4.1 release ever?
OK, I will include RC5 in the next Isabelle test bundle that should be published within the next few days. BTW, http://proofgeneral.inf.ed.ac.uk/download still shows RC4. I've updated this now, and the RC5 tarball is slightly updated since Friday, with some improved documentation as well as configuration patches discussed. Ideally this will really be final RC... - D. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] PG 4.1 release ever?
+ +(if (and window-system (fboundp 'tool-bar-mode)) (tool-bar-mode t)) + +;; ;; Unicode ;; That doesn't sound right: tool-bar-mode is enabled globally by default, so forcefully re-enabling it can only undo the user's preference. The standard Mac port seems to disable it globally by default, this is what Makarius is trying to address. The code he's showing is only invoked when starting PG via Isabelle's wrapper script, not for all users with all provers, which I think makes it less objectionable. If a user is Emacs-savvy enough to not want the toolbar they can probably start Emacs directly and then load up PG and Isabelle (personally how I've always done it). - D. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
[PG-devel] PG 4.1 released!
Dear PG-dev'ers, This morning I made the release of PG 4.1, almost a year after 4.0. I plan to announce a little bit more widely later this week, please let me know asap if there are any hiccups. Meanwhile, a big Thank-You to all on this list who have contributed improvements and bug reports and testing, I'm very grateful. - David ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
[PG-devel] Possible License Change
Dear PG developers, We're considering a change of license for Proof General (Emacs) from GPL to a BSD-style license (probably the Modified BSD). The main reason for a change to a more permissive license is so that colleagues at MSR and elsewhere can collaborate more easily with us. I expect/hope that this would not impact any of the 3rd party packagers and Linux distributions shipping Proof General. I'm waiting for University folk to discuss further with me on exact details, but wanted to check first with PG developers whether anyone would raise objection. The simplest plan is probably to switch license with the next release version. Once there is a clearer proposal for the precise license and switch plans, I'll consult on the users list. If you have any concerns, please let me know. Best wishes, - David ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] Proof-tree merge
Thanks to Hendrik for this impressive addition! I have made a pre-release today which distributes the new feature: http://proofgeneral.inf.ed.ac.uk/releases/ProofGeneral-4.2pre120104.tgz Happy New Year, - David On 03/01/12 10:29, Hendrik Tews wrote: 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 ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] PGIP warning messages
Hello Edward Interesting that you're trying this! Although I should warn that we haven't been actively developing the PGIP infrastructure for a while: which interface are you hoping to use it with? Anyway, you should have no problem with multiple in PGIP. You need to set the fatality attribute to "warning" (or anything except "fatal"/"panic"). The restriction you mention applies to the plain text protocol used inside Emacs for real errors, which correspond to PGIP . Hope this helps, - David On 6 Apr 2012, at 04:15, Edward Z. Yang wrote: > Hello all, > > I'm working on partial PGIP support Coq, and one thing that I would like > to support is the case when Coq outputs "warning" messages, of which > there are many but which are nonfatal. I'm wondering what the right > tag for these are. is not correct, because we're only > allowed to have one before . Is correct? > It seems too generic, and where am I supposed to attach other metadata? > > Cheers, > Edward > ___ > ProofGeneral-devel mailing list > ProofGeneral-devel@inf.ed.ac.uk > http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel > -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] Re: PGIP warning messages
For this one I'm not sure if we finalised a markup form that distinguished the different semantic parts of proofstate output, although it was certainly discussed and seems useful. The Eclipse interface uses an xslt style sheet to render to an HTML widget, so you could add your own tags and interpret them as you like. I would be tempted to duplicate the names of the hypotheses in attributes, ..., so they are there for the interface to manipulate. - David On 6 Apr 2012, at 08:29, Edward Z. Yang wrote: > In sort of the same vein, in Coq, we have named hypotheses in our > proof contexts which render like: > > Hyp0 : Hyp (P x) > Hyp1 : Hyp (P z) > > or (P x) (or (forall y : U, P y) False) > > I'd like to add some PGML so that it looks something like this: > > > > Hyp0 : Hyp (P x) > Hyp1 : Hyp (P z) > > > or (P x) (or (forall y : U, P y) False) > > > > But I don't know what the right PGIP/PGML tags are. > > Edward > > Excerpts from Edward Z. Yang's message of Thu Apr 05 23:15:50 -0400 2012: >> Hello all, >> >> I'm working on partial PGIP support Coq, and one thing that I would like >> to support is the case when Coq outputs "warning" messages, of which >> there are many but which are nonfatal. I'm wondering what the right >> tag for these are. is not correct, because we're only >> allowed to have one before . Is correct? >> It seems too generic, and where am I supposed to attach other metadata? >> >> Cheers, >> Edward > ___ > ProofGeneral-devel mailing list > ProofGeneral-devel@inf.ed.ac.uk > http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel > -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] PGIP warning messages
Sounds interesting! Good luck and let us know if we can help again. - D. On 6 Apr 2012, at 09:04, Edward Z. Yang wrote: > Hello David, > > I'm actually building a domain-specific frontend for Coq, and I didn't > feel like reimplementing all of ProofGeneral's parsing hacks! It's > not much: it's going to be a pedagogical theorem prover for first > order logic, but the idea is to closely support different deduction > styles (e.g. natural deduction, sequent calculus, etc.) > > Thanks, > Edward > > Excerpts from David Aspinall's message of Fri Apr 06 03:49:29 -0400 2012: >> Hello Edward >> >> Interesting that you're trying this! Although I should warn that we haven't >> been actively developing the PGIP infrastructure for a while: which >> interface are you hoping to use it with? >> >> Anyway, you should have no problem with multiple in PGIP. >> You need to set the fatality attribute to "warning" (or anything except >> "fatal"/"panic"). The restriction you mention applies to the plain text >> protocol used inside Emacs for real errors, which correspond to PGIP >> . >> >> Hope this helps, >> >> - David >> >> On 6 Apr 2012, at 04:15, Edward Z. Yang wrote: >> >>> Hello all, >>> >>> I'm working on partial PGIP support Coq, and one thing that I would like >>> to support is the case when Coq outputs "warning" messages, of which >>> there are many but which are nonfatal. I'm wondering what the right >>> tag for these are. is not correct, because we're only >>> allowed to have one before . Is correct? >>> It seems too generic, and where am I supposed to attach other metadata? >>> >>> Cheers, >>> Edward >>> ___ >>> ProofGeneral-devel mailing list >>> ProofGeneral-devel@inf.ed.ac.uk >>> http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel >>> >> > -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ___ 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*
Hi, I'm not sure if the reason for the cursor change was explained: the hollow box indicating cursor position was sometimes causing confusion with mathematical notation appearing in the output (e.g. box operator). > I believe setting cursor-in-non-selected-windows to nil (and > leaving cursor-type unchanged) in *goals* and *response* would be > more appropriate. I agree, especially since its effect is local. Not sure why the other setting was chosen originally. Thanks for the improvement. I've pushed another pre-release just now. - David ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] Emacs 24
Thanks for the report, I've put it into Trac here:
http://proofgeneral.inf.ed.ac.uk/trac/ticket/442
Would help to clarify: which version of PG you are using?
- D.
On 15/06/12 09:34, Paolo Herms wrote:
Hello,
I tried proofgeneral on the newly released emacs and it works at first sight
but seems to have some problems with long input, like the one produced by this
bash script:
function mk { echo "Check fun n, match n with "; s=O; for ((i=0;i<$1;i++)); do
echo " | $s => n"; s="(S $s)"; done; echo " | _ => n end."; }> x.v
Processing x.v for small arguments like
$ mk 10
works but for bigger ones like
$ mk 100
it blocks without consuming cpu.
Weirdly for me the threshold seems to be 42...
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
Re: [PG-devel] speed up Coq Proof General by processing complete proofs
On 09/08/12 11:11, Lionel Elie Mamane wrote: That's why (back when it was available), I preferred to use the "coq-interface" protocol rather than the "coqtop -emacs" protocol, which has chunking multiple commands cleanly. I haven't looked at it recently, but it seems to be the PCoq interface protocol was moved to the contribs, and can still be taken from there? Yves Bertot asked me years ago why Proof General never used this mechanism, and at the time I wasn't convinced it was much of a saving over sending commands individually. The simpler mechanism was a least common denominator for different systems and doesn't require special modifications to standard read-eval-print loops. These days it seems more likely that the communication would often dominate the processing time for a single command so batching on the prover side would clearly be a better mechanism. In fact, so is having the prover (or some intermediate component) manage the *whole* document, which is the PIDE model. If there was still enough Emacs love in the world we could surely have an Emacs mode for that! But porting PG to it might be more hassle than useful, and possibly the "Set/Unset Prompt" route would be more expedient. Yes, probably... The thing to watch out for is the error behaviour, though. If one command in a batch fails, PG needs to know which command is responsible (or else that the prover considers the whole transaction failed). - D. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
[PG-devel] Reboot: Release of PG 4.2
Dear PG devs, 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... I'm guilty myself with the experiment in Trac #444 (eager window layout), I will revert that change (Pierre, I understand from comments it wasn't what you wanted anyway, do you consider #444 solved with your own fixes now?). On the list of what's left http://goo.gl/uZg2b there are a couple of Coq input issues that users have raised (#296,#445) as well as a mysterious problem with long inputs (#447). If anyone has a moment to look at any of those I'd be grateful, otherwise we probably have to push them onto the 4.3 list. Cheers, - David ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] Reboot: Release of PG 4.2
Thanks for followup, Hendrik. 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 think it's best to disable it for now, have just done so. There is some more effort available to work on this again after Oct (Hendrik, I'll talk to you about this separately). 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 That's a good suggestion. Unfortunately I have very little bandwidth personally this month: to help smooth things out effectively I'd like to fix/extend the automatic tests and add proper regression tests for fixed bugs (Coq parsing is the most thorny). I'd like to support Emacs 24 properly although there are API updates which are tricky to support in two versions --- esp when the rightly increasingly rigorous byte compiler tries to compile code for old versions and barfs. 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 Sounds good (if you want to add to Trac we can know when you've done these things). - D. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] Reboot: Release of PG 4.2
On 04/09/12 13:33, Stefan Monnier wrote: I'd like to support Emacs 24 properly although there are API updates which are tricky to support in two versions --- esp when the rightly increasingly rigorous byte compiler tries to compile code for old versions and barfs. I can probably help in this area, except that I do not know the concrete problems that need fixing. If you can send me some details, I can take a look at it. Thanks Stefan! I'll send you a message off list. - D. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] Tracker questions
Sorry (to all) for the problems with trac. The current instance will not be fixed by local sysadmins. We have a migration route to a supported Trac instance which means moving to svn, but an alternative would be to move to an outsourced system such as github. Meanwhile, I recommend simply ticking the "ticket details" on the timeline view: http://proofgeneral.inf.ed.ac.uk/trac/timeline there are not so many issues or comments that you won't be able to easily pick out relevant ones from there. So it's still pull, but you can always use the RSS feed at the bottom of the page... - D. On 14/09/12 14:11, Hendrik Tews wrote: 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 ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] Reboot: Release of PG 4.2
Hi Hendrik Thanks for the nudge --- no blockers I don't think, except extreme overwork, 8-). I'll try to push the button soon, just need a spare hour to run checks and update all the pieces. Apologies for the delay. - David On 17/10/12 15:25, Hendrik Tews wrote: 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 ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] pg-finish-tracing-display ?
Hi Hendrik, I am missing the documentation comment for pg-finish-tracing-display. What is it used for? I've just added it: "Handle the end of possibly voluminous tracing-style output. If the output update was slowed down, show it now" Tracing output is defined with a regexp, it isn't used by Coq. In Isabelle it's used when people want to debug looping simplifier rules, etc. Special treatment is because there can be masses of output which we don't want to eagerly parse, convert to symbols, display, etc as it's too expensive. (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...) Sounds exciting and ambitious!Let me know if I can help further. - D. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] first version of parallel background compilation for Coq
> 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? - David -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] proof-shell-pre-interrupt-hook ?
> I just came across proof-shell-pre-interrupt-hook. I can't find > any location where this hook is run. Am I missing something? Likely obsolete but let me check some old versions: http://proofgeneral.inf.ed.ac.uk/trac/ticket/457 -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ___ 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
> 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. I agree, please go ahead Pierre. > By the way is there a "emacs gui recommendations somewhere?" > > I don't know any. Me neither. There are recommendations about Emacs conventions scattered through the Lisp reference manuals and apart from that I try to follow what Emacs itself does and the standard applications it ships with. - D. -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ___ 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.2 byte-compilation fails with Emacs 24.2.90
Thanks, now at http://proofgeneral.inf.ed.ac.uk/trac/ticket/458. - D. On 30 Nov 2012, at 12:34, Ulrich Mueller wrote: > Byte-compilation of ProofGeneral 4.2 with the Emacs 24.2.90 pretest > version fails in pg-response.el: > > In toplevel form: > generic/pg-response.el:104:23:Error: `special-display-regexps' is an > obsolete variable (as of 24.3); use `display-buffer-alist' instead. > ___ > ProofGeneral-devel mailing list > ProofGeneral-devel@inf.ed.ac.uk > http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel > -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ___ 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
Hello Hendrik 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? Maybe prooftree input is different case to prover input. 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. A more robust mechanism might be to try to send new input from the main event loop instead, but that would be a significant reworking. (Or could you do that just for proof tree?) - David On 08/01/13 10:41, Hendrik Tews wrote: 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 ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] overlapping calls to proof-shell-filter
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? - D. On 09/01/13 20:53, Hendrik Tews wrote: Hi, here is a patch that solves the problem for me. Any comments? Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] status of support for Proof General
Hello Hendrik, It is a good idea to add a note to the trac. I would say that the support is currently by best efforts of people who have other jobs and little spare time -- such as you and I. I think there are other people on this list but probably no very active developers at the moment. (If anyone is keen to devote support effort to PG, they should get in touch with me, there might be ways to help provide a bit of project work.) In general, the support problem is of course a typical problem with research software in our discipline, where it seems hard to get funding to provide baseline support for a system, and it is often done "on the side" with some research topic. Proof General has only ever been supported indirectly by minor contributions from other research projects --- impressive that it has lasted and been maintained so well despite that, and I'm grateful for all the time people have dedicated. - David On 26/02/13 14:21, Hendrik Tews wrote: 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 ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] urgent message hide errors?
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? From Proof General's point of view, the first of these is the problem, since the behaviour has been well specified for a long time and I guess that Coq's behaviour has changed over time. See fragment of documentation from proof-shell-filter below. - David Error or interrupt messages are expected to terminate an interactive output and appear last before a prompt and will always be processed. Error messages and interrupt messages are therefore *not* considered as urgent messages. see: http://proofgeneral.inf.ed.ac.uk/htmlshow.php?title=Proof+General+adapting+manual&file=releases%2FProofGeneral%2Fdoc%2FPG-adapting%2FPG-adapting_15.html#index-proof_002dshell_002dfilter ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
[PG-devel] Reminder: CICM/MKM deadline nearly here!
Dear PG users and developers, Hopefully many of you will know the CICM conference and have seen the CFP: http://www.cicm-conference.org/2013/cicm.php?event=&menu=cfp I'm the track chair for MKM (Mathematical Knowledge Management) this year, I'm keen to see plenty of submissions for our track to put together an interesting programme. If you've been using Proof General (or even another tool) to manage large developments, maybe there is something to write about? The deadline for final submissions is Fri 8th March (abstracts ideally by this Friday). Best Wishes, - David ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] non-fatal warnings for make compile
Hendrik, Thanks a lot for tackling this, I looked at it a while ago and saw it was going to be a nuisance to fix... - David. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] ProofGeneral symlink?
I don't feel strongly about it. If it causes a problem, let's remove it. - David On 26/05/2013 21:44, Hendrik Tews wrote: 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 ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] non-fatal warnings for make compile
This fix was helpful but unfortunately means that developers are more likely to introduce bugs unless they run make clean; make check before committing. E.g., I have just tried to make a pre-release but I now get the error In toplevel form: coq/coq.el:1040:67:Error: reference to free variable `coq-project-filename' (Hendrik, I think this is yours?) - David On 22/05/13 21:40, Hendrik Tews wrote: 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 ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
[PG-devel] Move to Github
Dear PG Devs, 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 and propose small patches. And it looks as if the Github issue tracking system is now reasonable enough to use that we can move things over from trac. Last time I suggested making a license change as well, this time I'm not suggesting that. Any objections to doing this? The plan would be to make a release of version 4.3 first, then embark on a move and clean up. Best wishes, - David ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] non-fatal warnings for make compile
On 04/07/13 12:21, Hendrik Tews wrote: If you think these compilation errors are an issue, I volunteer to implement one or both suggestions. Thanks indeed! I think an automatic build would definitely be nice to have if you have inclination/interest. Recently I found about Travis https://travis-ci.org/ which appears to offer a free build server for OS projects hosted on Github. Don't know quite how they finance the cycles (but building PG shouldn't take many). - D. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] Move to Github
On 11/07/2013 08:00, Hendrik Tews wrote: 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. A plain text file can be shown like the README (linked on home page) http://proofgeneral.inf.ed.ac.uk/fileshow.php?file=releases%2FProofGeneral%2Fcoq%2FREADME (In future I hope to move to a statically generated site, we can include Markdown files in the same way) - D. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] Migrating Proof-General to Git
Hello Clément, all, This is a very timely message! I have indeed started to think of making this migration again. Although I don't have a lot of time to work on it, I would like to see it done. There is an old attempt here: https://github.com/DavidAspinall/ProofGeneral but it didn't get updated and indeed we could do a better job with the user names. I'll take a look at your attempt soon (which tool did you use?). I agree that we probably need to set a cut-off date and disconnect the old CVS repo, the sync options don't look robust. What I could most do with help is converting the packaging/publishing tools to use the github repo. (The web pages also badly need replacing but I'm not sure if anyone would have the stomach to do that?) I'm slightly wary of needing to manage merge requests so I thought of using a GitHub organisation for this to share the job and to host a central repo. Hence: https://github.com/ProofGeneral If anyone on this list would like to join, please tell me your GitHub user name. - David On 20/04/2015 19:29, Clément Pit--Claudel wrote: Hi Pierre and David (and proofgeneral-devel), There were talks a while ago on the mailing list about a migration to git. I think this would be really cool. I experimented with various export options, and came up with the repo at https://github.com/cpitclaudel/proof-general/ . The problem with the process that I used is that it makes it hard to incrementally track changes (we would need to migrate once and for all). Most of the history seems to have been preserved just fine, but it would be nice to map CVS usernames to proper names and emails; the authors in the CVS tree seem to be [assia, crr, cxl, da, djs, fionam, gklein, hhg, joheras, lego, makarius, mark, markus, monnier, patrl, pier, proofgen, pxc, sberghof, tews, tms, weber]. Is there a list of names and emails somewhere matching these usernames? It would be great to get feedback on the history as recorded in https://github.com/cpitclaudel/proof-general/ ; also, if a migration was eventually decided, I could help with the process. One reason for migrating to Git and hosting on Github would be lowering the barrier of entry to new contributors: many of the changes that I made in my company-coq plugin could in fact be ported to proof-general. It could also allow for simplified distribution of extensions and updated versions, via emacs' package system. Clément. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Re: [PG-devel] Migrating Proof-General to Git
Hello Clément, Sorry I haven't looked in detail yet, hope soon. Thanks for sending the tips of what you did. I want to try again to get the names right and maybe some other minor surgery (looking at reposurgeon for that but haven't tried it yet). I think your suggestion for Trac is sensible. We might leave it up but make it read only, perhaps. I've made a team for PG developers on GitHub, Clément you are invited, anyone else please let me know your GitHub username. - David On 26/04/2015 02:01, Clément Pit--Claudel wrote: > Hi David & list, > > David: Have you had time to look at my attempt to migrate to git? My username > on github is cpitclaudel. > > List: I had a quick look at options to migrate trac tickets to GitHub. There > seems to exist solutions, but nothing too robust. There hasn't been loads of > activity on trac in the last few years though, so I'm not sure if such a > migration is really needed. And (as opposed to CVS) there is no need to > retire Trac immediately after the migration. > > Clément. > > On 04/20/2015 03:49 PM, David Aspinall wrote: >> Hello Clément, all, >> >> This is a very timely message! I have indeed started to think of making >> this migration again. Although I don't have a lot of time to work on it, I >> would like to see it done. There is an old attempt here: >> >> https://github.com/DavidAspinall/ProofGeneral >> >> but it didn't get updated and indeed we could do a better job with the user >> names. I'll take a look at your attempt soon (which tool did you use?). >> >> I agree that we probably need to set a cut-off date and disconnect the old >> CVS repo, the sync options don't look robust. What I could most do with >> help is converting the packaging/publishing tools to use the github repo. >> (The web pages also badly need replacing but I'm not sure if anyone would >> have the stomach to do that?) >> >> I'm slightly wary of needing to manage merge requests so I thought of using >> a GitHub organisation for this to share the job and to host a central repo. >> Hence: >> >> https://github.com/ProofGeneral >> >> If anyone on this list would like to join, please tell me your GitHub user >> name. >> >> - David >> >> On 20/04/2015 19:29, Clément Pit--Claudel wrote: >>> Hi Pierre and David (and proofgeneral-devel), >>> >>> There were talks a while ago on the mailing list about a migration to git. >>> I think this would be really cool. I experimented with various export >>> options, and came up with the repo at >>> https://github.com/cpitclaudel/proof-general/ . The problem with the >>> process that I used is that it makes it hard to incrementally track changes >>> (we would need to migrate once and for all). >>> >>> Most of the history seems to have been preserved just fine, but it would be >>> nice to map CVS usernames to proper names and emails; the authors in the >>> CVS tree seem to be [assia, crr, cxl, da, djs, fionam, gklein, hhg, >>> joheras, lego, makarius, mark, markus, monnier, patrl, pier, proofgen, pxc, >>> sberghof, tews, tms, weber]. Is there a list of names and emails somewhere >>> matching these usernames? >>> >>> It would be great to get feedback on the history as recorded in >>> https://github.com/cpitclaudel/proof-general/ ; also, if a migration was >>> eventually decided, I could help with the process. One reason for migrating >>> to Git and hosting on Github would be lowering the barrier of entry to new >>> contributors: many of the changes that I made in my company-coq plugin >>> could in fact be ported to proof-general. It could also allow for >>> simplified distribution of extensions and updated versions, via emacs' >>> package system. >>> >>> Clément. >>> >> >> > -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ___ 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 Pierre/all, Sorry for delay replying, I was away then returned but now very busy with start of term... Have made a new Admin team now with you and Clément as members. BTW, a mapping of names->emails is in the Makefile somewhere, although it may be incomplete (try "make ChangeLog"). If we're going to switch to Github properly I'd like to switch off the cvs server and then update the webpages, would you be able to help with the web page updates too? There is another repo that I can add to GitHub. - David On 14/09/2015 17:00, Pierre Courtieu wrote: > Hi pg dev! > > Trying to wake up this thread 5 months later. > > Coq-8.5 is not yet released but its beta version is already quite > spread and used. IMHO it is the right time for a release of PG. > > I suggest that Clément performs the migration to github now and that > we make a release quickly from git. The best would be an elpa (or > melpa) package release + a tarball. > > David is it ok for you? > > Best regards, > Pierre > > > > > > > > 2015-04-28 14:36 GMT+02:00 Clément Pit--Claudel : >> On 04/28/2015 04:53 AM, David Aspinall wrote: >>> Hello Clément, >>> >>> Sorry I haven't looked in detail yet, hope soon. Thanks for sending the >>> tips of what you did. I want to try again to get the names right and >>> maybe some other minor surgery (looking at reposurgeon for that but >>> haven't tried it yet). >> >> No problem, thanks for the quick response! >> cvs2git has a mapping of cvs usernames to git usernames, so it should just >> be a matter of finding the names and emails of each PG developer. >> >>> I think your suggestion for Trac is sensible. We might leave it up but >>> make it read only, perhaps. >> >> That sounds great. >> >>> I've made a team for PG developers on GitHub, Clément you are invited, >>> anyone else please let me know your GitHub username. >> >> Great, thanks! >> >>> - David >>> >>> On 26/04/2015 02:01, Clément Pit--Claudel wrote: >>>> Hi David & list, >>>> >>>> David: Have you had time to look at my attempt to migrate to git? My >>>> username on github is cpitclaudel. >>>> >>>> List: I had a quick look at options to migrate trac tickets to GitHub. >>>> There seems to exist solutions, but nothing too robust. There hasn't been >>>> loads of activity on trac in the last few years though, so I'm not sure if >>>> such a migration is really needed. And (as opposed to CVS) there is no >>>> need to retire Trac immediately after the migration. >>>> >>>> Clément. >>>> >>>> On 04/20/2015 03:49 PM, David Aspinall wrote: >>>>> Hello Clément, all, >>>>> >>>>> This is a very timely message! I have indeed started to think of making >>>>> this migration again. Although I don't have a lot of time to work on it, >>>>> I would like to see it done. There is an old attempt here: >>>>> >>>>> https://github.com/DavidAspinall/ProofGeneral >>>>> >>>>> but it didn't get updated and indeed we could do a better job with the >>>>> user names. I'll take a look at your attempt soon (which tool did you >>>>> use?). >>>>> >>>>> I agree that we probably need to set a cut-off date and disconnect the >>>>> old CVS repo, the sync options don't look robust. What I could most do >>>>> with help is converting the packaging/publishing tools to use the github >>>>> repo. (The web pages also badly need replacing but I'm not sure if >>>>> anyone would have the stomach to do that?) >>>>> >>>>> I'm slightly wary of needing to manage merge requests so I thought of >>>>> using a GitHub organisation for this to share the job and to host a >>>>> central repo. Hence: >>>>> >>>>> https://github.com/ProofGeneral >>>>> >>>>> If anyone on this list would like to join, please tell me your GitHub >>>>> user name. >>>>> >>>>> - David >>>>> >>>>> On 20/04/2015 19:29, Clément Pit--Claudel wrote: >>>>>> Hi Pierre and David (and proofgeneral-devel), >>>>>> >>>>>> There were talks a while ago on the mailing list about a migration to >>&g
Re: [PG-devel] Migrating Proof-General to Git
Hi Erik, > If you are thinking of adding a GitHub repo dedicated to the webpages > sources, maybe it would be convenient to host the webpages themselves > at GitHub too? Because according to https://pages.github.com/ and > https://help.github.com/categories/github-pages-basics/ it would > suffice to name this extra repo "proofgeneral.github.io" ... > What is your opinion? Sure, maybe this is a better hosting provider than University of Edinburgh, I don't really mind. We could easily redirect from proofgeneral.inf. Erik, I've just invited you to join the admin group, apologies I missed your message from earlier in the year. Best wishes, - David -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] Last Call for Papers: Workshop on User Interfaces for Theorem Provers (UITP 2016 @ IJCAR), Coimbra, Portugal, Deadline May 17th *NEW* (was May 9th, 2016)
Subject: [Stp] Last Call for Papers: Workshop on User Interfaces for Theorem Provers (UITP 2016 @ IJCAR), Coimbra, Portugal, Deadline May 17th *NEW* (was May 9th, 2016) Date: Fri, 6 May 2016 06:40:13 + From: Grov, Gudmund To: s...@macs.hw.ac.uk , d...@macs.hw.ac.uk Last Call for Papers UITP 2016 12th International Workshop on User Interfaces for Theorem Provers in connection with IJCAR 2016 July 2nd, 2016, Coimbra, Portugal http://www.informatik.uni-bremen.de/uitp/current/ * NEW Submission deadline: May 17th, 2016 * -- NEWS: - Invited Speaker: Sylvain Conchon (LRI, France) giving a talk about "AltGr-Ergo, a graphical user interface for the SMT solver Alt-Ergo" - Submission deadline postponed by one week to May, 17th, 2016 -- The User Interfaces for Theorem Provers workshop series brings together researchers interested in designing, developing and evaluating interfaces for interactive proof systems, such as theorem provers, formal method tools, and other tools manipulating and presenting mathematical formulas. While the reasoning capabilities of interactive proof systems have increased dramatically over the last years, the system interfaces have often not enjoyed the same attention as the proof engines themselves. In many cases, interfaces remain relatively basic and under-designed. The User Interfaces for Theorem Provers workshop series provides a forum for researchers interested in improving human interaction with proof systems. We welcome participation and contributions from the theorem proving, formal methods and tools, and HCI communities, both to report on experience with existing systems, and to discuss new directions. Topics covered include, but are not limited to: - Application-specific interaction mechanisms or designs for prover interfaces Experiments and evaluation of prover interfaces - Languages and tools for authoring, exchanging and presenting proof - Implementation techniques (e.g. web services, custom middleware, DSLs) - Integration of interfaces and tools to explore and construct proof - Representation and manipulation of mathematical knowledge or objects - Visualisation of mathematical objects and proof - System descriptions UITP 2016 is a one-day workshop to be held on Saturday, July 2nd, 2016 in Coimbra, Portugal, as a IJCAR 2016 workshop. ** Submissions ** Submitted papers should describe previously unpublished work (completed or in progress), and be at least 4 pages and at most 12 pages. We encourage concise and relevant papers. Submissions should be in PDF format, and typeset with the EPTCS LaTeX document class (which can be downloaded from http://style.eptcs.org/). Submission should be done via EasyChair at https://www.easychair.org/conferences/?conf=uitp16 All papers will be peer reviewed by members of the programme committee and selected by the organizers in accordance with the referee reports. At least one author/presenter of accepted papers must attend the workshop and present their work. ** Proceedings ** Authors will have the opportunity to incorporate feedback and insights gathered during the workshop to improve their accepted papers before publication in the Electronic Proceedings in Theoretical Computer Science (EPTCS - http://www.eptcs.org/). ** Important dates ** Submission deadline: May 17th, 2016 Acceptance notification: June 6th, 2016 Camera-ready copy: June 20th, 2016 Workshop: July 2nd, 2016 ** Programme Committee ** Serge Autexier, DFKI Bremen, Germany (Co-Chair) Pedro Quaresma, U Coimbra, Portugal (Co-Chair) David Aspinall, University of Edinburgh, Scotland Chris Benzmüller, FU Berlin, Germany & Stanford, USA Yves Bertot, INRIA Sophia-Antipolis, France Gudmund Grov, Heriott-Watt University, Scotland Zoltán Kovács, RISC, Austria Christoph Lüth, University of Bremen and DFKI Bremen, Germany Alexander Lyaletski, Kiev National Taras Shevchenko Univ., Ukraine Michael Norrish, NICTA, Australia Andrei Paskevich, LRI, France Christian Sternagel, University Innsbruck, Austria Enrico Tassi, INRIA Sophia-Antipolis, France Laurent Théry, INRIA Sophia-Antipolis, France Makarius Wenzel, Sketis, Germany Wolfgang Windsteiger, RISC Linz, Austria Bruno Woltzenlogel Paleo, TU Vienna, Austria -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] PG and Coq ideslave mode
I did something like this once to support PGIP, which was a sort of pre-cursor of PIDE based on exchanging XML messages. You can find the source in the CVS repo PG Kit repo (Kit/src/pgemacs). But it probably isn't useful: it's about 10 years old and the case we wanted to allow was input coming voluntarily from the prover to PG (think progress/annotations etc), rather than the other way around. - David On 06/05/2016 11:48, Paul A. Steckler wrote: > Proof General defines a shell mode, proof-shell, and an associated > message filter. My thought now is to define an alternate-universe > shell mode, proof-shell-noprompt and an associated message filter. > > -- Paul > > > > On Fri, May 6, 2016 at 1:27 AM, Pierre Courtieu > wrote: >> I am sorry to say that I already asked myself about everything you >> asked here, and, despite you suggest more smart answers than I did >> myself I don't see any good enough idea yet. About the prompt: a *lot* >> of things (everything really) in pg depend on the fact that 1 command >> = 1 prompt exactly. >> >> Once again, don't dismiss starting from scratch without thinking a >> while about it. Actually large parts of pg could be reused. >> >> P. >> >> >> 2016-05-05 19:59 GMT+02:00 Clément Pit--Claudel : >>> I entirely agree with this point; I argued in this direction on a recent >>> coq-dev thread. >>> >>> On 2016-05-05 12:24, Paul A. Steckler wrote: I'm not a fan of this idea. The IDE and the prover should be only loosely-coupled, with a clearly-defined communication protocol between them. A plugin introduces a tight coupling between these components. Yes, it's only a plugin, so the scope of the coupling is limited. But it still seems undesirable to me. -- Paul On Thu, May 5, 2016 at 4:58 PM, Clément Pit--Claudel wrote: > Not entirely clear to me :) I think there'd be some amount of design work > there as well. > > On 2016-05-05 10:39, Paul A. Steckler wrote: >> With that toploop plugin installed on the coqtop side installed, what >> does Proof General see from its shell? >> >> -- Paul >> >> On Thu, May 5, 2016 at 4:34 PM, Clément Pit--Claudel >> wrote: >>> Hi Paul, >>> >>> Here's another approach that I forgot to mention: we could build a >>> separate Emacs toploop as a plugin, which would inherit most of >>> CoqIDE's toploop (you know that I have mixed feelings about that, but >>> it may be the most pragmatic approach). >>> >>> Clément. >>> >>> On 2016-05-05 10:17, Clément Pit--Claudel wrote: Hi Paul, You could indeed modify PG to handle the first prompt differently, or even Coq. In the long run, though, I don't think the approach is sustainable. PG is very much hardcoded to expect one prompt for every query it sends: thus, even though you may get something working pretty quickly by hacking around this prompt thing, I think we'll see more breakages with every evolution of the new protocol. Here's a slightly different idea. Right now, PG adds an abstraction layer on top of a REPL model. What you could do is reimplement the same abstraction, but on top of Coq's new asynchronous model. Concretely, my suggestion is to make a separate library to talk to Coq's new API, which would provide the same interface (proof-shell-invisible-command, proof-shell-ready-prover, proof-shell-invisible-cmd-get-result, etc.). I think this would make your life easier. You would: 1. Identify a small (hopefully) collection of functions that Coq-ProofGeneral actually depends on (some sort of semi-explicit interface, essentially). 2. Implement support for these functions using Coq's new API model 3. Modify the current implementation to call these functions or the legacy ones depending on the version of Coq. What do you think? Clément. On 2016-05-05 09:48, Paul A. Steckler wrote: > I've already mentioned the issue described below to Clément > Pit-Claudel > and Pierre Courtieu, maybe others on this list have thoughts on it. > > Proof General is welded to a model of receiving prompts from a prover. > After it's received a prompt, PG can send something back to the > prover. > > The ideslave (politically incorrectly-named) mode in Coq, developed > for CoqIDE abandons that model. In that mode, Coq just waits for XML > from an IDE, without first offering a prompt. > > In ideslave mode, it seems that Coq sends back responses wrapped in > tags, so you can use that as a pseudo-prompt. Hmm, I think the > prompt regexp would have to look for both the closi
Re: [PG-devel] PG and Coq ideslave mode
That sounds right (but could lead to confusion!). What I did was to fork a version of PG and cut it down to something fairly minimal. - D. On 06/05/2016 14:34, Paul A. Steckler wrote: The proof-shell mode comes with a lot of associated state, like regexps, buffers, etc. Some bits of that state would be useful in the new mode I'm creating, others not. I'm thinking that I can share the same state variables for the new mode, because I'll never have an active proof shell mode and the new mode active at the same time. Yes? I'd hate to have to duplicate state. If I load two .v files in emacs, it seems I can only work on one at a time using Proof General, and there's only one proof-shell mode window active. -- Paul On Fri, May 6, 2016 at 3:15 PM, David Aspinall wrote: I did something like this once to support PGIP, which was a sort of pre-cursor of PIDE based on exchanging XML messages. You can find the source in the CVS repo PG Kit repo (Kit/src/pgemacs). But it probably isn't useful: it's about 10 years old and the case we wanted to allow was input coming voluntarily from the prover to PG (think progress/annotations etc), rather than the other way around. - David On 06/05/2016 11:48, Paul A. Steckler wrote: Proof General defines a shell mode, proof-shell, and an associated message filter. My thought now is to define an alternate-universe shell mode, proof-shell-noprompt and an associated message filter. -- Paul On Fri, May 6, 2016 at 1:27 AM, Pierre Courtieu wrote: I am sorry to say that I already asked myself about everything you asked here, and, despite you suggest more smart answers than I did myself I don't see any good enough idea yet. About the prompt: a *lot* of things (everything really) in pg depend on the fact that 1 command = 1 prompt exactly. Once again, don't dismiss starting from scratch without thinking a while about it. Actually large parts of pg could be reused. P. 2016-05-05 19:59 GMT+02:00 Clément Pit--Claudel : I entirely agree with this point; I argued in this direction on a recent coq-dev thread. On 2016-05-05 12:24, Paul A. Steckler wrote: I'm not a fan of this idea. The IDE and the prover should be only loosely-coupled, with a clearly-defined communication protocol between them. A plugin introduces a tight coupling between these components. Yes, it's only a plugin, so the scope of the coupling is limited. But it still seems undesirable to me. -- Paul On Thu, May 5, 2016 at 4:58 PM, Clément Pit--Claudel wrote: Not entirely clear to me :) I think there'd be some amount of design work there as well. On 2016-05-05 10:39, Paul A. Steckler wrote: With that toploop plugin installed on the coqtop side installed, what does Proof General see from its shell? -- Paul On Thu, May 5, 2016 at 4:34 PM, Clément Pit--Claudel wrote: Hi Paul, Here's another approach that I forgot to mention: we could build a separate Emacs toploop as a plugin, which would inherit most of CoqIDE's toploop (you know that I have mixed feelings about that, but it may be the most pragmatic approach). Clément. On 2016-05-05 10:17, Clément Pit--Claudel wrote: Hi Paul, You could indeed modify PG to handle the first prompt differently, or even Coq. In the long run, though, I don't think the approach is sustainable. PG is very much hardcoded to expect one prompt for every query it sends: thus, even though you may get something working pretty quickly by hacking around this prompt thing, I think we'll see more breakages with every evolution of the new protocol. Here's a slightly different idea. Right now, PG adds an abstraction layer on top of a REPL model. What you could do is reimplement the same abstraction, but on top of Coq's new asynchronous model. Concretely, my suggestion is to make a separate library to talk to Coq's new API, which would provide the same interface (proof-shell-invisible-command, proof-shell-ready-prover, proof-shell-invisible-cmd-get-result, etc.). I think this would make your life easier. You would: 1. Identify a small (hopefully) collection of functions that Coq-ProofGeneral actually depends on (some sort of semi-explicit interface, essentially). 2. Implement support for these functions using Coq's new API model 3. Modify the current implementation to call these functions or the legacy ones depending on the version of Coq. What do you think? Clément. On 2016-05-05 09:48, Paul A. Steckler wrote: I've already mentioned the issue described below to Clément Pit-Claudel and Pierre Courtieu, maybe others on this list have thoughts on it. Proof General is welded to a model of receiving prompts from a prover. After it's received a prompt, PG can send something back to the prover. The ideslave (politically incorrectly-named) mode in Coq, developed for CoqIDE abandons that model. In that mode, Coq just waits for XML from an IDE, without f
Re: [PG-devel] Status of PGIP?
Essentially it's defunct. Isabelle 2014 uses some of the messages e.g., for configuring options on start up. But if we're dropping support for older Isabelle versions then it can be removed. I would be sad to see support for other provers being taken away though. We put a lot of effort into making it easy to configure Proof General to use with CLI tools (even bash). Maybe the script management code could be refactored into a standalone mode. I still see people in conferences cutting and pasting text into command lines! - D. On 26/07/2016 21:55, Paul A. Steckler wrote: > What is the status of the PGIP code in Proof General? > > Are there any provers that use the protocol? > > -- Paul > ___ > ProofGeneral-devel mailing list > ProofGeneral-devel@inf.ed.ac.uk > http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel > -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] Shutdown of proofgeneral and proofgeneral-devel lists
Dear all, The two Proof General mailing lists hosted here at Edinburgh have become somewhat defunct and the signup pages are targets for spammers. So we are planning to retire them properly later this month. If you would like to retrieve previous postings meanwhile you should be able to access the public archives here: http://lists.inf.ed.ac.uk/pipermail/proofgeneral/ http://lists.inf.ed.ac.uk/pipermail/proofgeneral-devel/ As most will know, Proof General development and support has moved to Github now and is focused mainly on Coq: https://github.com/ProofGeneral/PG As well as the usual Github mechanisms, there are some links to Zulip chats there where PG developers and users can discuss. Thanks to list members still here for their contributions over the years! Best wishes, - David -- Prof. David Aspinall, Email: david.aspin...@ed.ac.uk LFCS, School of Informatics The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. Is e buidheann carthannais a th’ ann an Oilthigh Dhùn Èideann, clàraichte an Alba, àireamh clàraidh SC005336. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] Fwd: Shutdown of proofgeneral and proofgeneral-devel lists
-- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. Forwarded Message Subject: Re: [PG-devel] Shutdown of proofgeneral and proofgeneral-devel lists Date: Wed, 15 Jun 2022 12:59:47 +0200 From: Erik Martin-Dorel To: David Aspinall Thank you David! Let me give some direct pointers as a follow-up of your e-mail: Two communication channels are indeed preferred to get in touch with PG devs/users: Zulip and GitHub. So feel free to do one or both of the following actions if you're interested: 1. Subscribe as a "Watcher" of the PG GitHub repository https://github.com/ProofGeneral/PG/ (to get automatic notifications from issues and releases; in particular we plan to do a major release soonish) 2. Subscribe to the coq zulip chat system https://coq.zulipchat.com/ (and use one of these streams: https://coq.zulipchat.com/#narrow/stream/304019-Proof-General.20users https://coq.zulipchat.com/#narrow/stream/304020-Proof-General.20devs ), but note that despite the name, this communication channel is not intended to be Coq-specific: EasyCrypt, PhoX, and QRHL users can post there just as well! Kind regards, Erik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
