aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--.gitlab-ci.yml2
-rw-r--r--README_Kalray.md5
2 files changed, 7 insertions, 0 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 7bb51ff2..442b56e0 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -272,6 +272,8 @@ pages:
- eval `opam config env`
- opam update
- opam install -y menhir
+ - opam repo add coq-released https://coq.inria.fr/opam/released
+ - opam install coq-coq2html
script:
- source /opt/kalray/accesscore/kalray.sh && ./config_kvx.sh
- source /opt/kalray/accesscore/kalray.sh && make -j "$NJOBS" documentation
diff --git a/README_Kalray.md b/README_Kalray.md
index 7dba03dd..86c49ad1 100644
--- a/README_Kalray.md
+++ b/README_Kalray.md
@@ -16,6 +16,11 @@ This delivery contains (in addition to features from CompCert master branch):
Please follow the instructions in `INSTALL.md`
+## Documentation of the Coq sources
+
+The documentation is available [online](https://certicompil.gricad-pages.univ-grenoble-alpes.fr/compcert-kvx).
+You may also generate it locally from `make documentation` (after installation via `INSTALL.md`): the entry-point is in `doc/index-kvx.html`.
+
## Testing
We modified most of the CompCert tests of the `c` folder in order for them to be executable in reasonable time by the simulator.