From 6ed58d0f7a800b3ce1ca815b7b348a9cbf7af0eb Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 6 Dec 2021 18:51:59 +0100 Subject: update the README and INSTALL documents --- INSTALL.md | 47 ++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 38 insertions(+), 9 deletions(-) (limited to 'INSTALL.md') diff --git a/INSTALL.md b/INSTALL.md index f072a211..5e2e800d 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -16,6 +16,7 @@ sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install. ``` ## Post-install + Run ``` eval `opam config env` @@ -26,8 +27,8 @@ Add this to your `.bashrc` or `.bash_profile` ``` Switch to a recent OCaml compiler version ``` -opam switch create 4.09.0 -opam switch 4.09.0 +opam switch create 4.12.0 +opam switch 4.12.0 ``` Install dependencies available through opam ``` @@ -37,18 +38,20 @@ 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 +opam pin add coq 8.12.2 # example of Coq version ``` ## Compilation -Pre-compilation configure replace the placeholder with your desired platform -(for Kalray Coolidge it is `kvx-cos`) + +You can choose change the installation directory by modifying the +`config_simple.sh` file before running the configuration script. + +Then, use the configuration script corresponding to your desired platform: +(for Kalray Coolidge it is `config_kvx.sh`) ``` -./configure -prefix ~/.usr +./config_.sh ``` -`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) ``` @@ -56,8 +59,22 @@ make -j12 make install ``` +## Tests + +## Documentation + +You can generate the documentation locally with: +``` +make documentation +``` + +Note that you need to install [coq2html](https://github.com/xavierleroy/coq2html) +before doing so. + ## Utilization -`ccomp` binaries are installed at `$(PREFIX)/bin` + +`ccomp` binaries are installed at `$(CCOMP_INSTALL_PREFIX)/bin` +(variable defined in `config_simple.sh`). Make sure to add that to your path to ease its use Now you may use it like a regular compiler ``` @@ -66,9 +83,21 @@ ccomp -O3 test.c -o test.bin ``` ## Changing platform + If you decide to change the platform, for instance from kvx-cos to kvx-mbr, you should change the `compcert.ini` file with the respective tools and then run ``` make install ``` +## Cleaning + +To clean only object files while keeping the platform configuration: +``` +make clean +``` + +To clean everything (to then reconfigure for another platform): +``` +make distclean +``` -- cgit