Ignat Insarov (Oct 01 2021 at 16:09): 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?
Pierre-Marie Pédrot (Oct 01 2021 at 21:09):Please read the documentation.
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.
Ignat Insarov (Oct 02 2021 at 07:22):To be honest, your answer soured my morning big way.
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.
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.
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.
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.
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.
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?
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.
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).
Does it take a whole reference to explain this simple issue?
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.
This is an answer I accept!
Ignat Insarov (Oct 02 2021 at 08:33):The «why» remains but at least the reference acknowledges the problem.
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.
Notification Bot (Oct 02 2021 at 08:41):Ignat Insarov has marked this topic as resolved.
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.
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
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.
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.
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.
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.
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.
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.
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.
Ignat Insarov (Oct 02 2021 at 12:03):I also read so much that my eyes hurt every day.
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.
Ignat Insarov (Oct 02 2021 at 12:03):I am really very sad by how this all turned out.
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.
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.
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.
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.
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.
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?
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.
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
Paolo Giarrusso (Oct 02 2021 at 12:15):@Enrico Tassi Some kind of tutorial would certainly be better
Paolo Giarrusso (Oct 02 2021 at 12:15):for instance, ssreflect's has multiple tutorials which are certainly helpful!
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.
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.
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
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.
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: Apr 16 2024 at 06:01 UTC