coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	[spawn] don't create a control socket on Unix (Fix #7713)	Enrico Tassi	2018-06-15
\|
*	Fix #5983 (many frequent AppVeyor failures) by increasing spawn timeout.	Théo Zimmermann	2018-05-24
\|
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|
*	Fix FIXME: use OCaml 4.02 generative functors when available.	Gaëtan Gilbert	2017-11-01
\| \| \| \|	4.02.3 has been the minimal OCaml version for a while now.
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\|
*	Drop '.' from CErrors.anomaly, insert it in args	Jason Gross	2017-06-02
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	As per https://github.com/coq/coq/pull/716#issuecomment-305140839 Partially using ```bash git grep --name-only 'anomaly\s$~label:"[^"]"\s$\?$Pp.$\?($\(Pp.$\?str\)\?\s".[^\.!]")' \| xargs sed s'/$anomaly\s\(~label:"[^"]"\s$\?$Pp.$\?($\(Pp.$\?str\)\?\s".\s[^\.! ]\)\s")/\1.")/g' -i ``` and ```bash git grep --name-only ' !"' \| xargs sed s'/ !"/!"/g' -i ``` The rest were manually edited by looking at the results of ```bash git grep anomaly \| grep '\.ml' \| grep -v 'anomaly\s$~label:"[^"]"\s$\?$Pp\.$\?($\(Pp.$\?str\)\?\s".*$\.\\|!$")' \| grep 'anomaly$$\\|[^_]$' \| less ```
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵	Pierre Letouzey	2016-07-03
\| \| \| \| \| \|	module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
*	Removing dead code and unused opens.	Pierre-Marie Pédrot	2016-05-08
\|
*	Win: kill unreliable hence do not waitpid after kill -9 (Close #4369)	Enrico Tassi	2016-03-09
\| \| \| \|	This commit also completes 74bd95d10b9f4cccb4bd5b855786c444492b201b
*	Update copyright headers.	Maxime Dénès	2016-01-20
\|
*	spawn: fix leak of file descriptors	Enrico Tassi	2015-12-17
\| \| \| \| \| \|	The interesting manifestation of the bug was Unix.select returning no error but the empty list of descriptors, as if a timeout did happen.
*	Spawn: use each socket exclusively for writing or reading	Enrico Tassi	2015-10-08
\| \| \| \| \| \|	According to http://caml.inria.fr/mantis/view.php?id=5325 you can't use the same socket for both writing and reading. The result is lockups (may be fixed in 4.03).
*	Update headers.	Maxime Dénès	2015-01-12
\|
*	Inlining Spawn.kill_if in the one place were it was actually used, thus	Pierre-Marie Pédrot	2014-12-25
\| \| \| \|	removing the need of thread creation in the interface.
*	Spawn: fix request of Gc statistics	Enrico Tassi	2014-12-17
\|
*	Removing handshake from Spawn. It used marshalling, which is bad for	Pierre-Marie Pédrot	2014-04-09
\| \| \| \|	non-ML applications. Control channel can be also ignored.
*	Relaunch all Unix.waitpid when they ended with EINTR	Pierre Letouzey	2014-01-30
\| \| \| \|	Moreover, cleanup of System.connect (used by the "external" tactic).
*	Spawn: managed processes	Enrico Tassi	2014-01-26
	The Spawn and Spawned modules factor the operation of spawning a process. Both synchronous and asynchronous channels are supported. Both threaded and glib like main loop models are supported. Still, not all combinations are truly tested not equipped with a decent API: only async + glib and sync + thread are, since these are the models we use for coqide<->coqtop and coqtop<->worker respectively.