| Age | Commit message (Collapse) | Author |
|---|
|
This (partially) reverts commit 3984f3c1db51f7b788ad49eafb7647774e8d1f53.
This broke clients wanting to inspect the enviroment, see
https://github.com/coq/coq/pull/7745#issuecomment-411597610
There is a need for clients to inspect the global environment, we keep
the record private as to concerns regarding its use, so even if no
function in the kernel is taking a `globals` as an input, we transmit
to clients its read-only nature.
We take the opportunity to refactor the record into a module with
scoped constructors.
|
|
Reviewed-by: cpitclaudel
|
|
Reviewed-by: vbgl
|
|
|
|
|
|
|
|
reduce or not.
Reviewed-by: jfehrle
|
|
There were 2:
- when declaring a constraint to avoid monomorphic constraint
referring to polymorphic univs, this check is redundant with the
check in Section.ml
- when declaring a universe context to avoid redeclaring universes,
this is not necessary after recent commits.
|
|
|
|
The general idea is to move tests on scope=Discharge and on
Lib.sections_are_opened up in the call stack. This allows better
control over the universe manipulation.
There are some corner case behaviour change, eg:
- [Context (foo:=bla)] outside a section correctly declares an
axiom (fix #10668)
- (not observable) universes for [Variable A B : Type] in section are declared only once
- universes and universe names for [Axiom A B : Type] are declared
only once. This changes the qualification of the universe name:
before it was the last axiom (so [B.u0]), now it's the first
one ([A.u0]).
Probably nobody cares about this.
- context outside section uses different [kind]
I'm not sure why context outside a section behaves differently based
on whether we're in a module type, I tried to preserve it but maybe we
should uniformize.
The universe manipulation for Axiom (in the declare_assumptions
function) is a bit awkward, maybe when there are multiple monomorphic
axioms instead of trying to attach the universes to the first one we
should just declare them separately like with Context. OTOH unlike
with context dropping the universe names seems incorrect.
|
|
Primitives don't have anything to do with assumptions.
|
|
(letins still declare universes in declare_variable as they use
entries)
The section check_same_poly is moved to declare_universe_context (it
makes more sense there, universe polymorphism doesn't apply to the
variables/letins themselves)
|
|
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
|
|
|
|
database
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
We only do it for entries and not declarations because the upper layers
rely on the kernel being able to quickly tell that a definition is improperly
used inside a section. Typically, tactics can mess with the named context
and thus make the use of section definitions illegal. This cannot happen in
the kernel but we cannot remove it due to the code dependency.
Probably fixing a soundness bug reachable via ML code only. We were doing
fancy things w.r.t. computation of the transitive closure of the the variables,
in particular lack of proper sanitization of the kernel input.
|
|
sections
Reviewed-by: ppedrot
|
|
|
|
|
|
|
|
projections
Reviewed-by: fajb
|
|
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
Ack-by: vbgl
|
|
|
|
Ack-by: SkySkimmer
Reviewed-by: herbelin
Reviewed-by: ppedrot
|
|
- Specialised hash and equality functions.
Avoid collisions in extreme scenarios.
- Flags to disable the use of the caches.
fixes #10772
|
|
universe unification
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
|
|
We disallow adding univ constraints wich refer to polymorphic
universes, and monomorphic constants and inductives when polymorphic
universes or constraints are present.
Every other combination is already correctly discharged by the kernel.
|
|
|
|
Reviewed-by: maximedenes
|
|
Should be 1:1 equivalent to the previous code, this is semantics preserving
factorization.
|
|
|
|
|
|
|
|
Reviewed-by: SkySkimmer
Reviewed-by: maximedenes
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
No need to keep track of it this way now that this data is part of the
kernel.
|
|
This allows to remove the double declaration of monomorphic universes of
discharged section constants. This also makes it much clearer that only
the first declaration of a constant is allowed to declare delayed
constraints.
As a nice bonus, this simplifies the Opaqueproof API.
|
|
This patch is minimalistic, insofar as it is only untying the dependency
loop between Declare and Safe_typing. Nonetheless, it is already quite
big, thus we will polish it afterwards.
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: gares
Reviewed-by: maximedenes
|
|
|
|
|
|
Due to the redundancy with some other declaration-specific data from the
kernel, we also seize the opportunity to clean it up. Note also that
discharging is still performed outside of the kernel for now.
|
|
This is not quite pretty, but it is needed by the section mechanism to rebuild
an inductive when closing a section. Hopefully this can be moved back at some
point.
|
|
For now we only keep a count of the number of open sections, discriminating
between polymorphic and monomorphic ones.
|
|
The section local universes are undoubtedly ordered, but the API was requiring
an unordered ContextSet. We also move the naming one level up.
Unfortunately, some callers are currently defining the same polymorphic
universes in a section several times, notably the "Variable" command. I had
to hack around this behaviour.
|
|
Reviewed-by: herbelin
|
|
Reviewed-by: ppedrot
|
|
intropattern entry in #10239)
Reviewed-by: ppedrot
|
|
Cf. https://docs.gitlab.com/ee/ci/yaml/#timeout.
|
