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