| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
| |
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.
|
| |\ |
|
| | |
| |
| |
| |
| |
| | |
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.
|
| |/
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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...
|
| |
|
|
|
|
|
|
|
| |
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.
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
... in favor of having Public/Internal sub modules in each and
every module grouping functions according to their intended client.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
| |
- 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.
|
| | |
|
| | |
|
| |
|
|
| |
linking chain.
|
| | |
|
| | |
|
| |
|
|
| |
This makes sense for clients willing to link to richpp.
|
| |
|
|
| |
This makes the dll path consistent both in `-local` and non-local Coq install.
|
| | |
|
| | |
|
| | |
|
| | |
|
|
|
This allows building SerAPI and jsCoq using ocamlbuild.
|
Emilio Jesus Gallego Arias
Enrico Tassi
Cyprien Mangin
Matej Kosik
Théo Zimmermann