Pierre Courtieu <pierre.court...@cnam.fr> writes:

   2011/1/13 Hendrik Tews <t...@os.inf.tu-dresden.de>

   > I just tried, changes in the LoadPath are not undone by
   > Backtrack. 

   If you really think it could be useful I may implement this as an option in
   coq.

>From a user perspective I find it very odd, that Add LoadPath is
not undone when I retract. For a correct coq-ProofGeneral
experience ProofGeneral should probably refuse to retract to some
point before an already asserted Add LoadPath...  But this is not
so important, because nobody is using Add LoadPath in real live
anyway.

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? 

Only if this restarting approach doesn't work out, I would come
back to the approach of undoing Add LoadPath.

   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.
   >
   >
   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. 

Bye,

Hendrik
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Reply via email to