aboutsummaryrefslogtreecommitdiff
path: root/Makefile.build
AgeCommit message (Collapse)Author
2009-08-01csdpcert + unixfbesson
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12256 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-06Makefile made compatible with Solaris 10 (bug #2078, continued - seeherbelin
revisions 12063 and 12065). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12169 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-08Backport of Eric Le Lay's patch (bug report #2078) from v8.2 branchherbelin
(r12063) for smooth compilation/installation under Solaris (/bin/sh -> /bin/bash, -or -> -o in find, echo -n -> printf, ! in test rather than in if). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12065 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-31Complementary fix to have ocamlopt_shared_os5fix.sh working correctlyherbelin
(tested on MacOS 10.5). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12042 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-30Fix the fix script for ocamlopt -shared in MacOS 10.5 (remarks by Hugo)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12041 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-29ocamlbuild: many improvements (macos 10.5 fix, correct dllpath, etc)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12033 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-26bin/coq-{parser,interface}: use this coqtop, not the first in $PATHlmamane
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12015 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-25make coqdep_boot in stage1, not stage2lmamane
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12014 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-20Makefile: avoid $(ML4FILES:.ml4=.ml) since this is $(ML4FILESML)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12001 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-20Compatibility with Apple's non-gnu sed.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11997 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-18renamed %-mod.ml into %_mod.ml to avoid ocaml warningbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11994 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-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-16Makefile: fix ignored errors, several attempts to clarify thingsletouzey
* 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
2009-03-16Makefile: minor improvementsletouzey
* no need anymore for special rules for -rectypes: we use it everywhere * $(REVISIONCMO) is obsolete * avoid triple references to almost all files of kernel/ git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11982 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-14Better mechanism for loading initial pluginsletouzey
Instead of dirty hacks in toplevel/coqtop.ml, we simply add some Declare ML Module in Prelude.v. Gain: now that coqdep is clever enough, dependencies are automatic, and we can simplify the Makefile quite a lot: no more references to INITPLUGINSBEST and the like. Besides, mltop.ml4 can also be simplified a lot: by giving $(CONTRIBSTATIC) to coqmktop instead of contrib.cma, now coqtop is aware that it already contain the static plugins (or not), and subsequent ML Module are ignored correctly without us having to do anything :-) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11979 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-14Makefile: ml dependencies of contribs are moved to .mllib filesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11977 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-03-09in natdynlink, lack of uniformity between general %.vo and Init/%.vo rules ↵barras
resulted in cyclic dependencies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11970 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-06fixed groebner as a plugin + pattern matching Timeoutbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11967 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-05ajout de la tactique groebner de Loic Pottierbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11964 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-02porting r11900 11905 and 11953 to trunkbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11954 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-02-20coq-interface and coq-parser can be calls to coqtop with adequate code dynlinkletouzey
From files in contrib/interface, we create (if natdynlink is available) two plugins named coqinterface_plugin.{cma,cmxs} and coqparser_plugin.{cma,cmxs}. These plugins are loaded respectively by CoqInterface.v and CoqParser.v. So coq-interface can be "coqtop -require CoqInterface", and coq-parser can be "coqtop -batch -l CoqParser" (this one cannot be compiled into a .vo, otherwise a customized toplevel is launched during the compilation). Turing coq-interface and coq-parser and their .opt versions into shell scripts allow to spare around 40 Mb of disk space... Nota: at dynlink, parse.ml was conflicting with the module Parse of the ocaml runtime, so I renamed it into coqparser.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11940 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-02-16report de r11926: install de coqchkbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11928 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-02-11Backport of 11890 from branch v8.2 (compile tools with the bestherbelin
available compiler) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11922 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-02-11Fix de divers petits problèmes d'installationnotin
(cherry picked from commit 998a9a62874ba6cf26bdfe28f3ef0c72deaf0c25) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11918 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-11Add -coqtoolsbyteflags and -custom to ./configure...glondu
...and use -custom by default on Windows and MacOS (backport r11895) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11913 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-02-11config/revision.ml, git: handle case when not at tip of a branchlmamane
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11910 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-02-11Convert all uses of FIND_VCS_CLAUSE to recommended stylelmamane
(which allows to get rid of '-type f' hack) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11908 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-02-03Fix the installation of plugins (both initial and late ones)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11876 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-22Remplacement de cp --parents par un script shnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11833 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-20- Fixing bug 1891 (abusive instantiations of evar arguments inherbelin
evar-evar problems). - Fixing target "make programs". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11817 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-20Cette version là fonctionne correctement au moins pour certaines aspiwack
architectures. Désolé pour les cafouillages. Si quelqu'un a des ennuis en installant un trunk prévenez moi, c'est sûrement ma faute. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11813 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-20More fixes... aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11812 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-20Un fix sur le commit précédent. aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11811 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-20Patch de l'installation:aspiwack
Quand les plugins sont activés, ils devraient être installés par make install. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11810 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-13Workaround to compile the coq archive with dynamic loading on Mac OS 10.5herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11777 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-11- Deactivation of dynamic loading on Mac OS 10.5 (see bug #2024).herbelin
- Added dependency of mltop.ml4 into config/Makefile (see bug #2023). - Fixed bug #1963 (dependent inversion building a universe-ill-formed conversion problem). - Incidentally, moved "Large non-propositional inductive ..." error message to standard himsg.ml error displayer. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11774 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-10- Fixed the recompilation of config/revision.ml once every two conmpilations.herbelin
- Fixed an error message in configure - Support for filenames with spaces in coqmktop git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11772 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-07Fix build for git usersglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11760 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-06Conversion du fichier 'revision' en un fichier .ml + correction d'un bug ↵notin
dans le configure introduit par les révisions 11754 et 11755 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11756 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-06Installation des librairies: on utilise maintenant LINKCMO au lieu denotin
l'appel à find. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11753 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-04Moved JProver to a user contribution (as was decided a long time ago)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11746 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-22Typo in Makefile leading to empty quote_plugin.cmaletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11712 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 03:17:37 +0000