coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	[stm] Make toplevels standalone executables.	Emilio Jesus Gallego Arias	2018-05-21
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	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.
*	[build] Simpler byte/opt toplevel build.	Emilio Jesus Gallego Arias	2018-03-05
\| \| \| \| \| \| \| \| \|	Instead of playing static linking games, we just ship two different top-level files depending on whether we want to enable `Drop` support [bytecode case] or not. The savings of the old approach [1 line of code] were not worth the complexities of the linking hack.
*	[build] Remove coqmktop in favor of ocamlfind.	Emilio Jesus Gallego Arias	2017-12-10
	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.