| Age | Commit message (Collapse) | Author |
|---|
|
Now that the platform takes care of it.
|
|
|
|
We introduce a new package structure for Coq:
- `coq-core`: Coq's OCaml tools code and plugins
- `coq-stdlib`: Coq's stdlib [.vo files]
- `coq`: meta-package that pulls `coq-{core,stdlib}`
This has several advantages, in particular it allows to install Coq
without the stdlib which is useful in several scenarios, it also open
the door towards a versioning of the stdlib at the package level.
The main user-visible change is that Coq's ML development files now
live in `$lib/coq-core`, for compatibility in the regular build we
install a symlink and support both setups for a while.
Note that plugin developers and even `coq_makefile` should actually
rely on `ocamlfind` to locate Coq's OCaml libs as to be more robust.
There is a transient state where we actually look for both
`$coqlib/plugins` and `$coqlib/../coq-core/plugins` as to support
the non-ocamlfind plus custom variables.
This will be much improved once #13617 is merged (which requires this
PR first), then, we will introduce a `coq.boot` library so finally
`coqdep`, `coqchk`, etc... can share the same path setup code.
IMHO the plan should work fine.
|
|
We also spill (some) non-generic arguments and initialization code
out of coqargs and to coqtop, namely colors for the terminal. There are
more of these, left to later commits.
|
|
|
|
|
|
I believe this renaming makes it easier for new contributors to discover
the code of `ring`.
|
|
Reviewed-by: gares
Reviewed-by: ppedrot
Reviewed-by: silene
|
|
|
|
|
|
Alternative to adding this feature to coqbot (coq/bot#14).
|
|
|
|
This allows coqbot to reply back with a minimized
version of some code reproducing a bug, using the
coq-bug-minimizer program from Jason Gross.
See https://github.com/JasonGross/coq-tools#coq-bug-minimizer.
|
|
|
|
|
|
Reviewed-by: Zimmi48
|
|
Currently, `.v` under the `Coq.` prefix are found in both `theories`
and `plugins`. Usually these two directories are merged by special
loadpath code that allows double-binding of the prefix.
This adds some complexity to the build and loadpath system; and in
particular, it prevents from handling the `Coq.*` prefix in the
simple, `-R theories Coq` standard way.
We thus move all `.v` files to theories, leaving `plugins` as an
OCaml-only directory, and modify accordingly the loadpath / build
infrastructure.
Note that in general `plugins/foo/Foo.v` was not self-contained, in
the sense that it depended on files in `theories` and files in
`theories` depended on it; moreover, Coq saw all these files as
belonging to the same namespace so it didn't really care where they
lived.
This could also imply a performance gain as we now effectively
traverse less directories when locating a library.
See also discussion in #10003
|
|
|
|
Integrate merging doc in the main contributing document.
|
|
It was decided during the Coq WG that code owner teams are more
convenient, in particular because they allow adding and removing team
members without going through a pull request. For each team, we
should aim to have at least three code owners, even if in some cases
we are going to start with less.
We also stop triggering review requests for changelog entries as was
also decided during the WG.
|
|
I want to be notified when these are changed
|
|
|
|
|
|
|
|
Who should be secondary owner?
|
|
A link to this file will be displayed when people start opening an
issue, and maybe in some other places.
See also:
https://help.github.com/en/articles/adding-support-resources-to-your-project
|
|
Move existing entries.
|
|
|
|
|
|
|
|
Reviewed-by: ejgallego
Reviewed-by: gares
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
changes.
|
|
|
|
|
|
Fixes #8621
|
|
compat updates to do as part of a release.
|
|
Also test that the compat updating script hasn't become outdated on the
CI.
|
|
As requested in
https://github.com/coq/coq/issues/8311#issuecomment-415976318
the release process describes the steps to take.
All automatable steps are taken by the new script
dev/tools/update-compat.py
I've tried to make the script relatively easy to update if functions get
renamed or moved, but since it's doing unstructured source manipulation,
it is sort-of fragile.
We could plausibly add a file to the test-suite to ensure that we catch
script-breakage early, but this would require dropping compatibility
support much earlier in the development cycle (the compatibility changes
would have to come right when the new version is branched, rather than
shortly before the beta release).
|
|
This was kept as a fallback for some time, not worth keeping it
anymore as our GitLab setup seems mature and reliable enough.
|
|
|
