aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.doc
Commit message (Collapse)AuthorAge
* Remove some unused parts of the reference manual.Gravatar Guillaume Melquiond2017-09-22
|
* Merge PR #979: Fix install-doc target and other gitlab failuresGravatar Maxime Dénès2017-09-15
|\
| * Fix install-doc targetGravatar Gaëtan Gilbert2017-08-31
| | | | | | | | | | | | Since 8995d0857277019b54c24672439d3e19b2fcb5af [make doc] puts css files in subdirectories of doc/refman/html. These subdirectories cause a failure when doing [install doc/refman/html/* target].
* | [general] Merge parsing with highparsing, put toplevel at the top of the ↵Gravatar Emilio Jesus Gallego Arias2017-08-29
|/ | | | linking chain.
* Port ssr manual to Coq's latex/hevea styleGravatar Enrico Tassi2017-08-02
| | | | Work done by Assia Mahboubi and Enrico Tassi
* Makefile.doc: implement serve-refman-8080 targetGravatar Enrico Tassi2017-08-02
| | | | | | We make it so that, by default, the HTML reference manual looks like the one published online (same .css) and we provide a target to serve it locally (requires python).
* Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
|
* Gitlab CIGravatar Gaëtan Gilbert2017-05-28
|
* Farewell decl_modeGravatar Enrico Tassi2017-03-07
| | | | | This commit removes from the source tree plugins/decl_mode, its chapter in the reference manual and related tests.
* Avoid concurrent runs when producing html documentation (bug #5269).Gravatar Guillaume Melquiond2016-12-19
| | | | | | | | | | | | Make does not allow for rules that produce multiple outputs (unless they are pattern rules). As a consequence, the hacha rule could be run several times concurrently, thus causing doc/refman/html to be deleted under the feet of some runs. This commit fixes the issue by turning the rule into a single-output rule and adding a dummy rule to handle all the other indexes. Note that this is not a perfect solution since, if the user were to manually delete one of the auxiliary index, it would not be rebuilt until the main index is.
* Merge remote-tracking branch 'gforge/v8.5' into v8.6Gravatar Matthieu Sozeau2016-10-21
|\
| * Change the order of arguments of fig2dev.Gravatar Théo Zimmermann2016-10-19
| | | | | | | | | | | | For some reason, with my version of transfig (which seems to be the latest), the order of arguments of the fig2dev command matters: -L png must come before -m 2. I suppose that this fix shouldn't break things for others.
* | Makefile.doc: fix 'make doc'Gravatar Pierre Letouzey2016-06-23
| | | | | | | | | | | | Now, only 'phony' targets could be declared just via dependencies. For 'real-file' targets such as doc/refman/html/index.html, there should be a concrete production rule.
* | Makefile.build split in many smaller files : Makefile.{ide,checker,dev,install}Gravatar Pierre Letouzey2016-06-08
|/ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | General idea : Makefile.build was far too big to be easy to grasp or maintain, with information scattered everywhere. Let's try to tidy that! Normally, this commit is transparent for the user. We simply regroup some parts of Makefile.build in several new dedicated files: - Makefile.ide - Makefile.checker - Makefile.dev (for printers, revision, extra partial targets, otags) - Makefile.install These new files are "included" at the start of Makefile.build, to provide the same behavior as before, but with a Makefile.build shrinked by 50% (to approx 600 lines). Makefile.build now handles in priority the build of coqtop, minor tools, theories and plugins. Note: this is *not* a separate build system for coqchk nor coqide, even if this can be seen as a first step in this direction (won't be easy anyway to continue, due to the sharing of various stuff in lib and more). In particular Makefile.{coqchk,ide} may rely here and there on some generic rules left in Mafefile.build. Conversely, be sure to prefix rules in Makefile.{coqchk,ide} by checker/... or ide/... in order to avoid interferences with generic rules. Makefile.common is still there, but quite simplified. For instance, some variables that were used only once (e.g. lists of cmo files to link in the various tools) are now defined in Makefile.build, directly where they're needed. THEORIESVO and PLUGINSVO are made directly out of the theories/*/vo.itarget and plugins/*/vo.itarget files, no long manual list of subdirs anymore. Specific sub-targets such as 'reals' still exist, but in Makefile.dev, and they aren't mandatory. Makefile.doc is augmented by the rules building the documentation of the sources via ocamldoc. This classification attempt could probably be improved. For instance, the install rules for coqide are currently in Makefile.ide, but could also go in Makefile.install. Note that I've removed install-library-light which was broken anyway (arith isn't self-contained anymore).
* Remove generatable documentation files from repository. (Fix bug #4315)Gravatar Guillaume Melquiond2015-08-17
|
* Separate index for vernacular options.Gravatar Maxime Dénès2015-02-17
|
* Run coqdoc on the .v files from the plugins directory. (Fix for bug #2195)Gravatar Guillaume Melquiond2015-02-10
|
* Port to trunk the old commit r14895 of v8.4 (styles for the stdlib ↵Gravatar notin2014-12-09
| | | | | | documentation) This commit r14895 comes apparently itself from commit r12010 in branch v8.2
* doc: version number in cover.html + updates in coq.inria.fr styleGravatar Pierre Letouzey2014-11-07
|
* Install index_urls.txt in a location where coqide might actually find it.Gravatar Guillaume Melquiond2014-10-24
|
* Fix generation of the index_urls.txt file.Gravatar Guillaume Melquiond2014-10-24
| | | | | | Hevea has stopped producing HTML4 code two years ago. So the old sed expression was producing an empty index file for any user with a non-deprecated version of hevea.
* configure: get rid of the -src option and of ${COQSRC}Gravatar letouzey2012-08-23
| | | | | | | | | The -src option was antic and probably broken (many references to source files without the $COQRSC prefix). Instead, it's quite simpler to refer to paths in relative way (and safer in win32 where the base path may include spaces and other horrors). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15748 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improved synchronisation of stdlib index page with current library state.Gravatar herbelin2012-02-01
| | | | | | | | | | - Made generation of index page fail if a file is missing in list or listed but unbound in existing theories - Added a file hidden-files to optionally list library files not to show in the index page (though it is currently empty) - Added directory Unicode (why not to have it after all?) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14957 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile.doc: attempt to solve race condition for creating doc/refman/html.Gravatar herbelin2012-01-03
| | | | | | | | | Indeed, $INDEXURLS requires files from $INDEXES to be built and all of these files plus target doc/refman/html/index.html ask in parallel to erase and rebuild the doc/refman/html. Tried to use an intermediate phony target to factorize the rebuilding of doc/refman/html. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14872 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug 2669 and more: make full-stdlibGravatar pboutill2011-12-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14869 85f007b7-540e-0410-9357-904b9bb8a0f7
* Force dependency of Reference-Manual.pdf over Reference-Manual.dviGravatar herbelin2011-10-05
| | | | | | | | | to ensure not only that several passes are done and the references are correct but also to avoid one of the targets Reference-Manual.dvi or Reference-Manual.pdf reading .aux files modified concurrently by the other target. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14510 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile.doc: typo, index_url.txt should be index_urls.txtGravatar letouzey2011-09-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14481 85f007b7-540e-0410-9357-904b9bb8a0f7
* Various fixes in the MakefilesGravatar letouzey2011-09-17
| | | | | | | | | | | | | | | | | | | After a successful build, re-doing make world should almost do nothing. For that: - Many targets added to .PHONY, especially "tools" since a "tools" directory exists. And anyway this is said to speed-up make a bit. - Concerning fake_ide, mentionning the .cm* instead of the .ml* avoid rebuilding these .cm*, and hence possibly many other things. - in Makefile.doc: fix the rule building index_url.txt - coqtop.* is now built by $(BESTCOQMKTOP) instead of $(COQMKTOP) (which is the symlink). This avoids a situation where a first "make" could redo just a few files while a second "make" will rebuild many more. Typical scenario : touch the Makefile, 1st make was re-doing tolink.ml and then coqmktop, but no more, a 2nd make was then detecting that coqtop and the stdlib was to be redone git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14476 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add "make full-stdlib" to make all the doc in pdf as ask by bug 2395Gravatar pboutill2011-04-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13976 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added doc/refman/coqide.eps and coqide-queries.eps to remove the need for ↵Gravatar emakarov2010-09-06
| | | | | | pngtopnm and pnmtops git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13401 85f007b7-540e-0410-9357-904b9bb8a0f7
* Small improvements around coqdoc (including fix for bug #2288)Gravatar herbelin2010-03-30
| | | | | | | | | | | | - Local Definitions were considered Global Definitions in globalization file (bug #2288) [I made them "var" which makes them indexed like Variables, should we have an extra category just for Let's?] - the syntax of "[[" was not properly enforced in parse-comments mode - improved documentation of a few vernac file of the library - fixed a bug in Makefile.doc leading to build a bigger and bigger Library.pdf file git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12894 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix the stdlib doc compilation + switch all .v file to utf8Gravatar letouzey2009-09-28
| | | | | | | | | | | | | | | | | | | 1) compilation of Library.tex was failing on a "Ext_" in Diaconescu.v In fact coqdoc was trying to recognize the end of a _emphasis_ and hence inserted a bogus }. For the moment I've enclosed the phrase with [ ], but this emphasis "feature" of coqdoc seems _really_ easy to broke. Matthieu ? 2) By the way, this Library document was made from latin1 and utf8 source file, hence bogus characters. All .v containing special characters are converted to utf8, and their first line is now mentionning this. (+ killed some old french comments and some other avoidable special characters). PLEASE: let's stick to this convention and avoid latin1, at least in .v files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12363 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Tentatively made order-dependency wrt .vo files a full dependencyGravatar herbelin2009-09-15
| | | | | | | | | | | of the doc (use "make QUICK=1" to shortcut it) otherwise, the compilation of the doc is re-checked only when the doc files are removed. - Fixed a typo in coqdoc.sty and a redundancy in Makefile.common . git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12334 85f007b7-540e-0410-9357-904b9bb8a0f7
* install-doc* are PHONYGravatar lmamane2009-08-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12292 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tried to make F1 documentation tool working in CoqIDE.Gravatar herbelin2009-08-14
| | | | | | | | | | | | | | | | | | | | | | | In trunk: New strategy for compiling and finding index_url.txt. After all, this file is not specific to CoqIDE but to the documentation. Hence, it seems better to install it close to the documentation. If the documentation is locally installed, it is easy to find the file index_url.txt but what to do if the documentation is remote? We would need a http getter. Does this mean we have to rely on wget or so? In the absence of answer to this question, it seems reasonable, first to assume the doc to be locally installed, second to have a local copy of index_url.txt ready in the installation directory of CoqIDE. Also added an "automatic" field in the CoqIDE url preference to prevent the user to have to update his preference file every time a new version of Coq is out and the link to the doc change. In 8.2: Added a minima the installation of index_urls.txt but the user will have to update its preferences because the links "http://coq.inria.fr/doc/Reference-Manual010.html#..." do not longer exist. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12278 85f007b7-540e-0410-9357-904b9bb8a0f7
* Directory 'contrib' renamed into 'plugins', to end confusion with archive of ↵Gravatar letouzey2009-03-20
| | | | | | user contribs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile: fix ignored errors, several attempts to clarify thingsGravatar letouzey2009-03-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | * I encountered error messages during compilation, for instance ocamlopt complaining about non-existing coq_config.cmi when compiling coq_config.ml. Moreover, make was _not_ stopping at these errors (WTF?!). After some debug, it turned out to be (indirectly) my fault: I placed earlier the inclusion of the new .mllib.d in Makefile.stage1, but this is too early, coqdep, which is used to compute these files, isn't built yet. Due to the semantics of "-include", make tries to build it, fails with the above error, and goes on happily. Arrgh. After moving the inclusion of these .mllib.d to Makefile.stage2, everything seems to work ok now. * Since we're using such "nice" non-trivial features of make, I've started a small FAQ section about them at the beginning of Makefile * Recursive calls to make are now done with two options: --no-builtin-rules : let's avoid builtin rules like "%:%.o" ... --warn-undefined-variable : using a non-defined variable isn't necessarily bad, but I found a few bugs with this option, and I suggest we keep it. * Clarified the rules about stage* in Makefile and their STAGE*_TARGETS variables in Makefile.common. Now a newcomer _might_ have a chance to grasp in less than a day what's going on ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11983 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification du style du manuel de référenceGravatar notin2009-02-11
| | | | | | (cherry picked from commit b44a87556b68c08b7cd2fcbdaf2b4067b8a77427) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11916 85f007b7-540e-0410-9357-904b9bb8a0f7
* A few fixes for bug #2032 (backport r11857)Gravatar glondu2009-02-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11914 85f007b7-540e-0410-9357-904b9bb8a0f7
* More portable way to pipe stderrGravatar glondu2009-01-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11874 85f007b7-540e-0410-9357-904b9bb8a0f7
* Solves some warning and hides some not-bad ones in doc. It remains aGravatar herbelin2009-01-29
| | | | | | | | | few hevea warning (failure to put a vector on an expression in Classes.tex, failure to support multirow in RecTutorial.tex). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11868 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fixed various Overfull in documentation.Gravatar herbelin2009-01-27
| | | | | | | | | | - Removed useless coq-tex preprocessing of RecTutorial. - Make "Set Printing Width" applies to "Show Script" too. - Completed documentation (specially of ltac) according to CHANGES file. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11863 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backporting from v8.2 to trunk:Gravatar herbelin2009-01-18
| | | | | | | | | | - Filtering of doc compilation messages (11793,11795,11796). - Fixing bug #1925 and cleaning around bug #1894 (11796, 11801). - Adding some tests. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11802 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor doc fixes:Gravatar msozeau2009-01-08
| | | | | | | | | | | - Set BIBINPUTS variable correctly so that we do not use any random biblio.bib file. - Update setoid_rewrite doc to new typeclasses syntax and fix verb -> texttt - Stop using less than 100% line heights in coqdoc.css git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11767 85f007b7-540e-0410-9357-904b9bb8a0f7
* Produce better html code with coqdoc and improve doc:Gravatar msozeau2008-12-29
| | | | | | | | | | - correct nesting of a and div (fixes bug #2022) - use span instead of div for inline parts - fix standard lib template missing/new links - use -g to produce the stdlib doc (no proofs) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11724 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage des variables Coq et amélioration de coqmktop. LesGravatar notin2008-12-19
| | | | | | | | | | | | | | | | | | | | | | | | | | | principaux changements sont: - coqtop (et coqc) maintenant insensible aux variables d'environnement COQTOP, COQBIN et COQLIB; le chemin vers les librairies Coq peut être spécifié par l'option -coqlib - coqmktop prend 4 nouvelles options: -boot, -coqlib, -camlbin et -camlp4bin; en mode boot, coqmktop se réfère à Coq_config pour les chemins des exécutables OCaml; en dehors du mode boot, coqmktop cherche les exécutables OCaml dans PATH - installation des *.cmxs *.o et *.a en plus des *.cm[ioxa]; ceux-ci étant installé en copiant l'architecture des sources (ie lib.cmxa est installé dans COQLIB/lib/lib.cmxa) - coq_makefile prend maintenant 3 paramètres sous forme de variables d'environnement: COQBIN pour dire où trouver les exécutables Coq, CAMLBIN et CAMLP4BIN pour les exécutables OCaml et Camlp4/5; les chemins vers les librairies sont déduits en utilisant -where Le tout a testé avec Ssreflect (cf coq-contribs) en essayant de simuler les conditions de la vie réelle (Ocaml pas dans le PATH, installation binaire relocalisée, ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11707 85f007b7-540e-0410-9357-904b9bb8a0f7
* make doc ne compilait plus la doc de stdlib (bug #1996)Gravatar notin2008-11-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11588 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #1995Gravatar notin2008-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11580 85f007b7-540e-0410-9357-904b9bb8a0f7
* Oups...Gravatar notin2008-10-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11520 85f007b7-540e-0410-9357-904b9bb8a0f7
* Dépendance des cibles de la documentation envers les cibles de CoqGravatar notin2008-10-29
| | | | | | | | (devrait résoudre les problèmes avec 'make -j world') git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11519 85f007b7-540e-0410-9357-904b9bb8a0f7