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