diff options
author | Cyril Six <cyril.six@univ-grenoble-alpes.fr> | 2019-07-12 10:09:11 +0200 |
---|---|---|
committer | Cyril Six <cyril.six@univ-grenoble-alpes.fr> | 2019-07-12 10:09:11 +0200 |
commit | 5d69b44d38730c7112634bf6f815168065ac9aad (patch) | |
tree | abb4bdbc5b27fa8c9ecf0d576c9907b498e8e5f6 /INSTALL.md | |
parent | ad8831a83451fc9802a8438256e68e25df5c243d (diff) | |
parent | 579f9df3d1f77e9db1696cb438ba00f6e3043ff3 (diff) | |
download | compcert-kvx-5d69b44d38730c7112634bf6f815168065ac9aad.tar.gz compcert-kvx-5d69b44d38730c7112634bf6f815168065ac9aad.zip |
Merge branch '140-install-instructions' into 'mppa-work'
Initial version of install instructions
See merge request sixcy/CompCert!1
Diffstat (limited to 'INSTALL.md')
-rw-r--r-- | INSTALL.md | 62 |
1 files changed, 62 insertions, 0 deletions
diff --git a/INSTALL.md b/INSTALL.md new file mode 100644 index 00000000..bcfec78f --- /dev/null +++ b/INSTALL.md @@ -0,0 +1,62 @@ +# CompCert Install Instructions + +## Dependencies +### Additional dependencies +Replace with the package manager for your distribution +``` +sudo <pkg-manager> install -y mercurial darcs ocaml + +``` + +### Opam +``` +sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh) +``` + +## Post-install +Run +``` +eval `opam config env` +``` +Add this to your `.bashrc` or `.bash_profile` +``` +. /nfs/home/mschuh/.opam/opam-init/init.sh > /dev/null 2> /dev/null || true +``` +Switch to last compiler version +``` +opam switch 4.07.0 +``` +Install dependecies available through opam +``` +opam install coq menhir +``` + +## Compilation +Pre-compilation configure replace the placeholder with your desired platform +(for Kalray it is k1c-cos or k1c-mbr) +``` +./configure <platform> +``` +If using Kalray's platform, make sure that the k1 tools are on your path +Compile (adapt -j# to the number of cores and available RAM) +``` +make -j12 +make install +``` + +## Utilization +`ccomp` binaries are installed at `$(HOME)/.usr/bin` +Make sure to add that to your path to ease its use +Now you may use it like a regular compiler +``` +ccomp -O3 test.c -S +ccomp -O3 test.c -o test.bin +``` + +## Changing platform +If you decide to change the platform, for instance from k1c-cos to k1c-mbr, you +should change the `compcert.ini` file with the respective tools and then run +``` +make install +``` + |