diff options
| -rw-r--r-- | .gitlab-ci.yml | 15 | ||||
| -rw-r--r-- | Makefile.dune | 7 | ||||
| -rw-r--r-- | dev/ci/README.md | 7 | ||||
| -rw-r--r-- | kernel/constr.mli | 4 | ||||
| -rw-r--r-- | kernel/type_errors.mli | 2 | ||||
| -rw-r--r-- | lib/genarg.mli | 4 | ||||
| -rw-r--r-- | pretyping/tacred.mli | 2 |
7 files changed, 32 insertions, 9 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index ce4da41bf6..0115ac9eff 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -275,7 +275,7 @@ doc:refman: dependencies: - build:base -doc:ml-api: +doc:ml-api:ocamldoc: stage: test dependencies: - build:edge @@ -287,6 +287,19 @@ doc:ml-api: paths: - dev/ocamldoc +doc:ml-api:odoc: + <<: *dune-template + stage: test + dependencies: + - build:egde:dune:dev + variables: + OPAM_SWITCH: edge + DUNE_TARGET: apidoc + artifacts: + name: "$CI_JOB_NAME" + paths: + - _build/default/_doc/ + test-suite:base: <<: *test-suite-template dependencies: diff --git a/Makefile.dune b/Makefile.dune index f90f555557..e04982650f 100644 --- a/Makefile.dune +++ b/Makefile.dune @@ -13,6 +13,7 @@ help: @echo " - states: build a minimal functional coqtop" @echo " - world: build all binaries and libraries" @echo " - release: build Coq in release mode" + @echo " - apidoc: build ML API documentation" @echo " - clean: remove build directory and autogenerated files" @echo " - help: show this message" @@ -29,6 +30,12 @@ world: voboot release: voboot dune build $(DUNEOPT) -p coq +apidoc: + # Ugly workaround for https://github.com/ocaml/odoc/issues/148 + mv checker/dune checker/dune.disabled || true + dune build $(DUNEOPT) @doc + mv checker/dune.disabled checker/dune || true + clean: dune clean diff --git a/dev/ci/README.md b/dev/ci/README.md index 95892ebe0a..3a179a9431 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -157,7 +157,7 @@ Currently available artifacts are: 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 + 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: @@ -167,7 +167,10 @@ Currently available artifacts are: + 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 + https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/dev/ocamldoc/html/index.html?job=doc:ml-api:ocamldoc + + 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 diff --git a/kernel/constr.mli b/kernel/constr.mli index 70acf19328..8fe77d448e 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -285,8 +285,8 @@ val destMeta : constr -> metavariable (** Destructs a variable *) val destVar : constr -> Id.t -(** Destructs a sort. [is_Prop] recognizes the sort {% \textsf{%}Prop{% }%}, whether - [isprop] recognizes both {% \textsf{%}Prop{% }%} and {% \textsf{%}Set{% }%}. *) +(** Destructs a sort. [is_Prop] recognizes the sort [Prop], whether + [isprop] recognizes both [Prop] and [Set]. *) val destSort : constr -> Sorts.t (** Destructs a casted term *) diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index 9c6ef64b50..3fd40a7f42 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -12,7 +12,7 @@ open Names open Constr open Environ -(** Type errors. {% \label{%}typeerrors{% }%} *) +(** Type errors. {% \label{typeerrors} %} *) (*i Rem: NotEnoughAbstractionInFixBody should only occur with "/i" Fix notation i*) diff --git a/lib/genarg.mli b/lib/genarg.mli index bb85f99e3c..52db3df088 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -13,7 +13,7 @@ (** The route of a generic argument, from parsing to evaluation. In the following diagram, "object" can be tactic_expr, constr, tactic_arg, etc. -{% \begin{%}verbatim{% }%} +{% \begin{verbatim} %} parsing in_raw out_raw char stream ---> raw_object ---> raw_object generic_argument -------+ encapsulation decaps| @@ -36,7 +36,7 @@ In the following diagram, "object" can be tactic_expr, constr, tactic_arg, etc. | V effective use -{% \end{%}verbatim{% }%} +{% \end{verbatim} %} To distinguish between the uninterpreted, globalized and interpreted worlds, we annotate the type [generic_argument] by a diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index e6065dda87..bf38c30a1f 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -23,7 +23,7 @@ type reduction_tactic_error = exception ReductionTacticError of reduction_tactic_error -(** {6 Reduction functions associated to tactics. {% \label{%}tacred{% }%} } *) +(** {6 Reduction functions associated to tactics. } *) (** Evaluable global reference *) |