Ralf Jung (Oct 02 2023 at 15:45): Ralf Jung (Oct 02 2023 at 15:45):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?
Ralf Jung (Oct 02 2023 at 15:48):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.
Jason Gross (Oct 02 2023 at 20:59):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
Jason Gross (Oct 02 2023 at 21:03):I've created https://github.com/coq/coq/issues/18116 to track this
Jason Gross (Oct 02 2023 at 22:29):Apparently https://coq.inria.fr/doc/v8.18/stdlib/Ltac2.Ltac2.html exists
Jason Gross (Oct 02 2023 at 22:29):But it's not indexed
Jason Gross (Oct 02 2023 at 22:31):cf https://github.com/coq/coq/issues/15617
Paolo Giarrusso (Oct 03 2023 at 02:20):Ralf: you're probably not missing much — Ltac2's documentation overall is far from the quality of Ltac1 documentation.
Paolo Giarrusso (Oct 03 2023 at 02:21):Anecdote: to find docs for Ltac2 Control.focus, I had to navigate down to the ML API tclFOCUS.
Ralf Jung (Oct 03 2023 at 07:40):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?
Ralf Jung (Oct 03 2023 at 07:41):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
Gaëtan Gilbert (Oct 03 2023 at 07:41):CSS seems broken everywhere not just ltac2
Ralf Jung (Oct 03 2023 at 07:42):ah, probably related to whatever website thing happened yesterday then
Gaëtan Gilbert (Oct 03 2023 at 07:42):the comments missing is probably not related though
Ralf Jung (Oct 03 2023 at 07:44):yeah there might just be no comments^^
Ralf Jung (Oct 03 2023 at 07:44):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.
Paolo Giarrusso (Oct 03 2023 at 08:43):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