aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.build
Commit message (Collapse)AuthorAge
* Makefile.build: follow-up of commits by Matej on VERBOSE and READABLE_ML4Gravatar Pierre Letouzey2016-07-12
| | | | | | | - With the ?= construction, we avoid warnings about undefined variables, while tolerating both 'make VERBOSE=1' and 'VERBOSE=1 make' - Some extra documentation and cleanup
* Removing "READABLE_ML4=" from "Makefile.build"Gravatar Matej Kosik2016-07-12
|
* Removing "VERBOSE=" from "Makefile.build"Gravatar Matej Kosik2016-07-11
|
* Revert "Merge remote-tracking branch 'github/pr/229' into trunk"Gravatar Maxime Dénès2016-07-05
| | | | | | | | | This reverts commit b2f8f9edd5c1bb0a9c8c4f4b049381b979d3e385, reversing changes made to da99355b4d6de31aec5a660f7afe100190a8e683. Hugo asked for more discussion on this topic, and it was not in the roadmap. I merged it prematurely because I thought there was a consensus. Also, I missed that it was changing coq_makefile. Sorry about that.
* Merge remote-tracking branch 'github/pr/229' into trunkGravatar Maxime Dénès2016-07-04
|\ | | | | | | Was PR#229: Bytecode compilation in a new 'make byte' rule apart from 'make world'
* | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵Gravatar Pierre Letouzey2016-07-03
| | | | | | | | | | | | module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
| * Makefile: $(BEST) controls which coqtop is used to build .voGravatar Pierre Letouzey2016-06-29
| | | | | | | | | | | | | | This allows to grant a wish by Hugo: to build coqtop.byte and prelude with it, you could do: make -j BEST=byte states
| * Makefile: no bytecode compilation in make world, see make byte insteadGravatar Pierre Letouzey2016-06-29
|/ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | On a machine for which ocamlopt is available, the make world will now perform bytecode compilation only in grammar/ (up to the syntax extension grammar.cma), and then exclusively use ocamlopt. In particular, make world do not build bin/coqtop.byte. A separate rule 'make byte' does it, as well as bytecode plugins and things like dev/printers.cma. 'make install' deals only with the part built by 'make', while a new rule 'make install-byte' installs the part built by 'make byte'. IMPORTANT: PLEASE AVOID doing things like 'make -j world byte' or any parallel mix of native and byte rules. These are known to crash sometimes, see below. Instead, do rather 'make -j && make -j byte'. Indeed, apart from marginal compilation speed-up for users not interested in byte versions, the main reason for this commit is to discourage any simultaneous use of OCaml native and byte compilers. Indeed, ocamlopt and ocamlc will both happily destroy and recreate .cmi for .ml files with no .mli, and in case of parallel build this may happen at the very moment another ocaml(c|opt) is accessing this .cmi. Until now, this issue has been handled via nasty hacks (see the former MLWITHOUTMLI and HACKMLI vars in Makefile.build). But these hacks weren't obvious to extend to ocamlopt -pack vs. ocamlopt -pack. coqdep_boot takes a "-dyndep" option to control precisely how a Declare ML Module influences the .v.d dependency file. Possible values are: -dyndep opt : regular situation now, depends only on .cmxs -dyndep byte : no ocamlopt, or compilation forced to bytecode, depends on .cm(o|a) -dyndep both : earlier behavior, dependency over both .cm(o|a) and .cmxs -dyndep none : interesting for coqtop with statically linked plugins -dyndep var : place Makefile variables $(DYNLIB) and $(DYNOBJ) in .v.d instead of extensions .cm*, so that the choice is made in the rest of the makefile (see next commit about coq_makedile) NB: two extra mli added to avoid building unecessary .cmo during 'make world', without having to use the ocamldep -native option. NB: we should state somewhere that coqmktop -top won't work unless 'make byte' was done first
* A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
| | | | | | | | | | | | | | | | | | | | | | | | | | On the user side, coqtop and coqc take a list of warning names or categories after -w. No prefix means activate the warning, a "-" prefix means deactivate it, and "+" means turn the warning into an error. Special categories include "all", and "default" which contains the warnings enabled by default. We also provide a vernacular Set Warnings which takes the same flags as argument. Note that coqc now prints warnings. The name and category of a warning are printed with the warning itself. On the developer side, Feedback.msg_warning is still accessible, but the recommended way to print a warning is in two steps: 1) create it by: let warn_my_warning = CWarnings.create ~name:"my-warning" ~category:"my-category" (fun args -> Pp.strbrk ...) 2) print it by: warn_my_warning args
* remove an old workaround for OCaml 3.11 + MacOS natdynlinkGravatar Pierre Letouzey2016-06-24
|
* Makefile.build: mitigate potential issues with multiple creations of pack .cmiGravatar Pierre Letouzey2016-06-24
|
* Makefile.build: "make;make" should redo nothingGravatar Pierre Letouzey2016-06-22
| | | | | | | | | | | | | | | | | | As reported by PMP, this was not yet the case. The culprit was the build of coqdep_boot by a one-liner ocamlopt taking all the necessary .ml files as arguments (in the right order). This was nice and short, and correct wrt dependencies, but had the inconvenient of building some .cmi *after* their corresponding .cmx, while the rest of the Makefile relies on the reverse order (see the section about MLWITHOUTMLI). Hence on the next run, make was thinking that these .cmx weren't up-to-date. For solving this issue, we now build coqdep_boot (and other tools) via a list of .cmx and let our infractructure build them (after their .cmi). The only drawback is the 6 extra lines to hardcode the dependencies of the *.cm(o|i|x) needed for coqdep_boot. (since the .ml.d aren't already taken in account by make at that time).
* Makefile: compat5* moved in grammar/, less -I given to camlp4oGravatar Pierre Letouzey2016-06-21
|
* Makefile.build: ensure a build failure in case of a missing ruleGravatar Pierre Letouzey2016-06-15
| | | | | | | | | Earlier (as in #4812), a target with some declared dependencies (e.g. in a .d) but no building rule would lead to a successful build, even though it is actually incomplete. Side effect: it is now mandatory to declare phony targets in a .PHONY statement.
* Repair the build of ide/coqidetop.cmxs (fix #4812)Gravatar Pierre Letouzey2016-06-14
| | | | | | | | | Restore the .cmxa-->.cmxs rule from the Makefile. Sorry, I was thinking that all plugins would now be built from .mlpack (hence using only the .cmx-->.cmxs rule), and I forgot about this coqidetop business. Now the really intersting question is : why on earth 'make world' was silently failing to build this file but succeeding nonetheless ?!
* Compilation via pack for plugins of the stdlibGravatar Pierre Letouzey2016-06-08
| | | | | | | | | | | | | | | | | | | | | | | | For now, the pack name reuse the previous .cma name of the plugin, (extraction_plugin, etc). The earlier .mllib files in plugins are now named .mlpack. They are also handled by bin/ocamllibdep, just as .mllib. We've slightly modified ocamllibdep to help setting the -for-pack options: in *.mlpack.d files, there are some extra variables such as foo/bar_FORPACK := -for-pack Baz when foo/bar.ml is mentioned in baz.mlpack. When a plugin is calling a function from another plugin, the name need to be qualified (Foo_plugin.Bar.baz instead of Bar.baz). Btw, we discard the generated files plugins/*/*_mod.ml, they are obsolete now, replaced by DECLARE PLUGIN. Nota: there's a potential problem in the micromega directory, some .ml files are linked both in micromega_plugin and in csdpcert. And we now compile these files with a -for-pack, even if they are not packed in the case of csdpcert. In practice, csdpcert seems to work well, but we should verify with OCaml experts.
* Makefile.build split in many smaller files : Makefile.{ide,checker,dev,install}Gravatar Pierre Letouzey2016-06-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | General idea : Makefile.build was far too big to be easy to grasp or maintain, with information scattered everywhere. Let's try to tidy that! Normally, this commit is transparent for the user. We simply regroup some parts of Makefile.build in several new dedicated files: - Makefile.ide - Makefile.checker - Makefile.dev (for printers, revision, extra partial targets, otags) - Makefile.install These new files are "included" at the start of Makefile.build, to provide the same behavior as before, but with a Makefile.build shrinked by 50% (to approx 600 lines). Makefile.build now handles in priority the build of coqtop, minor tools, theories and plugins. Note: this is *not* a separate build system for coqchk nor coqide, even if this can be seen as a first step in this direction (won't be easy anyway to continue, due to the sharing of various stuff in lib and more). In particular Makefile.{coqchk,ide} may rely here and there on some generic rules left in Mafefile.build. Conversely, be sure to prefix rules in Makefile.{coqchk,ide} by checker/... or ide/... in order to avoid interferences with generic rules. Makefile.common is still there, but quite simplified. For instance, some variables that were used only once (e.g. lists of cmo files to link in the various tools) are now defined in Makefile.build, directly where they're needed. THEORIESVO and PLUGINSVO are made directly out of the theories/*/vo.itarget and plugins/*/vo.itarget files, no long manual list of subdirs anymore. Specific sub-targets such as 'reals' still exist, but in Makefile.dev, and they aren't mandatory. Makefile.doc is augmented by the rules building the documentation of the sources via ocamldoc. This classification attempt could probably be improved. For instance, the install rules for coqide are currently in Makefile.ide, but could also go in Makefile.install. Note that I've removed install-library-light which was broken anyway (arith isn't self-contained anymore).
* Makefile: avoid overwriting test.ml when testing grammar.cmaGravatar Pierre Letouzey2016-06-08
|
* Removing the Q_constr file.Gravatar Pierre-Marie Pédrot2016-06-05
|
* Move ide serialization libraries from lib/ to ide/Gravatar Emilio Jesus Gallego Arias2016-06-02
| | | | | | | This makes the core free from particular protocol choices. It should help with the ppx serialization project and shrinks clib.cma a bit.
* Makefile.build: clean a bit the way MacOS binaries are signedGravatar Pierre Letouzey2016-06-02
|
* Makefile.build : follow-up of previous commitGravatar Pierre Letouzey2016-06-01
| | | | | - the particlar rule for dev/printers.cma is adapted as for %.cma:%.mllib - some more removal of | .d in rules
* Makefile.build : improved rules about .cm(x)aGravatar Pierre Letouzey2016-06-01
| | | | | | | | | | | | We add a dependency of .cma over .mllib. This dependency over the .mllib is somewhat artificial, since ocamlc -a won't use this file, hence the $(filter-out ...) below. But this ensures that the .cm(x)a is rebuilt when needed, (especially when removing a module in the .mllib). We also remove all "order-only" dependencies over *.d in rules, since the -include mechanism should already ensure that we have up-to-date dependencies known by make.
* Makefile.build : update the otags ruleGravatar Pierre Letouzey2016-06-01
| | | | | | There were a forgotten CAMLP4DEPS macro. We also avoid otags failure with camlp5 (in this case, it only builds the tags of regular .ml files, not .ml4).
* Yet another Makefile reform : a unique phase without nasty make tricksGravatar Pierre Letouzey2016-06-01
| | | | | | | | | | | | | | | | | | | | We're back to a unique build phase (as before e372b72), but without relying on the awkward include-deps-failed-lets-retry feature of make. Since PMP has made grammar/ self-contained, we could now build grammar.cma in a rather straightforward way, no need for a specific sub-call to $(MAKE) for that. The dependencies between files of grammar/ are stated explicitely, since .d files aren't fully available initially. Some Makefile simplifications, for instance remove the CAMLP4DEPS shell horror. Instead, we generalize the use of two different filename extensions : - a .mlp do not need grammar.cma (they are in grammar/ and tools/compat5*.mlp) - a .ml4 is now always preprocessed with grammar.cma (and q_constr.cmo), except coqide_main.ml4 and its specific rule Note that we do not generate .ml4.d anymore (thanks to the .mlp vs. .ml4 dichotomy)
* Makefile: restore the use of coqdep_boot for creating .v.d filesGravatar Pierre Letouzey2016-06-01
| | | | | | | Coqdep_boot has almost no dependencies, and hence can be compiled very early during the build, without relying on .ml.d files. Some code of system.ml is now in a separate file minisys.ml, which is also included in system.ml for compatibility.
* Revert "Adding a target for beautification."Gravatar Hugo Herbelin2016-04-27
| | | | This reverts commit c2249c3b4c3387a3c8510e68fc447274d7299695.
* Revert "Adding a target check-beautify for testing reparsability of"Gravatar Hugo Herbelin2016-04-27
| | | | This reverts commit 973b6c69f0861c113f7bd5b94604d2497520a334.
* Revert "Add plugins to Makefile."Gravatar Hugo Herbelin2016-04-27
| | | | This reverts commit 5e9b37a815795efaafd64ab8fe19bf8560d70203.
* Revert "Re-add -beautify by default."Gravatar Hugo Herbelin2016-04-27
| | | | This reverts commit d28c1d7d908fe9d5fc719d58433a6b87c12390ba.
* Revert "Revert "Re-add -beautify by default.""Gravatar Hugo Herbelin2016-04-27
| | | | This reverts commit 67335c832a55cbd0ca559906bbe1af2485241353.
* Revert "Re-add -beautify by default."Gravatar Hugo Herbelin2016-04-27
| | | | This reverts commit 1171590c544492842a848c6765b61c70fca19a01.
* Re-add -beautify by default.Gravatar Hugo Herbelin2016-04-27
|
* Add plugins to Makefile.Gravatar Hugo Herbelin2016-04-27
|
* Adding a target check-beautify for testing reparsability ofGravatar Hugo Herbelin2016-04-27
| | | | | | beautification of the standard library. Currently not intrusive but needs two extra phases of compilation.
* Adding a target for beautification.Gravatar Hugo Herbelin2016-04-27
|
* Creating a dedicated ltac/ folder for Hightactics.Gravatar Pierre-Marie Pédrot2016-03-21
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-09
|\
| * Re-enable OCaml warnings disabled by mistake as part of e759333.Gravatar Maxime Dénès2016-03-07
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.Gravatar Maxime Dénès2016-01-15
| |
| * MMaps: remove it from final 8.5 release, since this new library isn't mature ↵Gravatar Pierre Letouzey2016-01-13
| | | | | | | | | | | | | | | | enough In particular, its interface might still change (in interaction with interested colleagues). So let's not give it too much visibility yet. Instead, I'll turn it as an opam packages for now.
* | mergeGravatar Matej Kosik2016-01-11
|\ \
| * | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The structure of the Context module was refined in such a way that: - Types and functions related to rel-context declarations were put into the Context.Rel.Declaration module. - Types and functions related to rel-context were put into the Context.Rel module. - Types and functions related to named-context declarations were put into the Context.Named.Declaration module. - Types and functions related to named-context were put into the Context.Named module. - Types and functions related to named-list-context declarations were put into Context.NamedList.Declaration module. - Types and functions related to named-list-context were put into Context.NamedList module. Some missing comments were added to the *.mli file. The output of ocamldoc was checked whether it looks in a reasonable way. "TODO: cleanup" was removed The order in which are exported functions listed in the *.mli file was changed. (as in a mature modules, this order usually is not random) The order of exported functions in Context.{Rel,Named} modules is now consistent. (as there is no special reason why that order should be different) The order in which are functions defined in the *.ml file is the same as the order in which they are listed in the *.mli file. (as there is no special reason to define them in a different order) The name of the original fold_{rel,named}_context{,_reverse} functions was changed to better indicate what those functions do. (Now they are called Context.{Rel,Named}.fold_{inside,outside}) The original comments originally attached to the fold_{rel,named}_context{,_reverse} did not full make sense so they were updated. Thrown exceptions are now documented. Naming of formal parameters was made more consistent across different functions. Comments of similar functions in different modules are now consistent. Comments from *.mli files were copied to *.ml file. (We need that information in *.mli files because that is were ocamldoc needs it. It is nice to have it also in *.ml files because when we are using Merlin and jump to the definion of the function, we can see the comments also there and do not need to open a different file if we want to see it.) When we invoke ocamldoc, we instruct it to generate UTF-8 HTML instead of (default) ISO-8859-1. (UTF-8 characters are used in our ocamldoc markup) "open Context" was removed from all *.mli and *.ml files. (Originally, it was OK to do that. Now it is not.) An entry to dev/doc/changes.txt file was added that describes how the names of types and functions have changed.
* | | Merge remote-tracking branch 'origin/v8.5' into trunkGravatar Guillaume Melquiond2016-01-06
|\ \ \ | |/ / |/| / | |/ | | Conflicts: lib/cSig.mli
| * Avoid warning 31: test printer was linked twice with Dynlink and Str.Gravatar Maxime Dénès2016-01-05
| | | | | | | | | | Linking a module twice is unsafe and warning 31 will be fatal by default in OCaml 4.03. See PR#5461.
| * Fix order of files in mllib.Gravatar Maxime Dénès2016-01-05
| | | | | | | | | | | | | | | | CString was linked after Serialize, although the later was using CString.equal. This had not been noticed so far because OCaml was ignoring functions marked as external in interfaces (which is the case of CString.equal) when considering link dependencies. This was changed on the OCaml side as part of the fix of PR#6956, so linking was now failing in several places.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-08
|\|
| * Fixing a minor problem in Makefile.build that was prevening ↵Gravatar Matej Kosik2015-12-07
| | | | | | | | "dev/printers.cma" to be loadable within "ocamldebug".
* | Making output of target source-doc a bit less verbose.Gravatar Hugo Herbelin2015-12-05
| |