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

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

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

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

ProofGeneral-devel mailing list

Reply via email to