Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] recompiling coq libraries on recompiling coq

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] recompiling coq libraries on recompiling coq


Chronological Thread 
  • From: Guillaume Melquiond <guillaume.melquiond AT inria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] recompiling coq libraries on recompiling coq
  • Date: Wed, 9 Dec 2020 18:28:47 +0100

Le 09/12/2020 à 17:05, Abhishek Anand a écrit :
> Suppose you built coq from sources S and then built some Coq library
> (with many .v files) X.
> Then, without changing anything else in the system/environment
> (ocaml/opam/...), you `make clean` and rebuild coq from S. would you
> need to rebuild the library X in order to import it in other projects?
> In other words, does Coq use the timestamp of when coqc was built to
> track whether the vo file was generated by the "same" coqc?
> If so, can we get rid of the timestamp tracking and track only the
> aspects that really matter extensionally (e.g. ocaml version/ sys arch/)?

No, no, and thus yes.

Best regards,

Guillaume



Archive powered by MHonArc 2.6.19+.

Top of Page