| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
| |
This has no effect anymore, verbose printing is controlled now by
the regular, common `quiet` flag.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
| |
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.
|
| |\ |
|
| |\ \ |
|
| | | | |
|
| | | | |
|
| | | | |
|
| |/ /
| |
| |
| | |
Bug introduced by 675a1dc401eb9a5540ba5bc9a522c1f84d4c3d54
|
| |/ |
|
|
|
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.
|
Emilio Jesus Gallego Arias
Hugo Herbelin
Maxime Dénès
Théo Zimmermann
Gaëtan Gilbert
Jasper Hugunin