aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.build
Commit message (Collapse)AuthorAge
* Makefile.build: (slightly) more robust sed invocation for parsing ↵Gravatar letouzey2010-03-18
| | | | | | | | | | camlp4deps/use lines The build error Y. Makarov recently reported on coq-club was caused by some .ml4 having dos-style end-of-line in his source-tree, and hence \r appearing in the camlp4o commandline. We now simply discard what appears after camlp4xxx "...". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12871 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile: some more cleanupGravatar letouzey2010-03-05
| | | | | | | | | | | | | - avoid recomputing CAMLP4DEPS in the %.ml:%.ml4 rule - a macro for compiling the tools by the best ocaml compiler - use of $(if ...) rather that $ifdef - some variables of Makefile.common were not that useful (e.g. $(COQCCMX), which is $(COQCCCMO:.cmo=.cmx), used only once) - the build of coqc.* should not depend upon coqtop, only its launch (or I'm missing something) - useless $(CAMLP4EXTENDFLAGS) variable git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12846 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile: a nicer hack concerning ocamlopt with no .mli: -intf-suffix .cmi ↵Gravatar letouzey2010-03-04
| | | | | | (thanks A. Frisch) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12841 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile: cleanup of comments + a few words about recent changes in ↵Gravatar letouzey2010-03-04
| | | | | | dev/doc/build*.txt git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12840 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile: no more separate stagesGravatar letouzey2010-03-04
| | | | | | | | | | | | | | - Instead of the separate stage mechanism, we let make handle the build and inclusion of all .d. Some initial calls to camlp4o will fail, but make tries again later, and this finally works great. These initial error message are made nice to avoid bad interaction with M-x next-error - The only recursive call to a sub-make is Makefile calling Makefile.build in which the includes of .d take place. This allows to avoid compiling anything for a make clean or make tags git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12839 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile: try to avoid rare make failures related with make -j + ocamlopt + .cmiGravatar letouzey2010-03-04
| | | | | | | | | | | | | | | | | | As said now in a comment of Makefile.build: NB: for the moment ocamlopt erases and recreates .cmi if there's no .mli around. This can lead to nasty things with make -j (e.g. another process accessing a partial .cmi). To avoid that: 1) We make .cmx always depend on .cmi 2) This .cmi will be created from the .mli, or trigger the compilation of the .cmo if there's no .mli (see rule below about MLWITHOUTMLI) 3) We tell ocamlopt to output to temporary names, remove the temp .cmi (since the actual .cmi should already be there and up-to-date) and move the temp .cmx and .o back in place Ok, this is quite a hack. I'll make a proper bug report to ocaml asap... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12837 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile: cleanup of variables containing lists of files, such as MLFILESGravatar letouzey2010-03-04
| | | | | | | | | | | | | | - We clarify their definition via some custom make function: find, diff... - We avoid duplications via some $(sort ...) - Some name changes: * old $(MLFILES) now corresponds to $(MLSTATICFILES) (but .ml from .mly and .mll aren't in it anymore). * new $(MLFILES) contains all .ml, either static or generated from .mly .mll .ml4 or _mod.ml made out of .mllib * $(ML4FILESML) is now $(GENML4FILES) ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12836 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile: factorization of default rules for .cmi/.cmo/.cmxGravatar letouzey2010-03-04
| | | | | | | | We use some conditional variables $(if ...) to set the proper flags instead of fully duplicating the rules according to the path checker/%.cm? ide/%.cm? %.cm? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12834 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile: the .ml of .ml4 are now produced explicitely (in binary ast form)Gravatar letouzey2010-03-04
| | | | | | | | | | | | | | | | - This way, the Makefile.build gets shorter and simplier, with a few nasty hacks removed. - In particular, we stop creating dummy .ml of .ml4 early "to please ocamldep". Instead, we now use ocamldep -modules, and process its output via coqdep_boot. This ways, *.cm* of .ml4 are correctly located, even when some .ml files aren't generated yet. - There is no risk of editing the .ml of a .ml4 by mistake, since it is by default in a binary format (cf pr_o.cmo and variable READABLE_ML4). M-x next-error still open the right .ml4 at the right location. - mltop.byteml is now mltop.ml, while mltop.optml keeps its name - .ml of .ml4 are added to .gitignore git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12833 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile: hide the trick ...||(RV=$$?;rm $@; exit $${RV}) under a macro ↵Gravatar letouzey2010-03-04
| | | | | | $(TOTARGET) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12832 85f007b7-540e-0410-9357-904b9bb8a0f7
* In the git-specific part of Makefile.build, call to hostname gave optionGravatar thutchin2010-02-25
| | | | | | | | | --fqdn. Changed this to -f (which has the same behavior) so it will work on Mac OS 10.6 Note: Previous versions of Mac OS 10 don't have this option. Most BSD's don't either. Their default behavior is to output the FQDN where Linux defaults to outputting the short name. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12810 85f007b7-540e-0410-9357-904b9bb8a0f7
* Polishing the setup of CoqIDE Input MethodGravatar vgross2010-02-18
| | | | | | | | autodetection via ./configure, automated installation target "install-im", and no more patching. Plus documentation of the procedure in the reference manual. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12790 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile.build: avoid warning about undefined variable during make installGravatar letouzey2010-02-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12778 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile: also install the .cmi of pluginsGravatar letouzey2010-02-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12776 85f007b7-540e-0410-9357-904b9bb8a0f7
* make init + NMake.v/NMake_gen.vGravatar notin2010-01-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12690 85f007b7-540e-0410-9357-904b9bb8a0f7
* NMake: several things need not be macro-generatedGravatar letouzey2010-01-25
| | | | | | | The macro-generated .v file is now NMake_gen.v, while NMake.v now contain the static things (i.e. definition of gcd via mod). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12687 85f007b7-540e-0410-9357-904b9bb8a0f7
* Disable validateGravatar glondu2010-01-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12666 85f007b7-540e-0410-9357-904b9bb8a0f7
* use TIMECMD instead of TIME in makefile (unix cmd time reads its format in TIME)Gravatar letouzey2010-01-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12628 85f007b7-540e-0410-9357-904b9bb8a0f7
* Factorisation between Makefile and ocamlbuild systems : .vo to compile are ↵Gravatar letouzey2009-12-09
| | | | | | | | | | | | in */*/vo.itarget On the way: no more -fsets (yes|no) and -reals (yes|no) option of configure if you want a partial build, make a specific rule such as theories-light Beware: these vo.itarget should not contain comments. Even if this is legal for ocamlbuild, the $(shell cat ...) we do in Makefile can't accept that. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12574 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove interface pluginGravatar glondu2009-12-02
| | | | | | It has moved to the contribs (Sophia-Antipolis/Interface). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12555 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed installation of Coqide interface/library files (bug #2147).Gravatar gmelquio2009-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12376 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added profile.cmo in grammar.cma so that any functions in one of theGravatar herbelin2009-08-14
| | | | | | files embedded in grammar.cma can be profiled with the Profile module. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12279 85f007b7-540e-0410-9357-904b9bb8a0f7
* csdpcert + unixGravatar fbesson2009-08-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12256 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile made compatible with Solaris 10 (bug #2078, continued - seeGravatar herbelin2009-06-06
| | | | | | revisions 12063 and 12065). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12169 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backport of Eric Le Lay's patch (bug report #2078) from v8.2 branchGravatar herbelin2009-04-08
| | | | | | | | | | (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
* Complementary fix to have ocamlopt_shared_os5fix.sh working correctlyGravatar herbelin2009-03-31
| | | | | | | (tested on MacOS 10.5). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12042 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix the fix script for ocamlopt -shared in MacOS 10.5 (remarks by Hugo)Gravatar letouzey2009-03-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12041 85f007b7-540e-0410-9357-904b9bb8a0f7
* ocamlbuild: many improvements (macos 10.5 fix, correct dllpath, etc)Gravatar letouzey2009-03-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12033 85f007b7-540e-0410-9357-904b9bb8a0f7
* bin/coq-{parser,interface}: use this coqtop, not the first in $PATHGravatar lmamane2009-03-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12015 85f007b7-540e-0410-9357-904b9bb8a0f7
* make coqdep_boot in stage1, not stage2Gravatar lmamane2009-03-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12014 85f007b7-540e-0410-9357-904b9bb8a0f7
* Many changes in the Makefile infrastructure + a beginning of ocamlbuildGravatar letouzey2009-03-20
| | | | | | | | | | | | | | | | | | | | | | | | * 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
* Makefile: avoid $(ML4FILES:.ml4=.ml) since this is $(ML4FILESML)Gravatar letouzey2009-03-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12001 85f007b7-540e-0410-9357-904b9bb8a0f7
* Compatibility with Apple's non-gnu sed.Gravatar msozeau2009-03-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11997 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
* renamed %-mod.ml into %_mod.ml to avoid ocaml warningGravatar barras2009-03-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11994 85f007b7-540e-0410-9357-904b9bb8a0f7
* - configure: affiche si le natdynlink est positionneGravatar barras2009-03-17
| | | | | | | | | | | - 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
* coqdep_boot: a specialized and dependency-free coqdep for killing one of the ↵Gravatar letouzey2009-03-16
| | | | | | build stages git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11984 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
* Makefile: minor improvementsGravatar letouzey2009-03-16
| | | | | | | | * 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
* Better mechanism for loading initial pluginsGravatar letouzey2009-03-14
| | | | | | | | | | | | | | | | 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
* Makefile: ml dependencies of contribs are moved to .mllib filesGravatar letouzey2009-03-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11977 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleanup: avoid the warning about Coq-tex not being a valid Ocaml module nameGravatar letouzey2009-03-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11974 85f007b7-540e-0410-9357-904b9bb8a0f7
* in natdynlink, lack of uniformity between general %.vo and Init/%.vo rules ↵Gravatar barras2009-03-09
| | | | | | resulted in cyclic dependencies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11970 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixed groebner as a plugin + pattern matching TimeoutGravatar barras2009-03-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11967 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout de la tactique groebner de Loic PottierGravatar barras2009-03-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11964 85f007b7-540e-0410-9357-904b9bb8a0f7
* porting r11900 11905 and 11953 to trunkGravatar barras2009-03-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11954 85f007b7-540e-0410-9357-904b9bb8a0f7
* coq-interface and coq-parser can be calls to coqtop with adequate code dynlinkGravatar letouzey2009-02-20
| | | | | | | | | | | | | | | | 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
* report de r11926: install de coqchkGravatar barras2009-02-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11928 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backport of 11890 from branch v8.2 (compile tools with the bestGravatar herbelin2009-02-11
| | | | | | | available compiler) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11922 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix de divers petits problèmes d'installationGravatar notin2009-02-11
| | | | | | (cherry picked from commit 998a9a62874ba6cf26bdfe28f3ef0c72deaf0c25) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11918 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 06:36:50 +0000