| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
|
|
|
|
|
| |
We mostly separate command line argument parsing from interpretation,
some (minor) imperative actions are still done at argument parsing
time. This tidies up the code quite a bit and allows to better follow
the complicated command line handling code.
To this effect, we group the key actions to be performed by the
toplevel into a new record type. There is still room to improve.
|
| |
|
|
|
| |
Fixes #6707, indeed, the STM was treating some errors as recoverable
thus `-quick` did succeed too often.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
We allow to provide a Coq load path at document creation time. This is
natural as the document naming process is sensible to a particular
load path, thus clarifying this API point.
The changes are minimal, as #6663 did most of the work here. The only
point of interest is that we have split the initial load path into two
components:
- a ML-only load path that is used to locate "plugable" toplevels.
- the normal loadpath that includes `theories` and `user-contrib`,
command line options, etc...
|
| |
|
|
|
|
|
| |
Refinement of the toplevel codepath requires to be more careful about
the conditions for coqtop to be interactive.
Fixes #6691. We also tweak the vio auxiliary function.
|
| |
|
|
|
|
|
|
| |
We gather (almost) all the STM options in a record, now set at
document creation time.
This is refactoring is convenient for some other ongoing
functionalization work.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
We refactor top-level load path handling. This is in preparation to
make load paths become local to a particular document.
To this effect, we introduce a new data type `coq_path` that includes
the full specification of a load path:
```
type add_ml = AddNoML | AddTopML | AddRecML
type vo_path_spec = {
unix_path : string; (* Filesystem path contaning vo/ml files *)
coq_path : Names.DirPath.t; (* Coq prefix for the path *)
implicit : bool; (* [implicit = true] avoids having to qualify with [coq_path] *)
has_ml : add_ml; (* If [has_ml] is true, the directory will also be search for plugins *)
}
type coq_path_spec =
| VoPath of vo_path_spec
| MlPath of string
type coq_path = {
path_spec: coq_path_spec;
recursive: bool;
}
```
Then, initialization of load paths is split into building a list of
load paths and actually making them effective. A future commit will
make thus the list of load paths a parameter for document creation.
This API is necessarily internal [for now] thus I don't think a
changes entry is needed.
|
| |
|
|
| |
One less global flag.
|
| |\ |
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
We move the main async flags to the STM in preparation for
more state encapsulation.
There is still more work to do, in particular we should make some of
the defaults a parameter instead of a flag.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
We remove coqmktop in favor of a couple of simple makefile rules using
ocamlfind. In order to do that, we introduce a new top-level file that
calls the coqtop main entry.
This is very convenient in order to use other builds systems such as
`ocamlbuild` or `jbuilder`.
An additional consideration is that we must perform a side-effect on
init depending on whether we have an OCaml toplevel available [byte]
or not. We do that by using two different object files, one for the
bytecode version other for the native one, but we may want to review
our choice.
We also perform some smaller cleanups taking profit from ocamlfind.
|
| |/ /
| |
| |
| |
| | |
New module introduced in OCaml 4.05 I think, can create problems when
linking with the OCaml toplevel for `Drop`.
|
| |/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The patch has three parts:
- Introduction of a configure flag `-bytecode-compiler (yes|no)`
(due to static initialization this is a configure-time option)
- Installing the hooks that register the VM with the pretyper and the
kernel conditionally on the flag.
- Replacing the normalization function in `Redexpr` by compute if the
VM is disabled.
We also rename `Coq_config.no_native_compiler` to `native_compiler`
and `Flags.native_compiler` to `output_native_objects` [see #4607].
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
We'd like to handle proofs functionally we thus recommend not to use
printing functions without an explicit context.
We also adapt most of the code, making more explicit where the
printing environment is coming from.
An open task is to refactor some code so we gradually make the
`Pfedit.get_current_context ()` disappear.
|
| |/
|
|
|
|
|
|
| |
This setting is a debug assertion, due to the many flags we still
over-approximate setting the flag to true to all interactive
environments. [So the assert is checked in vo compilation]
Fixes #6152.
|
| |
|
|
|
|
| |
After `Drop`, `Coqtop.drop_last_doc` will contain the current document
used by `Coqloop`. This is useful for people wanting to restart Coq
after a `Drop`.
|
| |\ |
|
| | |
| |
| |
| |
| | |
Julien Narboux confirmed that it was dead code (GeoProof is not to be
confused with GeoCoq).
|
| |/
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |\ |
|
| |\ \ |
|
| | | | |
|
| | |/ |
|
| |/
|
|
|
|
|
|
|
|
|
| |
An incoming commit is removing some toplevel-specific global flags in
favor of local toplevel state; this commit flags `Flags` use so it
becomes clearer in the code whether we are relying on some "global"
settable status in code.
A good candidate for further cleanup is the pattern:
`Flags.if_verbose Feedback.msg_info`
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| | |
This is a second try at removing the hooks for the legacy xml export
system which can't currently be tested.
It is also not included in the API, so it should either be included in
it or this PR be applied.
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
`G_vernac` was depending on `toplevel` just for parsing the compat
number information. IMHO this was not the right place, so I have moved
the parsing bits to parsing and updated the files.
This allows to finally separate the `toplevel` from Coq, which avoids
linking it in alternative toplevels.
|
| | |/
|/|
| |
| | |
Minor clean up, no sense in having these as they do nothing.
|
| |\ \
| | |
| | |
| | | |
flag is set.
|
| | | | |
|
| | |/
|/| |
|
| |/
|
|
|
|
| |
Calling it only when there is something to profile, or when profiling
is explicitly required with the profile flags, so that profiling in
plugins is possible.
|
| |
|
|
|
|
|
|
| |
This is usable for no-color terminal.
For instance, a typical application in mind is the Coq-generate names
marker which can be rendered with a color if the interface supports it
and a prefix "~" if the interface does not support colors.
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
versions.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Plugin-writers can now use:
-bypass-API
parameter with "coq_makefile".
The effect of that is that instead of
-I API
the plugin will be compiled with:
-I config" -I dev -I lib -I kernel -I library -I engine -I pretyping -I interp -I parsing -I proofs -I tactics -I toplevel -I printing -I intf -I grammar -I ide -I stm -I vernac
|
| |
|
|
|
| |
We remove the emacs-specific printing code from the core of Coq, now
`-emacs` is a printing flag controlled by the toplevel.
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
This is the continuation of #244, we now deprecate `CErrors.error`,
the single entry point in Coq is `user_err`.
The rationale is to allow for easier grepping, and to ease a future
cleanup of error messages. In particular, we would like to
systematically classify all error messages raised by Coq and be sure
they are properly documented.
We restore the two functions removed in #244 to improve compatibility,
but mark them deprecated.
|
| |\ |
|
| |\ \ |
|
| |\ \ \ |
|
| | |/ / |
|
Emilio Jesus Gallego Arias
Maxime Dénès
Guillaume Melquiond
Hugo Herbelin
Pierre-Marie Pédrot
Matej Košík
Enrico Tassi