To find documentation about Ltac tactics, and to find candidates for useful Ltac tactics, the index at https://coq.inria.fr/refman/coq-tacindex.html is tremendously useful. Is there anything like that for Ltac2?

all I found so far is

Ltac2 provides over 150 API functions that provide various capabilities. These are declared with Ltac2 external in lib/coq/user-contrib/Ltac2/*.v.

which doesn't even have a hyperlink to those files. am I expected to manually dig them out of the github repo and then randomly open files in https://github.com/coq/coq/tree/master/user-contrib/Ltac2 until I find the API I need? I feel like I'm missing something.

Maybe we should build coqdoc files a la https://coq.inria.fr/doc/v8.18/stdlib/ and link to something like that? Granted this would only be a bit better, though it should come with an index

I've created https://github.com/coq/coq/issues/18116 to track this

Apparently https://coq.inria.fr/doc/v8.18/stdlib/Ltac2.Ltac2.html exists

But it's not indexed

cf https://github.com/coq/coq/issues/15617

Ralf: you're probably not missing much — Ltac2's documentation overall is far from the quality of Ltac1 documentation.

Anecdote: to find docs for Ltac2 Control.focus, I had to navigate down to the ML API tclFOCUS.

Jason Gross said:

Apparently https://coq.inria.fr/doc/v8.18/stdlib/Ltac2.Ltac2.html exists

is CSS broken or is that supposed to be not in the usual stylesheet?

it's not just not indexed, it looks like just a copy of the sourcecode, without any comments?

https://coq.inria.fr/doc/v8.18/stdlib/Ltac2.Array.html

CSS seems broken everywhere not just ltac2

ah, probably related to whatever website thing happened yesterday then

the comments missing is probably not related though

yeah there might just be no comments^^

The documentation page should probably also not show the implementation of these functions; as the user of a function I certainly don't want to reverse-engineer its behavior from the source code.

you shouldn't have to, OTOH sometimes it works. Here's my example:

```
Ltac2 @ external focus : int -> int -> (unit -> 'a) -> 'a := "coq-core.plugins.ltac2" "focus".
[...]
(** int -> int -> (unit -> 'a) -> 'a *)
let () = define3 "focus" int int closure begin fun i j tac ->
Proofview.tclFOCUS i j (thaw tac)
end
[...]
(** [tclFOCUS ?nosuchgoal i j t] applies [t] in a context where
only the goals numbered [i] to [j] are focused (the rest of the goals
is restored at the end of the tactic). If the range [i]-[j] is not
valid, then it [tclFOCUS_gen nosuchgoal i j t] is [nosuchgoal]. *)
let tclFOCUS ?nosuchgoal i j t =
```

https://github.com/coq/coq/blob/227a087cd898704eed72f395b977937c071402cc/user-contrib/Ltac2/Control.v#L30-L31

https://github.com/coq/coq/blob/227a087cd898704eed72f395b977937c071402cc/plugins/ltac2/tac2core.ml#L968-L969

https://github.com/coq/coq/blob/227a087cd898704eed72f395b977937c071402cc/engine/proofview.ml#L364-L365

Last updated: Oct 12 2024 at 13:01 UTC