diff options
Diffstat (limited to 'dev/ci/README.md')
| -rw-r--r-- | dev/ci/README.md | 50 |
1 files changed, 36 insertions, 14 deletions
diff --git a/dev/ci/README.md b/dev/ci/README.md index 45176581cd..3a179a9431 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -75,9 +75,6 @@ We are currently running tests on the following platforms: camlp5, and with warnings as errors; it runs the test-suite and tests the compilation of several external developments. -- Circle CI runs tests that are redundant with GitLab CI and may be removed - eventually. - - Travis CI is used to test the compilation of Coq and run the test-suite on macOS. It also runs a linter that checks whitespace discipline. A [pre-commit hook](../tools/pre-commit) is automatically installed by @@ -139,15 +136,41 @@ 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 + +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 + + Additionally, an experimental Dune build is provided: + https://gitlab.com/coq/coq/-/jobs/artifacts/master/browse/_build/?job=build:edge:dune:dev + +- 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=doc:refman + + 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:ocamldoc -As an exception to the above, jobs testing that compilation triggers -no OCaml warnings build Coq in parallel with other tests. + The dune job also provides its own API documentation using the newer `odoc` tool: + https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_build/default/_doc/_html/index.html?job=doc:ml-api:odoc ### GitLab and Windows @@ -165,8 +188,7 @@ automatically built and uploaded to your GitLab registry, and is loaded by subsequent jobs. **IMPORTANT**: When updating Coq's CI docker image, you must modify -the `CACHEKEY` variable in [`.gitlab-ci.yml`](../../.gitlab-ci.yml), -[`.circleci/config.yml`](../../.circleci/config.yml), +the `CACHEKEY` variable in [`.gitlab-ci.yml`](../../.gitlab-ci.yml) and [`Dockerfile`](docker/bionic_coq/Dockerfile) The Docker building job reuses the uploaded image if it is available, @@ -175,6 +197,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). |