coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Paolo Giarrusso <p.giarrusso AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] recompiling coq libraries on recompiling coq
Date: Thu, 10 Dec 2020 04:46:00 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=p.giarrusso AT gmail.com; spf=Pass smtp.mailfrom=p.giarrusso AT gmail.com; spf=None smtp.helo=postmaster AT mail-pl1-f181.google.com
Ironport-phdr: 9a23:FOSrDRVMJYgl8Yieqx2obJq1t6zV8LGtZVwlr6E/grcLSJyIuqrYbBWCt8tkgFKBZ4jH8fUM07OQ7/m/HzVfsN3b4TgrS99lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUhrwOhBoKevrB4Xck9q41/yo+53Ufg5EmCexbal9IRmrrwjdrNQajIlmJ6o+1BfEpmZDdvhLy29vOV+dhQv36N2q/J5k/SRQuvYh+NBFXK7nYak2TqFWASo/PWwt68LlqRfMTQ2U5nsBSWoWiQZHAxLE7B7hQJj8tDbxu/dn1ymbOc32Sq00WSin4qx2RhLklDsLOjgk+2zRl8d+jr9UoAi5qhNwzY7bYoGbOvR9cK3AY90VWWVPU91NVyxYGI6wc5cDA/YDMOtesoLzp0EOrRy7BQS0Hu3g0DhIhnvx3aYn0uohEBvJ3BY6H9ITq3TUt9L1P7oVXOCt1qXIwjTDYOlM2Tfn9YjIaQshofaXULJ/dMre00gvFwffglqMrozlOiqY2+IQuGeU8+RuT/igi3I7qw5vuDivwN8hh4bIi48Rzl3J9jl0zZg1KNC2RkB3fN6qHptRui2GK4Z7XswsTmJptSs1xLALuZG1cigFxpkpwxPSaOCKfpaV7x/lSe2fIi94iWp7dL6jgxu+60utx+3mWsWqzVpHoTBJnsTPu3wQ0RHY99KJReFn/ki73DaCzwDT5f9AIUAzjafbLoQuwr80lpYKqUTDGjL6lFz4jKOLdUgo5/Kk6+vgYrXhqZ+cM5F7hhviPaQpn8yzGeU4Mg4QUGiH4emwyqHv8EnjTLhJjvA6iLfVvI3VKMgBu6K0ABJZ3p4m6xmlDjem1NoYnWMALFJAYB+Hl5LlO17PIP/iF/e/mUmskCxwx/DBJbDhDZDNIWLCkLflZ7py90lcyA8rwdBF+51UEq0BIO70WkLpqNPYCQY5PxWozObjFdVyzZgTWXmPA6+cKKPdq0WE5uMpI+mWZY8aoizxK/Y/562msXhsklgEOKKtwJE/aXaiH/0gLV/KT2Drh4I5GGAOuUIRTeXwkkCZSjkbM270UKM1/CsmE5mhJYjGT4GpxreG2XHoTdVtemlaBwXUQj/TfIKeVqJUMX7AEopaijUBEIOZZco5zxj37V31zrNmKqzf/ShK7cu+hugw3PXakFQJzRIxD8mZ1DvTHWR9n2dNXztvma4m8RU7xVCE3qx1xfdfEI4LvqIbYkIBLZfZitdCJZX3UwPFcM2OTQ//ENqjCDA1CNk2xo1Xbg==

What else does matter? We ran into this problem a while ago and never
investigated. We _might_ have changed OCaml version or used a
different Linux distribution. Is there a list of what factors are
recorded by Coq in vo files?

On Thu, 10 Dec 2020 at 02:24, Guillaume Melquiond
<guillaume.melquiond AT inria.fr> wrote:
>
> 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

--
Paolo G. Giarrusso

[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