aboutsummaryrefslogtreecommitdiff
path: root/Makefile.build
AgeCommit message (Collapse)Author
2010-07-24Fix installation of emacs filesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13325 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-09Finish adding out-of-the-box support for camlp4letouzey
If you want to try, it should be now as simple as: make clean && ./configure -local -usecamlp4 && make For the moment, the default stays camlp5, hence ./configure -usecamlp5 and ./configure are equivalent. Thanks to a suggestion by N. Pouillard, the remaining incompatibilities are now handled via some token filtering in camlp4. See compat5*.mlp. Morally, these files should be named .ml4, but I prefer having them not in $(...ML4) variables, it might confuse the Makefile... The empty compat5*.ml are used to build empty .cmo for making camlp5 happy. For camlp4, - tools/compat5.cmo changes GEXTEND into EXTEND. Safe, always loaded - tools/compat5b.cmo changes EXTEND into EXTEND Gram. Interact badly with syntax such that VERNAC EXTEND, we only load it for a few files via camlp4deps TODO: check that my quick adaptation of camlp5-specific code in tactics/extratactics.ml4 is ok. It seems the code by Chung-Kil Hur is hiding information in the locations ?! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13274 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-26Backporting modifications to nsatz (doc + fix of bug #2328) from trunk to v8.3.herbelin
Fixing tests 2145.v about Nsatz. Adding nsatz target in Makefile. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13203 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-22Fixing dependencies for coqidevgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13178 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-02Do not link system library into installed .cmaglondu
Linking a system library into a .cma can lead to some system module (such as Unix) being linked twice in an executable, resulting in possibly hard-to-debug errors. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13054 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-05-19static (and shared) camlp4use instead of per-file declarationletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13016 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-03ocamldoc related fixespboutill
- coq logo isn't destructed anymore - Erase debug printers not implemented for new proofs - ocamldoc compatible comments for pretyping/rawterm.mli git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12988 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-05-03Re-enable validation in "make check", run it in parallel with test-suiteglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12986 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-29"make source-doc" builds documentation of mli in html and pdf atpboutill
dev/ocamldoc/ old "make source-doc" that documents ml files and didn't work is now "make ml-doc" but still don't work :-) "make clean" cleans dev/ocamldoc/ properly wierd? calls of dependency graph generation leave unchanged git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12978 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-04-10Run parallelized test-suite in "check" target of main Makefileglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12926 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-18Makefile.build: (slightly) more robust sed invocation for parsing ↵letouzey
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
2010-03-05Makefile: some more cleanupletouzey
- 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
2010-03-04Makefile: a nicer hack concerning ocamlopt with no .mli: -intf-suffix .cmi ↵letouzey
(thanks A. Frisch) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12841 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-04Makefile: cleanup of comments + a few words about recent changes in ↵letouzey
dev/doc/build*.txt git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12840 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-03-04Makefile: no more separate stagesletouzey
- 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
2010-03-04Makefile: try to avoid rare make failures related with make -j + ocamlopt + .cmiletouzey
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
2010-03-04Makefile: cleanup of variables containing lists of files, such as MLFILESletouzey
- 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
2010-03-04Makefile: factorization of default rules for .cmi/.cmo/.cmxletouzey
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
2010-03-04Makefile: the .ml of .ml4 are now produced explicitely (in binary ast form)letouzey
- 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
2010-03-04Makefile: hide the trick ...||(RV=$$?;rm $@; exit $${RV}) under a macro ↵letouzey
$(TOTARGET) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12832 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-25In the git-specific part of Makefile.build, call to hostname gave optionthutchin
--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
2010-02-18Polishing the setup of CoqIDE Input Methodvgross
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
2010-02-16Makefile.build: avoid warning about undefined variable during make installletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12778 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-16Makefile: also install the .cmi of pluginsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12776 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-26make init + NMake.v/NMake_gen.vnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12690 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-25NMake: several things need not be macro-generatedletouzey
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
2010-01-14Disable validateglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12666 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-01-05use TIMECMD instead of TIME in makefile (unix cmd time reads its format in TIME)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12628 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-12-09Factorisation between Makefile and ocamlbuild systems : .vo to compile are ↵letouzey
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
2009-12-02Remove interface pluginglondu
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
2009-10-06Fixed installation of Coqide interface/library files (bug #2147).gmelquio
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12376 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-14Added profile.cmo in grammar.cma so that any functions in one of theherbelin
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
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 10:42:28 +0000