Hi,
I'm working on a big project. Sometimes, when I'm trying to prove lem_foo42
in foo.v
, I need to slightly modify the pre- or post-conditions in Lemma lem_bar37
which is found in bar.v
.
The problem is that:
make bar.vo
, then I will have a library inconsistency issue when interpret back foo.v
to `lem_foo42.v``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 bar
to foo
As long as I have not finished proving lem_foo42
, I don't always need to check that everything is alright in -between foo
and 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?
Isn't make vos
what you are looking for?
https://coq.inria.fr/refman/practical-tools/coq-commands.html#compiled-interfaces-produced-using-vos
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