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 LoadPath, coq reorders the LoadPath, a subsequent remove will not yield the starting state. 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? Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
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?
2011/1/13 Pierre Courtieu pierre.court...@cnam.fr This is not entirely true. The backtrack mechanism of coq/pg is more robust than that, thanks to state numbers of coq you can undo most invisible commands by going back to a point in the file that was scripted before the 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. Hendrik I don't understand why you need to add a load path by yourself. The user should have put -I options to coqtop from the beginning, no? Or they should have put LoadPath in there files. Or is it that you want to parse the required file itself?? To be more precise, nowadays in order to script a Require the user already must have put the right directory in the load path. So why do you need to add more? I would suggest you do not try to alter coqtop options, as users already know how to do that. I recommend using file variables in each coq file and restart coq when changing file so that the correct command line is used. As you said: in coq one must retract a file before starting a new one, so restarting Coq is not a problem: it takes no time. So I plan to use your feature by using another file variable: (* *** Local Variables: *** *** coq-prog-name: coqtop *** *** coq-prog-args: (-I . -I ../../ALEA/src) *** *** coq-load-path: (../../ALEA/src) *** *** End: *** *) The only improve I see is to use coq-load-path to set coq-prog-args when opening a new file. P. 2011/1/13 David Aspinall david.aspin...@ed.ac.uk 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. ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
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 changing the active scripting buffer we have to restart coqtop. It also means we can stop this discussion. It only remains the following question: Hendrik I don't understand why you need to add a load path by yourself. I want to provide a solution, where the user specifies extensions in the load path in one place only: coq-load-path. Especially changing the coqtop command to include a series of -I options should not be necessary. All you have to do is set coq-load-path, the rest is done by ProofGeneral. This means that the contents of coq-load-path must be somehow passed to all invocations of coqdep, coqc and coqtop. For coqdep and coqc I translate coq-load-path into a series of -I options for the command line. This works already. For coqtop, which is running behind *coq* I translated coq-load-path into a series of Add LoadPath commands. This approach was based on the wrong assumption that Add LoadPath commands can be undone. So I plan to use your feature by using another file variable: (* *** Local Variables: *** *** coq-prog-name: coqtop *** *** coq-prog-args: (-I . -I ../../ALEA/src) *** *** coq-load-path: (../../ALEA/src) *** *** End: *** *) I hope that (* *** Local Variables: *** *** coq-load-path: (../../ALEA/src) *** *** End: *** *) will be sufficient. The -I arguments can be derived from coq-load-path and coqtop is default. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
Re: [PG-devel] 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?
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 several added for Coq..). OK, I got it now. prog-args becomes a function and for coq it appends (the value of) coq-prog-args and the contents of coq-load-path (the latter interspersed with -I's). If one of you wants to do this, please do, I am busy enough with other stuff. You might want to use the function coq-include-options. That's exactly what I mean, but i thing Hendrik wants to use Add LoadPath No, restarting coqtop on every buffer change and passing coq-load-path as -I options to coqtop is fine with me. Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
