coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	STM: code refactoring	Enrico Tassi	2014-11-03
\| \| \| \| \|	This is mainly shuffling code around and removing internal refs that are not needed anymore.
*	Feedback message: hold extra info to help routing	Enrico Tassi	2014-10-31
\| \| \| \| \|	PIDE based GUIs can take advantage of multiple panels and get some feedback routed there. E.g. query panel
*	STM: new worker for queries	Enrico Tassi	2014-10-31
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	With the options -async-queries-always-delegate queries are always delegated to a worker process (Eval, Check, ...). Users of PIDE based UIs (in Denmark) reported that the current behavior of processing query synchronously is rather unexpected when one is used to get proofs processed asynchronously. Non instantaneous queries are part of many scripts and are there as "tests" for testing the execution of recursive functions. A standard proof script shape in an ongoing work by Appel and Bengtson is made of blocks like: - recursive function definition, - some tests, - some proofs And one cannot quickly jump over the tests (only the proofs). Enclosing the queries into dummy proofs to recover a reactive UI is just annoying. Hence this patch. Currently CoqIDE is not able to integrate the asynchronous feedback of the query workers into the document, hence if one passes the option to CoqIDE one only gets a boolean out of queries (processed/error).
*	STM: primitives to snapshot a .vi while in interactive mode	Enrico Tassi	2014-10-13
\|
*	library/opaqueTables: enable their use in interactive mode	Enrico Tassi	2014-10-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	Before this patch opaque tables were only growing, making them unusable in interactive mode (leak on Undo). With this patch the opaque tables are functional and part of the env. I.e. a constant_body can point to the proof term in 2 ways: 1) directly (before the constant is discharged) 2) indirectly, via an int, that is mapped by the opaque table to the proof term. This is now consistent in batch/interactive mode This is step 0 to make an interactive coqtop able to dump a .vo/.vi
*	XML pretty printing for AST (work by François Poulain, project DoCoq)	Enrico Tassi	2014-09-29
\| \| \| \|	It is not 100% complete, but the main part is there.
*	STM: new "par:" goal selector, like "all:" but in parallel	Enrico Tassi	2014-08-05
\| \| \| \| \|	par: distributes the goals among a number of workers given by -async-proofs-tac-j (defaults to 2).
*	STM: code restructured to reuse task queue for tactics	Enrico Tassi	2014-08-05
\|
*	STM: VtQuery holds the id of the state it refers to	Carst Tankink	2014-08-04
\|
*	STM: add optionally takes the id of the new tip	Enrico Tassi	2014-07-11
\|
*	STM: export the observe function (useful for pide)	Enrico Tassi	2014-07-11
\|
*	all coqide specific files moved into ide/	Enrico Tassi	2014-06-25
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	lib/interface split into: - lib/feedback subscribe-based feedback bus (also used by coqidetop) - ide/interface definition of coqide protocol messages lib/pp structured info/err/warn messages lib/serialize split into: - lib/serialize generic xml serialization (list, pairs, int, loc, ...) used by coqide but potentially useful to other interfaces - ide/xmlprotocol serialization of protocol messages as in ide/interface the only drawback is that coqidetop needs -thread and I had to pass that option to all files in ide/
*	Adding a stm/ folder, as asked during last workgroup. It was essentially moving	Pierre-Marie Pédrot	2014-04-25
	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.