diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2020-05-04 13:12:39 +0200 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2020-05-04 13:12:39 +0200 |
commit | 4f6c5833a149d0659f4bffaaeb464cd9864b3a9b (patch) | |
tree | 8310bebdd87a8ffde2e714bd0d61cffee91d496c | |
parent | cb7f9dae1d354bbf94d8da87e3d4c72057992965 (diff) | |
download | compcert-kvx-4f6c5833a149d0659f4bffaaeb464cd9864b3a9b.tar.gz compcert-kvx-4f6c5833a149d0659f4bffaaeb464cd9864b3a9b.zip |
Update on testsuite and INSTALL.md
-rw-r--r-- | INSTALL.md | 17 | ||||
-rwxr-xr-x | test/mppa/simucheck.sh | 4 | ||||
-rwxr-xr-x | test/mppa/simutest.sh | 4 |
3 files changed, 16 insertions, 9 deletions
@@ -1,14 +1,16 @@ # CompCert Install Instructions ## Dependencies + ### Additional dependencies + Replace with the package manager for your distribution ``` -sudo <pkg-manager> install -y mercurial darcs ocaml - +sudo <pkg-manager> install -y mercurial darcs ocaml bubblewrap ``` ### Opam + ``` sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh) ``` @@ -20,20 +22,21 @@ 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 +. $HOME/.opam/opam-init/init.sh > /dev/null 2> /dev/null || true ``` -Switch to last compiler version +Switch to a recent OCaml compiler version ``` -opam switch 4.07.0 +opam switch create 4.09.0 +opam switch 4.09.0 ``` -Install dependecies available through opam +Install dependencies 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) +(for Kalray Coolidge it is `k1c-cos`) ``` ./configure <platform> ``` diff --git a/test/mppa/simucheck.sh b/test/mppa/simucheck.sh index 25fb9947..48698e35 100755 --- a/test/mppa/simucheck.sh +++ b/test/mppa/simucheck.sh @@ -1,6 +1,8 @@ #!/bin/bash # Tests the execution of the binaries produced by CompCert, by simulation +cores=$(grep -c ^processor /proc/cpuinfo) + source do_test.sh -do_test check $1 +do_test check $cores diff --git a/test/mppa/simutest.sh b/test/mppa/simutest.sh index 3b1021e6..729d1ba0 100755 --- a/test/mppa/simutest.sh +++ b/test/mppa/simutest.sh @@ -1,6 +1,8 @@ #!/bin/bash # Tests the validity of the tests, in simulator +cores=$(grep -c ^processor /proc/cpuinfo) + source do_test.sh -do_test test $1 +do_test test $cores |