diff options
| author | ymherklotz <ymherklotz@users.noreply.github.com> | 2021-01-16 22:46:00 +0000 |
|---|---|---|
| committer | ymherklotz <ymherklotz@users.noreply.github.com> | 2021-01-16 22:46:00 +0000 |
| commit | 04e130c7208c7ed29f11892d6b53c734fdcf03ac (patch) | |
| tree | 8de694b153aeba61485c1ae7b833dd2ab6fe4a72 /docs/building | |
| parent | 3be488277ce46005570f08888fbf3125b9187c88 (diff) | |
| download | vericert-docs-04e130c7208c7ed29f11892d6b53c734fdcf03ac.tar.gz vericert-docs-04e130c7208c7ed29f11892d6b53c734fdcf03ac.zip | |
deploy: 926cda1879a6c8bae3ba21de41763aac3e4f5637
Diffstat (limited to 'docs/building')
| -rw-r--r-- | docs/building/index.html | 2 |
1 files changed, 1 insertions, 1 deletions
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."><meta name=theme-color content="#FFFFFF"><meta property="og:title" content="Building Vericert"><meta property="og:description" content="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."><meta property="og:type" content="article"><meta property="og:url" content="https://ymherklotz.github.io/vericert-docs/docs/building/"><title>Building Vericert | Vericert</title><link rel=manifest href=/vericert-docs/manifest.json><link rel=icon href=/vericert-docs/favicon.png type=image/x-icon><link rel=stylesheet href=/vericert-docs/book.min.9a01d8047438cc0bac3d13e2a238c5a321f8116bf4a172e80d498712a58ce50d.css integrity="sha256-mgHYBHQ4zAusPRPiojjFoyH4EWv0oXLoDUmHEqWM5Q0="><script defer src=/vericert-docs/en.search.min.77eecb367a48b50a7df2acdb69aba4b0107b4b1306bd8f7510bb929a260db0b1.js integrity="sha256-d+7LNnpItQp98qzbaauksBB7SxMGvY91ELuSmiYNsLE="></script></head><body><input type=checkbox class="hidden toggle" id=menu-control> + Coq: theorem prover that is used to also program the HLS tool."><meta property="og:type" content="article"><meta property="og:url" content="https://ymherklotz.github.io/vericert-docs/docs/building/"><title>Building Vericert | Vericert</title><link rel=manifest href=/vericert-docs/manifest.json><link rel=icon href=/vericert-docs/favicon.png type=image/x-icon><link rel=stylesheet href=/vericert-docs/book.min.f293138e0a08c254389412feb3e3e0d37d986a59b4b3a535af7719b0831b81bd.css integrity="sha256-8pMTjgoIwlQ4lBL+s+Pg032Yalm0s6U1r3cZsIMbgb0="><script defer src=/vericert-docs/en.search.min.77eecb367a48b50a7df2acdb69aba4b0107b4b1306bd8f7510bb929a260db0b1.js integrity="sha256-d+7LNnpItQp98qzbaauksBB7SxMGvY91ELuSmiYNsLE="></script></head><body><input type=checkbox class="hidden toggle" id=menu-control> <input type=checkbox class="hidden toggle" id=toc-control><main class="container flex"><aside class=book-menu><nav><h2 class=book-brand><a href=/vericert-docs><span>Vericert</span></a></h2><div class=book-search><input type=text id=book-search-input placeholder=Search aria-label=Search maxlength=64 data-hotkeys=s/><div class="book-search-spinner hidden"></div><ul id=book-search-results></ul></div><ul><li><a href=https://ymherklotz.github.io/vericert-docs/docs/>Docs</a><ul><li><a href=https://ymherklotz.github.io/vericert-docs/docs/building/ class=active>Building Vericert</a></li><li><a href=https://ymherklotz.github.io/vericert-docs/docs/using-vericert/>Using Vericert</a></li></ul></li></ul><ul><li><a href=https://github.com/ymherklotz/vericert target=_blank rel=noopener>Github</a></li></ul></nav><script>(function(){var menu=document.querySelector("aside.book-menu nav");addEventListener("beforeunload",function(event){localStorage.setItem("menu.scrollTop",menu.scrollTop);});menu.scrollTop=localStorage.getItem("menu.scrollTop");})();</script></aside><div class=book-page><header class=book-header><div class="flex align-center justify-between"><label for=menu-control><img src=/vericert-docs/svg/menu.svg class=book-icon alt=Menu></label> <strong>Building Vericert</strong> <label for=toc-control><img src=/vericert-docs/svg/toc.svg class=book-icon alt="Table of Contents"></label></div><aside class="hidden clearfix"><nav id=TableOfContents><ul><li><ul><li><a href=#downloading-compcert>Downloading CompCert</a></li><li><a href=#setting-up-nix>Setting up Nix</a></li><li><a href=#makefile-build>Makefile build</a></li><li><a href=#testing>Testing</a></li></ul></li></ul></nav></aside></header><article class=markdown><p>To build Vericert, the provided Makefile can be used. External dependencies are needed to build the project, which can be pulled in automatically with <a href=https://nixos.org/nix/>nix</a> using the provided <code>default.nix</code> and <code>shell.nix</code> files.</p><p>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:</p><ul><li><a href=https://coq.inria.fr/>Coq</a>: theorem prover that is used to also program the HLS tool.</li><li><a href=https://ocaml.org/>OCaml</a>: the OCaml compiler to compile the extracted files.</li><li><a href=https://github.com/mit-plv/bbv>bbv</a>: an efficient bit vector library.</li><li><a href=https://github.com/ocaml/dune>dune</a>: build tool for ocaml projects to gather all the ocaml files and compile them in the right order.</li><li><a href=http://gallium.inria.fr/~fpottier/menhir/>menhir</a>: parser generator for ocaml.</li><li><a href=https://github.com/ocaml/ocamlfind>findlib</a> to find installed OCaml libraries.</li><li><a href=https://gcc.gnu.org/>GCC</a>: compiler to help build CompCert.</li></ul><p>These dependencies can be installed manually, or automatically through Nix.</p><div class=highlight><pre class=chroma><code class=language-coq data-lang=coq><span class=kn>Definition</span> <span class=n>help</span> <span class=o>:=</span> <span class=n>0</span><span class=o>.</span> |