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

Re: [PG-devel] -quick

[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 background?
> 
> 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.

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:

>> - 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 background?

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!

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,

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 minutes.  Thanks a lot for all your work on PG!

>> 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 "Require"s everything in _CoqProject,
>> including all the magic to be able to jump to where the error was and
>> everything.
> 
> OK, lets call this the compile-everything thingy. What do you
> want when
> 
> - 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 background?

> - while fixing B you realize you want to change the imports of A?
>   Restart compile-everything automatically after you saved A to
>   disk?

See above.

> - you decide to do a git pull to get the patch that fixed the
>   problem in some file from you colleague?

Sounds like I'd be asking for trouble, just like if I would do git pull
while the dependencies of a file are compiled by PG.  If this could be
safely cancelled, I think that's all I can hope for.

> Note that in all these cases you might end up with inconsistent
> vo files on disk if you just let compile-everything continue.

Generally, I'd be fine with compile-everything being cancelled whenever
it can't be safely continued -- even more so if there was a user action
that triggered this abort.

The motivation for this is to save time. Right now, when I change a file
in our prelude (which is the folder containing a lot of basic
definitions, essentially an extended standard library; everything
depends in it), I then go to the console and do "make -j4". I see which
is the first file to break (that may take 1 minute or two), navigate to
that file in PG, and fix it. While I think about how to fix this, the
CPU is idling. Once I fixed this file, I go to the console, do "make
-j4" again, wait another minute or two for the next issue to come up,
and repeat until the build works.  Sometimes of course I have to go back
to the prelude and change something there because I made a mistake, then
the entire thing starts over.  (Compiling everything from scratch takes
~6 minutes, but the sum of the waiting times here is larger because
fewer things are compiled at once, so less parallelism is used.)
  My hope would be that the time it takes me to fix a file can be used
better. Right now, all or all but one CPU core will be idle during that
time; sometimes, I even manually do another "make -j4" in background to
make sure I find the next mistake. 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.  This is a case
of suddenly learning about a feature I didn't even know I longed for all
the time.  Of course it's not as convenient as having this in PG as I
have to navigate to the file manually, but it should still help a lot.
Next time this comes up, I'll see whether this feels sufficiently efficient.

If I'm the only one wishing for such a feature, it's probably not worth
the effort. I've just been dreaming a little here ;)

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

[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 bug hits
me because I did a plain "make -j4" in background on a console).

However, I don't see any hint of the feature I am requesting. "Keep
Going" *sounds* right, but it's not what I mean -- according to the docs
(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.
What I am looking for is something that compiles more of the current
*project* (i.e., things listed in the _CoqProject), even if everything
that the current file depends on is already compiled.

So say I have three files, A B C, and B C depend on A. I do a change in
A, switch to B to fix things there that broke. What I am looking for is
something that compiles C in background so that, if that file happens to
still work, I don't need to wait later for it to finish compiling. This
could save me enormous amounts of time if the breakage is somewhere in
the leafs of the development, because all the intermediate files would
be compiled while I am fixing some breakage, instead of being compiled
only *after* I fixed the breakage and look for the next.

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 of
a universe inconsistency missed by vio2vo. I currently see two options:

* Right before push, I do "make -j4". That will however recompile many
  files that PG already created with vio2vo, because the .vo files'
  timestamps do not match their dependency order when created by vio2vo.
* Right before push, I do "make quick -j4 ; make vio2vo J=4". That will
  however always re-check all proofs because vio2vo is not incremental.

Am I missing something here? Is it maybe possible to make vio2vo
incremental?  I feel like currently, the problem is just that the make
target is too simplistic.  A smarter "make vio2vo" could filter the list
of .vo files for those that are older than their respective .v files,
and only compile those -- is that correct? If yes, I may try to write
such a make target.  (Something even smarter would run "make quick" and
"make vio2vo" in parallel, i.e., add .vio files to th schedule as they
are created and already start producing the .vo files before all .vio
files are done. I don't have a good idea though for how to implement that.)

Kind regards,
Ralf

On 06.01.2017 17:39, Hendrik Tews wrote:
> 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 the option
> `coq-compile-quick' or the subsection "11.3.3 Quick compilation
> and .vio Files" in the Coq reference manual." May I ask that you
> follow one of these links? I believe all your questions are
> answered there and you will also find the documentation about the
> feature that you are requesting!
> 
> Best regards,
> 
> 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 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
> completely, but it contains a pointer: "See the option
> `coq-compile-quick' or the subsection "11.3.3 Quick compilation
> and .vio Files" in the Coq reference manual." May I ask that you
> follow one of these links? I believe all your questions are
> answered there and you will also find the documentation about the
> feature that you are requesting!

Unfortunately, the CHANGES file does not contain any links (as in
literal hyperlinks) to the right sections, and if I look up section
11.3.3 of the reference manual myself, this is where I end up:

That's... probably not the section you meant ;)
I have to admit I did not consult that document before writing the mail,
because many of my questions are PG-specific and I did not expect any
help about that in the Coq reference manual. I should of course still
have done the lookup, in which case however I'd have been stuck at the
above document.

I only just now realized you are talking about the *ProofGeneral*
reference manual, a document of which I didn't even know it existed:

Maybe the text in the CHANGES file could be improved to clarify which
reference manual it is talking about.  After all, when referring to a
Coq feature, a reference to the Coq reference manual (the one linked to
in my first paragraph) is not entirely unexpected -- but clearly, that's
not what is meant here.

I may come back later with more questions, once I read the docs ;)

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,

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 the option
`coq-compile-quick' or the subsection "11.3.3 Quick compilation
and .vio Files" in the Coq reference manual." May I ask that you
follow one of these links? I believe all your questions are
answered there and you will also find the documentation about the
feature that you are requesting!

Best regards,

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

[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 informed the list owner about this.)

Your email did get through (thanks for the thoughts!). I'll let Hendrik reply 
on the technical aspects :)



signature.asc
Description: OpenPGP digital signature
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel