coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Early alpha port of CompCert to 32-bit RISC-V

From: Prashanth Mundkur <pmundkur.fm AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Early alpha port of CompCert to 32-bit RISC-V
Date: Fri, 2 Sep 2016 11:10:55 -0700
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=pmundkur.fm AT gmail.com; spf=Pass smtp.mailfrom=pmundkur.fm AT gmail.com; spf=None smtp.helo=postmaster AT mail-pf0-f180.google.com
Ironport-phdr: 9a23:vljgTB1z+gw4yBDtsmDT+DRfVm0co7zxezQtwd8ZsegQKPad9pjvdHbS+e9qxAeQG96KsrQZ0KGP6/CoGTRZp83Q6DZaKN0EfiRGoP1epxYnDs+BBB+zB9/RRAt+Iv5/UkR49WqwK0lfFZW2TVTTpnqv8WxaQU2nZkJLL+j4UrTfk96wn7jrvcaCOkMV33HkOeM6bE3v616A7o9O2coqA51y4yOBmmFPdeVSyDEgDnOotDG42P2N+oV++T9bofMr+p0Ie6z7e6MlUe4QV2x+YChmrPHs4BLEVE6E4mYWemQQiBtBRQbfvz/gWZKkijHzrep03jWadejrS7w3RC7qu79uVRnkizodcTA82G7Sg810yqlcpUTy9FRE34fIbdTNZ7JFdaTHcIZCSA==

Hi Jeehoon,

On 02:12 Sat 03 Sep, Jeehoon Kang wrote:
> That's very cool! Thank you for sharing your development.
>
> I wonder if why you port an old version of CompCert. More concretely, are
> there any technical difficulties in porting CompCert 2.7 to RISC V?

None, other than a lack of time. CompCert 2.6 was the latest version
when I started the port. I have a local tree for 2.7.1, but I've not
been getting enough time to finish it as I'd like.

It seemed better to make the announcement instead of waiting longer,
since port was known to some but its status was not clear since no
public announcement had been made.

--prashanth

[Coq-Club] Early alpha port of CompCert to 32-bit RISC-V, Prashanth Mundkur, 09/02/2016
- Re: [Coq-Club] Early alpha port of CompCert to 32-bit RISC-V, Jeehoon Kang, 09/02/2016
  - Re: [Coq-Club] Early alpha port of CompCert to 32-bit RISC-V, Prashanth Mundkur, 09/02/2016