From 4f6c5833a149d0659f4bffaaeb464cd9864b3a9b Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Mon, 4 May 2020 13:12:39 +0200 Subject: Update on testsuite and INSTALL.md --- INSTALL.md | 17 ++++++++++------- test/mppa/simucheck.sh | 4 +++- test/mppa/simutest.sh | 4 +++- 3 files changed, 16 insertions(+), 9 deletions(-) diff --git a/INSTALL.md b/INSTALL.md index bcfec78f..256bfa4e 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -1,14 +1,16 @@ # CompCert Install Instructions ## Dependencies + ### Additional dependencies + Replace with the package manager for your distribution ``` -sudo install -y mercurial darcs ocaml - +sudo 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 ``` 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 -- cgit