confusing error on incorrect _CoqProject file

[gasche]

The error

I have an incorrect _CoqProject file with the following content:

-R Category

When running Emacs+PG on a .v file in the same directory, the "Next step" or "Use buffer" commands error with an obscure message:

Bad bounding indices: 0, 2

Repro script:

$ mkdir repro
$ cd repro
$ echo "-R Foo" > _CoqProject
$ echo "Check true." > test.v
$ emacs test.v

Versions:

• Emacs: 28.3
• PG 20230414.931 from Elpa

(I observed the failure on older versions before, but I tried to make the issue go away by upgrading.)

How I traced the error to the _CoqProject

I googled "Bad bounding indices", there were no hits whatsoever on the Coq resources, but some Github issues on some totally unrelated Emacs modes that were related to the cl-subseq function.

I then grepped the PG sources, there is a single use of cl-subseq:

PG/coq/coq-system.el

Lines 550 to 559 in e7aad1d

	(defun coq--read-one-option-from-project-file (switch arity raw-args)
	"Cons SWITCH with ARITY arguments from RAW-ARGS.
	If ARITY is nil, return SWITCH."
	(if arity
	(let ((arguments
	(condition-case-unless-debug nil
	(cl-subseq raw-args 0 arity)
	(warn "Invalid _CoqProject: not enough arguments for %S" switch))))
	(cons switch arguments))
	switch))

It looks like the code is trying to be robust against failures, but for some reason (maybe the unless-debug part?) this attempt fails on my machine and PG is unusable with broken _CoqProject files -- with a very obscure error message.