summaryrefslogtreecommitdiff
path: root/dev/ci/README.md
diff options
context:
space:
mode:
Diffstat (limited to 'dev/ci/README.md')
-rw-r--r--dev/ci/README.md45
1 files changed, 35 insertions, 10 deletions
diff --git a/dev/ci/README.md b/dev/ci/README.md
index 43d680af..60a86362 100644
--- a/dev/ci/README.md
+++ b/dev/ci/README.md
@@ -126,7 +126,7 @@ patch (or ask someone to prepare a patch) to fix the project:
developer who merges the PR on Coq. There are plans to improve this, cf.
[#6724](https://github.com/coq/coq/issues/6724).
-Moreover your PR must absolutely update the [`CHANGES`](../../CHANGES) file.
+Moreover your PR must absolutely update the [`CHANGES.md`](../../CHANGES.md) file.
Advanced GitLab CI information
------------------------------
@@ -136,15 +136,35 @@ rebuilding Coq. In one job, Coq is built with `./configure -prefix _install_ci`
and `make install` is run, then the `_install_ci` directory
persists to and is used by the next jobs.
-Artifacts can also be downloaded from the GitLab repository.
-Currently, available artifacts are:
-- the Coq executables and stdlib, in three copies varying in
- architecture and OCaml version used to build Coq.
-- the Coq documentation, built only in the `build:base` job. When submitting
- a documentation PR, this can help reviewers checking the rendered result.
+### Artifacts
-As an exception to the above, jobs testing that compilation triggers
-no OCaml warnings build Coq in parallel with other tests.
+Build artifacts from GitLab can be linked / downloaded in a systematic
+way, see [GitLab's documentation](https://docs.gitlab.com/ce/user/project/pipelines/job_artifacts.html#downloading-the-latest-job-artifacts)
+for more information. For example, to access the documentation of the
+`master` branch, you can do:
+
+https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/sphinx/html/index.html?job=doc:refman
+
+Browsing artifacts is also possible:
+https://gitlab.com/coq/coq/-/jobs/artifacts/master/browse/_install_ci/?job=build:base
+
+Above, you can replace `master` and `job` by the desired GitLab branch and job name.
+
+Currently available artifacts are:
+
+- the Coq executables and stdlib, in four copies varying in
+ architecture and OCaml version used to build Coq:
+ https://gitlab.com/coq/coq/-/jobs/artifacts/master/browse/_install_ci/?job=build:base
+
+- the Coq documentation, built in the `doc:*` jobs. When submitting
+ a documentation PR, this can help reviewers checking the rendered result:
+
+ + Coq's Reference Manual [master branch]
+ https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/sphinx/html/index.html?job=doc:refman
+ + Coq's Standard Library Documentation [master branch]
+ https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/html/stdlib/index.html?job=build:base
+ + Coq's ML API Documentation [master branch]
+ https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/dev/ocamldoc/html/index.html?job=doc:ml-api
### GitLab and Windows
@@ -152,6 +172,11 @@ If your repository has access to runners tagged `windows`, setting the
secret variable `WINDOWS` to `enabled` will add jobs building Windows
versions of Coq (32bit and 64bit).
+If the secret variable `WINDOWS` is set to `enabled_all_addons`,
+an extended set of addons will be added to the Windows installer.
+This leads to a considerable runtime in CI so this is not enabled
+by default for pipelines for pull requests.
+
The Windows jobs are enabled on Coq's repository, where pipelines for
pull requests run.
@@ -171,6 +196,6 @@ but if you wish to save more time you can skip the job by setting
This means you will need to change its value when the Docker image
needs to be updated. You can do so for a single pipeline by starting
-it through the web interface..
+it through the web interface.
See also [`docker/README.md`](docker/README.md).