| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: JasonGross
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
|
|
Reviewed-by: SkySkimmer
|
|
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
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
Ack-by: jfehrle
|
|
Reviewed-by: ejgallego
Reviewed-by: erikmd
|
|
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.
|
|
Closes #12351.
We set the parameters of the redirect formatter to be same than the
ones in stdout.
I guess the original semantics was to ignore the parameters, so I'm
unsure we want to do this.
While we are a it, we include a fix on the formatter, which _must_ be
flushed before closing its associated channel.
|
|
The main reason for this change is to reduce the number of places
where the Coq version is hardcoded.
But moreover, I don't see why that wouldn't work since dev is
precisely the version that is defined in the opam files.
|
|
Reviewed-by: Zimmi48
Reviewed-by: cpitclaudel
|
|
|
|
|
|
|
|
This seems like a recurring pattern, and IMO makes a bit better API.
We also remove `merge_universe_subst` as it is not needed so far, as
we were creating stale `evar_map`s just for this purpose.
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: SkySkimmer
Ack-by: ppedrot
|
|
|
|
|
|
Fixes #11936.
Co-authored-by: Jim Fehrle <jfehrle@sbcglobal.net>
|
|
|
|
We complete some arduous refactoring in order to bring all the
internals and code of constant / proof saving into the same module.
In particular, this PR moves the remaining parts of proof saving from
`Lemmas` to `Declare`.
The reduction in exposed internals is considerable; in particular, we
remove the export of the internals of `proof_entry` and `proof_object`
[used in delayed proofs], which will allow us to start to address many
issues with the current setup, such as #10363 .
There are still some TODOs, that will be addressed in subsequent PRs:
- Remove `declare_constant` in favor of higher-level APIs
- Then, remove access to `proof_entry` entirely
- Refactor current very verbose handling of proof info.
- Remove compat modules / API.
- Rework handling of delayed proofs [this may be hard due to state and the STM]
- Reify Hook API for the case where it acts as a continuation [that is to say, declaring constants from the Hook]
List of remaining offenders for `proof_entry` / `declare_constant` in
the codebase:
- File "vernac/comHints.ml"
- File "vernac/indschemes.ml"
- File "vernac/comProgramFixpoint.ml"
- File "vernac/comAssumption.ml"
- File "vernac/record.ml"
- File "plugins/ltac/leminv.ml"
- File "plugins/setoid_ring/newring.ml"
- File "plugins/funind/recdef.ml"
- File "plugins/funind/gen_principle.ml"
|
|
This is needed as a first step to refactor and unify the obligation
save path and state; in particular `Equations` is a heavy user of
Hooks to modify obligations state, thus in order to make the hook
aware of this we need to place the obligation state before the hook.
As a good side-effect, `inline_private_constants` and `Hook.call` are
not exported from `Declare` anymore.
|
|
In our quest to unify all the declaration paths, an important step
is to account for the state pertaining to `Program` declarations.
Whereas regular proofs keep are kept in a stack-like structure;
obligations for constants defined by `Program` are stored in a global
map which is manipulated by almost regular open/close proof primitives.
This PR is in preparation for the switch to a purely functional state
in #11836 ; the full switch requires deeper changes so it is helpful
to have this PR preparing most of the structure.
Most of the PR is routine; only remarkable change is that the hook for
admitted obligations is now called explicitly in `finish_admitted` as
it had to learn about the different types of proof_endings. Before,
obligations set it in `start_lemma` but only used in the `Admitted`
path.
|
|
|
|
|
|
Reviewed-by: herbelin
|
|
This is needed for the case the sources are set to read-only mode, for
example when using Dune >= 2.5 [needed for the global cache support]
Fixes #12264
Co-authored-by: Ignat Insarov <kindaro@gmail.com>
|
|
Reviewed-by: ejgallego
|
|
Part of this PR was automatically generated by running dev/doc/update-compat.py --master
|
|
Reviewed-by: ejgallego
Ack-by: herbelin
|
|
from ssreflect
Reviewed-by: Zimmi48
Ack-by: gares
|
|
|
|
This is akin to what we do for Gitlab.
|
|
Reviewed-by: ejgallego
|
|
but ssrsearch is not loaded.
Fixes #12338
|
|
|
|
cf "If this is implemented, long names might cause a printing
problem:" in #11852
|
|
reductions
Reviewed-by: JasonGross
Ack-by: Zimmi48
|
|
This reverts commits 71ea3ca8b4d3a6fa6b005e48ff7586176b06259e and
0976a670cf853c9bc61b3eee6dceae4a429e066f.
|
|
|
|
Since `ocaml_pwd.ml` was added this unquoted glob would be expanded by
the shell before being passed to `find`.
|
|
|
|
Reviewed-by: MSoegtropIMC
Reviewed-by: Zimmi48
|
