coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2019-07-08	Usage: bypassing a useless detour via a reference.	Hugo Herbelin

2019-07-08	An even more uniform treatment of the -help option across executables.	Hugo Herbelin
	Incidentally fix some missing newline in coqc help, and give proper help for coqidetop and the "coq*worker"s.
2019-07-08	Some common points between coqc and other coq binaries.	Hugo Herbelin
	- Binding coqc execution to the generic support for Coq binaries (i.e. to start_coq). - Moving init_toploop to the init part of coq executables so that coqc can avoid to call it. By the way, it is unclear what workerloop should do with it. Also, it is unclear how much the -l option should be considered an coqidetop or coq*worker option. In any case, it should be disallowed in coqc, I guess? - Moving the custom init part at the end of the initialization phase. Seems ok, despites the few involved side effects.
2019-07-08	Passing command-line option async_proofs_worker_priority functionally.	Hugo Herbelin
	We lose track of it at some time in "known_state" and assume that the reference cur_opt has not been modified in between the time it was set (in "new_doc") and "known_state".
2019-07-08	An attempt to reorganize further coqtop initialization into semantic units.	Hugo Herbelin
	Incidentally moving parsing of "-batch" to the coqtop binary.
2019-07-08	Adding methods help and parse_extra to custom toplevels data.	Hugo Herbelin
	In particular, method init does not do parsing any more. This allows for instance to let coqidetop treats itself the "-filteropts" option.
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann

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.