aboutsummaryrefslogtreecommitdiff
path: root/tools/coq_makefile.ml4
AgeCommit message (Collapse)Author
2011-09-01Creation of ide/project_file.ml4pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14433 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-01Coq_makefile: Bug fix of check_deppboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14431 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-01Coq_makefile: process_cmd_line is purely functional.pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14430 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-01Coq_makefile: No other function than split_arguments uses a target type.pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14429 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-01Coq_makefile: New option -arg to specify a compiler option.pboutill
Consequently, option -impredicative-set is deprecated. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14428 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-01Coq_makefile drops the '/' at the end of physical path of -I and -Rpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14427 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-22Allow custom targets without commands specifiedpboutill
$ coq_makefile -custom "" "install2" "install" for instance does: install: install2 If you tried to do this before, coq_makefile used to insert a TAB after the rule. Signed-off-by: Paolo Herms <paolo.herms@cea.fr> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14290 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-11Makefiles generated by coq_makefile can build %.cmx?a from %.mllibpboutill
A problem remains with the "install" rule because every cmo/cmx is installed even if installing only the generated cma/cmxa could be sufficient. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14275 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-07coq_makefile logical path ending with '.' are correctly convert to physical pathpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14272 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-07coq_makefile bug fix 2405: cmxs are now made from cmx filespboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14271 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-07coq_makefile documentation in Refman and -hpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14270 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-07coq_makefile doesn't complain anymore when a dir is both -I and -Rpboutill
It used to deal correctly with that so why a warning ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14269 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-06Typo.gmelquio
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14162 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-29when -camlbin is explicitly given in configure, $OCAML* are $CAMLBIN/exec.pboutill
Coq_makefile wrote $CAMLBIN twice... This should fix ssreflect in bench. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14088 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-28coq_makefile big cleanuppboutill
For everybody: variable customization should be easier. (Bug 2533 & more) For plugins: mli files are accepted, doc of them is done, ml4 files really work, ml files aren't camlp* preprocced, ready to build with camlp4 is your code is ready too, should work on any architecture nevermind the one on which you've done the coq_makefile. For others: html doc installation in $DOCDIR/users-contrib/"you"/ git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14081 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-04-08A kind of reply to bug 2444pboutill
coq_makefile uses ocaml{c,opt}.opt if it uses coqc -opt and ocaml‘c,opt} if it uses coqc -byte. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13980 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-24Updated all headers for 8.3 and trunkherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-02Remove dependency to Unix from module Profileglondu
Looking at the source code of Sys.time reveals that it is exactly what is computed by Profile.get_time. This can also be tested by evaluating: Sys.time () -. Unix.(let x = times () in x.tms_utime +. x.tms_stime);; in an OCaml toplevel with Unix. This allows to put Profile in grammar.cma without the dependency to unix.cma while preprocessing. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13233 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-03Add unix.cma on camlp4 command-line in coq_makefile (Closes: #2326)glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13060 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-19Add (almost) compatibility with camlp4, without breaking support for camlp5letouzey
The choice between camlp4/5 is done during configure with flags -usecamlp5 (default for the moment) vs. -usecamlp4. Currently, to have a full camlp4 compatibility, you need to change all "EXTEND" and "GEXTEND Gram" into "EXTEND Gram", and change "EOI" into "`EOI" in grammar entries. I've a sed script that does that (actually the converse), but I prefer to re-think it and check a few things before branching this sed into the build mechanism. lib/compat.ml4 is heavily used to hide incompatibilities between camlp4/5 and try to propose a common interface (cf LexerSig / GrammarSig). A few incompatible quotations have been turned into underlying code manually, in order to make the IFDEF CAMLP5 THEN ... ELSE ... END parsable by both camlp4 and 5. See in particular the fate of <:str_item< declare ... end >> Stdpp isn't used anymore, but rather Ploc (hidden behind local module Loc). This forces to use camlp5 > 5.01. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13019 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
- Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-15Report de la révision #12676notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12677 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-05Correction du bug #2153 (-D n'est pas une option standard de install)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12469 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-10-27Add a new vernacular command for controling implicit generalization ofmsozeau
variables with syntax: [Local?|Global] Generalizable Variable(s)? [all|none|id1 idn]. By default no variable is generalizable, so this patch breaks backward compatibility with files that used implicit generalization (through Instance declarations for example). To get back the old behavior, one just needs to use [Global Generalizable Variables all]. Make coq_makefile more robust using [mkdir -p]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12428 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-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-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-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-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-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-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-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-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-12- configure: do not strip coqtop on Darwin so as to support dynamic loadingherbelin
- configure: remove useless newline (hoping it is OK for everyone) - coqc: added option -no-glob in accordance with coqc -usage - coq_makefile: support for installation of all .cmo and all .cmxs in user-contrib git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11676 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-11-13Tentative d'amélioration de la robustesse des Makefile générés parnotin
coq_makefile en présence de fichiers .ml : - ajout d'une option -config à coqtop qui affiche les informations de configuration (COQTOP, COQBIN, COQLIB, CAMLP4, CAMLP4LIB, CAMLBIN, LOCAL) - coq_makefile inclut un fichier Makefile.config qui contient les valeurs des variables sus-mentionnées git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11584 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-07Suite #11533notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11554 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-07Correction du bug #1926notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11553 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-06Correction d'un petit bug en cas de redéfintion par l'utilisateur de ↵notin
variables utilisées dans PP git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11546 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-11-042 petites améliorations de coq_makefile (traitement des .ml4 + cibles ↵notin
génériques dans -custom git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11535 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-10-20Syntaxe de COQBINnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11475 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-10-18- Merge modifs coq_makefile.ml4 de la 8.1 vers le trunk (commit 11429)herbelin
- Makefile: typo apparente avec .ml4.preprocessed - test-suite: ajout d'un test sur eta qui trainait dans le coin git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11465 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-18Affichage intempestif d'information de globalisation + numéro de version ↵notin
dans coq_makefile git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11234 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-17- coqdoc: correction d'un bug sur les commentaires imbriquésnotin
- coq_makefile: amélioration des chemins de camlp4/5 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11231 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 19:16:17 +0000