coq - The formal proof system

Age	Commit message (Collapse)	Author
2021-04-09	Make critical sections safe in the presence of exceptions	Lasse Blaauwbroek
	We introduce the `with_lock` combinator that locks a mutex in an atomic fashion. This ensures that exceptions thrown by signals will not leave the system in a deadlocked state.
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2019-11-21	[coq] Untabify the whole ML codebase.	Emilio Jesus Gallego Arias
	We also remove trailing whitespace. Script used: ```bash for i in `find . -name '.ml' -or -name '.mli' -or -name '.mlg'`; do expand -i "$i" \| sponge "$i"; sed -e's/[[:space:]]$//' -i.bak "$i"; done ```
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-06-17	Update ml-style headers to new year.	Théo Zimmermann

2019-01-22	[thread] protect threads against sigalrm	Enrico Tassi
	This makes the implementation of Timeout on unix more reliable since only the main thread will receive the signal for timeout.
2018-02-27	Update headers following #6543.	Théo Zimmermann

2017-07-04	Bump year in headers.	Pierre-Marie Pédrot

2016-07-03	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵	Pierre Letouzey
	module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
2016-01-20	Update copyright headers.	Maxime Dénès

2015-01-12	Update headers.	Maxime Dénès

2014-12-17	Fix compilation with ocaml 4.0.0	Enrico Tassi

2014-12-17	WorkerPool: simpler fuctor and no more parking area	Enrico Tassi

2014-12-17	CThread: use a different type for thread friendly in_channels	Enrico Tassi

2014-11-27	WorkerPool: API to move a worker from an active pool to a parking one	Enrico Tassi
	This lets me have a pool of active workers of a fixed size, plus a parking area where workers that completed their job can stay holding their state (and eventually one can ask them to query such state afterwards).
2014-08-05	STM: new "par:" goal selector, like "all:" but in parallel	Enrico Tassi
	par: distributes the goals among a number of workers given by -async-proofs-tac-j (defaults to 2).
2014-08-05	STM: code restructured to reuse task queue for tactics	Enrico Tassi

2014-04-25	Adding a stm/ folder, as asked during last workgroup. It was essentially moving	Pierre-Marie Pédrot
	files around. A bunch of files from lib/ that were only used in the STM were moved, as well as part of toplevel/ related to the STM.