aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.doc
Commit message (Collapse)AuthorAge
* 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
* Suppression de la dépendance de install-doc envers doc :Gravatar notin2008-10-17
| | | | | | | | | | - make install ne compile plus la doc - make world compile la doc (sauf si option --with-doc no) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11460 85f007b7-540e-0410-9357-904b9bb8a0f7
* report de la révision r11451 (nouveau style html pour le manuel de référence)Gravatar notin2008-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11452 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite commit #11311Gravatar notin2008-08-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11321 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix typoGravatar glondu2008-07-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11287 85f007b7-540e-0410-9357-904b9bb8a0f7
* Use COQINSTALLPREFIX for doc tooGravatar glondu2008-07-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11286 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de cibles pour le manuel de référence (refman-nodep, stdlib-nodep, ↵Gravatar notin2008-07-16
| | | | | | refman-quick) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11229 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mauvaise dépendance dans Makefile.docGravatar notin2008-06-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11180 85f007b7-540e-0410-9357-904b9bb8a0f7
* Report de la révision #11175 de la branche v8.2 vers le trunkGravatar notin2008-06-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11176 85f007b7-540e-0410-9357-904b9bb8a0f7
* Installation de la documentationGravatar notin2008-06-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11174 85f007b7-540e-0410-9357-904b9bb8a0f7
* Numéros de version dans la docGravatar notin2008-06-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11123 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement des 'cp' et 'mkdir' par 'install'Gravatar notin2008-06-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11112 85f007b7-540e-0410-9357-904b9bb8a0f7
* 2-3 petites modifs sur la docGravatar notin2008-06-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11091 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ créditsGravatar herbelin2008-05-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10948 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Changement du code de Zplus pour accomoder ring qui sinon prend uneGravatar herbelin2008-05-11
| | | | | | | | | | | | | | | complexité exponentielle dans la machine lazy depuis que l'algo de compilation du filtrage évite systématiquement d'expanser quand le filtrage n'est pas dépendant. - Un peu plus de colorisation dans coqide. - Utilisation de formats pour améliorer de l'affichage des notations Utf8. - Systématisation paire Local/Global dans g_vernac.ml4 (même si le défaut n'est pas toujours le même) - Bug Makefile git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10918 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-04 09:23:24 +0000