Stream: Coq users

Topic: ✔ Library-wise unsafe coqc mode


view this post on Zulip 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:

  1. If I do make bar.vo, then I will have a library inconsistency issue when interpret back foo.v to `lem_foo42.v``
  2. If I do 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?

view this post on Zulip Théo Zimmermann (Oct 26 2022 at 11:52):

Isn't make vos what you are looking for?

view this post on Zulip Théo Zimmermann (Oct 26 2022 at 11:52):

https://coq.inria.fr/refman/practical-tools/coq-commands.html#compiled-interfaces-produced-using-vos

view this post on Zulip Pierre Vial (Oct 26 2022 at 12:00):

Oh, thanks, I had read this paragraph but I hadn't understood it!

view this post on Zulip Notification Bot (Oct 26 2022 at 18:16):

Pierre Vial has marked this topic as resolved.


Last updated: Jun 20 2024 at 11:02 UTC