8000 GitHub - andres-erbsen/riscv-coq: RISC-V Specification in Coq
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

andres-erbsen/riscv-coq

 
 

Repository files navigation

RISC-V Specification in Coq

Generated from the RISCV Semantics in Haskell using hs-to-coq, with some manually written Coq files too.

Build

You will need Coq 8.9 or master.

riscv-coq depends on the coqutil library. You can get this dependency and build the project using the following commands:

git clone https://github.com/mit-plv/coqutil.git
git clone https://github.com/mit-plv/riscv-coq.git
make -C coqutil
cd riscv-coq/
make

If it doesn't build

If something doesn't work, you could try to do exactly the same as bedrock2 does, which uses riscv-coq as a dependency and has Travis Continuous Integration, so if you pick a commit with a green tick there, you can be sure to have a working version.

About

RISC-V Specification in Coq

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages

  • Rocq Prover 61.5%
  • Python 17.4%
  • C++ 14.9%
  • C 4.3%
  • Other 1.9%
0