| Age | Commit message (Collapse) | Author |
|---|
|
|
|
This adds back `$(MKDIR) $(FULLCOQLIB)/toploop`, which was lost between
8.6 and 8.7.
|
|
|
|
STM (BZ#5556)
|
|
directory` on every execution
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
More dependencies / linking fixes.
|
|
|
|
printing-ony Notations
|
|
|
|
IS is intended for testing nullity.
|
|
Fixes BZ#5779
|
|
This reverts commit 587e556a909fcd2e1507a9230d9cdaffa3f9394e from PR #1024.
This commit did not solve any issue at the time it was merged but made the
macOS package we produce compatible only with macOS 10.12 and later.
|
|
Specifically since e88dfedd99a84e9e375f3583be6fd1de3de36c72.
There seem to have been no actual errors due to this, only ocaml
complaining about missing .cmi files.
|
|
This overlay is now useless (change pushed upstream in bignums) and
moreover does not contain my commit making bignums resilient to PR#768.
|
|
|
|
We make the Stm API functional over an opaque `doc` type. This allows
to have a much better picture of what the toplevel is doing; now
almost all users of STM private data are marked by typing.
For now only, the API is functional; a PR switching the internals
should come soon thou; however we must first fix some initialization
bugs.
Due to some users, we modify `feedback` internally to include a
"document id" field; we don't expose this change in the IDE protocol
yet.
|
|
We move toplevel/STM flags from `Flags` to their proper components;
this ensures that low-level code doesn't depend on them, which was
incorrect and source of many problems wrt the interfaces.
Lower-level components should not be aware whether they are running in
batch or interactive mode, but instead provide a functional interface.
In particular:
== Added flags ==
- `Safe_typing.allow_delayed_constants`
Allow delayed constants in the kernel.
- `Flags.record_aux_file`
Output `Proof using` information from the kernel.
- `System.trust_file_cache`
Assume that the file system won't change during our run.
== Deleted flags ==
- `Flags.compilation_mode`
- `Flags.batch_mode`
Additionally, we modify the STM entry point and `coqtop` to account
for the needed state. Note that testing may be necessary and the
number of combinations possible exceeds what the test-suite / regular
use does.
The next step is to fix the initialization problems [c.f. Bugzilla],
which will require a larger rework of the STM interface.
|
|
We remove `init_library_roots` as there is no point in resetting this
internal variable. Its only user is `init_load_path` and this function
is not meant (and is not) idempotent now.
|
|
|
