coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Ensuring that OCaml files come from the right version of Coq?

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Ensuring that OCaml files come from the right version of Coq?
Date: Sun, 21 Feb 2016 00:55:19 +0000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-ob0-f178.google.com
Ironport-phdr: 9a23:IsVA5REuVMOUUl6aciw9bZ1GYnF86YWxBRYc798ds5kLTJ75o8WwAkXT6L1XgUPTWs2DsrQf27WQ7vqrADxeqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLsh7/0pseYOlUWzBOGIppMbzyO5T3LsccXhYYwYo0Q8TDu5kVyRuJN2GlzLkiSlRuvru25/Zpk7jgC86l5r50IAu3GePEzSqUdBzA7OShh78ry8BLHUAGn530GU2xQnAAeUCbf6xSvfJ7qtS2ymfB6wzLSac//VrcyVi6l9Lw6YBDtgSYDcTU+9TeE2YRLkKtHrUf59FREyInObdTNOQ==

Is there a way to detect whether or not an included .cmo file comes from the right version of Coq? In particular, say that you `make install` Coq 8.5, and then you `make install` Coq 8.4, then the file:

let test = Universes.constr_of_global

will successfully compile using coq_makefile. Is there something else I can add to this file (e.g., a reference to the Coq version number) or something I can do (e.g., turning it into enough of a plugin that I can load it in a .v file, whence coq will complain) that I can use this strategy to do feature-tests for the various versions of Coq?

Thanks,

Jason

[Coq-Club] Ensuring that OCaml files come from the right version of Coq?, Jason Gross, 02/21/2016