aboutsummaryrefslogtreecommitdiff
path: root/tools/coqdep.ml
AgeCommit message (Collapse)Author
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-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-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-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
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
2008-11-23- Synchronized subst_object with load_object (load_and_subst_objects)herbelin
and set Declare ML Module as a regular substitutive object so that Declare ML Module is treated at the right place in the order of appearance of substitutive declarations of a required module. - Note: The full load/import mechanism for modules is not so clear: the Require part of a Require Import inside a module is set outside the module at module closing but the Import part remains inside (why not to put the "special" objects in the module too?); moreover the "substitute" and "keep" objects of a module are desynchronised at module closing (is that really harmless/necessary?). - Treatment of .cmxs targets in coq_makefile and in coqdep. - Better make clean in coq_makefile generated makefiles. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11623 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-24Suppression de l'option -dump-glob et ajout d'une option -no-globnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11167 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-21Code cleanup in typeclasses, remove dead and duplicated code.msozeau
Change from named_context to rel_context for class params and fields. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11163 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-03- Correction d'un bug de coq_makefile sur les variables CAMLLIBS etnotin
COQLIBS. - Ajout d'un message d'erreur si Camlp5 est compilé en mode strict git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10746 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-26Bug dans la gestion des dépendances vers les .mlnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10722 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-26Correction du bug #1814 (trunk et v8.1) + améliorations dans coqdep et ↵notin
coq_makefile git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10721 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-25Correction d'un bug dans la gestion des 'Declare ML Module'notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10717 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-19Various improvements of coqdep, resulting in a big speedupletouzey
* use of Hashtbl for large sets/maps * reorganisation of directory-traversal functions, in order to avoid redundant stat / open * all files and directory whose names start by . are skipped while tranversing directories: no more visits of .svn ! * new option -boot to be used when computing dependencies of the stdlib: - no need in this case to records the system .vo in coqlibKnown - add directly inside coqdep the equivalent of -R theories Coq and -R contrib Coq As a result, coqdep'ing all the .vo of the stdlib now takes 25s on my machine instead of 2min30 earlier. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10695 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-14New option -glob for coqdep, in order to avoid nasty tricks with sed in Makefileletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10668 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-08Calcul des dependances sous Windowsnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10196 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-24Améliorations utiles pour les Makefile répartis sur plusieurs répertoiresherbelin
coqdep : - fonction de "canonisation" du nom des cibles plus performante (elle traverse notamment les "..") coq_makefile : - ajout automatique de "-I ." dans COQLIBS seulement si pas déjà déclaré (utile pour éviter les cibles en double dans coqdep en présence de -R) - explicitation de "-byte" dans la cible "byte:" (son absence semble remonter à l'époque où l'exécution en byte était le défaut) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9676 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-25coqdep -slashbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9276 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-08Warning ocaml 3.09 pour variable inutileherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8923 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-26Prise en compte du Require multipleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8737 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-17Modification des propriétés (svn:executable)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8642 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-21coqdep connait maintenant user-contribfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7158 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Nouvelle en-têteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-17suppression du ./ devant (et .\ sous Windows)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5522 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-15identification ./f et f dans coqdep -sortfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5483 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-18- fixed the Assert_failure error in kernel/modopsbarras
- fixed the problem with passing atomic tactics to ltacs - restructured the distrib Makefile (can build a package from the CVS working dir) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5358 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Message pour les erreursherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4382 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-14prise en compte des sous-repertoires Coq de maniere dynamiquefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3682 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-04mdule --> modulemohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3374 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-15commit du calcul des dependances un peu plus robustebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3147 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-10gestion coherente de l'option -R et des Require A.B.C.barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3112 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-08-31prise en compte de Load par coqdepfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1918 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-16compat -sort et -suffixfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1854 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-07-16utilisation de printf (simplif)filliatr
option -sort pour trier les .v selon les dépendances git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1852 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-20support option -R pour coqdepfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1640 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-15entetesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-08nouveau load pathfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@828 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-12-11outils (manquent encore les deux filtres)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@235 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-18 22:03:19 +0000