coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] recompiling coq libraries on recompiling coq
Date: Sat, 30 Jul 2022 20:08:02 -0400
Authentication-results: mail2-smtp-roc.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-lf1-f48.google.com
Ironport-data: A9a23:d/kJwKJIpoY9yqFrFE+R6JMlxSXFcZb7ZxGr2PjKsXjdYENShTEAz 2NMXzzVbPiLMTHze4hyYY3i9kwD78fdmN5jHAsd+CA2RRqmi+KVXIXDdh+Y0wC6d5CYEho/t 63yTvGacajYm1eF/k/F3oDJ9CU6jefSLlbFILas1hpZHGeIcw98z0M48wIFqtQw24LhXFjV4 YiaT/D3YTdJ5RYkagr41IrY8HuDjNyq0N/PlgFWiVhj5TcyplFNZH4tDfnZw0jQHuG4KtWHq 9Prl9lVyI92EyAFUbtJmp6jGqEDryW70QKm0hK6UID66vROS7BbPqsTbJIhhUlrZzqhvPBR5 thsnLOKbxYOZYeQwOUGUBh0KnQrVUFG0OevzXmXtMWSywjCfSKpzak+Sk4xOoIc96B8BmQmG f4wcmhcKEDewbvon/TnGoGAhex7RCXvFIoVunB7zTzaS/8gSJbPBaTL+dBw0zI5h8QIFvHbD yYcQWYwMEWYPEUXUrsRILIHveSamEjcSiYG+GvOnac15HnYyDUkhdABN/KMIoDQLSlPpW6To XuD9GDkCDkBJdmHwHyE9Gitj6nBh0vGtJk6EbS58rtujgTWyDBDThIRUlS/rL+yjUvWt89jx 1I82QoOg6UT3WORaMjaBDfk+H+fvR8wYo8FewEl0z2lxq3R6gefI2ELSD9dddAr3PPaoxR6i TdlePu5VVRSXK2ppWG1rejL8GvjUcQBBSpTOn9eFFptD8zL+dlr1nryosBf/LlZZ+AZ9Bn1y jGO6Sww3vAd0Z5N2KK88lTKxTmro/AlrzLZBC2GBApJDSsjP+ZJgrBED3CFtp6sy67HEjG8U IAswZT20Qz3JcjleNaxaOsMBqq1wP2OLSfRh1Vid7F4qWn8oSb+LdoAvWkjTKuMDiriUW+2C KM0kVMBjKK/wFP3BUOKS9nsVZp0lPCI+SrND6CLN4QmjmdNmP+vpXkyPyZ8Lkjil08jlaxXB HtoWZfEMJruMow+lGDeb75Fj9cDn3lirUuOG82T50n4idK2OS/NIZ9YYQDmRr1ovMus/l+Jm /4BbJDi40sEAIXDjtz/q9F7waYidihlW/gbaqV/Koa+H+aRMDp9VqeLmOJ9J90NcmY8vr6gw 0xRk3RwkDLX7UAr4y3TApy6QL+wD5t5s1whOikgYQSh13Q5MNSg6a4ec908erx+rL5vyvt9T v8kfcScA6QXGm6XpWhFNZSt/pZ/cBmLhB6VO3X3bTU6ealmTVOb99LheDzp6yRTXDG8stEzo uH72w6CGcgDSg1uAdz4cvWqy1/t73ERlPgjDUTNK9hXPk7r9dEyeSD2i/Y2JeAKKAnClmPKj VbIXU9AqLCU8YEv8dTPiaSVlKuTErNzThhAAm3WzbeqLi2FrGeuxIl3VuzXLz3QUWXD/rr7O bdYwvT6B/0wnFhQtr16Hbs2n7k14MHipuMDwwlpQCfLYlCsBu8yK3WKx5MU5KhEx7scvQXvH 0zTqp9VPrKGPM6jG1kUfVJ3YuOG3PASuz/T8fVlfxmgtXEvpOKKARdIIh2BqC1BN78pYokr9 uEs5ZwN4Aulhxt2b9uL0nJO+2KXIiBSWqkrrMtBUoriiw5uzl8bJJKAWmn555aAb9gKOU4ve 2fGiK3HjrVa50zDb3tjSiSXjLQF3cwD6EJQ0VsPB1WVgd6Z1PU56xtcrGYsRQNPwxQbju9+N wCH7aGuyXliItupuCRCY4xoMwRIBRnc/kKojlVVxCvWSE6nUmGLJ2o4UQpIEIb17EoEFgW3P pnBoIombdouVM701yo2H0VirpQPiPRvoxbalpnP89utRvEHjPmMvkNqTWUNohrjR8g2gSUrY AWsEPlYMcXGCMLbn0H350R2G1jdpNBo6VGumc1cwZ4=
Ironport-hdrordr: A9a23:oAT3Y6AGRL7qBdrlHemV55DYdb4zR+YMi2TDtnoBMCC9F/bzqy nApoV/6faZskdyZJhko6HiBEDiexLhHPxOkO0s1N6ZNWGMhILrFuFfBODZslrd8kPFh4hgPG RbH5SWyuecMbG3t6nHCcCDfeod/A==
Ironport-phdr: A9a23:MC9oUBKO38ECPB9KDNmcuP5sWUAX0o4c3iYr45Yqw4hDbr6kt8y7e hCFvrM31geCB9STwskHotKei7rnV20E7MTJm1E5W7sIaSU4j94LlRcrGs+PBB6zBvfraysnA JYKDwc9rDm0PkdPBcnxeUDZrGGs4j4OABX/Mhd+KvjoFoLIgMm7ye6/94fNbwlWmDaxbq1+I RGrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+V rxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4 aV2Rx/ykCoIODA5/2PXhMJ+j6xVvQyvqABkzoHOfI2YLuBzcr/Bcd4YQ2dKQ8ZfVzZGAoO5d 4YCE/EOPeZZr4nmp1sBsxi+DhSwCePp0DBIgGL51rA93us7Cg7G3A0gH8kOsHvKr9X5Lr0dU eavw6nO0DrPdfJW2Tbh6IjHaR0hrvSMUqhxccrV00UgCwTFjlCJpIHjIjia2fgDvXKB4Op8S eKglXQnqwdprzWzxMogl4fEip8Ux1zY+yh3zoI4KMC8RUN4fNOoDIdcuiOZOoZ2Xs4sTGFmt SQnxrAIp5O3YCcExZo5yhPbZPKKdZWD7BzkVOaUOzh4hXRldaqjiBa160igzPPzVs2w0FpQs CVKj8TMumgR2BzU88iIVvx9/kGv2TaO2ADf8OREIUQymKHGKJAh2qY9moQPvUnHBCP7m0X7g LWLekgl+OWk8evqb7bgq5SBLYF7kBv+Pb4rmsGnAeQ3LAwOX2+D9OS5zrLj/En5TKxOjv04j 6XVqZ7aKMsYq6KjDA9V1YEj6xm7Dzi4ytgXgX4HLFdddBKGiYjmJU3OLejmAfujh1mgijRmy vDcMrH8A5jALGLPnbjicLpl7k5T0gszzdRR55JODbEBJer+VVXqu9zYDx85KAy0zPjkCNlnz IweX3iAAqmEP6/IsF+I5/4vI+aXaY8avTbyMfkl5/r0gXAlnl8deLGl3Z0MZ3+gBPRpP12ZY WbwgtcGCWoGoxIyTPb2h12aTT5Te3GyUrog6TE8EYKqFJvMRoSwgLOaxyq7BZ1XZmVeCl+WC 3vodoOEW+0NaC2IOMNhnCYEBvCdTNoq0gjrvwvnwZJmKPDV82sWr8HNzt9wssTZlRAp9TF3R +2b2meBBzV9lGMJXD873+Z2p0V7xhGC0LR3q/NdHN1XofhOV1FpZtbn0+VmBoWqCUr6ddCTR QP+Kj3HKTQ4T9ZrhsQLf144AdKpyBbKwyutBbYR0b2NHp09tKzGjDDqP8go7XHA2eE6ikU+B NNVPDivjK5+7AjeBMjAlUyfm+CrdLgT9CHI/WaHi2GJuRIQSxZ+BJ3MRmtXfU7KtZL870LGQ aWpDOEuOAtA0s6PKe1DbNTvgRNHRevsENvbamO13Wy3AEXA3auCOaztfWhVxyDBEA4EngQUq G6BLhQ7Dzy9rnj2CTVvERfrbRqp/7Uu7ny8SUAwwkeBaEgJO6Od3BkTiLTcTvoS2uhBoyI9s 3BuG1372dvKCt2Grg4nfaNGYNp77k0VnWTe/xdwOJCtNcUAzhYXbhh3skXy1h52FpQIkM4kq 2kvxRZzLqTQ2U1IdjeR15T9crPNLWy68BeqYq/QklbQtbTesq4F6PUjq1jg+givH0wutXRmz 9Z93H6V55GMBw0XENrwXksx6xlmtuTCeCBuguGcnXZoMKSyrnrDw4dzXLpjmkvmJokAdv/UR 2qQW4UACsOjKfIngQ2sZxMAZqVJ8bIsetmhfL2A0bKqO+BpmHSni35G6cZzyBHplWI0R+jW0 pIC2/zd0BGAUmK2hV2hs9v3lIMCbDcbGGb5yCn4C6ZeY6RzecAADmLkcKjVjp1uwoXgXXJV7 gvpDlkG2dSpdBnUZlr02wEW1EULrlSonCK5y3p/lDRj/c/9lGTehu/lchQAIGtCQmJv2EztL YaDhNcfREG0bgItmXNJ/G7CzrNA7OR6JmjXGwJTejTuantlWe22v6aDZMhG7NUptz9WWaKye wLSRrn4qhocmyTtegkWjDkxdzCxupj62RV8gWSRandysHXxdsR5xBOZ79vZDfJcxTsJQiBkh CKfXADteYn0u4zKyNGf4qi3TAfDHtVLfDPuzJ+cuSfz/mBsDRCl3riyltDhDQkmwHr+3thuW z/PqUW0aY3q2qKmdON/KxMwVRmstowjRN44zttj4fNYkWIXjZiU43cdxGL6MNEBnLn7cGJIX zkAhdjc/Ani3kRnaHOP3YPwEHuHka4DL5G3ZH0b3iUl4oVEEqCRufZNlyt0uVq1rkTYZ/F7k nEcyOchwHEfiuAN/gEqy2/OZ9JaVVkdJiHqmxmSupq3pqVWf2aicv650kN4kZagDa2Nig5ZU Xf9PJwlGGUji6c3eEKJ23r15Ib+fdDWZt9GrRyYnSDLiO1NIY4wnP4H1mJ3fHjwtno/x6snn ARjiNuk6ZOfJTwnr8fbSlZIcyf4bMQJ9nTxgLZCy4yIipu3EMwpGy1XDsC1C6v5SHRI6auhb 0HUTHU9sivJR+aZR1TErh449zSXVMn6UhPfbHgBkYc8Gl/EfBYZ2EZMG29i1p8hSlL0moq7L BY/tmhXvhmi8lNN0r46aEO5CzuZ/VbyLG9zEcj6TlIe7xketRiJd5XEs6QrWXkfp8PprRTRe DXDN0IRUj5PCgrcQAq6dri2uYuZrLPeX7viaaOIOfLX94k8H7+J3c79iNM3uWbRcJzVbj86S KRkkktbASIjQpqfxmVJEn1N0XqKNp/TpQ/gqHcu8Iblq6WtA1ipvczWWt4weZ158hSyy89vL sa2gyB0YXZd35IInzrTzaQHmUQVgGdofiWsFrIJsWjMSrjRk+lZFUxTbSQ7L8ZO468mu2sFc cfGltP40KJ5hf8pGh9EU1LmgMSgec0NJSm0KlrGAE+BMLnOKyfMxon7Zqa1SLsYi+sx1VX4o TGAD0rqJSiOjRHsXhGrdOVC1WSVYEwYt4a6fRJgT2PkSZOuaxG2NsN2kSxjwbAwgSCvVyZUO jx9fkVR67yIuHkA07MvRioYsCUjcbnX/kTRp/PVIZsXr/ZxVyF9luYApW8/16MQ9iZPAvp8h CrVqNdq5VCgiOiGjDR9A38s4n5GgpyGuUJ6NODX7J5FDDzN9hIM9mWdCFIDodJjBpvuurxf4 tfKnaP3bjxF9piHmKlUT9iRM8+BPHc7ZFDxHyXICQIeUTOxHWTWhkgYlP/Ls3PJ/t41rZ/jn JdIQbheHg9QdLtSGgFuG9oMJ41yVzUvnOuAjcIG0nG5qQHYWMRQup2vvhO6BPzuLHOdg+ABa UdYh7z/KosXO8vw3EkwMjGSeazFHkPRWZZGpSgzNmfcT21C9XF/Sis43Ee3M2uQ
Ironport-sdr: OMEXMSSWi8CF6rh44ybk/5LQ4JfA5bcGYyQHZObvrbEIeHJPYYchMagwkQhAG7wSHmejNvjJqW 2UCy6KP5r7xSklxZB7j3nGpqJC1gaAII5WketlNGHFDUk/kGQjx6Me91as7P88S5JSAxGPFX/W BDmCT3y955ETmsEdjUmXLZSW9bN6ARBHJoRT2a798cyP0jJ2eFyM9Mg62gNwFhMfJqBvdCr4CO vuXN2oT67jdeLmHH4xA8xhEhTUDQ+jpvFDUBOOik1yEEsfDr5GIFQA3p49uYIejyFU6GLQVFdh tD+kQTpFAoA7Jj++lXW0AcYd

i have the exact same ocaml version and coq version in docker (7dbaab056386) and on my desktop (optiplex), yet the coq on my desktop does not accept the A.vo I built in docker and transferred to my desktop:

[abhishek@optiplex vok]$ coqc --version
The Coq Proof Assistant, version 8.15.1
compiled with OCaml 4.14.0
[abhishek@optiplex vok]$ docker attach 7dbaab056386 
coq@7dbaab056386:~$ coqc --version
The Coq Proof Assistant, version 8.15.1
compiled with OCaml 4.14.0
coq@7dbaab056386:~$ cd vok/
coq@7dbaab056386:~/vok$ ls
A.v  B.v  C.v  CoqMakefile.conf  Makefile  Makefile.conf  Makefile.coq  Makefile.coq.conf  _CoqProject
coq@7dbaab056386:~/vok$ cat A.v
Require Import NArith.

Lemma xx : 2 = 1+1.
Proof using.
  do 10000 idtac.
  reflexivity.
Qed.

coq@7dbaab056386:~/vok$ cat B.v
Require Import vok.A.

Definition xxx := xx=xx.
coq@7dbaab056386:~/vok$ make A.vo
COQDEP VFILES
COQC A.v
coq@7dbaab056386:~/vok$ logout
[abhishek@optiplex vok]$ docker cp 7dbaab056386:/home/coq/vok/A.vo ./
[abhishek@optiplex vok]$ make B.vo
COQDEP VFILES
COQC B.v
File "./B.v", line 1, characters 0-21:
Error:
Compiled library vok.A (in file /home/abhishek/work/temp/vok/A.vo) makes inconsistent assumptions over library Coq.Init.Ltac

make: *** [Makefile:720: B.vo] Error 1

(what I didnt show in the terminal log is that the contents of vok/A.v and vok/B.v are the same on my desktop and in docker. Also, ignore the name "vok": this issue has nothing to do with vok files.)

Background: we need this to work so that we can reuse the dune .vo cache we have in the CIs on our local development machines.

-- Abhishek

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

On Thu, Dec 10, 2020 at 6:25 AM Guillaume Melquiond <guillaume.melquiond AT inria.fr> wrote:

Le 10/12/2020 à 10:39, Enrico Tassi a écrit :
> Vo files contain a "hash" of Coq. From config/coq_config.ml in one of
> my checkouts:
>
> let caml_version = "4.07.1"
> let date = "November 2020"
> let compile_date = "Nov 24 2020 13:18:16"
>
> You did re-run ./configure, after make clean, I guess.

I don't think the date ever becomes part of the .vo files, even indirectly.

But Coq_config.caml_version does, and so does Coq_config.vo_version. The
former is critical for marshalling, and the latter is constant for a
given version of Coq.

Best regards,

Guillaume

Re: [Coq-Club] recompiling coq libraries on recompiling coq, Abhishek Anand, 07/31/2022