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

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. That'd be tremendously useful to make sure the entire
project compiles, and to quickly fix issues that could come up.
Ideally, this could work in background (after being started manually) so
that I can keep working on one file while other files are compiled --
once the issue in the current file is fixed, it will already have found
the next file that's broken, so I don't have to wait.

For now, in case someone is interested, I implemented "incremental
vio2vo" via Makefile hackery, see
<https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/Makefile#L27> and
<https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/awk.Makefile>. This
essentially implements the "build all remaining files of the project" I
asked for above, but outside PG. I will move this part of the discussion
to coq-club since it's just about coq_makefile.

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

Reply via email to