Re: [PG-devel] -quick

2017-01-08 Thread 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

Re: [PG-devel] -quick

2017-01-08 Thread 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

Re: [PG-devel] -quick

2017-01-08 Thread 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.

Re: [PG-devel] -quick

2017-01-08 Thread 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

Re: [PG-devel] -quick

2017-01-08 Thread 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

Re: [PG-devel] -quick

2017-01-07 Thread Ralf Jung
Hi, >>> - you start scripting in file A (for instance to fix a proof) >>> while compile-everything is still in progress? Have 2 >>> compilations in parallel or abort compile-everything? >> >> Aborting when the active file is changed sounds fine. I guess that's >> what vio2vo also does in

Re: [PG-devel] -quick

2017-01-06 Thread Clément Pit--Claudel
On 01/06/2017 05:45 PM, Ralf Jung wrote: > I only today learned about "make -k" from your changes, that will be > very useful indeed and may already be enough -- it will tell me which > other files need fixing. Yesh, that's what I was going to suggest from your post :) It's the default if you

Re: [PG-devel] -quick

2017-01-06 Thread Hendrik Tews
Ralf Jung writes: >> - you start scripting in file A (for instance to fix a proof) >> while compile-everything is still in progress? Have 2 >> compilations in parallel or abort compile-everything? > > Aborting when the active file is changed sounds fine. I guess that's >

Re: [PG-devel] -quick

2017-01-06 Thread Ralf Jung
Hi, Now that the "make quick"-mode is all set up correctly and that I succeeded with my Makefile hackery, I got a very significant speed-up already for lots of my daily work. :) Not having to wait for all the proofs in the dependencies to be checked makes a huge difference, up to multiple

Re: [PG-devel] -quick

2017-01-06 Thread Hendrik Tews
Ralf Jung writes: > To follow-up on this: I guess what I am asking for is some command in PG > to say "now please compile everything", that command should be as smart > about compilation as the compilation on import. It should behave just as > if I would step over a file that

Re: [PG-devel] -quick

2017-01-06 Thread Hendrik Tews
Ralf Jung writes: > (and from what I see it do), "Keep Going" is about compiling more of the > dependencies of the current file even if other dependencies failed. Right. > What I am looking for is something that compiles more of the current > *project* (i.e., things listed in

Re: [PG-devel] -quick

2017-01-06 Thread Ralf Jung
Hi again, > Furthermore (and maybe not entirely related), when using one of the > quick modes, is there a good way to incrementally check that the entire > development compiles before pushing to git? Note that "compiles with > vio2vo" is good enough; we have CI set up to catch the unlikely event

Re: [PG-devel] -quick

2017-01-06 Thread Ralf Jung
Hi, all right, I'm back from reading the docs. Sorry again for not doing this earlier. Most of my questions have been answered, including some I didn't even pose (like why I keep getting "A makes inconsistent assumptions over B", even though I don't even run the vio2vo-mode -- turns out that

Re: [PG-devel] -quick

2017-01-06 Thread Ralf Jung
Hi Hendrik, > your first email got through and thanks for you positive > feedback! Thanks or the quick reply! > I have the impression that you have not read any documentation > about the quick compilation feature. The CHANGES file is > unfortunately not the place to describe a complex feature >

Re: [PG-devel] -quick

2017-01-06 Thread Hendrik Tews
Ralf, your first email got through and thanks for you positive feedback! I have the impression that you have not read any documentation about the quick compilation feature. The CHANGES file is unfortunately not the place to describe a complex feature completely, but it contains a pointer: "See

Re: [PG-devel] -quick

2017-01-06 Thread Clément Pit--Claudel
On 01/06/2017 09:46 AM, Ralf Jung wrote: > (I don't know if my previous mail got through, as I didn't get the mail > myself via the list -- and I cannot access the list subscriber options > to check whether I enabled getting my own mails, because the website is > not working properly either. I

Re: [PG-devel] -quick

2017-01-06 Thread Ralf Jung
Hi, > I opend a PR for comments with a first version of -quick support, > see the quick branch on g...@github.com:hendriktews/PG.git. The > solution has advantages over using make because the quick options > accept an up-to-date .vo file for prerequisites (make insists on > producing .vio files

Re: [PG-devel] -quick

2017-01-06 Thread Ralf Jung
Hi again, (I don't know if my previous mail got through, as I didn't get the mail myself via the list -- and I cannot access the list subscriber options to check whether I enabled getting my own mails, because the website is not working properly either. I informed the list owner about this.) >

Re: [PG-devel] -quick

2016-11-16 Thread Clément Pit--Claudel
Very nice! On 2016-11-16 06:06, Hendrik Tews wrote: > Hi, > > I opend a PR for comments with a first version of -quick support, > see the quick branch on g...@github.com:hendriktews/PG.git. The > solution has advantages over using make because the quick options > accept an up-to-date .vo file