Stream: Coq devs & plugin devs

Topic: tauto plugin


view this post on Zulip Gaëtan Gilbert (Nov 22 2021 at 14:15):

Why is tauto_plugin separate from ltac_plugin?

view this post on Zulip Karl Palmskog (Nov 22 2021 at 14:22):

I thought tauto was considered a general tactic not tied to Ltac? At least this was what I thought meant sense to say in the draft of the planned user survey.

view this post on Zulip Gaëtan Gilbert (Nov 22 2021 at 14:31):

it's mentioned in the survey?
I would say tauto is about as separate from ltac as rewrite, but rewrite is in ltac_plugin

view this post on Zulip Pierre-Marie Pédrot (Nov 22 2021 at 14:31):

@Gaëtan Gilbert you could ask the same question for any plugin defining tactics

view this post on Zulip Gaëtan Gilbert (Nov 22 2021 at 14:31):

actually tauto is half implemented in ltac so it's less separate than rewrite

view this post on Zulip Pierre-Marie Pédrot (Nov 22 2021 at 14:32):

@Karl Palmskog IMO the whole Ltac vs. "proof language" stuff is very misleading

view this post on Zulip Pierre-Marie Pédrot (Nov 22 2021 at 14:32):

all of this stuff are Ltac definitions / notations

view this post on Zulip Pierre-Marie Pédrot (Nov 22 2021 at 14:33):

I think it's a historical accident that we keep insisting so much on Ltac being the glue around the basic proof primitives

view this post on Zulip Karl Palmskog (Nov 22 2021 at 14:33):

in the manual, I don't think the presentation of Micromega and "Logic/equality tactics" is fundamentally different. It's basically some magic words you use to solve goals in different contexts.

view this post on Zulip Pierre-Marie Pédrot (Nov 22 2021 at 14:33):

which are not basic at all, anyways

view this post on Zulip Karl Palmskog (Nov 22 2021 at 14:35):

should users really (have to) care about whether some domain-specific automation is implemented in Ltac or OCaml? My assumption has been that they normally shouldn't

view this post on Zulip Pierre-Marie Pédrot (Nov 22 2021 at 14:58):

They shouldn't indeed. But the current discussion is mostly about OCaml code organization, so it's irrelevant for the end user

view this post on Zulip Karl Palmskog (Nov 22 2021 at 15:05):

OK, still valuable to know that the tie between tauto-ltac is so tight, so if one wants to got Ltac2-only one will have to skip tauto and friends...


Last updated: Mar 28 2024 at 15:01 UTC