coqdoc -Q foo "" fails with invalid_argument

[tom-p-reichel]

Description of the problem

I am using Coqdoc in perhaps an unintended manner: building documentation for entire switches at once with long, automatically generated lists of -Q bindings and vfiles. It would be difficult to provide a reproducible example of my current issue and I haven't identified any clear minimal example.

In 2022, a small change was made to coqdoc (commit 662baba) that replaced usage of a standard library function Arg.Rest_All with what the author of the diff referred to as a "hack" that should be replaced as soon as the version of the ocaml standard library used alongside Coq was sufficiently updated.

git bisect indicates that this commit is where all the trouble started-- my tool can't use versions of Coqdoc past this commit because when fed my very long, automatically generated argument list, it immediately produces a Fatal error: exception Invalid_argument("index out of bounds").

Have we updated to a version of the ocaml standard library that allows this change to be reverted? If so, here is a patch that returns to the old behavior.

diff --git a/tools/coqdoc/cmdArgs.ml b/tools/coqdoc/cmdArgs.ml
index e829f43050..b7ebaf0d8e 100644
--- a/tools/coqdoc/cmdArgs.ml
+++ b/tools/coqdoc/cmdArgs.ml
@@ -69,22 +69,14 @@ let arg_set f = Arg.Unit (fun () -> prefs := f !prefs)
 let arg_string f = Arg.String (fun s -> prefs := f !prefs s)
 let arg_file f = Arg.String (fun s -> FileUtil.check_if_file_exists s; prefs := f !prefs s)
 let arg_int f = Arg.Int (fun d -> prefs := f !prefs d)
-
-(* TODO: replace these hacks with Arg.Rest_all, when coq moves to a newer version of OCaml stdlib *)
-let arg_path f = Arg.String (fun s ->
-  if Array.length Sys.argv < !Arg.current + 3 ||
-    Sys.argv.(!Arg.current + 2).[0] = '-' then
-    raise (Arg.Bad ("Two arguments expected: <dir> and <name>"))
-  else
-    Arg.current := !Arg.current + 1;
-    prefs := f !prefs (normalize_path s, Sys.argv.(!Arg.current + 1)))
-let arg_url_path f = Arg.String (fun s ->
-  if Array.length Sys.argv < !Arg.current + 3 ||
-    Sys.argv.(!Arg.current + 2).[0] = '-' then
-    raise (Arg.Bad ("Two arguments expected: <url> and <path>"))
-  else
-    Arg.current := !Arg.current + 1;
-    f s Sys.argv.(!Arg.current + 1))
+let arg_path f = Arg.Rest_all (fun l ->
+  match l with
+  | dir :: name :: [] -> prefs := f !prefs (normalize_path dir, name)
+  | _ -> raise (Arg.Bad ("Two arguments expected: <dir> and <name>")))
+let arg_url_path f = Arg.Rest_all (fun l ->
+  match l with
+  | url :: path :: [] -> f path url
+  | _ -> raise (Arg.Bad ("Two arguments expected: <url> and <path>")))
 
 let args_options = Arg.align [
   "--html", arg_set (fun p -> { p with targetlang = HTML }),

I have checked that on the current main branch of Coq this diff can be applied and corrects the bug I'm observing, but only that.

Small Coq file to reproduce the bug

N/A

Version of Coq where this bug occurs

commit 662baba onwards (8.18)

Last version of Coq where the bug did not occur

before commit 662baba

[SkySkimmer]

Please provide a way to reproduce the error eg as an attached file of the generated arguments.

Have we updated to a version of the ocaml standard library that allows this change to be reverted?

We're on 4.09 and AFAICT Rest_all is 4.12 so no.

[SkySkimmer]

@tom-p-reichel

Please provide a way to reproduce the error eg as an attached file of the generated arguments.

ping

[tom-p-reichel]

I felt bad about potentially uploading a 68 kilobyte file so I resolved to come up with an actual minimal example: this seems to be happening because of blank "root" logical paths. This is a minimal example:

coqdoc -Q "asdf" ""

results in

Fatal error: exception Invalid_argument("index out of bounds")

but this does not happen in Coqdoc 8.16.1, which appears to correctly generate a file which is mapped under the root logical directory when given these kinds of arguments. In some libraries (UniCoq, relation-algebra, mtac2), the test-suite or examples are assigned to be under the root logical path (according to their glob files). This means that their physical directory indeed ought to be mapped to logical path "".

Although, I'm not sure if "" was supposed to work in the first place. According to some documentation I found once but can no longer find, giving "<>" is a definitely supported way of referring to the root directory, which still seems to work in Coq 8.18. Checking for this on my end and giving "<>" when "" is the logical path seems to be a functioning workaround for me.

[SkySkimmer]

#19036