aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorSylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>2020-05-27 19:13:58 +0200
committerSylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>2020-05-27 19:13:58 +0200
commitaa78d4a8f9621d67dedc78ce5670b808eb2ef2c3 (patch)
tree42975153841c7b09b744eb56c57516dc38ec1140
parent9473c1fae4f1421666d9862fa16a26de182bcdf4 (diff)
downloadcompcert-kvx-aa78d4a8f9621d67dedc78ce5670b808eb2ef2c3.tar.gz
compcert-kvx-aa78d4a8f9621d67dedc78ce5670b808eb2ef2c3.zip
add coq2html for pages
-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.