2026-10-10  Michael Herstine  <sp1ff@pobox.com>

	Cut release 0.0.9.

	Hygienic commit.
	Update copyrights; make a small addition to the README.

2026-10-10  rvs314  <71688932+rvs314@users.noreply.github.com>
	    Claude Opus 5.5 (1M context)  <noreply@anthropic.com>
	    Michael Herstine  <sp1ff@pobox.com>

	Support Rocq 9 (#3)
	* Support Rocq 9, and strip the welcome message in sessions.

	This commit updates ob-coq for Rocq 9 and fixes a related bug:

	    1) `ob-coq--strip-welcome' now recognizes Rocq 9's banner
	       ("Welcome to Rocq 9.2"), which uses a different name and a
	       two-part version number
	    2) the welcome message is now stripped for every new process,
	       not only for blocks without a `:session'; previously the first
	       result in a named session began with the banner (this also
	       affected Coq 8, but was masked once any session-less block had
	       run, since the hook is added globally)

	The tests are updated accordingly: the ZArith block in the corpus
	silences Rocq 9's deprecation warning for the unqualified `Require',
	`ob-coq-tests-issue-2' accepts both `%Z_scope' and `%_Z_scope', and
	the new `ob-coq-tests-session-welcome' covers the session fix.

	To use Rocq 9 without the coqtop compatibility package, set
	`inf-coq-program-name' to "rocq" and `inf-coq-program-args' to
	("repl").

	Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

	* Document how to run ob-coq with Rocq 9.

	Rocq 9 doesn't install `coqtop' unless the `coq-core' compatibility
	package is also installed, so the default `inf-coq-program-name'
	fails. The README now says how to use `rocq repl' instead.

	Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

	* Minor change to ob-coq-tests-blog-post to make it more robust

	---------

2025-06-12  Michael Herstine  <sp1ff@pobox.com>

	Cut release 0.0.8.
	This is a hygienic release that:

	    - bumps the version number
	    - updates the copyrights throughout
	    - updates the INSTALL file

2025-06-12  Michael Herstine  <sp1ff@pobox.com>

	Updating copyrights & INSTALL

2024-06-18  Michael Herstine  <sp1ff@pobox.com>

	Cutting 0.0.7

2024-06-18  Michael Herstine  <sp1ff@pobox.com>

	Add the options to coalesce blank lines & elide informational lines.
	This commit adds two new options governing the output of
	`inf-coq-send-string':

	    1) `inf-coq-coalesce-blank-lines': if set to t, multiple blank
	       lines will be coalesced into one
	    2) `inf-coq-elide-informational-lines': if set to t, remove
	       lines that appear to be informational (such as
	       "[Loading ML file ring_plugin.cmxs (using legacy method)
	       ... done]"

2024-06-18  Michael Herstine  <sp1ff@pobox.com>

	Cutting 0.0.6

2024-06-18  Michael Herstine  <sp1ff@pobox.com>

	Change the way in which complete input is detected.
	This commit once again changes the way in which `info-coq-send-string'
	detects that output from the most recent text block has completed. It
	now counts the number of newlines ('\n') in the input, and expects an
	equal number of prompt instances back from the coqtop process.

	In a breach of the "one commit per concern" rule of thumb, I've
	also added some supporting scripts and the first Github action for
	this repo.

2024-04-30  Michael Herstine  <sp1ff@pobox.com>

	Cutting release 0.0.5

2024-04-30  Michael Herstine  <sp1ff@pobox.com>

	Fix `inf-coq-prompt-regexp'.
	Prior to this patch, `inf-coq-prompt-regexp' began with "\\b", which
	matches the empty string at the start of a word. This regrettably
	would match any line with a '>' character in it, causing the output
	of Coq evaluation to be extremely confusing.

	This patch changes the "\\b" to "^", meaning that the text must
	begin at the start of the line. `coqtop` seems to indent intermediate
	output, perhaps for this very reason.

2024-04-16  Michael Herstine  <sp1ff@pobox.com>

	Cut release 0.0.4

2024-04-16  Michael Herstine  <sp1ff@pobox.com>

	Change the default value for `inf-coq-prompt-regexp'...
	This patch will take care of two small housekeeping items:

	    - update the default setting for `inf-coq-prompt-regexp' to
	      better conform to the Coq documents
	    - have `inf-coq-run-coq', when called interactively, pop
	      the new comint buffer to the foreground

2024-04-16  Michael Herstine  <sp1ff@pobox.com>

	Revamp the algorithm for detecting output is complete.
	This patch changes the way in which `info-coq-send-string' detects
	that output from the most recent text block has completed. It now
	counts the number of periods ('.') in the input, and expects an
	equal number of prompt instances back from the coqtop process.

2024-04-15  Michael Herstine  <sp1ff@pobox.com>

	Cutting build 0.0.3

2024-04-15  Michael Herstine  <sp1ff@pobox.com>

	[#1] Stop `inf-coq-quit' from prompting.
	When `kill-buffer' is invoked, the hook `kill-buffer-query-functions'
	is run. By default, one function in that hook is
	`process-kill-buffer-query-function' which will, if the buffer has
	an active process, prompt "Buffer NAME has a running process; kill
	it?".

	This patch short-circuits that by setting the coqtop process'
	"query-on-exit-flag" to nil before killing the `inf-coq' comint
	buffer.

2024-04-09  Michael Herstine  <sp1ff@pobox.com>

	Cutting release 0.0.2

2024-04-09  Michael Herstine  <sp1ff@pobox.com>

	Update `inf-coq-prompt-regexp'.
	This commit does a few things:

	    - Update `inf-coq-prompt-regexp' to reflect that the `coqtop`
	      prompt changes (during proofs, e.g.)
	    - Add an upper limit on the number of times `inf-coq-send-string`
	      will poll the process for output (to prevent infinite loops)
	    - Add an Emacs package to the build

	Also, the source is now linted using:

	    - checkdoc
	    - package-lint

	This commit also contains naming & docstring changes prompted by the
	linters.

2024-04-04  Michael Herstine  <sp1ff@pobox.com>

	Initial commit of ob-coq.
	ob-coq provides Org Babel evaluation support for Coq.
