aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.install
Commit message (Collapse)AuthorAge
* Remove unneeded fix for BZ#1715Gravatar Gaëtan Gilbert2017-09-11
| | | | | It hasn't been necessary since 6aad0d9cd2104b5343ed7c831a4ad0bbe34007cb introduced $(INSTALLLIB)
* Makefile: install-byte works even if -coqide noGravatar Enrico Tassi2017-08-04
|
* Add timing scriptsGravatar Jason Gross2017-07-11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commit adds timing scripts from https://github.com/JasonGross/coq-scripts/tree/master/timing into the tools folder, and integrates them into coq_makefile and Coq's makefile. The main added makefile targets are: - the `TIMING` variable - when non-empty, this creates for each built `.v` file a `.v.timing` variable (or `.v.before-timing` or `.v.after-timing` for `TIMING=before` and `TIMING=after`, respectively) - `pretty-timed TGTS=...` - runs `make $(TGTS)` and prints a table of sorted timings at the end, saving it to `time-of-build-pretty.log` - `make-pretty-timed-before TGTS=...`, `make-pretty-timed-after TGTS=...` - runs `make $(TGTS)`, and saves the timing data to the file `time-of-build-before.log` or `time-of-build-after.log`, respectively - `print-pretty-timed-diff` - prints a table with the difference between the logs recorded by `make-pretty-timed-before` and `make-pretty-timed-after`, saving the table to `time-of-build-both.log` - `print-pretty-single-time-diff BEFORE=... AFTER=...` - this prints a table with the differences between two `.v.timing` files, and saves the output to `time-of-build-pretty.log` - `*.v.timing.diff` - this saves the result of `print-pretty-single-time-diff` for each target to the `.v.timing.diff` file - `all.timing.diff` (`world.timing.diff` and `coq.timing.diff` in Coq's own Makefile) - makes all `*.v.timing.diff` targets N.B. We need to make `make pretty-timed` fail if `make` fails. To do this, we need to get around the fact that pipes swallow exit codes. There are a few solutions in https://stackoverflow.com/questions/23079651/equivalent-of-pipefail-in-gnu-make; we choose the temporary file rather than requiring the shell of the makefile to be bash.
* Makefile: no bytecode compilation in make world, see make byte insteadGravatar Pierre Letouzey2017-05-30
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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 a future commit about coq_makefile) 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
* enters coq_makefile2Gravatar Enrico Tassi2017-05-23
|
* [META] [build] Install dlls to kernel/byterunGravatar Emilio Jesus Gallego Arias2017-03-10
| | | | This makes the dll path consistent both in `-local` and non-local Coq install.
* [build] Add a target to install the META file.Gravatar Emilio Jesus Gallego Arias2016-10-28
|
* 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.
* 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
* Makefile.install: fix a typo in last commit c954bb5, sorryGravatar Pierre Letouzey2016-06-24
|
* Makefile.install: fix the install of plugin cmiGravatar Pierre Letouzey2016-06-24
| | | | | | | | | | Now that the plugins are packed, a plugin forms now a unique compilation unit, and we only need to install the main cmi file of this plugin (foo_plugin.cmi). Btw, better variable names (e.g. OMEGACMO instead of OMEGACMA) and some other cleanup in Makefile.common (no more INITPLUGINS variable, for instance).
* 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).