| Age | Commit message (Collapse) | Author |
|---|
|
Also make `Check S` no longer anomaly
Add a couple more test cases for numeral notations
Also add another possibly-confusing error message to the doc.
Respond to Hugo's doc request with Zimmi48's suggestion
From https://github.com/coq/coq/pull/8064/files#r204191608
|
|
Some of this code is cargo-culted or kludged to work.
As I understand it, the situation is as follows:
There are two sorts of use-cases that need to be supported:
1. A plugin registers an OCaml function as a numeral interpreter. In
this case, the function registration must be synchronized with the
document state, but the functions should not be marshelled / stored
in the .vo.
2. A vernacular registers a Gallina function as a numeral interpreter.
In this case, the registration must be synchronized, and the function
should be marshelled / stored in the .vo.
In case (1), we can compare functions by pointer equality, and we should
be able to rely on globally unique keys, even across backtracking.
In case (2), we cannot compare functions by pointer equality (because
they must be regenerated on unmarshelling when `Require`ing a .vo file),
and we also cannot rely on any sort of unique key being both unique and
persistent across files.
The solution we use here is that we ask clients to provide "unique"
keys, and that clients tell us whether or not to overwrite existing
registered functions, i.e., to tell us whether or not we should expect
interpreter functions to be globally unique under pointer equality. For
plugins, a simple string suffices, as long as the string does not clash
between different plugins. In the case of vernacular-registered
functions, use marshell a description of all of the data used to
generate the function, and use that string as a unique key which is
expected to persist across files. Because we cannot rely on
function-pointer uniqueness here, we tell the
interpretation-registration to allow overwriting.
----
Some of this code is response to comments on the PR
----
Some code is to fix an issue that bignums revealed:
Both Int31 and bignums registered numeral notations in int31_scope. We
now prepend a globally unique identifier when registering numeral
notations from OCaml plugins. This is permissible because we don't
store the uid information for such notations in .vo files (assuming I'm
understanding the code correctly).
|
|
|
|
Earlier, the nat_syntax_plugin was loaded as soon as Datatypes.v.
This would now implies to make Datatypes.v depends on Decimal.v.
Instead, we postpone the Numeral Notation for nat until Prelude.v,
and we adapt those three tests that happen to live strictly between
Datatypes and Prelude.
|
|
The first part (e.g. register_bignumeral_interpretation) deals only with
the interp/uninterp closures. It should typically be done as a side
effect during a syntax plugin loading. No prim notation are active yet
after this phase.
The second part (enable_prim_token_interpretation) activates the prim
notation. It is now correctly talking to Summary and to the LibStack.
To avoid "phantom" objects in libstack after a mere Require, this
second part should be done inside a Mltop.declare_cache_obj
The link between the two parts is a prim_token_uid (a string), which
should be unique for each primitive notation. When this primitive
notation is specific to a scope, the scope_name could be used as uid.
Btw, the list of "patterns" for detecting when an uninterpreter should
be considered is now restricted to a list of global_reference
(inductive constructors, or injection functions such as IZR).
The earlier API was accepting a glob_constr list, but was actually
only working well for global_reference.
A minimal compatibility is provided (declare_numeral_interpreter),
but is discouraged, since it is known to store uncessary objects
in the libstack.
|
|
|
|
|
|
|
|
|
|
|
|
(NB: only variables whose binder is inside the constructor argument,
ie
Inductive foo := C : forall A : Type -> Type, A Type -> foo.
does not trigger the bug because A becomes a RelKey.)
|
|
This change is based on noticing that we use a default value for the
`sideff` argument even though we have a similarly named `side_eff`
available. Someone who knows how side effects and universes are
supposed to interact should check this.
|
|
|
|
Fixes #8158
|
|
|
|
Also prevents to use an entry name already defined.
|
|
- New command "Declare Custom Entry bar".
- Entries can have levels.
- Printing is done using a notion of coercion between grammar
entries. This typically corresponds to rules of the form
'Notation "[ x ]" := x (x custom myconstr).' but also
'Notation "{ x }" := x (in custom myconstr, x constr).'.
- Rules declaring idents such as 'Notation "x" := x (in custom myconstr, x ident).'
are natively recognized.
- Rules declaring globals such as 'Notation "x" := x (in custom myconstr, x global).'
are natively recognized.
Incidentally merging ETConstr and ETConstrAsBinder.
Noticed in passing that parsing binder as custom was not done as in
constr.
Probably some fine-tuning still to do (priority of notations,
interactions between scopes and entries, ...). To be tested live
further.
|
|
This is in preparation of changes in level_eq, to check that the
semantics is preserved.
|
|
GitLab setup is quite stable these days thanks to the work of many
people and `coqbot`. We decided to keep CircleCI support for a while
as a safeguard in case something happened in the migration to GitLab,
but these days we are just wasting resources to them and to us. As I'm
afraid CircleCI won't scale for us, the time to remove it has arrived.
Still, CircleCI had some awesome functionality that GitLab's CI
doesn't offer yet, see the links at:
https://github.com/coq/coq/issues/6919#issuecomment-395885573
- https://gitlab.com/gitlab-org/gitlab-ce/issues/29347
- https://gitlab.com/gitlab-org/gitlab-ce/issues/35222
- https://gitlab.com/gitlab-org/gitlab-ce/issues/41947
- https://gitlab.com/gitlab-org/gitlab-ce/issues/47063
|
|
Print the expected and actual types for the option value (which is one
of bool, int, or string).
|
|
Même causes, mêmes effets, similar fix to #8119:
- Do not pass let-bound arguments to evars.
We seize the opportunity to remove the useless type information for Aevar.
Special fixes to native compilation:
- Evars are not handled correctly when iterating over lambda terms.
- Names.id_of_string is gone.
- Evar instances are not reified in the right order.
|
|
|
|
pattern (closes #7777)
|
|
which has no matching clauses.
|
|
Internal lemmas are inlined in obligations bodies, hence their universes
have to be declared with the obligations themselves. ~sideff:true was
not including the side effects universes and constraints in that case.
|
|
|
|
This is particularly useful when the pattern is part of a disjunction.
Maybe this could be improved though, not mentioning the pattern when
there is no disjunction, but that would be more work.
|
|
If a term is matched only against variables, it will not introduce a
"match" and thus, even if the term is of an inductive type, its
indices will not be taken into account in the current algorithm
(though one could imagine an algorithm which does an expansion
specially in order to filter on indices).
This allows to tell the unification not to use dependencies which the
pattern-matching algorithm is not able to exploit in practice.
See example in file 2733.v.
|
|
There were actually two broken things with VM + evars, the fixes are:
- Do not pass let-bound arguments to evars.
- Use the right order for evar arguments.
Native compilation seems to be suffering from the same shortcomings, I will
open a separate bug and adapt the PR.
|
|
|
|
|
|
No reason not to collapse inner applications with explicit arguments.
This is compatible with the ad hoc encoding of @f as GApp(f,[])/NApp(f,[]).
|
|
underline, etc.)
|
|
|
|
|
|
Remove forward reference to lexer.
|
|
Proof General requires minor changes to make the diffs visible, but this code
shouldn't break the existing version of PG.
Diffs are computed for the hypotheses and conclusion of the first goal between
the old and new proofs. Strings are split into tokens using the Coq lexer,
then the list of tokens are diffed using the Myers algorithm. A fixup routine
(Pp_diff.shorten_diff_span) shortens the span of the diff result in some cases.
Diffs can be enabled with the Coq commmand "Set Diffs on|off|removed." or
"-diffs on|off|removed" on the OS command line. The "on" option shows only the
new item with added text, while "removed" shows each modified item twice--once
with the old value showing removed text and once with the new value showing
added text.
The highlights use 4 tags to specify the color and underline/strikeout.
These are "diffs.added", "diffs.removed", "diffs.added.bg" and "diffs.removed.bg".
The first two are for added or removed text; the last two are for
unmodified parts of a modified item.
Diffs that span multiple strings in the Pp are tagged with "start.diff.*" and
"end.diff.*", but only on the first and last strings of the span.
|
|
|
|
(e.g. for debugging)
|
|
case of missing record field
|
|
|
|
As stated in the manual, the fourier tactic is subsumed by lra.
|
|
While we were adding a new field into `QuestionMark`, we
decided to go ahead and refactor the constructor to hold
an actual record. This record now holds the name, obligations, and
whether the evar represents a missing record field.
This is used to provide better error messages on missing record
fields.
|
|
Closes #7967.
|
|
For now we only copy the templates, but we could do more fancy stuff.
This helps to be compatible with build systems that take care of these
files automatically, see:
https://github.com/coq/coq/pull/6857#discussion_r202096579
|
|
We use a more abstract representation for accumulators in the native
compilation scheme, that requires less fiddling with low-level implementation
details. It might be slower though.
|
|
We make it possible to deprecate tactics defined by `Ltac`, `Tactic
Notation` or ML.
For the first two variants, we anticipate the syntax of attributes:
`#[deprecated(since = "XX", note = "YY")]`
In ML, the syntax is:
```
let reflexivity_depr =
let open CWarnings in
{ since = "8.5"; note = "Use admit instead." }
TACTIC EXTEND reflexivity DEPRECATED reflexivity_depr
[ "reflexivity" ] -> [ Tactics.intros_reflexivity ]
END
```
A warning is shown at the point where the tactic is used (either
a direct call or when defining another tactic):
Tactic `foo` is deprecated since XX. YY
YY is typically meant to be "Use bar instead.".
|
|
|
|
|
|
|
