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

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.


ProofGeneral-devel mailing list

Reply via email to