Ralf Jung <j...@mpi-sws.org> 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.


> 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.

OK, sorry, then I misunderstood. I thought quick-and-vio2vo is
what you were looking for. This option at least compiles some
files to .vo while you can make some progress in your scripting

What you want - compiling files unrelated to the current
scripting buffer - is currently not available. I can only suggest
the following workaround: Create a file that imports everything.
After a change, do C-c C-b in that file. If quick compilation
finds an error, that file is unlocked and you can go there and
start fixing it (however, if you start scripting there, the keep
going background compilation of the import everything will be
aborted). If only vio2vo finds an error, the erroneous file is
not unlocked and you need to select an ancestor looking mode that
permits you to change the locked region.

The assumption behind the current background compilation is that
it is explicitly triggered by the user in a state where the file
dependencies do not change. It is therefore fine to compute the
dependencies only once at the beginning of the compilation. If
the user triggers a second compilation after the first one has
finished, the dependencies are computed again.

If you have a continuously running background compilation
process, then this process must be notified when some file
changes on the disk because it then has to invalidate this file
and everything depending on it. I can imagine that this would be
useful for big projects, but it would be a lot of work. (Just
imagine you switch git branches while the background compilation
is in progress...)

> 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

Do C-c C-b in a buffer that imports everything with
quick-and-vio2vo, this will run vio2vo on all those files that
don't have an up-to-date .vo.

> * 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, Proof General runs vio2vo usually in the right order (but
there are exceptions), but if B depends on A, vio2vo on B might
start immediately after starting A and thus finish before A.

It would be not too difficult to enforce that in case B depends
on A, vio2vo on B only starts when A is finished. The dependency
information is there, it is just not used for vio2vo.

However, you might always run into the situation where B depends
on A and where only the .vo file for A is missing. What do you
want in this case? Run vio2vo on B again?

> * 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.

The make targets that coq_makefile generates are not very
sophisticated, but I believe you would need quite a bit of
makefile hacking to get the features that you want.

ProofGeneral-devel mailing list

Reply via email to