| Age | Commit message (Collapse) | Author |
|---|
|
1. Fix casing of build_prep_overlay argument.
Follow-up of 6cc6b87f997d7a5e848203b49bfedfaa96c53bb2
2. Call autoconf directly.
Adapted from a9996619e2d2352e0e60faf4dbde78fa1549b2af
|
|
some machines.
Reviewed-by: SkySkimmer
Reviewed-by: cpitclaudel
|
|
|
|
The will make it possible to put a VsCoq toplevel in `ide/vscoq`.
|
|
Note that this should reduce the overall build time of fiat-crypto
related targets by about 10--20 minutes, as I've removed the heaviest
jobs (about 25--30 minutes in serial) from the OCaml target.
I'd like to keep the OCaml target around just to make sure that Coq
doesn't introduce a change to extraction that breaks compilation of
extracted OCaml code. See https://github.com/ocaml/ocaml/issues/7826
for the issue tracking performance of compiling the extracted OCaml
code (and perhaps there should be another issue opened on the OCaml bug
tracker about flambda on the fiat-crypto extracted files?)
Alternative to #12405
Closes #12405
Fixes #12400
|
|
|
|
Fixes #12386
|
|
|
|
|
|
Reviewed-by: SkySkimmer
Reviewed-by: vbgl
|
|
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
}
```
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
Ack-by: jfehrle
|
|
|
|
This is a new development where I'm aggregating a specific set of
benchmarks. It's intended to be relatively lightweight, taking only a
handful of minutes. It's probably one of the few developments currently
testing Ltac2.
|
|
cc: #12350
|
|
Reviewed-by: Zimmi48
Reviewed-by: cpitclaudel
|
|
Reviewed-by: ejgallego
|
|
Fixes #11936.
Co-authored-by: Jim Fehrle <jfehrle@sbcglobal.net>
|
|
|
|
|
|
|
|
Part of this PR was automatically generated by running dev/doc/update-compat.py --master
|
|
|
|
- use a different mirror for main cygwin archive
- (always) publish build log as artifact
- fix call to dune makefiles
- we do just build Coq for now, as:
+ dune is rebuilding Coq to run the test-suite, this needs move
investigation.
+ the test suite seems to take long and it times-out on Win.
|
|
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
Ack-by: kyoDralliam
|
|
Reviewed-by: Zimmi48
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
|
|
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
|
|
Ack-by: SkySkimmer
Reviewed-by: ejgallego
|
|
|
|
Reviewed-by: JasonGross
Ack-by: Zimmi48
Ack-by: herbelin
|
|
Reviewed-by: MSoegtropIMC
|
|
Re-raising inside exception handlers must be done with care in order
to preserve backtraces; even if newer OCaml versions do a better job
in automatically spilling `%reraise` in places that matter, there is
no guarantee for that to happen.
I've done a best-effort pass of places that were re-raising
incorrectly, hopefully I got the logic right.
There is the special case of `Nametab.error_global_not_found` which is
raised many times in response to a `Not_found` error; IMHO this error
should be converted to something more specific, however the scope of
that change would be huge as to do easily...
|
|
Reviewed-by: Matafou
Ack-by: SkySkimmer
Reviewed-by: gares
|
|
We move from the previous complex CI download setup to a much more
straightforward public mirror repository.
Thanks to Yishuai Li and Benjamin Pierce for the very quick response.
Closes #12290
|
|
|
|
|
|
Reviewed-by: Zimmi48
|
|
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: maximedenes
|
|
|
|
|
|
|
|
|
|
Also fix an installation issue
|
