From 04e130c7208c7ed29f11892d6b53c734fdcf03ac Mon Sep 17 00:00:00 2001 From: ymherklotz Date: Sat, 16 Jan 2021 22:46:00 +0000 Subject: deploy: 926cda1879a6c8bae3ba21de41763aac3e4f5637 --- docs/building/index.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'docs/building/index.html') diff --git a/docs/building/index.html b/docs/building/index.html index ddff1f7..80e35ed 100644 --- a/docs/building/index.html +++ b/docs/building/index.html @@ -2,7 +2,7 @@ The project is written in Coq, a theorem prover, which is extracted to OCaml so that it can then be compiled and executed. The dependencies of this project are the following: Coq: theorem prover that is used to also program the HLS tool.">Building Vericert | Vericert + Coq: theorem prover that is used to also program the HLS tool.">Building Vericert | Vericert
Building Vericert

To build Vericert, the provided Makefile can be used. External dependencies are needed to build the project, which can be pulled in automatically with nix using the provided default.nix and shell.nix files.

The project is written in Coq, a theorem prover, which is extracted to OCaml so that it can then be compiled and executed. The dependencies of this project are the following:

  • Coq: theorem prover that is used to also program the HLS tool.
  • OCaml: the OCaml compiler to compile the extracted files.
  • bbv: an efficient bit vector library.
  • dune: build tool for ocaml projects to gather all the ocaml files and compile them in the right order.
  • menhir: parser generator for ocaml.
  • findlib to find installed OCaml libraries.
  • GCC: compiler to help build CompCert.

These dependencies can be installed manually, or automatically through Nix.

Definition help := 0.
-- 
cgit