| Age | Commit message (Collapse) | Author |
|---|
|
|
|
The definition of Vernacexpr.VernacDeclareTacticDefinition was changed.
The original definition allowed us to represent non-sensical value such as:
VernacDeclareTacticDefinition(Qualid ..., false, ...)
The new definition prevents that.
|
|
command is mapped.
|
|
Originally, "VernacTime" and "VernacRedirect" were defined like this:
type vernac_expr =
...
| VernacTime of vernac_list
| VernacRedirect of string * vernac_list
...
where
type vernac_list = located_vernac_expr list
Currently, that list always contained one and only one element.
So I propose changing the definition of these two variants in the following way:
| VernacTime of located_vernac_expr
| VernacRedirect of string * located_vernac_expr
which covers all our current needs and enforces the invariant
related to the number of commands that are part of the
"VernacTime" and "VernacRedirect" variants.
|
|
Actually, we never mix the various uses of each dynamic type created through
the Dyn module. To enforce this statically, we functorize the Dyn module so
that we recover a fresh instance at each use point.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
The "master" label used to be reset to the wrong id
|
|
|
|
|
|
involving Futures.
|
|
universes are declared correctly in the enclosing proofs evar_map's.
|
|
|
|
Side effects are now an opaque data type, called private_constant, you can
only obtain from safe_typing. When add_constant is called on a
definition_entry that contains private constants, they are either
- inlined in the main proof term but not re-checked
- declared globally without re-checking them
As a safety measure, the opaque data type contains a pointer to the
revstruct (an internal field of safe_env that changes every time a new
constant is added), and such pointer is compared with the current value
store in safe_env when the private_constant is inlined. Only when the
comparison is successful the private_constant is not re-checked. Otherwise
else it is. In short, we accept into the kernel private constant only
when they arrive in the very same order and on top of the very same env
they arrived when we fist checked them.
Note: private_constants produced by workers never pass the safety
measure (the revstruct pointer is an Ephemeron). Sending back the
entire revstruct is possible but: 1. we lack a way to quickly compare
two revstructs, 2. it can be large.
|
|
|
|
|
|
|
|
|
|
failing for unresolved evars (regression).
|
|
|
|
The splines=ortho option seems to make dot crash sometimes, so this commit
removes it from the STM debugging output
|
|
|
|
|
|
PIDEtop needs these to implement its new transaction mechanism
|
|
This lets hooks treat different exceptions in different ways; in
particular, user interrupts can now be safely ignored
|
|
|
|
We artificially restrict the syntax though, because it is unclear of
what the semantics of several axioms in a row is, in particular about the
resolution of remaining evars.
|
|
- "Proof using p*" means: use p and any section var about p.
- Simplify the grammar/parser for proof using <expression>.
- Section variables with a body (let-in) are pulled in automatically
since they are safe to be used (add no extra quantification)
- automatic clear of "unused" section variables made optional:
Set Proof Using Clear Unused.
since clearing section hypotheses does not "always work" (e.g. hint
databases are not really cleaned)
- term_typing: trigger a "suggest proof using" message also for Let
theorems.
|
|
According to http://caml.inria.fr/mantis/view.php?id=5325
you can't use the same socket for both writing and reading.
The result is lockups (may be fixed in 4.03).
|
|
|
|
|
|
|
|
|
|
Allowing universes to be instantiated if the body of the proof
requires it (the levels stay flexible). Not allowed for non-polymorphic
cases, to be compatible with the stm's invariant that the type should
not change.
|
|
- When there are side effects which might enrich the initial universes
of a proof, keep the initial and refined universe contexts apart like
for delayed proofs, ensuring universes are declared before they are
used in the right order.
- Fix undefined levels in proof statements so that they can't be lowered
to Set by a subsequent, delayed proof.
|
|
|
|
The single remaining use is in library/states.ml. This use should be
reviewed, as it is most certainly broken.
The other uses of Loadpath.get_paths did not disappear by miracle though.
They were replaced by a new function Loadpath.locate_file which factors
all the uses of the function. This function should not be used as it is as
broken as Loadpath.get_paths, by definition.
Vernac.load_vernac now takes a complete path rather than looking up for
the file. That is the way it was used most of the time, so the lookup was
unnecessary. For instance, Vernac.compile was calling Library.start_library
which already expected a complete path.
Another consequence is that System.find_file_in_path is almost no longer
used (except for Loadpath.locate_file, obviously). The two remaining uses
are System.intern_state (used by States.intern_state, cf above) and
Mltop.dir_ml_load for dynamically loading compiled .ml files.
|
|
The evar counter has been moved from Evarutil to Evd, and all functions in
Evarutil now go through a dedicated primitive to create a fresh evar from
an evarmap.
|
|
|
|
|
|
|
|
... lemmas and inductives to control which universes are bound and where
in universe polymorphic definitions. Names stay outside the kernel.
|
|
|
|
|
|
In PIDE based UIs queries can be delegated too, hence to speed up
things I was saving a shallow state. Unfortunately a shallow state
breaks section/modules commands, and a query can be the last entry
of a section/module. (A shallow state does essentially drop the libstack).
The easy solution is to save a complete state.
A better one would be to refine the static analysis of the document and
decide which kind of saved state one needs.
|
|
|
