Pierre Vial (Oct 26 2022 at 11:48): Pierre Vial (Oct 26 2022 at 11:48):Hi,
I'm working on a big project. Sometimes, when I'm trying to prove lem_foo42in foo.v, I need to slightly modify the pre- or post-conditions in Lemma lem_bar37which 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 fooAs 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?
Théo Zimmermann (Oct 26 2022 at 11:52):Isn't make vos what you are looking for?
Théo Zimmermann (Oct 26 2022 at 11:52):https://coq.inria.fr/refman/practical-tools/coq-commands.html#compiled-interfaces-produced-using-vos
Pierre Vial (Oct 26 2022 at 12:00):Oh, thanks, I had read this paragraph but I hadn't understood it!
Notification Bot (Oct 26 2022 at 18:16):Pierre Vial has marked this topic as resolved.
Last updated: Apr 20 2024 at 08:02 UTC