| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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.
|
|
Reviewed-by: Zimmi48
Reviewed-by: gares
|
|
This component holds the code for initializing Coq:
- parsing arguments not specific to the toplevel
- initializing all components from vernac downwards (no stm)
This commit moves stm specific arguments parsing to stm/stmargs.ml
|
|
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
|
|
|
|
incidentally the "projects" array can be queried to get the list
of projects
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: gares
|
|
|
|
Checked by the linter so we don't forget to update it.
Also checked by before_script so we don't run jobs for nothing.
|
|
This avoids the need to rebase the overlay when nothing has changed.
|
|
|
|
We make it compatible by expanding "[0-9]\+" into "[0-9][0-9]*".
|
|
Fixes #12386
|
|
|
|
|
|
h/t SkySkimmer at
https://github.com/coq/coq/pull/12316#issuecomment-630952659
|
|
As per PR review request
|
|
Fixes #12300
Note that I currently only paginate the API call for the number of
reviews, not the main API call, because (a) the main API call doesn't
seem subject to pagination (it returns a dict, not an array), and (b)
because fetching the total number of pages incurs an extra API call for
each one that we want to paginate, even if there is only one page. We
could work around (b) with a significantly more complicated
`curl_paginate` function which heuristically recognizes the end of the
header/beginning of the body, such as
```bash
curl_paginate() {
# as per https://developer.github.com/v3/guides/traversing-with-pagination/#changing-the-number-of-items-received, GitHub will never give us more than 100
url="$1?per_page=100"
# We need to process the header to get the pagination. We have two
# options:
#
# 1. We can make an extra API call at the beginning to get the total
# number of pages, search for a rel="last" link, and then loop
# over all the pages.
#
# 2. We can ask for the header info with every single curl request,
# search for a rel="next" link to follow to the next page, and
# then parse out the body from the header.
#
# Although (1) is simpler, we choose to do (2) to save an extra API
# call per invocation of curl.
while [ ! -z "${url}" ]; do
response="$(curl -si "${url}")"
# we search for something like 'link: <https://api.github.com/repositories/1377159/pulls/12129/reviews?page=2>; rel="next", <https://api.github.com/repositories/1377159/pulls/12129/reviews?page=2>; rel="last"' and take the first 'next' url
url="$(echo "${response}" | grep -m 1 -io '^link: .*>; rel="next"' | grep -o '<[^>]*>; rel="next"' | grep -o '<[^>]*>' | sed s'/[<>]//g')"
echo "Response: ${response}" >&2
echo "${response}" |
{
is_header="yes"
while read line; do
if [ "${is_header}" == "yes" ]; then
if echo "${line}" | grep -q '^\s*[\[{]'; then # we treat lines beginning with [ or { as the beginning of the response body
is_header="no"
echo "${line}"
fi
else
echo "${line}"
fi
done
}
done
}
```
|
|
Ack-by: SkySkimmer
Reviewed-by: ejgallego
|
|
Cf. #12049.
|
|
|
|
The idea is very simple: use the list in the release branch to know
which changelog entries to include, but do the work of removing these
entries and consolidating the released changelog in the master branch
(so that it is applied both to the master branch and to the release
branch following the backporting process).
|
|
Reviewed-by: JasonGross
|
|
Fix #11967
|
|
Thanks to `.ocamlformat-ignore`, we can call ocamlformat blindly but
only the non-ignored files will be affected.
Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
|
|
|
|
|
|
|
|
Ack-by: JasonGross
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
|
|
The message was confusing and the prompt let one reviewer think the
merge script would take care of doing the pull, which it doesn't.
|
|
And simplify a lot the compatibility infrastructure following this.
Update dev/tools/update-compat.py
Remove much complexity.
Co-authored-by: Jason Gross <jgross@mit.edu>
|
|
It is useful for the release process, and there is no reason for somebody
to lose time reimplementing it again.
|
|
|
|
c.f. https://github.com/coq/coq/pull/11032#issue-335944369
Also, change the default from python2 to python3 for update-compat while
we're at it, and update file unicode handling accordingly.
(Note that this file still works with both python2 and python3.)
|
|
|
|
|
|
|
|
This removes spurious Ack-by lines
|
|
Fixes #10465
Following discussion we don't allow a generic `/usr/bin/python`
shebang anymore. We thus move all the scripts [but one] to python3,
and add python3 to the Azure base environment.
Unfortunately we still depend on python2 for the update-compat.py
script, see #10491
We thus have to complement #10467 adding python2 back to Nix,
until #10491 is fixed.
|
|
Remove other types of lines before copyright headers.
|
|
ml-style headers.
|
|
definitions
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ggonthier
Reviewed-by: herbelin
|
|
We also slightly change the semantics of the `compat` syntax modifier to
re-express it in terms of the `deprecated` attribute, and we deprecate
it in favor of the latter.
|
|
|
|
- use coqc instead of coqtop (since -compile doesn't work anymore this
is better)
- pass through extra arguments to dune-dbg
- auto detect the need to pass -emacs to ocamldebug
- instructions for emacs users
The dune-dbg dependencies are still broken ;_;
|
|
It now uses the origin/master branch rather than the master branch, thus
avoiding the need for local merges.
More importantly, it no longer creates a subshell in case of conflicts,
but instead gives control back to the user. Once conflicts are solved, it
suffices to relaunch the script (instead of exiting the subshell). The
reason is that, otherwise, there was no sane way of giving up a backport,
due to the infinite subshell loop.
|
