aboutsummaryrefslogtreecommitdiffstats
path: root/INSTALL.md
diff options
context:
space:
mode:
authorCyril SIX <cyril.six@kalray.eu>2021-06-01 18:28:11 +0200
committerCyril SIX <cyril.six@kalray.eu>2021-06-01 18:28:11 +0200
commit3181fe5407ed0221714830e2bd1e19850eac5461 (patch)
tree2dac9283c1a36182b1a80b76483aed6c16dfdbc8 /INSTALL.md
parent14b113df3ed94998707b6ac851e0d550ed7f14e1 (diff)
downloadcompcert-kvx-3181fe5407ed0221714830e2bd1e19850eac5461.tar.gz
compcert-kvx-3181fe5407ed0221714830e2bd1e19850eac5461.zip
Remove install path bricolage for kvxv3.9_kvx
Diffstat (limited to 'INSTALL.md')
-rw-r--r--INSTALL.md7
1 files changed, 5 insertions, 2 deletions
diff --git a/INSTALL.md b/INSTALL.md
index e80fb600..f072a211 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -44,8 +44,11 @@ opam pin add coq 8.11.0 # example of Coq version
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)
```
@@ -54,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
```