aboutsummaryrefslogtreecommitdiff
path: root/tools
AgeCommit message (Collapse)Author
2009-10-27Added option --external to coqdoc to bind an url to an external library.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12426 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-13Better handling of emphasis.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12385 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-29Add support for Local Declare ML Moduleglondu
Instead of failing with some obscure error message *after* loading the module, accept Local Declare ML Module with the usual semantics. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12366 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-15- Tentatively made order-dependency wrt .vo files a full dependencyherbelin
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
2009-09-10Fixes for toc depth handling and handling of substitles from Chris Casinghino.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12318 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-08Update coqdoc documentation, CHANGES and add a fix for the proofbox (patchmsozeau
by Chris Casinghino). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12311 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-08Fix the bug-ridden code used to choose leibniz or generalizedmsozeau
rewriting (thanks to Georges Gonthier for pointing it out). We try to find a declared rewrite relation when the equation does not look like an equality and otherwise try to reduce it to find a leibniz equality but don't backtrack on generalized rewriting if this fails. This new behavior make two fsets scripts fail as they are trying to use an underlying leibniz equality for a declared rewrite relation, a [red] fixes it. Do some renaming from "setoid" to "rewrite". Fix [is_applied_rewrite_relation]'s bad handling of evars and the environment. Fix some [dual] hints in RelationClasses.v and assert that any declared [Equivalence] can be considered a [RewriteRelation]. Fix minor tex output problem in coqdoc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12310 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-04Incorporate coqdoc changes by the UPenn team (B.Pierce, C. Casinghino,msozeau
M. Greenberg) and add support for interpolation to HTML output. The patch is mostly backwards-compatible, except for the CSS style which needs more readaptation. Doc for the new options will come as well. - lists have been updated substantially. In particular, multiparagraph list items are now supported and sublists work better, using an "off-side" rule. - the "--index" flag allows one to change the name of the generated index file (good since index.html has a special meaning). - the "--toc-depth <int>" flag allows one to limit how many levels are included in the toc. - the "--lib-name <string>" flag allows one to specify what libraries are called, instead of just sticking "Library" before each module name (for example, "Module" or "Chapter" might be more sensible in some contexts). Additionally "--no-lib-name" eliminates this extra title completely. - the "--lib-subtitles" flag allows one to specify subtitles for libraries. When enabled, the beginning of each file is checked for a comment of the form: (** * ModuleName : text *) and the text will be printed as a subtitle in the appropriate places. - Text can be made italic by putting it inside underscores, as in: _emphasized text_. This has the advantage of looking OK in the .v file as well. A few simple rules are followed to make sure identifiers with underscores aren't accidentally made italic. - Various changes have been made in an attempt to beautify the output, especially in html, while allowing the .v sources to look decent as well. Mostly these involve whitespace. - The coqdoc.css file has been changed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12308 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-03Add --plain-comments patch by F. Garillot, which also addsmsozeau
interpretation of [[ etc... inside (* *) comments when --parse-comments is used. Add some additional fixes from B. Pierce on formatting verbatim and the HTML Toc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12307 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-06- Cleaning phase of the interfaces of libnames.ml and nametab.mlherbelin
(uniformisation of function names, classification). One of the most visible change is the renaming of section_path into full_path (the use of name section was obsolete due to the module system, but I don't know if the new name is the best chosen one - especially it remains some "sp" here and there). - Simplification of the interface of classify_object (first argument dropped). - Simplification of the code for vernac keyword "End". - Other small cleaning or dead code removal. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12265 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-09Allow coqdoc comments inside definition bodies.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12237 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-28Adapted the emacs mode to font-lock. Re-using code from ProofGeneral.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12152 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-24Report de la révision #12104 (Maj lien site web de Coq)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12105 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-08Take formatted into account in rules for dot.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12072 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-08Change HTML paragraph output to avoid too much space after bulletedmsozeau
lists, patch by B. Pierce. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12067 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-06Fix behavior on newlines with parse-comments and also do [] escaping as msozeau
usual in this mode (report and request by B. Pierce). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12054 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-27Coqdep: some dead code and code move (first experiment with Oug)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12025 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-26Coqdep_boot: one line with bad indentationletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12018 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-26Protect typeset arguments in titles in LaTeX output (fixes compilationmsozeau
errors in Library.coqdoc). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12017 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-24Fix coqdoc bugs reported by Ian Lynagh.msozeau
- Add coqdoccomment LaTeX environment to sty file - Fix buggy parsing in comments git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12013 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-24pretty.mll of coqdoc becomes cpretty.mll (avoid clash with a camlp5 file)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12011 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-22More elaborate handling of newlines in Gallina mode. Support inlinemsozeau
Qed's. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12005 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-22coqdoc fixes and support for parsing regular comments (request bymsozeau
B. Pierce on coq-club). - Output regular comments, enclosed in a span in HTML (with (* *) delimiters) and inside a new environment in LaTeX. - HTML output: put the span inside anchors in links, so as to keep the same style as for definitions (customizable in the CSS). - Better handling of Next Obligation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12004 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-20Many changes in the Makefile infrastructure + a beginning of ocamlbuildletouzey
* generalize the use of .mllib to build all cma, not only in plugins/ * the .mllib in plugins/ now mention Bruno's new _mod.ml files * lots of .cmo enumerations in Makefile.common are removed, since they are now in .mllib * the list of .cmo/.cmi can be retreive via a shell script line, see for instance rule install-library * Tolink.core_objs and Tolink.ide now contains ocaml _modules_, not _files_ * a -I option to coqdep_boot allows to control piority of includes (some files with the same names in kernel and checker ...) This is quite a lot of changes, you know who to blame / report to if something breaks. ... and last but not least I've started playing with ocamlbuild. The myocamlbuild.ml is far from complete now, but it already allows to build coqtop.{opt,byte} here. See comments at the top of myocamlbuild.ml, and don't hesitate to contribute, either for completing or simplifying it ! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12002 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ↵letouzey
user contribs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-19coq_makefile: -c and -shared conflict; tacinterp: delay evaluation of tactic ↵barras
genargs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11995 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-18coq_makefile: no ml dependency on coq sourcesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11991 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-17- configure: affiche si le natdynlink est positionnebarras
- coq_makefile: utilise Coq_config pour avoir la liste des contribs - mltop: normalisation des noms de modules ML (majuscule) - Makefiles: introduction de fichiers %-mod.ml qui se chargent de faire les declarations de modules ML d'un plugin git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11987 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-16missing -c option of ocamlc in coq_makefile; coqdep_boot main loop was ↵barras
included in coqdep git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11985 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-16coqdep_boot: a specialized and dependency-free coqdep for killing one of the ↵letouzey
build stages git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11984 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-14Coqdep: better handling of Declare ML Module (via .mllib) + many cleanupsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11976 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-14Coqdep: remove references to obsolete .zi and Require Implementation stuffletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11975 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-11Cleanup: avoid the warning about Coq-tex not being a valid Ocaml module nameletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11974 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-02-24Amélioration de coq_makefilenotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11945 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-02-11Report des revisions #11826, #11828 et #11829 de v8.2 vers trunknotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11915 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-02-06From v8.2 to trunk:herbelin
- commit 11871 (Miller's pattern detection bug) + a corresponding test - commit 11883 (.ml4 to .cmxs in coq_makefile) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11884 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-02-04Fix d'un bug avec l'option gallinanotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11880 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-21- Better deal with commands inside section titles in latex output usingmsozeau
the support from hyperref. - Rename n-ary 'exist' tactic to 'exists' in Program.Syntax. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11821 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-18Various little fixes:msozeau
- allow a new line after a (** printing *) directive in coqdoc so as not to output spurious new lines. - never directly unify the lemma with an evar in setoid_rewrite (they act as opaque constants). - Fix a useless dependency introduced by tauto which splits a record in SetoidList. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11799 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-15Patch by Brian Campbell to output more information on the exception thatmsozeau
made a glob file unreadable. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11788 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-09Oups... il n'y a pas d'option -impl pour ocamldepnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11771 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-08Minor doc fixes:msozeau
- 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
2009-01-07Sous Windows, 'coqtop -where' renvoit des chemins contenant des '\'notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11761 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-07Suite de la révision #11756notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11757 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-04Added installation of .cmi files in "make install" target of coq_makefile.herbelin
Updated CHANGES. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11747 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-29Produce better html code with coqdoc and improve doc:msozeau
- 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
2008-12-24- coq_makefile: target install now respects the original tree structureherbelin
of the archive to install in coq user-contrib installation directory. - Relaxed the validity check on identifiers from an error to a warning. - Added a filtering option to Print LoadPath. - Support for empty root in option -R. - Better handling of redundant paths in ml loadpath. - Makefile's: Added target initplugins and added initplugins to coqbinaries. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11713 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-12-19Nettoyage des variables Coq et amélioration de coqmktop. Lesnotin
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
2008-12-16Take advantage of natdynlink when available: almost all contribs become ↵letouzey
loadable plugins - Any contrib foo leads to contrib/foo/foo_plugin.cmxs (and .cma for bytecode). - Features that were available without any Require are now loaded systematically when launching coqtop (see Coqtop.load_initial_plugins): extraction, jprover, cc, ground, dp, recdef, xml - The other plugins are loaded when a corresponding Require is done: quote, ring, field, setoid_ring, omega, romega, micromega, fourier - I experienced a crash (segfault) while turning subtac into a plugin, so this one stays statically linked into coqtop for now - When the ocaml version doesn't support natdynlink, or if "-natdynlink no" is explicitely given to configure, coqtop is statically linked with all of the above code as usual. Some messages [Ignore ML file Foo_plugin] may appear. - How should coqdep handle a "Declare ML Module "foo"" if foo is an archive and not a ml file ? For now, we suppose that the foo.{cmxs,cma} are at the same location as the .v during the build, but can be moved later in any place of the ml loadpath. This is clearly an experimentation. Feedback most welcome... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11687 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 02:39:33 +0000