Stream: Ltac2

Topic: ✔ What to do instead of semicolons?


view this post on Zulip Ignat Insarov (Oct 01 2021 at 16:09):

How to fix this?

Ltac simplify_everything := simpl; simpl in *.
Fail Ltac2 simplify_everything := simpl; simpl in *.

Tactic definition must be a syntactical value

Semicolon composition is the most basic way to wield Ltac, and now it is forbidden?

(Taken from this thread.)

view this post on Zulip Pierre-Marie Pédrot (Oct 01 2021 at 21:09):

Please read the documentation.

view this post on Zulip Ignat Insarov (Oct 02 2021 at 06:50):

I asked for a tiny bit of help. At least you could have pointed me to a specific section. This document is long and technical. I am not going to be able to assimilate it as a whole any time soon.

view this post on Zulip Ignat Insarov (Oct 02 2021 at 07:22):

To be honest, your answer soured my morning big way.

view this post on Zulip Enrico Tassi (Oct 02 2021 at 07:55):

Ltac2 is a different language, with a different syntax and semantics. You can't transliterate ltac1 code.

view this post on Zulip Ignat Insarov (Oct 02 2021 at 08:01):

I did read some of that long and technical reference. It says:

There are various alternatives to Ltac1, such as Mtac or Rtac for instance. While those alternatives can be quite different from Ltac1, we designed Ltac2 to be as close as reasonably possible to Ltac1, while fixing the aforementioned defects.

This affirms my understanding that Ltac2 is not that different. Not by design.

view this post on Zulip Ignat Insarov (Oct 02 2021 at 08:05):

I also translated some simple pieces of Ltac and confirmed for myself that it mostly works out of the box. That is to say, one can easily transliterate a significant subset of Ltac to Ltac2.

view this post on Zulip Ignat Insarov (Oct 02 2021 at 08:08):

You can make an argument that anyone who wishes to wield Coq must be comfortable with learning a language from a formal grammar and semantics alone, and that such questions that can be answered through inference from reference are off topic. (This is what Pierre-Marie seems to imply.) If such is the consensus of the community, then I of course shall never more ask such questions. I shall simply go away and never return.

view this post on Zulip Ignat Insarov (Oct 02 2021 at 08:10):

I completely understand if a community of experts wishes to set a high barrier to entry. This is only fair. My problem is that I do not see a banner stating that such a barrier is indeed in place.

view this post on Zulip Ignat Insarov (Oct 02 2021 at 08:14):

You could also argue that Ltac2 is an especially advanced topic that Pierre-Marie is working on for his own ends. Then again a banner is missing. Why is it in Coq main line if the expert community does not wish others try it out?

view this post on Zulip Théo Winterhalter (Oct 02 2021 at 08:20):

I think you can think of it as something experimental. It already provides useful conveniences for people that need them, but as the manual says, it's quite not ready for everyday use (at least that's what I make of it).
But this kind of project can only evolve in the right direction if people are using it.

I think you probably should use LTac1 for the time being unless you are prepared to spend the time learning it in the current rough state, or in case you need something very specific that only LTac2 provides.

view this post on Zulip Ignat Insarov (Oct 02 2021 at 08:28):

I am prepared to spend the rest of my life doing computer-assisted formal proof. However I am not prepared to being sent to please read the long and technical reference when I am asking a simple question that anyone would ask upon seeing this small example:

Ltac2 tactic_with_argument useless_value := pose (true := true); pose (true := true).
Fail Ltac2 tactic_without_argument := pose (true := true); pose (true := true).

view this post on Zulip Ignat Insarov (Oct 02 2021 at 08:28):

Does it take a whole reference to explain this simple issue?

view this post on Zulip Gaëtan Gilbert (Oct 02 2021 at 08:31):

Ltac2 definitions need to be thunked https://coq.inria.fr/refman/proof-engine/ltac2.html#tactic-delay

Ltac foo := blah.

becomes

Ltac2 foo () := blah.

view this post on Zulip Ignat Insarov (Oct 02 2021 at 08:32):

This is an answer I accept!

view this post on Zulip Ignat Insarov (Oct 02 2021 at 08:33):

The «why» remains but at least the reference acknowledges the problem.

view this post on Zulip Ignat Insarov (Oct 02 2021 at 08:41):

I am still not sure if everyone secretly hates me and only Pierre-Marie is brave enough to say it straight, but whatever.

view this post on Zulip Notification Bot (Oct 02 2021 at 08:41):

Ignat Insarov has marked this topic as resolved.

view this post on Zulip Théo Winterhalter (Oct 02 2021 at 08:53):

Ignat Insarov said:

I am still not sure if everyone secretly hates me and only Pierre-Marie is brave enough to say it straight, but whatever.

I don't think so. I personally couldn't answer because I don't know.

view this post on Zulip Théo Zimmermann (Oct 02 2021 at 11:26):

Ignat Insarov said:

The «why» remains but at least the reference acknowledges the problem.

I've only seen this thread now but I've answered about the "why" in: https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/.E2.9C.94.20What.20is.20Ltac2.20and.20should.20I.20care.3F/near/255863590

view this post on Zulip Théo Zimmermann (Oct 02 2021 at 11:37):

Ignat Insarov said:

I am still not sure if everyone secretly hates me and only Pierre-Marie is brave enough to say it straight, but whatever.

This was reported to me (by someone outside the discussion) as a code of conduct violation. I personally wouldn't qualify this sentence like this, but I am still going to remind you of some basic rule to follow when discussing on forums like these: do not assume bad faith or bad intentions of other actors.

That being said, I do get the frustration of being answered something that amounts to "RTFM" without the offensive word. So @Pierre-Marie Pédrot, I suggest that you be more "friendly and patient" (to quote our code of conduct) or that you simply avoid answering. I do personally answer all the time to basic questions with links to the specific part of the documentation that is relevant. That's the best way to encourage people to actually read the documentation.

view this post on Zulip Enrico Tassi (Oct 02 2021 at 11:42):

If you read the thread carefully you will find some resistance to read the doc in the first place. And this is not a call center either.

view this post on Zulip Ignat Insarov (Oct 02 2021 at 11:59):

@Théo Zimmermann Thanks, I always appreciate when communication problems on my side are pointed out. However, you are reading in what is not there: I am not assuming anything. I am literally saying «not sure». The hypothesis that Pierre-Marie wants me to go away is not falsified by evidence — indeed you affirm its plausibility in the same message.

view this post on Zulip Théo Zimmermann (Oct 02 2021 at 12:00):

@Ignat Insarov What I mean is that you should completely avoid this kind of sentences. If you felt that people were aggressive toward you, you should report the behavior instead of writing this.

view this post on Zulip Ignat Insarov (Oct 02 2021 at 12:01):

I truly do not wish to be a nuisance. So the best Pierre-Marie could do at this time is to message me privately and tell me that I should leave. I am prepared to go away forever if this happens.

@Théo Zimmermann   I see, well this is fair.

view this post on Zulip Ignat Insarov (Oct 02 2021 at 12:01):

@Enrico Tassi   I do not see why you are saying this. Actually I am nearly in tears already.

view this post on Zulip Ignat Insarov (Oct 02 2021 at 12:02):

I deeply respect how such well learned people take their time to answer my most trivial questions. It is really hard and frustrating for me to move forward in my study of Coq. I am doing my best to be respectful.

view this post on Zulip Ignat Insarov (Oct 02 2021 at 12:03):

I also read so much that my eyes hurt every day.

view this post on Zulip Théo Zimmermann (Oct 02 2021 at 12:03):

Enrico Tassi said:

If you read the thread carefully you will find some resistance to read the doc in the first place. And this is not a call center either.

I agree that entitled users who want to have all the answers without making any efforts are annoying (I'm saying that in all generality, having no idea if that applies to the situation). But the solution to that is not a blunt "Read the documentation" message that can sound as pretty aggressive. Being patient and welcoming means doing efforts beyond that. And not answering is also a solution in case one does not want to make that kind of effort.

view this post on Zulip Ignat Insarov (Oct 02 2021 at 12:03):

I am really very sad by how this all turned out.

view this post on Zulip Théo Zimmermann (Oct 02 2021 at 12:05):

Communication on the internet is pretty hard. But do not take what anyone said too harshly. I'm pretty sure nobody wishes that you leave. Just if everyone could make an effort to sound less aggressive that would be good.

view this post on Zulip Théo Zimmermann (Oct 02 2021 at 12:06):

And once again, there is a difference between perceived aggressiveness and actual aggressiveness. Messages do often feel aggressive just because their author did not put enough care in writing them.

view this post on Zulip Paolo Giarrusso (Oct 02 2021 at 12:08):

@Ignat Insarov You're certainly not alone in being frustrated by the documentation. Keep in mind that writing good docs is a full-time job that takes tons of time.

view this post on Zulip Enrico Tassi (Oct 02 2021 at 12:08):

After all @Pierre-Marie Pédrot wrote the doc, which is a very boring and time consuming task. If it is not good enough, we can surely improve it. But we need feedback on it: the doc is a way to factor the effort here in helping users, we can't possibly answer all questions forever.

view this post on Zulip Paolo Giarrusso (Oct 02 2021 at 12:11):

@Enrico Tassi I'll rephrase the feedback as follows: that is a reference manual, hence linking it is _inappropriate_ in the situation.

view this post on Zulip Enrico Tassi (Oct 02 2021 at 12:14):

What would be better? A pointer to the section with the syntax? Or a completely different document, eg. a tutorial about Lta1 -> Ltac2 transition?

view this post on Zulip Ignat Insarov (Oct 02 2021 at 12:14):

There is this idea that there are 4 kinds of documentation. If it is to be believed, writing explanations into the reference is actually a wrong thing to do — those who need them would not be able to find them, and those who already understand and merely want to recall would be annoyed.

view this post on Zulip Gaëtan Gilbert (Oct 02 2021 at 12:15):

the refman should probably quote the error message so that it can be searched for, otherwise one needs almost to already know about it to connect it with the "tactic delay" section

view this post on Zulip Paolo Giarrusso (Oct 02 2021 at 12:15):

@Enrico Tassi Some kind of tutorial would certainly be better

view this post on Zulip Paolo Giarrusso (Oct 02 2021 at 12:15):

for instance, ssreflect's has multiple tutorials which are certainly helpful!

view this post on Zulip Paolo Giarrusso (Oct 02 2021 at 12:18):

FWIW, I don't mean to be entitled: nobody, not even the Coq devs, have a duty to write docs, to answer questions, _or_ to keep Ltac1 around (deprecation is being discussed these days). Except if you want to encourage users.

view this post on Zulip Théo Zimmermann (Oct 02 2021 at 12:18):

Ignat Insarov said:

There is this idea that there are 4 kinds of documentation. If it is to be believed, writing explanations into the reference is actually a wrong thing to do — those who need them would not be able to find them, and those who already understand and merely want to recall would be annoyed.

I'm aware of this and indeed, the Coq documentation might sometimes be wrong in interleaving everything together. On the other hand, it's a lot of work to rewrite everything. Getting the documentation to be more accurate is already a very time consuming task.

view this post on Zulip Karl Palmskog (Oct 02 2021 at 12:19):

Paolo Giarrusso said:

FWIW, I don't mean to be entitled: nobody, not even the Coq devs, have a duty to write docs, to answer questions, _or_ to keep Ltac1 around (deprecation is being discussed these days). Except if you want to encourage users.

well, you can pay people to assume that duty: https://coq.inria.fr/consortium

view this post on Zulip Théo Zimmermann (Oct 02 2021 at 12:20):

Indeed, though that brings us to the question of making it easier to accept small donations. Which was raised again by @Enrico Tassi this week.

view this post on Zulip Enrico Tassi (Oct 02 2021 at 12:36):

Ignat Insarov said:

There is this idea that there are 4 kinds of documentation. If it is to be believed, writing explanations into the reference is actually a wrong thing to do — those who need them would not be able to find them, and those who already understand and merely want to recall would be annoyed.

Thanks for the link, I'm only half way but I'm really linking it. Id added a dimension to my understanding of how to write doc!


Last updated: Jan 31 2023 at 09:01 UTC