Re: [PG-devel] first multiple coq files patch

David Aspinall david.aspin...@ed.ac.uk writes: 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? Sure, I've done that before the ProofGeneral-devel announcement.

[PG-devel] Automatically retract effects of proof-activate-scripting-hook?

Hi, I just noticed the following effect: When I send commands with proof-shell-invisible-command from a member of proof-activate-scripting-hook, then these commands are not automatically retracted changing the scripting buffer. Is this really a feature? Do I have to add a corresponding

Re: [PG-devel] Automatically retract effects of proof-activate-scripting-hook?

David Aspinall david.aspin...@ed.ac.uk writes: So, yes, you may need to adjust the load path manually with the scriting activate/deactivate hooks. Undoing those Add LoadPath commands with Remove LoadPath commands would be rather difficult. If one adds a directory which is already in the

Re: [PG-devel] Automatically retract effects of proof-activate-scripting-hook?

Pierre Courtieu pierre.court...@cnam.fr writes: invisble command. However LoadPath is probably not part of the undo model and Coq does not retract them when going back to a previous state. I just tried, changes in the LoadPath are not undone by Backtrack. This basically means that when

Re: [PG-devel] Automatically retract effects of proof-activate-scripting-hook?

Pierre Courtieu pierre.court...@cnam.fr writes: 2011/1/13 David Aspinall david.aspin...@ed.ac.uk 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

Re: [PG-devel] Automatically retract effects of proof-activate-scripting-hook?

David Aspinall david.aspin...@ed.ac.uk writes: 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

[PG-devel] no deactivation-hooks when killing fully asserted active buffer

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

Re: [PG-devel] no deactivation-hooks when killing fully asserted active buffer

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

[PG-devel] how to unlock ancestors

Hi, for coq I lock ancestor buffers inside the processing of Require commands. Because these Require commands may stand at arbitrary positions in the sources, I should unlock ancestors when Require commands are retracted. I found the following solutions: 1. convert span-delete-action into

[PG-devel] Inverse of proof-register-possibly-new-processed-file?

Hi, I looked around, but I could not find the inverse of proof-register-possibly-new-processed-file. This inverse should delete a file from proof-included-files-list and unlock its buffer, if it exists. There is proof-unregister-buffer-file-name, but - it only works on buffers - it does not

[PG-devel] defpacustom customization groups

Hi, is it really intended to add defpacustom variables to two customization groups, to proof-assistant-internals-cusgrp and to proof-assistant-setting? Is there a reason why the group proof-assistant-setting is not defined? Bye, Hendrik ___

[PG-devel] setting completion-ignored-extensions

Hi, AFAICT there is no support for completion-ignored-extensions in Proof General. For coq, setting completion-ignored-extensions would be nice, because the coq compiler clutters the directory with .vo and .glob files. My suggestion would be to extend proof-assistant-table with one row for a

Re: [PG-devel] Why does proof-retract-until-point call proof-activate-scripting?

David Aspinall david.aspin...@ed.ac.uk writes: why does proof-retract-until-point make the current buffer the active scripting buffer? It seems that Proof General anticipates that the user starts asserting immediately afterward. Not particularly, this is to enforce the

Re: [PG-devel] proof-follow-mode in invisible buffers

David Aspinall david.aspin...@ed.ac.uk writes: In order to do some changes in A the user unlocks A, thereby retracting B. If B is not visible, then the point in B will be moved to the beginning of the buffer. [ is there a difference between what happens with B invisible and

Re: [PG-devel] [PATCH] coq: Add option to ignore warning from coqdep in auto-compilation mode.

Tom Prince tom.pri...@ualberta.net writes: Some developments don't fully qualify their imports, and so coqdep gives warning about ambiguous imports. Allow these developments to use auto-compilation mode anyway. Could you describe an example? What is coqdep printing in these cases? -

Re: [PG-devel] A few major bugs about exiting ProofGeneral with current CVS version

Pierre Courtieu pierre.court...@cnam.fr writes: 2011/9/10 Erik Martin-Dorel erik.martin-do...@ens-lyon.fr: 3. Finally, it seems the function `proof-shell-exit' raises systematically an unexpected error. To reproduce it, run the (Coq) prover, then try: [M-: (setq

Re: [PG-devel] [PATCH] coq: Allow specifying recursive entries in coq-load-path.

That sounds OK, except there shouldn't be quotes in there: Sure, I've committed the change now, please test. Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Re: [PG-devel] [PATCH] coq: Add option to ignore warning from coqdep in auto-compilation mode.

Tom Prince tom.pri...@ualberta.net writes: Some developments don't fully qualify their imports, and so coqdep gives warning about ambiguous imports. Allow these developments to use auto-compilation mode anyway. Sorry about the delay, I somehow forgot about the issue. It's

Re: [PG-devel] Feature name conflict with Coq

Hendrik Tews t...@os.inf.tu-dresden.de writes: This is going to be a problem for those that want to use a manually installed Coq 8.4 with a Debian installation of Proof General. In Debian, manually installed stuff has precedence, so when proof-site requires 'coq, Emacs will actually

Re: [PG-devel] Feature name conflict with Coq

Stefan Monnier monn...@iro.umontreal.ca writes: Or by those who designed Emacs with a flat namespace for features and library files... Ahem! Please don't put .../ProofGeneral/coq in the load-path, and then simply do (require 'coq/coq). Where is this documented? I would even say

Re: [PG-devel] Reboot: Release of PG 4.2

Hendrik Tews t...@os.inf.tu-dresden.de writes: - support for braces and bullets This requires more work than I thought. I have to postpone this to October. Given that only few people use braces/bullets (because they are new) and even fewer use Prooftree, it doesn't make sense to delay

[PG-devel] proof-shell-pre-interrupt-hook ?

Hi, I just came across proof-shell-pre-interrupt-hook. I can't find any location where this hook is run. Am I missing something? Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk

[PG-devel] Coq menu entries

Hi, I just noticed that there are a view boolean settings in the Coq menu which are not done via defpacustom and which are therefore not in the Settings submenu. Is there a reason, why Toggle tooltips, Electric Terminator and Double Hit Electric Terminator are not in the Settings submenu? It

[PG-devel] first version of parallel background compilation for Coq

Hi, I just committed the first version of parallel background compilation for Coq. It is disabled by default in favor of the old synchronous compilation method. Parallel compilation required one fundamental and one minor change in the general proof shell treatment, see below. If you want to try

Re: [PG-devel] Coq menu entries

Pierre Courtieu pierre.court...@cnam.fr writes: Since double hit terminator is more or less an alternative to electric terminator, I have put them side by side in coq menu, to see if people OK, I thought double hit would modify the behavior of electric terminator. like it, but I did

[PG-devel] overlapping calls to proof-shell-filter

Hi, sometimes I see prooftree crashes with a cold disk cache (eg after reboot or after sync; sudo sh -c 'echo 3 /proc/sys/vm/drop_caches'). What apparently happens is that at some stage process-send-string blocks because the pipe to prooftree is full. This happens inside proof-shell-filter,

Re: [PG-devel] overlapping calls to proof-shell-filter

Stefan Monnier monn...@iro.umontreal.ca writes: I think this deserves an Emacs bug report. see http://debbugs.gnu.org/cgi/bugreport.cgi?bug=13400 There are definitely some documentation problems. process-send-string is not mentioned as function that might trigger a filter call. I think

Re: [PG-devel] overlapping calls to proof-shell-filter

I wrote: here is a patch that solves the problem for me. Any comments? I committed now. I deleted the argument of proof-shell-filter, to make sure, nobody will use it. Reasons are described in the doc comments. Hendrik ___ ProofGeneral-devel

[PG-devel] make clean deletes backup files

Hi, currently editor backup files are deleted by make clean. I find this unfortunate, because I have to use make clean quite often to remove elc files. If nobody disagrees, I move the removal of *~ to the distclean target. Bye, Hendrik ___

[PG-devel] prooftree users?

Hi, is anybody actually using prooftree with the cvs head of Proof General? For supporting bullets, braces and Grab Existential Variables I would like to make several commits that break compatibility with the current release of prooftree. A suitable prooftree release will follow within a month.

[PG-devel] status of support for Proof General

Hi, do we have a support problem for Proof General? I am asking because we have issues in the tracker that are quite old and nobody seems to care... for instance #460 or #463 to which I gave partial answers today. Do we have a lack of developers or do the developers not like to comment on

[PG-devel] Re: Ticket #467: vernacular command no longer displays timings

I remember how PG used to behave, but I do not recall which version it was. I started using Coq at version 8.3pl2, or there-abouts, so I can try to 8.3pl3 was released in December 2011, so it was probably Proof General 4-2pre111207 or earlier. Hendrik

[PG-devel] Re: Ticket #467: vernacular command no longer displays timings

I believe all Proof General versions (including the latest trunk) show the timing in the *goals* buffer when you use them with Coq 8.3pl4 or earlier. If you have more than one subgoal the timing is shown only when coq-hide-additional-subgoals is off. Then the *goals* buffer looks like

Re: [PG-devel] non-fatal warnings for make compile

David Aspinall david.aspin...@ed.ac.uk writes: This fix was helpful but unfortunately means that developers are more likely to introduce bugs unless they run make clean; make check I agree. But even before the change we had now and then compilation errors in the repository. From

Re: [PG-devel] Move to Github

Hi, I am happy to see Pierre you back on this list and back committing to Proof General. Regarding the 4.3 release: There are some indentation bugs in the tracker. Pierre, could you spend some time for them? I intend to fix #467 and have a look at #460. Does anybody else use the new parallel

Re: [PG-devel] Move to Github

Hendrik Tews t...@os.inf.tu-dresden.de writes: Regarding the 4.3 release: ... I have another issue that I would like to see resolved in 4.3: The feature name conflict with Coq, see http://lists.inf.ed.ac.uk/pipermail/proofgeneral-devel/2012/000241.html Both Proof General and Coq install

Re: [PG-devel] Moving to ELPA!

Hi, I don't have the knowledge to join the discussion about the relative benefits of different emacs package distribution systems. I once made significant contributions on PG and will join whatever the active majority here decides. At some stage I also prepared a PG debian packages - this was

Re: [PG-devel] Proof tree code

Hi, >> 2016-05-12 18:22 GMT+02:00 Paul A. Steckler : >>> The code in generic/proof-tree appears to rely on proof shell modes. >>> >>> Is the `prooftree' tool in common use among Coq users? I used it all the time ;-) For coq, prooftree needs the following: 1) a unique proof

Re: [PG-devel] State button for Coq, needed?

Hi, "Paul A. Steckler" writes: > Well, the current goal should always be shown, unless there's a bug. What if the user deletes the emacs window containing the current goal because he temporarily wants to use that screen space for something else? I used to do this quite

[PG-devel] future of coq-seq-compile.el

Hi, how long do we want to keep the sequential and blocking compilation implemented in coq-seq-compile.el? Is anybody actually using it? I am asking because I am not really motivated to maintain this code. If you look at the 8.5 changes, many things had to be done twice, in coq-seq-compile and

Re: [PG-devel] -quick

Ralf Jung writes: >> - you start scripting in file A (for instance to fix a proof) >> while compile-everything is still in progress? Have 2 >> compilations in parallel or abort compile-everything? > > Aborting when the active file is changed sounds fine. I guess that's >

Re: [PG-devel] -quick

>> OK, how about creating a emacs macro that does C-c C-b in the >> file that imports everything? You can easily bind this to F9 or >> or any other key - then you get everything with just one >> keystroke! > > That wouldn't be in background though, right? It'd stop interactive > mode in the file

Re: [PG-devel] -quick

Ralf Jung writes: > Ah, that's a good point. I should try that one time. Thanks for the hints! And if you define that procedure (changing to the import all file, doing C-c C-b there) as an emacs macro, then you can start the whole recompilation with just one key stroke.

Re: [PG-devel] -quick

Ralf, your first email got through and thanks for you positive feedback! I have the impression that you have not read any documentation about the quick compilation feature. The CHANGES file is unfortunately not the place to describe a complex feature completely, but it contains a pointer: "See