I'm working on a big project. Sometimes, when I'm trying to prove
foo.v, I need to slightly modify the pre- or post-conditions in
Lemma lem_bar37which is found in
The problem is that:
make bar.vo, then I will have a library inconsistency issue when interpret back
make foo.vo, then, in practice, I usually wait 2-3 minutes (which can actually go to close to 20 minutes) so that the build goes from
As long as I have not finished proving
lem_foo42, I don't always need to check that everything is alright in -between
bar (I usally have good reason to know that nothing will be broken).
Would there be a way to make
coqc ignore libraries inconsistencies when I want it to?
make vos what you are looking for?
Oh, thanks, I had read this paragraph but I hadn't understood it!
Pierre Vial has marked this topic as resolved.
Last updated: Oct 04 2023 at 19:01 UTC