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,

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

Reply via email to