aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.dev
Commit message (Collapse)AuthorAge
* [general] Merge parsing with highparsing, put toplevel at the top of the ↵Gravatar Emilio Jesus Gallego Arias2017-08-29
| | | | linking chain.
* Prelude : no more autoload of plugins extraction and recdefGravatar Pierre Letouzey2017-06-14
| | | | | | | | | | | | | | | | | The user now has to manually load them, respectively via: Require Extraction Require Import FunInd The "Import" in the case of FunInd is to ensure that the tactics functional induction and functional inversion are indeed in scope. Note that the Recdef.v file is still there as well (it contains complements used when doing Function with measures), and it also triggers a load of FunInd.v. This change is correctly documented in the refman, and the test-suite has been adapted.
* Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
|
* [checker] Add bin/votour to the coqocaml target.Gravatar Emilio Jesus Gallego Arias2017-05-26
|
* Travis: add -warn-error targets (standard and 4.04.1 ocaml)Gravatar Gaetan Gilbert2017-05-17
|
* [camlpX] Enrico's changes to camlp4 removal.Gravatar Emilio Jesus Gallego Arias2017-04-07
| | | | | This removes some remaining support for camlp4 in the infrastructure and documents the change.
* Ltac as a plugin.Gravatar Pierre-Marie Pédrot2017-02-17
| | | | | | | This commit is essentially moving files around. In particular, the corresponding plugin still relies on a mllib file rather than a mlpack one. Otherwise, this causes link-time issues for third-party plugins depending on modules defined in the Ltac plugin.
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-02
|\
| * Missing .PHONY targets.Gravatar Pierre-Marie Pédrot2016-08-30
| |
* | No more dev/printers.cmaGravatar Pierre Letouzey2016-07-26
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This file was only used during ocamldebug sessions (in the dev/db script). It was containing a large subset of the core cma files, up to the printing functions. There were a few notable exceptions, for instance no kernel/vm.cmo to avoid loading dllcoqrun.so in ocamldebug. But printers.cma was troublesome to maintain : almost each time an ML file was added/removed/renamed in the core of Coq, dev/printers.mllib had to be edited, in addition to the directory-specific .mllib (kernel/kernel.mllib and co). So I propose here to kill this file, and put instead in dev/db several "load_printer" of the core cma files. For that to work, we need to compile kernel/kernel.cma with the right -dllib and -dllpath options, but that shouldn't hurt (on the contrary). We also source now the camlpX cma in dev/db, via a new generated file dev/camlp4.dbg containing a load_printer of either gramlib.cma or camp4lib.cma. If one doesn't want to perform the whole "source db" at the start of an ocamldebug session, then the former "load_printer printers.cma" could be replaced by: source core.dbg load_printer top_printers.cmo See for instance the minimal dev/base_db.
* | Makefile.dev: fix a typo in the 'logic' ruleGravatar Pierre Letouzey2016-07-13
| |
| * Makefile.dev: fix a typo in the 'logic' ruleGravatar Pierre Letouzey2016-07-13
|/
* 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).