coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] recompiling coq libraries on recompiling coq, Abhishek Anand, 12/09/2020
- Re: [Coq-Club] recompiling coq libraries on recompiling coq, Guillaume Melquiond, 12/09/2020
- Re: [Coq-Club] recompiling coq libraries on recompiling coq, Paolo Giarrusso, 12/10/2020
- Re: [Coq-Club] recompiling coq libraries on recompiling coq, Enrico Tassi, 12/10/2020
- Re: [Coq-Club] recompiling coq libraries on recompiling coq, Guillaume Melquiond, 12/10/2020
- Re: [Coq-Club] recompiling coq libraries on recompiling coq, Enrico Tassi, 12/10/2020
- Re: [Coq-Club] recompiling coq libraries on recompiling coq, Paolo Giarrusso, 12/10/2020
- Re: [Coq-Club] recompiling coq libraries on recompiling coq, Guillaume Melquiond, 12/09/2020
Archive powered by MHonArc 2.6.19+.