Gaëtan Gilbert (Nov 22 2021 at 14:15): Gaëtan Gilbert (Nov 22 2021 at 14:15):Why is tauto_plugin separate from ltac_plugin?
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.
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
Pierre-Marie Pédrot (Nov 22 2021 at 14:31):@Gaëtan Gilbert you could ask the same question for any plugin defining tactics
Gaëtan Gilbert (Nov 22 2021 at 14:31):actually tauto is half implemented in ltac so it's less separate than rewrite
Pierre-Marie Pédrot (Nov 22 2021 at 14:32):@Karl Palmskog IMO the whole Ltac vs. "proof language" stuff is very misleading
Pierre-Marie Pédrot (Nov 22 2021 at 14:32):all of this stuff are Ltac definitions / notations
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
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.
Pierre-Marie Pédrot (Nov 22 2021 at 14:33):which are not basic at all, anyways
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
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
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: Jun 09 2023 at 07:01 UTC