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