aboutsummaryrefslogtreecommitdiffhomepage
path: root/META.coq
Commit message (Collapse)AuthorAge
* [api] [parsing] Move Egram* to `vernac/`Gravatar Emilio Jesus Gallego Arias2018-05-27
| | | | | | | The extension mechanism is specific to metasyntax and vernacinterp, thus it makes sense to place them next to each other. We also fix the META entry for the `grammar` camlp5 plugin.
* Merge PR #7575: [build] Add -cclib -lcoqrun options to build of kernel.cmxa.Gravatar Enrico Tassi2018-05-24
|\
* | [api] Move `Vernacexpr` to parsing.Gravatar Emilio Jesus Gallego Arias2018-05-23
| | | | | | | | | | | | There were a few spurious dependencies on the `Vernac` AST in the pretyper, we remove them and move `Vernacexpr` and `Extend` to parsing, where they do belong more.
| * [build] Add -cclib -lcoqrun options to build of kernel.cmxa.Gravatar Emilio Jesus Gallego Arias2018-05-22
|/ | | | | | | It seems that it is standard practice in the OCaml world to set the `-cclib` flags at library creation time, at least in native libraries. Indeed, this seems to make linking easier as seen for example in #7563.
* [api] Relocate `intf` modules according to dependency-order.Gravatar Emilio Jesus Gallego Arias2018-04-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In a component-based source code organization of Coq `intf` doesn't fit very well, as it sits in bit of "limbo" between different components, and indeed, encourages developers to place types in sometimes random places wrt the hierarchy. For example, lower parts of the system reference `Vernacexpr`, which morally lives in a pretty higher part of the system. We move all the files in `intf` to the lowest place their dependencies can accommodate: - `Misctypes`: is used by Declaremod, thus it has to go in `library` or below. Ideally, this file would disappear. - `Evar_kinds`: it is used by files in `engine`, so that seems its proper placement. - `Decl_kinds`: used in `library`, seems like the right place. [could also be merged. - `Glob_term`: belongs to pretyping, where it is placed. - `Locus`: ditto. - `Pattern`: ditto. - `Genredexpr`: depended by a few modules in `pretyping`, seems like the righ place. - `Constrexpr`: used in `pretyping`, the use is a bit unfortunate and could be fixed, as this module should be declared in `interp` which is the one eliminating it. - `Vernacexpr`: same problem than `Constrexpr`; this one can be fixed as it contains stuff it shouldn't. The right place should be `parsing`. - `Extend`: Is placed in `pretyping` due to being used by `Vernacexpr`. - `Notation_term`: First place used is `interp`, seems like the right place. Additionally, for some files it could be worth to merge files of the form `Foo` with `Foo_ops` in the medium term, as to create proper ADT modules as done in the kernel with `Name`, etc...
* [meta] Add `num` to the set of base libraries.Gravatar Emilio Jesus Gallego Arias2018-04-03
| | | | | | | | | In the META file, the set of base libraries is determined by the dependencies of the `coq.clib` package. We add `num` to the dependencies as otherwise dynamically loading `micromega` and `nsatz` will fail as they require the toplevel to have `num` linked in.
* [META] Update Coq version number.Gravatar Emilio Jesus Gallego Arias2018-03-11
|
* Rename coq.ltac to coq.plugins.ltac in META.coqGravatar Cyprien Mangin2018-01-16
|
* Add plugins to META.coqGravatar Cyprien Mangin2018-01-16
|
* [meta] Fix typo on Coq's META file following #6444.Gravatar Emilio Jesus Gallego Arias2018-01-09
|
* [API] remove large file containing duplicate interfacesGravatar Enrico Tassi2017-12-27
| | | | | ... in favor of having Public/Internal sub modules in each and every module grouping functions according to their intended client.
* [lib] Split auxiliary libraries into Coq-specific and general.Gravatar Emilio Jesus Gallego Arias2017-12-23
| | | | | | | | | | | | | | | | | | | | | | | | Up to this point the `lib` directory contained two different library archives, `clib.cma` and `lib.cma`, which a rough splitting between Coq-specific libraries and general-purpose ones. We know split the directory in two, as to make the distinction clear: - `clib`: contains libraries that are not Coq specific and implement common data structures and programming patterns. These libraries could be eventually replace with external dependencies and the rest of the code base wouldn't notice much. - `lib`: contains Coq-specific common libraries in widespread use along the codebase, but that are not considered part of other components. Examples are printing, error handling, or flags. In some cases we have coupling due to utility files depending on Coq specific flags, however this commit doesn't modify any files, but only moves them around, further cleanup is welcome, as indeed a few files in `lib` should likely be placed in `clib`. Also note that `Deque` is not used ATM.
* [make] More build fixes for static plugins and ocamlfind.Gravatar Emilio Jesus Gallego Arias2017-12-16
| | | | | | | | | | - In ocamlfind-based byte builds, link the VM statically as in native builds. This is the best way to get reliable, path-independent self-contained executables. - In `make install`, install the `.cmx` files for plugins too. To statically link Coq plugins in native mode, both the `.cmx` and `.o` files must be present.
* [meta] Minor linking fix.Gravatar Emilio Jesus Gallego Arias2017-12-13
|
* [META] Some dependency fixes.Gravatar Emilio Jesus Gallego Arias2017-12-09
|
* [general] Merge parsing with highparsing, put toplevel at the top of the ↵Gravatar Emilio Jesus Gallego Arias2017-08-29
| | | | linking chain.
* [meta] [api] Fix META file for API introduction.Gravatar Emilio Jesus Gallego Arias2017-06-29
|
* Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
|
* [META] add support for ide librariesGravatar Emilio Jesus Gallego Arias2017-03-23
| | | | This makes sense for clients willing to link to richpp.
* [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.
* [META] Ltac now a plugin.Gravatar Emilio Jesus Gallego Arias2017-03-10
|
* [META] Update version number.Gravatar Emilio Jesus Gallego Arias2017-03-10
|
* [ocamlbuild] fix small mistakes in descriptionsGravatar Théo Zimmermann2017-02-20
|
* [ocamlbuild] Update meta for the vernac split.Gravatar Emilio Jesus Gallego Arias2017-02-20
|
* [build] META file to enable plugin linking with ocamlfind.Gravatar Emilio Jesus Gallego Arias2016-10-28
This allows building SerAPI and jsCoq using ocamlbuild.