| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: ppedrot
|
|
top of declare.
This PR is a follow up to #10406 , moving the then introduced
`proof_entry` type to `Declare`.
This makes sense as `Declare` is the main consumer of the entry type,
and already provides the constructors for it.
This is a step towards making the entry type private, which will allow
us to enforce / handle invariants on entry data better.
A side-effect of this PR is that now `Proof_global` does depend on
`Declare`, not the other way around, but that makes sense given that
closing an interactive proof will be a client of declare.
Indeed, all `Declare` / `Pfedit` / and `Proof_global` are tied into
tactics due to `abstract`, at some point we may be able to unify all
them into a single file in `vernac`.
|
|
We replace some uses of `raise (UserError ...)` with
`CErrors.user_err`, ideally we would like to make the error raising
API not depend on the exception themselves, but that's still a long
way to go.
We also rename the `Timeout` exception as to clarify purpose in the
codebase, given that it has 3 different ones as of today.
cc: #7560
|
|
Reviewed-by: ppedrot
|
|
This could be Prop (for compat with usual Coq), Set (for HoTT),
or actually an arbitrary "i".
Take lower bound of universes into account in pretyping/engine
Reinstate proper elaboration of SProp <= l constraints:
replacing is_small with equality with lbound is _not_ semantics preserving!
lbound = Set
Elaborate template polymorphic inductives with lower bound Prop
This will make more constraints explicit
Check univ constraints with Prop as lower bound for template inductives
Restrict template polymorphic universes to those not bounded from below
Fixes #9294
fix suggested by Matthieu
Try second fix suggested by Matthieu
Take care of modifying elaboration for record declarations as well.
Rebase and export functions for debug
Remove exported functions used while debugging
Add a new typing flag "check_template" and option "-no-template-checl"
This parameterizes the new criterion on template polymorphic inductives
to allow bypassing it (necessary for backward compatibility).
Update checker to the new typing flags structure
Switch on the new template_check flag to allow old unsafe behavior in
indTyping.
This is the only change of code really impacting the kernel, together
with the commit implementing unbounded from below and parameterization
by the lower bound on universes.
Add deprecated option `Unset Template Check` allowing to make proof
scripts work with both 8.9 and 8.10 for a while
Fix `Template Check` option name and test it
Add `Unset Template Check` to Coq89.v
Cooking of inductives and template-check tests
Cleanup test-suite file for template check / universes(template) flags
cookind tests
Move test of `Unset Template Check` to the failure/ dir, but comment it
for now
Template test-suite test explanation
Overlays for PR 9918
Overlay for paramcoq
Add overlay for fiat_parsers (-no-template-check)
Add overlay for fiat_crypto_legacy
Update fiat-crypto legacy overlay
Now it points at the version that I plan on merging; I am hoping that doing this will guard against mistakes by adding an extra check that the target tested by Coq's CI on this branch works with the change I made.
Remove overlay that should no longer be necessary
The setting in the compat file should handle it
Remove now-merged fiat-crypto-legacy overlay
Update `Print Assumptions` to reflect the typing flag for template checking
Fix About and Print Assumptions for template poly, giving info on which
variables are actually polymorphic
Fix pretty printing to print global universe levels properly
Fix printing of template polymorphic universes
Fix pretty printing for template polymorphism on no universe
Fix interaction of template check and universes(template) flag
Fix indTyping to really check if there is any point in polymorphism: the
conclusion sort should be parameterized over at least one local universe
Indtyping fixes for template polymorphic Props
Allow explicit template polymorphism again
Adapt to new indTyping interface
Handle the case of template-polymorphic on no universes
correctly (morally Type0m univ represented as Prop).
Fix check of meaningfullness of template polymorphism in the kernel.
It is now done w.r.t the min_univ, the minimal universe inferred for the
inductive/record type, independently of the user-written annotation
which must only be larger than min_univ. This preserves compatibility
with UniMath and template-polymorphism as it has been implemented up-to
now.
Comment on identity non-template-polymorphism
Remove incorrect universes(template) attributes from ssr
simpl_fun can be meaningfully template-poly, as well as
pred_key (although the use is debatable: it could just
as well be in Prop).
Move `fun_of_simpl` coercion declaration out of section to respect
uniform inheritance
Remove incorrect uses of #[universes(template)] from the stdlib
Extraction of micromega changes due to moving an ind decl out of a section
Remove incorrect uses of #[universes(template)] from plugins
Fix test-suite files, removing incorrect #[universes(template)] attributes
Remove incorrect #[universes(template)] attributes in test-suite
Fix test-suite
Remove overlays as they have been merged upstream.
|
|
|
|
We remove calls of `Lemmas.Info.make` that where using the default
parameters, as this is mostly dead code now.
This brings into question quite a few things, in particular, the
uneven support of `scope` attributes by different commands / plugins.
We don't attempt to solve that yet, hopefully the ongoing constant
saving path refactoring will be able to take care of these
inconsistencies.
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: mattam82
|
|
We move `binder_kind` to the pretyping AST, removing the last data
type in the now orphaned file `Decl_kinds`.
This seems a better fit, as this data is not relevant to the lower
layers but only used in `Impargs`.
We also move state keeping to `Impargs`, so now implicit declaration
must include the type. We also remove a duplicated function.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
This source of slowness has been observed in VST, but it is probably
pervasive. Most of the unification problems are not mentioning evars,
it is thus useless to compute the set of frozen evars upfront.
We also seize the opportunity to reverse the flag, because it is always
used negatively.
|
|
We place control attributes on their own, datatype, similarly to
regular attributes.
This is a step towards fixing #10452 , as we can now decouple control
attributes from the vernac AST itself, allowing to pass them
independently.
|
|
`Mlutil.simpl` and `Mlutil.atomic_eta_red` did some unsound eta-reductions as
follows:
(fun x0 ... xn => MLexn x0 ... xn) ->eta MLexn.
`MLexn` raises an exception thus is not a value in OCaml. So the above
simplification may change the behavior of extracted programs. This patch
restricts `atomic_eta_red` to eta-redexes whose core is both atomic and value.
Acknowledgement: This work is financially supported by Peano System Inc.
on-behalf-of: @peano-system <info@peano-system.jp>
|
|
|
|
involving &
Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: gares
Ack-by: ggonthier
Ack-by: herbelin
Reviewed-by: maximedenes
Ack-by: vbgl
|
|
Changes:
* Add ssrclasses.v that redefines [Reflexive] and [iff_Reflexive];
* Add ssrsetoid.v that links
[ssrclasses.Reflexive] and [RelationClasses.Reflexive];
* Add [Require Coq.ssr.ssrsetoid] in Setoid.v;
* Update ssrfwd.ml accordingly, using a helper file ssrclasses.ml that
ports some non-exported material from rewrite.ml;
* Some upside in passing: ssrfwd.ml no more depends on Ltac_plugin;
* Update doc and tests as well.
Summary:
* We can now use the under tactic in two flavors:
- with the [eq] or [iff] relations: [Require Import ssreflect.]
- or a [RewriteRelation]: [Require Import ssreflect. Require Setoid.]
(while [ssreflect] does not require [RelationClasses] nor [Setoid],
and conversely [Setoid] does not require [ssreflect]).
* The file ssrsetoid.v could be skipped when porting under to stdlib2.
|
|
|
|
|
|
Reviewed-by: ppedrot
|
|
* Add an extra test with an Equivalence.
* Update the doc accordingly.
|
|
|
|
Ack-by: Zimmi48
Ack-by: silene
|
|
Reviewed-by: ppedrot
|
|
- Inline record projections by default (except for Haskell extraction).
- Extend `pp_record_proj` for record projections involving `MLmagic`.
- Remove special treatments for pretty-printing for record projections other
than `pp_record_proj`.
- `micromega.ml` had to be changed due to this change of the extraction plugin.
Acknowledgement: This work is financially supported by Peano System Inc.
on-behalf-of: @peano-system <info@peano-system.jp>
|
|
This removes the export of two internal functions, moving to their
only use place.
In particular, `make_scheme` was exposing the low-level `proof_entry`
object, which should not do.
This will allow to refactor all these constant-building functions
towards a more uniform use of the API. In particular, all the
functions manipulating proof entries directly are in `Gen_principle`.
|
|
|
|
|
|
We also attempt a version that may work with `Proofview.tactic` , may
need more work.
|
|
|
|
|
|
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: maximedenes
|
|
|
|
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
Pointed out by Gaëtan Gilbert.
|
|
We continue over the previous commit and remove redundant
`structured_fixpoint_expr` record in favor of the one used in the AST.
This removes some term-shuffling, tho we still have discrepancies
related to adjustments on the recursive annotation.
|
|
We turn the tuples used for (co)-fixpoints into records, cleaning up
their users.
More cleanup is be possible, in particular a few functions can now
shared among co and fixpoints, also `structured_fixpoint_expr` could
like be folded into the new record.
Feedback on the naming of the records fields is welcome.
This is a step towards cleaning up code in `funind`, as it is the main
consumer of this data structure, as it does quite a bit of fixpoint
manipulation.
cc: #6019
|
|
We register the ML tactics by hand using the low-level API.
|
|
Primitive operations addc, addcarryc, subc, subcarryc, and diveucl are
implemented in the kernel so that they can be used by OCaml code (e.g.,
extracted code) as the other primitives.
|
|
The ExtrOCamlInt63 module can be required to map primitives from the Int63
module to their OCaml implementation (module Uint63 from the kernel).
|
|
Redefine classical real numbers as a quotient of those constructive real numbers.
|
|
|
|
Reviewed-by: SkySkimmer
Ack-by: ppedrot
|
|
Reviewed-by: SkySkimmer
|
|
The current code does some "opacification" for `Let`s, however that's
pretty fragile in general and not all codepaths do respect it.
We need to decide what to do.
|
|
Not pretty, but it had to be done some day, as `Globnames` seems to be
on the way out.
I have taken the opportunity to reduce the number of `open` in the
codebase.
The qualified style would indeed allow us to use a bit nicer names
`GlobRef.Inductive` instead of `IndRef`, etc... once we have the
tooling to do large-scale refactoring that could be tried.
|
|
The changes are large due to `Pervasives` deprecation:
- the `Pervasives` module has been deprecated in favor of `Stdlib`, we
have opted for introducing a few wrapping functions in `Util` and
just unqualified the rest of occurrences. We avoid the shims as in
the previous attempt.
- a bug regarding partial application have been fixed.
- some formatting functions have been deprecated, but previous
versions don't include a replacement, thus the warning has been
disabled.
We may want to clean up things a bit more, in particular
w.r.t. modules once we can move to OCaml 4.07 as the minimum required
version.
Note that there is a clash between 4.08.0 modules `Option` and `Int`
and Coq's ones. It is not clear if we should resolve that clash or
not, see PR #10469 for more discussion.
On the good side, OCaml 4.08.0 does provide a few interesting
functionalities, including nice new warnings useful for devs.
|
|
We remove the special error printing pre-processing in favor of just
calling the standard printers.
Error printing has been a bit complex for a while due to an incomplete
migration to a new printing scheme based on registering exception
printers; this PR should alleviate that by completing the registration
approach.
After this cleanup, it should not be ever necessary for normal
functions to worry a lot about catching errors and re-raising them,
unless they have some very special needs.
This change also allows to consolidate the `explainErr` and `himsg`
modules into one, removing the need to export the error printing
functions. Ideally we would make the contents of `himsg` more
localized, but this can be done in a gradual way.
|
