Re: [PG-devel] Automatically retract effects of proof-activate-scripting-hook?
> This sounds wise, and what Pierre originally suggested, although if I've > followed it seems as if > that's not compatible with his convention of setting coq-prog-args in file > local variables. I looked again, I see you suggested coq-load-path for this already, not prog-args. Great. - 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?
> This is, however, not the expected simplification. I decided for > this simple change, because it keeps the functionality of other > proof assistants without that I have to touch their code. This sounds wise, and what Pierre originally suggested, although if I've followed it seems as if that's not compatible with his convention of setting coq-prog-args in file local variables. - 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?
David Aspinall writes: 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. I made a simple change to get the functionality I need for coq. The initialization of prog-name-list1 is now (if (functionp (proof-ass-sym prog-args)) ;; complex assistants define -prog-args as function ;; that computes the argument list. (cons proof-prog-name (funcall (proof-ass-sym prog-args))) (if (proof-ass prog-args) ;; Intermediate complex assistants set the value ;; of -prog-args to the argument list. (cons proof-prog-name (proof-ass prog-args)) ;; Trivial assistants simply set proof-prog-name (split-string proof-prog-name))) This is, however, not the expected simplification. I decided for this simple change, because it keeps the functionality of other proof assistants without that I have to touch their code. 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?
Pierre Courtieu writes: 2011/1/13 David Aspinall > 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
Re: [PG-devel] Automatically retract effects of proof-activate-scripting-hook?
2011/1/13 David Aspinall > > 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)? > > No, for the same reason backtrack does not work. Add LoadPath is considered transient by coq. > > 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..). > That's exactly what I mean, but i thing Hendrik wants to use Add LoadPath instead of modifying the command line. This may be a good idea, provided we are sure that doing Add LoadPath foo. is exactly the same as donig -I foo. P. ___ 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 writes:
2011/1/13 Hendrik Tews
> 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
Re: [PG-devel] Automatically retract effects of proof-activate-scripting-hook?
2011/1/13 Hendrik Tews
> Pierre Courtieu 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.
>
If you really think it could be useful I may implement this as an option in
coq.
> ...
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.
P.
___
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 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?
2011/1/13 Pierre Courtieu
> 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
>
> > 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?
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??
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
> > 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?
> 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?
David Aspinall 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?
> 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.
Re: [PG-devel] Automatically retract effects of proof-activate-scripting-hook?
Pierre Courtieu writes: Hi, 2011/1/12 Hendrik Tews > Hi, > > I just noticed the following effect: When I send commands with > proof-shell-invisible-command from a member of > proof-activate-scripting-hook, then these commands are not > automatically retracted changing the scripting buffer. > I don't understand what you mean by "retracted changing the scripting buffer". Commands are retracted when the user goes back in the script. If Sorry, in more detail: In your example from yesterday, one indirectly required file was in a different directory, say "other-dir". In order to get this running other-dir must be put into coq-load-path. Further, the contents of coq-load-path must be passed to invocations of coqdep and coqc via -I options. All this does work now: the dependencies are computed and the files are recompiled correctly (see cvs head). And now to the problem: In order to process the Require command in the scripting buffer, coq-load-path must also be put into coqtop, which is running behind. To achieve this I decided to add a function to proof-activate-scripting-hook. This function sends "Add LoadPath" for each element of coq-load-path via proof-shell-invisible-command. 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. 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?
Hi, 2011/1/12 Hendrik Tews > Hi, > > I just noticed the following effect: When I send commands with > proof-shell-invisible-command from a member of > proof-activate-scripting-hook, then these commands are not > automatically retracted changing the scripting buffer. > I don't understand what you mean by "retracted changing the scripting buffer". Commands are retracted when the user goes back in the script. If you go back to point scripted before the invisible command has been sent, it should retracted as well. > Is this really a feature? Do I have to add a corresponding > proof-deactivate-scripting-hook to undo the effects? > > Bye, > > Hendrik > ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
[PG-devel] Automatically retract effects of proof-activate-scripting-hook?
Hi, I just noticed the following effect: When I send commands with proof-shell-invisible-command from a member of proof-activate-scripting-hook, then these commands are not automatically retracted changing the scripting buffer. Is this really a feature? Do I have to add a corresponding proof-deactivate-scripting-hook to undo the effects? Bye, Hendrik ___ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
