Typos and comments in "The Tactic Language"

[jfehrle]

(upon my first reading ever; I've not used Ltac.)

Starting at https://coq.inria.fr/distrib/current/refman/proof-engine/ltac.html#syntax.

• As shown by the figure, tactical \|\| binds more than the prefix tacticals try, repeat, do and abstract

no backslashes

• Local application of tactics

The text for the main example (The expressions expri are evaluated to vi, for i=0,…,n and all have to be tactics.) seems like it doesn't apply to all the variants, eg it doesn't apply to Variant [> expr .. ]. The indentation of the variants suggests otherwise.

• If no tactic is given for the i-th goal, it behaves as if the tactic idtac were given. For instance, [> | auto] is a shortcut for [> idtac | auto ]

I don't understand the indexing. It looks to me like v0 is idtac and v1 is auto. Shouldn't this diagram require an initial | to match the grammar? Furthermore, the grammar doesn't seem to permit [> idtac | auto ].

• In this variant, token:expr is used for each goal coming after those covered by the first list of expr but before those coevered by the last list of expr.

How about using expr1, expr2 and expr3 in the diagram? Then the text is shorter and easier to understand since you don't need "the first list of" and "the last list of".

• but before those coevered by the last list of

covered

• In this variant, token:expr is used for each goal

Seems like token is meant as a formatting instruction.

• Variant [> expr .. ]

I don't see .. in the grammar. The Gallina lexical conventions only mention that it is a token. Nor does it seem to be a typo for .... This is in used several places right here. Or should the grammar have .. on its second and third lines? But it seems like ... just means repetition in the grammar. Perhaps ... for repetition could be rendered a little differently in the grammar?

• if there are no goal, the tactic is not run at all

goals

• This variant of local tactic application is paired with a sequence. In this variant, there must be as many expr in the list as goals generated by the application of the first expr to each of the individual goals independently.

Simpler to say "expr1 is applied to each of the goals independently, then each of the expr2 is applied to the list of goals generated by expr1. The number of expr2 must be the same as the number of goals generated by expr1."

• toplevel_selector : expr

doesn't appear in the grammar. I expected expr was the start symbol for this portion of the grammar (or at least the only thing in this portion that's referenced by the part of the overall grammar not shown in this section). Maybe need another symbol at the top of the grammar with ::= expr | toplevel_selector : expr | selector : expr?

• Goal selectors

For readability, I think the order of descriptions should closely match the order of productions in the grammar. The previous section "Local application of tactics" is at the top of the grammer, which "Goal selectors" is at the botom. There are other examples, hope someone will check the entire section on this point.

• For loop

There is no "for" construct, how about calling this a "do loop" or just a loop?

• do num expr

The ident form is not described.

• Variant num-num+, : expr

The grammar appears to require parentheses. Which is right?

• Error No such goal

Huh?

• Supposing num > 1, after the first application of v, v is applied, at least once, to the generated subgoals and so on.

Hard to understand. Also, need a description for the natural form.

• "do (natural | ident) tacexpr3"

I think "(" and ")" should be "[" and "]" but they appear to be metacharacters, not literals. And "|" is a metacharacter here whereas elsewhere it is a literal character. The "(natural | ident)" appears twice places in the grammar, maybe define it a production.

• Variant first expr and Variant solve expr

Not in the grammar.

• | fresh | fresh string | fresh qualid (in the grammar)

I think these are 3 separate productions in the grammar. It's confusing to overload the "|" to mean grammatical alternatives in some places and the literal character in others.

• | fail [natural] [message_token ... message_token] (in the grammar)

Here "[" is used as a metacharacter whereas it is a literal in "| expr ; [ expr | ... | expr ]" Confusing.

• Variant gfail

gfail is not mentioned in the grammar

• time string expr and The string argument is optional.

Need [ ] around "string" in the first quote

• time_constr expr

time_constr is not in the grammar

• | let [rec] let_clause with ... with let_clause in atom (grammar)

looks incorrect (with ... with??) and doesn't match the syntax in "Local definitions". Probably need a new way to mark repetitions.

• fun ident+ => expr

atom or "( expr )", etc.

OK, I stopped at "Applications" Surely more grammar stuff to fix up.

[jfehrle]

Here's the rest:

• The reference qualid must be bound to some defined tactic definition expecting at least as many arguments as the provided tacarg. The expressions expri are evaluated to vi, for i=1,…,n.

Could you explain what an application is? "expri" doesn't appear in the syntax diagram "qualid tacarg+"

• The syntax of cpattern is the same as that of terms, but it is extended with pattern matching metavariables.

How about a hyperlink for cpattern such as in Pattern matching on terms? Maybe add a comment in the main grammar adjacent to "term". And add a hyperlink for atomic_tactic, which appears not to be mentioned anywhere else in the document (or maybe remove it?). The hyperlinks for "natural" and "term" just above the quoted text jumps to the ssreflect chapter when it should go to the gallina chaper.

• The matching is non-linear: if a metavariable occurs more than once, it should match the same expression every time.

Is this the definition of non-linear matching? I've seen the term but not a definition, seems like that should appear in the documentation somewhere.

• The expression expr is evaluated ...

The first two paragraphs here are very dense and much of them seems like advanced details compared to paragraphs 3-5. Maybe start with a simple statement about matching and move the more advanced details down a bit. Matching is clearly very central to Ltac. Most every ltac user will want to read it multiple times. It deserves a clear and full explanation, perhaps with more example.

• Alternatively, when a metavariable of the form ?id occurs under binders

How about a hyperlink for "binder"? Looking elsewhere in the document, I find one in https://coq.inria.fr/distrib/current/refman/language/gallina-extensions.html?highlight=binder that leads to the SSReflect chapter. If it's also used in Ltac, it should be explained in a more-general section of the doc such as the Gallina chapter.

• Using multimatch instead of match will allow subsequent tactics to backtrack into a right-hand side tactic which has backtracking points left and trigger the selection of a new matching branch when all the backtracking points of the right-hand side have been consumed.

Ah, sounds sort of sensible but the details are pretty unclear. Would be better if it was not just one very long sentence. "subsequent tactics" means subsequent patterns within the match construct, right? I don't get the part about consuming backtracking points. Where is the concept of a backtracking point introduced? I can guess what's intended, but it would be a lot better to define it somewhere and list it in the index. Of course, I've seen little conceptual material in the doc so far (still a lot for me to read).

• Using lazymatch instead of match will perform the same pattern matching procedure but will commit to the first matching branch rather than trying a new matching if the right-hand side fails.

Probably could leave out "will perform the same pattern matching procedure" Start with the main difference in lazymatch: "will commit to the first matching branch rather than trying a new matching if the right-hand side fails."

• Local definitions (jumping back in the text)

What are scopes and scoping rules for a "local" definition? Please briefly contrast to how you create global definitions. (And isn't there some kind of module feature, too? How does that interact with both of these.)

• Variant context ident [cpattern]

After 10 minutes of examination, still pretty unclear on what this does and why it would be used. Is seems the example is recursive. It would help a lot to give a sentence or three explaining how the example works--it may make perfect sense if you already know the feature. It seems the use of 3+4 is to show how it won't match on the 4, and that the idtac is printing X as it recurs.

• match goal with hyp+ |- cpattern => expr+| | _ => expr end

Use expr1 and expr2. The text already uses expr1; change the other reference to expr2.

Also, this pattern doesn't cover all the possible context_rule productions in the grammar.

• The order of matching is the following: hypothesis patterns are examined from the right to the left (i.e. hypi,mi before hypi,1).`

maybe just "first to last" since the patterns may on separate lines. Also, I can't make sense of the parenthetical comment; it's more complicated than sentence it's trying to elaborate on.

• Computing in a constr https://coq.inria.fr/distrib/current/refman/proof-engine/tactics.html#coq:tacn.hnf only gives an example of what "hnf" is not: Example: The term forall n:nat, (plus (S n) (S n)) is not reduced by hnf.

• by the idtac tacticals 4.2 at the right possition in the script

position Also, is "4.2" intended to be a hyperlink? It doesn't go anywhere interesting.

• tactic local total calls max

Any way to get the columns to line up in the example? Maybe it had tab characters?

[Zimmi48]

Thank you for opening this issue. It is very interesting to get feedback from a user who discovers Ltac through the manual (and very rare to get such kind of feedback because people are usually less confident about opening issues when they are beginning). However, in the current state your feedback is hard to address because it contains so many items. In order to reduce the number of items to address, it would help if you could open a PR with your suggestions of modifications when you have some (for instance typos or rewording where you have a proposal, and then edit this message to remove the corresponding items). Then there is also the mixing between problems originating from the Sphinx migration (e.g. hard-coded reference "4.2") and problems whose origin is older than that (bad formulation, unclear example). To check if an error comes from the Sphinx migration or was there before, a good strategy can be to have a look at the previous version of the manual https://coq.inria.fr/distrib/V8.7.2/refman/ltac.html. In the case of the hard-coded reference, the "4.2" was a "9.2" there and it pointed the definition of idtac. Fixing this just means removing the "4.2" and using:

:tacn:`idtac`

in the text to have idtac clickable. (See also the doc of the Sphinx manual at https://github.com/coq/coq/tree/master/doc/sphinx#documenting-coq-with-sphinx.)

The text for the main example (The expressions expri are evaluated to vi, for i=0,…,n and all have to be tactics.) seems like it doesn't apply to all the variants, eg it doesn't apply to Variant [> expr .. ]. The indentation of the variants suggests otherwise.

We've tried to systematically indent variants (so that one can clearly see of what it is a variant, but indeed the first paragraph is generally a description of the tactic / tactical / command above and not of all the variants below). Maybe this was a bad strategy? This should anyways be discussed in a separate issue because this is a much more general question.

I don't understand the indexing. It looks to me like v0 is idtac and v1 is auto. Shouldn't this diagram require an initial | to match the grammar?

There is indeed an inconsistency in "The expressions expri are evaluated to vi, for i=0,...,n and all have to be tactics. The vi is applied to the i-th goal, for =1,...,n. It fails if the number of focused goals is not exactly n." In both case, i should start at 1. However, this is again an artifact of the migration (see the original there https://coq.inria.fr/distrib/V8.7.2/refman/ltac.html#sec469). In the new version, it would make sense not to talk about these ranges.

Furthermore, the grammar doesn't seem to permit [> idtac | auto ].

It actually does. The | character is a separator. However, the current presentation is incomplete because it doesn't include the case of now tactic being passed so it should actually be:

tacn:: [> {*, {? @expr } } ]

(Notice the additional {? which makes the inner expression optional.)

How about using expr1, expr2 and expr3 in the diagram? Then the text is shorter and easier to understand since you don't need "the first list of" and "the last list of".

That's not really supported at the current time but it would be interesting to open an issue to discuss this missing feature. Indeed, it could often come in handy.

Seems like token is meant as a formatting instruction.

Indeed, an initial : is missing before token.

I don't see .. in the grammar. The Gallina lexical conventions only mention that it is a token. Nor does it seem to be a typo for .... This is in used several places right here. Or should the grammar have .. on its second and third lines? But it seems like ... just means repetition in the grammar. Perhaps ... for repetition could be rendered a little differently in the grammar?

I agree with this remark. The three-dot character … is used in some places in the manual and could be used more frequently in place of ..., in particular in this grammar. This could help.

toplevel_selector : expr doesn't appear in the grammar. I expected expr was the start symbol for this portion of the grammar (or at least the only thing in this portion that's referenced by the part of the overall grammar not shown in this section). Maybe need another symbol at the top of the grammar with ::= expr | toplevel_selector : expr | selector : expr?

Yes, these are full tactic sentences. An extension of the sentence symbol described here https://coq.inria.fr/refman/language/gallina-specification-language.html#the-vernacular. I don't know what to do about this. I think discussing all the grammars present in the manual would deserve its own issue.

do num expr The ident form is not described.

I just discovered its existence. It can be used like this:

Goal True.
let n := 10 in do n idtac.

The grammar appears to require parentheses. Which is right?

Again, there is a confusion in the use of parentheses in the grammar: in this case, it is a way of showing the various options, like in do (natural | ident) tacexpr3 and the symbol ( is not used. Probably a question to discuss in this specific issue on grammars in the manual...

Error No such goal

This could use a description indeed. At the present time a lot of errors in the manual are listed without being properly documented. Here, an example where you can see this error is Goal True. 2: idtac.

Also, need a description for the natural form.

Using natural sometimes and num sometimes was (AFAICT) an inconsistency which has already been fixed in most places but probably not in the grammar. So everywhere there is still natural, it should become num.

looks incorrect (with ... with??) and doesn't match the syntax in "Local definitions". Probably need a new way to mark repetitions.

Actually, this is the way of marking repetitions with separators, see https://coq.inria.fr/refman/language/gallina-specification-language.html#about-the-grammars-in-the-manual.

How about a hyperlink for "binder"? Looking elsewhere in the document, I find one in https://coq.inria.fr/distrib/current/refman/language/gallina-extensions.html?highlight=binder that leads to the SSReflect chapter. If it's also used in Ltac, it should be explained in a more-general section of the doc such as the Gallina chapter.

There should be an hyperlink if it had been written like this:

:token:`binders`

Regarding the reference to the SSReflect chapter, see this bug report: #7432

[jfehrle]

Indeed, a myriad of details.

I've been told that improving the documentation is currently a priority. When I'm at the CIW next week, I'd like to understand the plan and if/how my comments may fit into that.

Are there already designated owners/reviewers for each part of the Sphinx doc? Are there instructions on how to run Sphinx locally to review the output (in particular, on Windows)?

Then there is also the mixing between problems originating from the Sphinx migration (e.g. hard-coded reference "4.2") and problems whose origin is older than that (bad formulation, unclear example).

Why does the distinction matter?

[Zimmi48]

I've been told that improving the documentation is currently a priority. When I'm at the CIW next week, I'd like to understand the plan and if/how my comments may fit into that.

The "plan" is not well fully known, but improvements are possible even before we get one.

Are there already designated owners/reviewers for each part of the Sphinx doc?

Because of the recent migration, the main owner is currently @maximedenes for the full thing because he supervised the migration. But when the main Sphinx migration artifacts have been fixed, we should switch to a component-based maintainer model. In the meantime we can still request reviews from competent people such as @ppedrot, @herbelin and @JasonGross on the Ltac topic.

  Are there instructions on how to run Sphinx locally to review the output (in particular, on Windows)?

You can find the dependencies in INSTALL.doc. The target is make sphinx. The Sphinx docs should be pretty cross-platform (since this is Python-based). Report any problem you have on Windows.

Why does the distinction matter?

Because the competent people won't be the same if the question is about the format or about the contents.

[jfehrle]

It might be interesting to see how often each page of the documentation is accessed. It would be intesting to see how many people use it and what sections get the most hits. Of course, it depends on whether Inria's webserver keeps such statistics.

[Zimmi48]

It is on a server administrated from within the development team and I doubt that such statistics are collected. Though maybe there are log files this kind of info can be extracted from.

[jfehrle]

How do I set up the required packages for Sphinx for Windows? I'm looking at INSTALL.doc.

• Any python 3 is OK?
• How do I install

  - latex (latex2e)
  - pdflatex
  - dvips
  - makeindex

which don't obviously correspond to anything in

pip3 install sphinx sphinx_rtd_theme beautifulsoup4 antlr4-python3-runtime pexpect sphinxcontrib-bibtex

Are they part of sphinxcontrib-bibtex? (Oh I guess they're all binaries to be installed independently.)

[Zimmi48]

You don't need any of these packages if you only compile Sphinx and not the full documentation. Only the python3 ones (and yes, any minor version should probably be OK, but I'm not fully sure).

[jfehrle]

Regarding INSTALL.doc:

• The file name is uninformative, particularly since it's in the toplevel coq directory in the tree. Seems to me it should be in the doc/sphinx directory, maybe with a different name, and
• Do we really want to have Microsoft Word docs in the source tree? Shouldn't it be an .md file or a text file?

[jfehrle]

Also unclear what's the difference between make doc-html and 'make sphinx'.

[jfehrle]

OK, it appears that's it's my GUI (IntelliJ) that looks at the .doc suffix and decides it must be a Word file. Trying to figure out if I can turn that off. It also affects Makefile.doc.

[Zimmi48]

I agree these .doc extensions are quite unfortunate. In the case of INSTALL.doc we could solve this issue by turning the file into a Markdown file. Documentation is more than the user manual, it also includes the standard library coqdoc-generated documentation and the man pages. So moving everything inside doc/sphinx wouldn't make sense and this explains also the difference between the sphinx target and the doc-html target.

[Zimmi48]

Cf. #7783