Re: [PG-devel] -quick

[Stefan Monnier]

> wiring M-x compile to "make vio2vo J=X" and then wiring that to a
> shortcut is going to be simpler.  (I didn't even know about M-x compile

FWIW, I happily use

(global-set-key "\C-c\C-c" 'compile)


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

Re: [PG-devel] -quick

[Ralf Jung]

Hi,

>> Ah, that's a good point.  I should try that one time.  Thanks for the hints!
> 
> And if you define that procedure (changing to the import all
> file, doing C-c C-b there) as an emacs macro, then you can start
> the whole recompilation with just one key stroke.

Right, but on the other hand, I then have to maintain the list of all
files in two places (_CoqProject and that import all file).  I guess
wiring M-x compile to "make vio2vo J=X" and then wiring that to a
shortcut is going to be simpler.  (I didn't even know about M-x compile
until it was brought up in this discussion.  Really, I only know about
emacs barely enough to use it for PG^^)

Kind regards,
Ralf
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Re: [PG-devel] -quick

[Hendrik Tews]

Ralf Jung  writes:

> Ah, that's a good point.  I should try that one time.  Thanks for the hints!

And if you define that procedure (changing to the import all
file, doing C-c C-b there) as an emacs macro, then you can start
the whole recompilation with just one key stroke.

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

Re: [PG-devel] -quick

[Ralf Jung]

Hi,

>>> OK, how about creating a emacs macro that does C-c C-b in the
>>> file that imports everything? You can easily bind this to F9 or
>>> or any other key - then you get everything with just one
>>> keystroke!
>>
>> That wouldn't be in background though, right?  It'd stop interactive
>> mode in the file I was in.
> 
> If I understood correctly, you wanted to compile the whole
> project after finishing some change in one of the files. This is
> what you get here: You process the require commands in the
> import-all file, thereby compiling everything in your project that
> is outdated. Then you wait for the first error in
> *coq-compile-respone*, when you see one, you can go there to
> examine the situation. Meanwhile the background compilation will
> go on as far as possible, possibly producing more errors in
> *coq-compile-respone*. 

Ah, that's a good point.  I should try that one time.  Thanks for the hints!

Kind regards,
Ralf
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Re: [PG-devel] -quick

[Hendrik Tews]

>> OK, how about creating a emacs macro that does C-c C-b in the
>> file that imports everything? You can easily bind this to F9 or
>> or any other key - then you get everything with just one
>> keystroke!
>
> That wouldn't be in background though, right?  It'd stop interactive
> mode in the file I was in.

If I understood correctly, you wanted to compile the whole
project after finishing some change in one of the files. This is
what you get here: You process the require commands in the
import-all file, thereby compiling everything in your project that
is outdated. Then you wait for the first error in
*coq-compile-respone*, when you see one, you can go there to
examine the situation. Meanwhile the background compilation will
go on as far as possible, possibly producing more errors in
*coq-compile-respone*. 

Bye,

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