coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] recompiling coq libraries on recompiling coq

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] recompiling coq libraries on recompiling coq
Date: Wed, 9 Dec 2020 08:05:07 -0800
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-il1-f175.google.com
Ironport-phdr: 9a23:62C2mB1XTFcSyBwDsmDT+DRfVm0co7zxezQtwd8ZseIfLfad9pjvdHbS+e9qxAeQG9mCtLQd1Lqd7vmocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmTiwbalvIBi0rgjduckbjZZ/Iast1xXFpWdFdf5Lzm1yP1KTmBj85sa0/JF99ilbpuws+c1dX6jkZqo0VbNXAigoPGAz/83rqALMTRCT6XsGU2UZiQRHDg7Y5xznRJjxsy/6tu1g2CmGOMD9UL45VSi+46ptVRTljjoMOTwk/2HNksF/g6JVrhyiqRJi3YDbfJqYO+Bicq7HZ94WWXZNU8RXWidcAo28dYwPD+8ZMOtEtIb9p1oOrQC+BQayB+Pk1yNFhnns0q08zusqDAbL0xY7ENIOsXTUt9X1O7kRUeyv1qbIyy/Mb/VL1jvn6YjIcwwhof6XULJ/dMre00gvFwffglqMrozlOiqY2+IQuGeU8+RuT/igi3I7qw5vuDivwN8hh5fJiI8L113J+ip3zZsrKdC2VkJ2YsKpHZVQuS2EOIZ7RsEvT3xqtSsnyrAIuZy2cSsIxZg72RLTdf+KfouG7x/lSe2fLzB4hHd/d7K+gRa/6VSvyurmVsmyzllKqi5FnsPSuX8Qyhze7NWMRPhl/kq5xzqDywTe5vtHLE00j6bXNp8sz78qmpYOs0nOHin7k1jsgqCMbEUr4O2o5vznYrr4op+cMJd5igTkPaQvnsyzGOU4MgwTU2SC9+Swyb/u8E3jTLVFif02labZsJTEKsgBuqG5BApV3p4i6xa5ETimzMwVkWcbIF9BYh6KjIjkN0vTLP35DPqzmUmgnTVryvzeO73uGJTNLnzNkLf7erZ97lZRxxAowtBf5pJUEbEBL+zwWkPrrtPYCAU2MwqpzOr9CdV9158eWW2UD6+WNaPdq16I5uY1L+aQY48VvS7xK+I56P72kX85hVgdcLG10psQcXC0B+hpI0GEYXX3mdoBCmcLvg8mTOPwklGCUDhTZ2yzX60m/D07BpimXs//QdWmh6XE1yOmFNUCbWdfT1uIDH3AdoOeWv5KZjjEceF7lTlRfLKhSpQh2BLmnQnzzbYveuPe+iwDtZ/gktFz7uvf0xAz6TNcAMGU0mXLRGZxyDBbDwQq1bxy9BQugmyI1rJ11qQBSI5joshRWwJ/Dqbyiux3D9eoBFDEd9aNDVeiG5CoWG5sCN02xNAKbgB2HNDw1kmSjRrvOKcckvmwPLJx96vd23brIMMkkiTJ0aAgix8tRc4dbDT61J46zBDaAsvyq2vcj7yjLP1O0yvE9WPFxm2L7hlV

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/)?

Thanks,

-- Abhishek

http://www.cs.cornell.edu/~aa755/

[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