The Coq mailing list

[Prashanth Mundkur <pmundkur.fm AT gmail.com>]

Hi,

I'd like to announce an early alpha version of an unofficial port of
CompCert to the 32-bit version of the RISC-V architecture.  More
information on RISC-V is at https://riscv.org

It is available on github, in the riscv-2.6-alpha branch of the below
repo; the readme is here:

https://github.com/pmundkur/CompCert/blob/riscv-2.6-alpha/README-rv32.md

Please note the early alpha status:

- Although integer support has been lightly tested and found to work,
  floating-point support is incomplete, and known broken.

- It is a port of an earlier release of CompCert, viz version 2.6,
  which requires Coq 8.4.

- It's been tested on the newlib version of the RISC-V GNU toolchain,
  as of a couple of months ago.  It has not been tested on glibc, or a
  recent toolchain.  The RISC-V toolchains are in a fair amount of
  flux.

I'm making this announcement despite the early alpha status since it
might be of interest to CompCert and Coq users, especially people in
the DeepSpec community.

Thanks,

--prashanth