| Age | Commit message (Collapse) | Author |
|---|
|
When encountering
```Coq
Module M : T.
...
Lemma c :...
...
Qed.
...
End M.
```
every field `c` without body in `T` but with a body in `M` is
registered as opacified in a table along with all constants
`opacified(c)` without body in the environment at this point (i.e.,
all axioms potentially used by c).
Then, when printing axioms, if `c` appears in the final environment it
is replaced by `opacified(c)` in the resulting list of axioms.
|
|
|
|
eta-expansion of "match" branches
Reviewed-by: gares
Ack-by: ppedrot
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
Reviewed-by: vbgl
|
|
Reviewed-by: JasonGross
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
|
|
Reviewed-by: SkySkimmer
|
|
This, for example, improves the CI display, so that `$ echo
'end:coq.test'` does not appear on the same line as the end of the
timing table.
|
|
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
|
|
|
|
This removes a use of internal obligation data `prg_poly` and a couple
of duplicate lines.
|
|
|
|
Not necessary anymore after the merge of obligation declaration into
the main path.
|
|
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.
|
|
cc: #12350
|
|
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
|
