coq - The formal proof system

Age	Commit message (Collapse)	Author
2019-02-01	[toplevel] Split interactive toplevel and compiler binaries.	Emilio Jesus Gallego Arias
	We make `coqc` a truly standalone binary, whereas `coqtop` is restricted to interactive use. Thus, `coqtop -compile` will emit a warning and call `coqc`. We have also refactored `Coqargs` into a common `Coqargs` module and a compilation-specific module `Coqcargs`. This solves problems related to `coqc` having its own argument parsing, and reduces the number of strange argument combinations a lot.
2018-11-24	[toplevel] Allow to specify default options.	Emilio Jesus Gallego Arias
	In some cases, toplevel ML clients may want to modify the default set of flags that is passed to the main initalization routine. This is for example useful for `idetop` to suppress some undesired printing at startup. I would say that clients ought to have more control, but I do expect that PRs such as #8690 will help providing a better separation thus a mode orthogonal API.
2018-05-21	[stm] Make toplevels standalone executables.	Emilio Jesus Gallego Arias
	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.