| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Co-authored-by: Jim Fehrle <jfehrle@sbcglobal.net>
|
|
Reviewed-by: cpitclaudel
|
|
Cf. #12332
|
|
|
|
Fixes #11936.
Co-authored-by: Jim Fehrle <jfehrle@sbcglobal.net>
|
|
|
|
Currently, `.v` under the `Coq.` prefix are found in both `theories`
and `plugins`. Usually these two directories are merged by special
loadpath code that allows double-binding of the prefix.
This adds some complexity to the build and loadpath system; and in
particular, it prevents from handling the `Coq.*` prefix in the
simple, `-R theories Coq` standard way.
We thus move all `.v` files to theories, leaving `plugins` as an
OCaml-only directory, and modify accordingly the loadpath / build
infrastructure.
Note that in general `plugins/foo/Foo.v` was not self-contained, in
the sense that it depended on files in `theories` and files in
`theories` depended on it; moreover, Coq saw all these files as
belonging to the same namespace so it didn't really care where they
lived.
This could also imply a performance gain as we now effectively
traverse less directories when locating a library.
See also discussion in #10003
|
|
|
|
|
|
The way to override this default is not exactly the same as in the legacy Makefile
but it has been documented as well.
|
|
New targets refman, refman-html and refman-pdf.
sphinx keeps its previous meaning (compatibility alias for refman-html).
install-doc-sphinx has been accidentally renamed.
|
|
as separate NotationObject types, include in index.
|
|
The minimum required versions of the Sphinx-related (and ANTLR)
Python packages for Coq 8.10 were chosen as the lower bound
between what is currently in Debian Buster and in NixOS 18.09
Jellyfish (in practice the lower bound was always met by NixOS
18.09 Jellyfish).
These minimum required versions were documented.
In the docker image used by GitLab CI, we install these
Python packages through pip as this allows us to pin them
to these specific versions.
In Travis, we let them unspecified to always test the
latest versions.
Finally, we also add the new dependencies of the Sphinx
PDF manual.
|
|
|
|
This is not optimal for we have to rebuild the `.cmi` as
`ocamldoc` cannot yet use the `_install_ci/` directory.
Overall the `mli` documentation is in a sorry state, however, I think
this is a first step in order to improve it.
Note that the `ml-doc` target seems broken in OCaml 4.07.0, needs
investigation.
cc: #7155
|
|
"treat errors as warnings" flag (-W) is applied. "1" or undefined
includes the flag, other values or undefined omit it.
Removed the "-warn-error" parameter to configure. "-profile XXX" will
no longer cause these flags to be used.
|
|
Relative links. Cf. #7800.
|
|
- Fix the Markdown.
- Add link to latest build of the refman for the master branch.
- Clarify what are the dependencies of the HTML doc.
[ci skip]
|
|
This will avoid in particular this ambiguous file extension.
[ci skip]
|
