coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Mario Alvarez <mmalvare AT eng.ucsd.edu>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] CompCert on Coq 8.5?
- Date: Tue, 19 Jan 2016 13:12:37 -0800
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mmalvare AT eng.ucsd.edu; spf=None smtp.mailfrom=mmalvare AT eng.ucsd.edu; spf=None smtp.helo=postmaster AT mail-ig0-f174.google.com
- Ironport-phdr: 9a23:kceBzxYzxOdlUBanH2obe/v/LSx+4OfEezUN459isYplN5qZpci6bnLW6fgltlLVR4KTs6sC0LqI9fGxEjVasd6oizMrTt9lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUiv2OQc9HOnpAIma153xjLDsvcyCKFwS1HKUWvBbElaflU3prM4YgI9veO4a6yDihT92QdlQ3n5iPlmJnhzxtY+a9Z9n9DlM6bp6r5YTGfayQ6NtRrtBST8iLmod5cvxtBCFQxHcyGEbVzAzmwBJBEDs6A/zRJrj+n//s+N5xiCAMOX7S79yRD+54+FmRAK+23RPDCIw7GyC0p84t6lcuh/0/xE=
Hi Coq Club,
I'm currently working on a development that depends on CompCert (mostly for floating-point operations, although we depend on CompCert's Fappli_IEEE_extras, so we can't just use vanilla Flocq). We want to make use of some of the features of 8.5, but there doesn't appear to be a released version of CompCert for 8.5.
Is anyone working on upgrading CompCert to work on top of Coq 8.5? If so, is there a way I could gain access to part of this development? I wouldn't need a port of the entire compiler, just the libraries related to floating-point numbers and their dependencies (so, Floats.v, Archi.v, Coqlib.v, Integers.v, perhaps a couple others I'm forgetting).
- [Coq-Club] CompCert on Coq 8.5?, Mario Alvarez, 01/19/2016
- Re: [Coq-Club] CompCert on Coq 8.5?, Jacques-Henri Jourdan, 01/20/2016
Archive powered by MHonArc 2.6.18.