| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
Users need to be careful wrt global state modification outside
`Vernacentries` without registering the functions.
In particular, our fail implementation also has to invalidate the cache.
|
|
We make Vernacentries.interp functional wrt state, and thus remove
state-handling from `Future`. Now, a future needs a closure if it
wants to preserve state.
Consequently, `Vernacentries.interp` takes a state, and returns the
new one.
We don't explicitly thread the state in the STM yet, instead, we
recover the state that was used before and pass it explicitly to
`interp`.
I have tested the commit with the files in interactive, but we aware
that some new bugs may appear or old ones be made more apparent.
However, I am confident that this step will improve our understanding
of bugs.
In some cases, we perform a bit more summary wrapping/unwrapping. This
will go away in future commits; informal timings for a full make:
- master:
real 2m11,027s
user 8m30,904s
sys 1m0,000s
- no_futures:
real 2m8,474s
user 8m34,380s
sys 0m59,156s
|
|
We still don't thread the state there, but this is a start of the
needed infrastructure.
|
|
We interpret meta-commands directly, instead of going by an
intermediate "classifier step".
The code could still use some further refactoring, in particular, the
`part_of_script` bit is a bit strange likely coming from some special
treatment of `VtMeta` in the `query` call, and should go away.
|
|
The vernacular classifier has a current special case for "Undo" like
commands, as it needs access to the document structure in order to
produce the proper "VtBack" classification, however the classifier is
defined before the document is.
We introduce a new delegation status `VtMeta` that allows us to
interpreted such commands outside the classifier itself.
|
|
|
|
|
|
|
|
The test suite cases are preserved until the feature is actually removed.
|
|
|
|
This adds back `$(MKDIR) $(FULLCOQLIB)/toploop`, which was lost between
8.6 and 8.7.
|
|
|
|
STM (BZ#5556)
|
|
|
|
directory` on every execution
|
|
Julien Narboux confirmed that it was dead code (GeoProof is not to be
confused with GeoCoq).
|
|
structure.
|
|
execution
|
|
We move delicate library/module instillation code to the STM so the
API guarantees that the first state snapshot is correct. That was not
the case in the past, which meant that the STM cache was unsound in
batch mode, however we never used its contents due to not backtracking
to the first state.
This provides quite an improvement in the API, however more work is
needed until the codepath is fully polished.
This is a critical step towards handling the STM functionally.
|
|
|
|
With suggest proof using out of the kernel the format of context_used
in .aux is just the list of ids wanted by get_hint_ctx.
(split x s when x doesn't appear in s just returns the singleton list [s])
|
|
|
|
|
|
|
|
We place `Proof_using` in the proper place [`vernac`] and we remove
gross parsing hacks.
The new placement should allow to use the printers and more convenient
structure, and reduce strange coupling between parsing and internal
representation.
|
|
Also add an output test for Suggest Proof Using.
This changes the .aux output: instead of getting a key
>context_used "$hyps;$suggest"
where $hyps is a list of the used hypotheses and $suggest is the
;-separated suggestions (or the empty string if Suggest Proof Using is
unset), there is a key
>context_used "$hyps"
and if Suggest Proof Using is set also a key
>suggest_proof_using "$suggest"
For instance instead of
112 116 context_used "B A;A B;All"
we get
112 116 context_used "B A"
112 116 suggest_proof_using "A B;All"
|
|
|
|
|
|
|
|
|
|
|
|
The test was abandoned at the time of merging subdirectory browsing
between coqdep and coqtop, and to limit at the same time the
dependency of coqdep in files such as unicode.cmo.
But checking ident validity speeds up browsing in arbitrary directory
structure and we restore it for this reason.
(One could also say that browsing arbitrary directory structures is
not intended, but in practice this may happen, as e.g. reported in
BZ#5734.)
|
|
|
|
|
|
|
|
|
|
|
|
This seems a safe choice as of today, but more advanced users would
like to tweak it, or we could even refine it by a configure option if
desired.
|
|
We add a new option to configure `-flambda-opts` to allow passing
custom flags to flambda. Example:
```
./configure -flambda-opts "-O3 -unbox-closures"
```
|
|
|
|
Morphism` forms.
|
|
|
|
|
|
|
|
|
|
|
