aboutsummaryrefslogtreecommitdiff
path: root/Makefile.doc
AgeCommit message (Collapse)Author
2019-12-02Remove latex files that should be regenerated by makeJim Fehrle
If these files are present in the latex directory, "make refman-pdf" may fail to generate CoqRefMan.pdf.
2019-11-20Update grammar in the Terms section of Gallina chapterJim Fehrle
Update doc_grammar tool The grammar in the doc is generated semi-automatically with doc_grammar: - the grammar is automatically extracted from the mlg files - developer-prepared editing scripts *.mlg_edit modify the extracted grammar for clarity, simplicity and ordering of productions - chunks of the resulting grammar are automatically inserted into the rsts using instructions embedded in the rsts Running doc_grammar is currently a manual step. The grammar updates in the rst files have been manually reviewed.
2019-06-17Update py-style headers to new year.Théo Zimmermann
2019-05-21Fixing typos - Part 1JPR
2019-05-05[make] build unreleased.rstEnrico Tassi
2019-04-27Amending CYGWIN fix in 63e7fb56923 so that it does not add a warning on MacOS.Hugo Herbelin
Indeed, MacOS has a BSD uname and BSD uname does not support the -o option. Based on the following resources about uname compatility: https://stackoverflow.com/questions/3466166/how-to-check-if-running-in-cygwin-mac-or-linux https://en.wikipedia.org/wiki/Uname
2019-03-26Fix make sphinx failureJim Fehrle
2019-03-05[make] Sphinx: install only `html/` and `latex/` directoriesVincent Laporte
2019-02-14[coqlib] Remove `-boot` option for setting the coqlibEmilio Jesus Gallego Arias
Instead, if the coqlib is special, we set it explicitly in the command line, as Dune does. This is a continuation of #9523. In Sphinx, we stop using -boot, and pass `-coqlib` through the environment instead. Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2019-02-12Fix undefined SPHINX_DEPS when QUICKGaëtan Gilbert
2019-01-17Merge PR #9326: [ci] compile with -quick & validate after vio2voGaëtan Gilbert
Reviewed-by: ejgallego Ack-by: SkySkimmer Ack-by: gares Ack-by: ppedrot
2019-01-10[make] support for QUICKEnrico Tassi
The variable QUICK enables the quick compilation chain: - all v files are compiled with -quick to vio files (also -native-compiler no, since it is quicker) - then all vio files are turned to vo files $NJOBS at a time All occurrences of .vo use now .$(VO) that can be either .vo or .vio depending of QUICK being defined. Targets that only make sense for .vo files have to use $(VAR:.$(VO)=.vo)
2019-01-08Integrate plugin tutorial after code importGaëtan Gilbert
2018-10-10Include all menu entries in the menu/short TOC so that users can viewJim Fehrle
menu options for all chapters without having to load a new chapter. Change "Introcution" title to "Introduction and Contents"
2018-10-02[doc] [api] Remove `ocamldoc` support in favor of `odoc`Emilio Jesus Gallego Arias
This PR removes support for `ocamldoc` in favor of `odoc`. Following a recent discussion in OCaml's discord, it turns out that basically all the ecosystem has migrated to odoc, thus we follow suit and may focus on `odoc` for Coq's ML API documentation.
2018-09-25Fix Sphinx manual targets.Théo Zimmermann
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.
2018-09-20Fix race condition.Théo Zimmermann
2018-09-20[doc] Add sphinx-html, sphinx-latex, and sphinx-pdf targetsClément Pit-Claudel
2018-09-03[doc] Build ML API documentation artifact.Emilio Jesus Gallego Arias
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
2018-08-29Create SPHINXWARNERROR variable that controls whether the SphinxJim Fehrle
"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.
2018-06-08gitlab: build sphinx doc in separate jobGaëtan Gilbert
2018-05-22[doc] Fix an incorrect use of $PWD in Makefile.docClément Pit-Claudel
2018-05-12Sphinx: a "QUICK=1" option to bypass recompilation of the library.Hugo Herbelin
2018-05-10Clean-up in Makefile.doc and include Sphinx in doc-html target.Théo Zimmermann
2018-05-10Remove tutorials.Théo Zimmermann
2018-04-28[doc] Remove unused dependencies.Emilio Jesus Gallego Arias
AFAICS `imagemagick` `hacha` and `transfig` are not used anymore.
2018-04-16Remove LaTeX refman, now that migration to Sphinx is completeMaxime Dénès
2018-04-14[Sphinx] Build with warnings as errorsMaxime Dénès
Most of these warnings should really be errors (ill-formed input, invalid cross references, etc.) so we make it the default.
2018-04-14[Sphinx] Move chapter 9 to new infrastructure.Théo Zimmermann
2018-04-13[Sphinx] Move chapter 1 to new infrastructureMaxime Dénès
2018-04-11[Sphinx] Move chapter 29 to new infrastructureMaxime Dénès
2018-04-10[Sphinx] Move chapter 6 to new infrastructureMaxime Dénès
2018-04-10[Sphinx] Move chapter 15 to new infrastructureMaxime Dénès
2018-04-09[Sphinx] Move chapter 7 to new infrastructureMaxime Dénès
2018-04-05[Sphinx] Move chapter 30 to new infrastructureMaxime Dénès
2018-04-04[Sphinx] Move chapter 28 to new infrastructureMaxime Dénès
2018-03-30[Sphinx] Move chapter 27 to new infrastructureMaxime Dénès
2018-03-30[Sphinx] Move chapter 25 to new infrastructureMaxime Dénès
2018-03-29[Sphinx] Move chapter 26 to new infrastructureMaxime Dénès
2018-03-29[Sphinx] Move chapter 24 to new infrastructureMaxime Dénès
2018-03-29[Sphinx] Move chapter 23 to new infrastructureMaxime Dénès
2018-03-29[Sphinx] Move chapter 18 to new infrastructureMaxime Dénès
2018-03-26Move Classes.tex to type-classes.rstMatthieu Sozeau
2018-03-22Merge branch 'master' into sphinx-doc-chapter-22Guillaume Melquiond
2018-03-22Merge branch 'master' into sphinx-doc-chapter-21Guillaume Melquiond
2018-03-22Merge branch 'master' into sphinx-doc-chapter-19Guillaume Melquiond
2018-03-22[Sphinx] Move chapter 22 to new infrastructureMaxime Dénès
2018-03-22[Sphinx] Move chapter 21 to new infrastructureMaxime Dénès
2018-03-22[Sphinx] Move chapter 19 to new infrastructureMaxime Dénès
2018-03-22[Sphinx] Move chapter 17 to new infrastructureMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:23:51 +0000