coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Safe to download and compile .v from evil source ?

From: Emilio Jesús Gallego Arias <e AT x80.org>
To: Timothy Carstens <intoverflow AT gmail.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Safe to download and compile .v from evil source ?
Date: Mon, 03 Feb 2020 19:21:28 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=e AT x80.org; spf=Pass smtp.mailfrom=e AT x80.org; spf=Pass smtp.helo=postmaster AT x80.org
Ironport-phdr: 9a23:q2WllhF3n4R2QWeSI9qLfp1GYnF86YWxBRYc798ds5kLTJ78osmwAkXT6L1XgUPTWs2DsrQY0raQ7/+rADRfqdbZ6TZeKccKD0dEwewt3CUYSPafDkP6KPO4JwcbJ+9lEGFfwnegLEJOE9z/bVCB6le77DoVBwmtfVEtfre9FYHdldm42P6v8JPPfQpImCC9YbRvJxmqsAndrMYbjZZtJ6orxRbEoHREd/lKyW5qOFmfmwrw6tqq8JNs7ihdtegt+9JcXan/Yq81UaFWADM6Pm4v+cblrwPDTQyB5nsdVmUZjB9FCBXb4R/5Q5n8rDL0uvJy1yeGM8L2S6s0WSm54KdwVBDokiYHOCUn/2zRl8d9kbhUoBOlpxx43o7UfISYP+dwc6/BYd8XQ3dKU8BMXCJDH4y8dZMCAeofM+hFqIn9qVUAohm9CwaiC+zg1iRFhmPq0aAgz+gtDRvL0Q4mEtkTsHrUttL1NKIKXO66yanIzDHDb/JR2Tjl7IbHbAshueuXXb1ocMTe000vFwfbgVWfrozqJy+Y1v4Ms2eB9OprSOWihHA8pgB+oTWj2t0gio7ThoIa013J8zhyzoUtJdCgVUJ2Yt2pHIFOuy2ENoZ6WN4uTmN1tCog17ELt4C3cDAKxZg9xxPSb+aLfoqI7x75SuqcLzl1iXR4c7ylnRmy61KvyujkW8m0zllKqi1Fn8HDt30OyxDf8M+HSuFy/ku52DaP0R7c6v1cLEwplqfWKIQtzqAumpcSq0jPAy37lFjsgKOLeEgo5PCk6+H9bbXnop+cOZV0igb7Mqk2hMOyGus5PwsSU2SB/uS8zrLj8VXjQLpWlv02jrXZsJfCKMsHoa65GhZZ3Zon6xaiFDiry88YnHkCLFJdYh2LlYnpO1fUIPD5F/izmVqskC04j8zBa4HgB5LRLmmLu777Zqpw7VUUnAs10ddB6ohaDrYeCP32U0718tffC0lqHRazxrPKDdR514Qpe2+UkLSuH6rWtVKH4dUGOeiFf8dBtR7te6Bj4OTh2yxq0WQBdLWkiMNEIEuzGe5rdh3AMCjcx+wZGGJPhTIQCenjiVmMSzlWNiSiD/p64Ss0Wtv/UNXzA7u1ibnE5x+VW51bYmcXWEDcSTHvbYrWAq5QOhLXGddol3k/bZbkU5UohEO+5Fe8zKBofLLZ
Organization: X80 Heavy Industries

Timothy Carstens
<intoverflow AT gmail.com>
writes:

> Getting to a place where .vo is platform/version agnostic, and where
> we have a decent library for checking/navigating .vo, would be
> FANTASTIC imho

The serialization machinery available on coq-serapi should work to
produce most of what it is on .vo files in a plain-text format that
should be loadable across a larger spectrum of compiled Coq, provided
you have the same plugins available etc...

The downside tho is that would lose sharing, I understand this is a huge
problem in practice.

E.

Re: [Coq-Club] Safe to download and compile .v from evil source ?, (continued)
- Re: [Coq-Club] Safe to download and compile .v from evil source ?, Emilio Jesús Gallego Arias, 02/02/2020