diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-06-11 11:41:37 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-06-11 11:41:37 +0200 |
| commit | af16cdae6d58033cc8aa06bca330f98b96ba12f2 (patch) | |
| tree | 4985e9ae8fa0d580bbf95a198edeca4f0bd6ff46 /INSTALL.md | |
| parent | 21c979fce33b068ce4b86e67d3d866b203411c6c (diff) | |
| parent | 02b169b444c435b8d1aacf54969dd7de57317a5c (diff) | |
| download | compcert-kvx-af16cdae6d58033cc8aa06bca330f98b96ba12f2.tar.gz compcert-kvx-af16cdae6d58033cc8aa06bca330f98b96ba12f2.zip | |
Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into BTL
Diffstat (limited to 'INSTALL.md')
| -rw-r--r-- | INSTALL.md | 13 |
1 files changed, 11 insertions, 2 deletions
@@ -34,12 +34,21 @@ Install dependencies available through opam opam install coq menhir ``` +Note: it may happen that a newer version of Coq is not supported yet. +You may downgrade to solve the problem: +``` +opam pin add coq 8.11.0 # example of Coq version +``` + ## Compilation Pre-compilation configure replace the placeholder with your desired platform (for Kalray Coolidge it is `kvx-cos`) ``` -./configure <platform> +./configure -prefix ~/.usr <platform> ``` + +`PREFIX` is where CompCert will be installed after `make install` + If using Kalray's platform, make sure that the kvx tools are on your path Compile (adapt -j# to the number of cores and available RAM) ``` @@ -48,7 +57,7 @@ make install ``` ## Utilization -`ccomp` binaries are installed at `$(HOME)/.usr/bin` +`ccomp` binaries are installed at `$(PREFIX)/bin` Make sure to add that to your path to ease its use Now you may use it like a regular compiler ``` |