| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
We turn coqtop "plugins" into standalone executables, which will be
installed in `COQBIN` and located using the standard `PATH`
mechanism. Using dynamic linking for `coqtop` customization didn't
make a lot of sense, given that only one of such "plugins" could be
loaded at a time. This cleans up some code and solves two problems:
- `coqtop` needing to locate plugins,
- dependency issues as plugins in `stm` depended on files in `toplevel`.
In order to implement this, we do some minor cleanup of the toplevel
API, making it functional, and implement uniform build rules. In
particular:
- `stm` and `toplevel` have become library-only directories,
- a new directory, `topbin`, contains the new executables,
- 4 new binaries have been introduced, for coqide and the stm.
- we provide a common and cleaned up way to locate toplevels.
|
| |
|
|
|
|
|
|
|
|
| |
This was a silly bug introduced in
675a1dc401eb9a5540ba5bc9a522c1f84d4c3d54 that forgot to properly
forward the command line option.
Thanks to @SkySkimmer for finding out the problem.
closes #7447
|
| |
|
|
|
|
|
|
|
|
| |
The five phases are command line interpretation, initialization,
prelude loading, rcfile loading, and sentence interpretation (only the
two latters are located).
We then parameterize the feedback handler with the given execution
phase, so as to possibly annotate the message with information
pertaining to the phase.
|
| |
|
|
|
|
| |
Done by simplifying the three "try" liable to be caught at
initialization time into one and by ensuring that the remaining one
reports about being in initialization phase.
|
| |\ |
|
| | | |
|
| |/
|
|
|
| |
Toplevels may want to modify for example the Stm flags,
which after #1108 are handled in a functional way.
|
| |
|
|
|
|
|
|
|
|
| |
The toplevel refactoring made path initialization per document,
however vio-checking and vio-tasks are not documents, so loadpath must
be initialized individually.
Patch by @gares, refactoring to avoid double-initialization by me.
Co-authored-by: <Enrico.Tassi@inria.fr>
|
| |
|
|
|
|
| |
This is a first step towards moving REPL-specific commands out of the
core layers. In particular, we remove `Quit` and `Drop` from the core
vernacular to specific toplevel-level parsing rules.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
Since 3fc02bb2034a ("[pp] Move terminal-specific tagging to the
toplevel."), the COQ_COLORS environment variable has been ignored,
since init_terminal_output unconditionally called init_tag_map with
the default colors, overwriting any custom colors that had been
previously set. Fix this by creating a separate function,
default_styles, to set the default colors.
Also, remove the clear_styles function, as it was only called in one
place and did nothing (since tag_map is empty to begin with).
|
| |\ |
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
`Drop` is implemented using exceptions-as-control flow, so the
toplevel state gets corrupted as `do_vernac` will never return when
`Drop` occurs in the input.
The right fix would be to remove `Drop` from the vernacular and make
it a toplevel-only command, but meanwhile we can just patch the state
in the exception handler.
We also need to keep the global state in `Coqloop` as the main
`coqtop` entry point won't be called by `go ()`.
Fixes #6872.
|
| |/ /
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
We first load the file, then we print it as a post-processing
step. This is both more flexible and clearer.
We also refactor the comments handling to minimize the logic that is
living in the Lexer. Indeed, the main API is now living in the
printer, and complex interactions with the state are not possible
anymore, including the removal of messing with low-level summary and
state setting!
|
| |/ |
|
| |
|
|
|
|
| |
We organize the toplevel execution as a record and pass it
around. This will be used by future PRs as to for example decouple
goal printing from the classifier.
|
| | |
|
| |
|
|
|
|
|
|
|
|
| |
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.
|
Emilio Jesus Gallego Arias
Hugo Herbelin
Enrico Tassi
Thomas Hebb
Maxime Dénès
Théo Zimmermann
Guillaume Melquiond