Convert ltac2 chapter to use prodn, update syntax #12085

jfehrle · 2020-04-12T22:03:22Z

Take a look at fullGrammar. Including ltac2 changes the definition of about 25 existing nonterminals, also adding about 90 new nonterminals. For example, "$" ident is added in a couple places.

For the documentation, it's awkward to show the additional productions for the 25 existing nonterminals. Here are some possibilities:

include them under the associated nonterminal outside the Ltac2 chapter, but marked "(* ltac2 *) with a description
keep the production and description in the ltac2 chapter, insert linking nonterminals such as ltac2_XXX in the other chapters where needed so the added productions are discoverable but it's fairly apparent that they are for ltac2
perhaps some of the additions could be added to the main grammar (i.e., excluding ltac2). Some may even work, others may parse but give an error message if ltac2 is not loaded. And we ought to understand whether the new productions work properly for, say, Ltac1 constructs if Ltac2 is loaded. We'd have to work this out with PMP.

Another issue is whether any material should be shared between the 2 Ltac chapters. That sounds like it could be complicated. It may be better to have them independent. That may mean the index has to qualify repeated items, e.g. match (Ltac1) and match (Ltac2).

There will be more details. Doing the Ltac chapter first will help.

Zimmi48

keep the production and description in the ltac2 chapter, insert linking nonterminals such as ltac2_XXX in the other chapters where needed so the added productions are discoverable but it's fairly apparent that they are for ltac2

Sounds like the right thing to do in many cases

Another issue is whether any material should be shared between the 2 Ltac chapters. That sounds like it could be complicated. It may be better to have them independent.

Yes, it would be better to keep the two chapters independent. However, we also have the issue that grammar rules for tactics are added in the Ltac1 and Ltac2 plugins, but we shouldn't have to repeat the documentation for those.

That may mean the index has to qualify repeated items, e.g. match (Ltac1) and match (Ltac2).

This is perfectly reasonable.

Zimmi48 · 2020-04-13T13:52:36Z

doc/sphinx/language/gallina-specification-language.rst

@@ -448,7 +448,7 @@ Definition by cases: match
 .. insertprodn term_match pattern0

 .. prodn::
-   term_match ::= match {+, @case_item } {? return @term100 } with {? %| } {*| @eqn } end
+   term_match ::= match {+, @case_item } {? return @term100 } with {| {? %| } {*| @eqn } | | %| {+| @branch } | {+| @branch } } end


There might be some inappropriate factorization (probably a non-terminal to rename). It is not normal that Ltac2 could modify the syntax of the match construct. (However, like Ltac1, it has its own match construct.)

Zimmi48 · 2020-04-13T14:02:52Z

doc/tools/docgram/fullGrammar

 ]

 induction_clause: [
 | destruction_arg as_or_and_ipat eqn_ipat opt_clause
+| destruction_arg as_or_and_ipat eqn_ipat OPT clause


There are some grammar rules that are both in the Ltac1 and Ltac2 plugin but which are grammar rules for tactics themselves, so independent of which version of Ltac is used. It would be interesting to figure out if it is possible to factorize them, but I'm not so hopeful.

Zimmi48 · 2020-04-13T14:04:28Z

doc/tools/docgram/fullGrammar

 ]

 oriented_rewriter: [
 | orient_rw rewriter
+| ltac2_orient rewriter


In some cases (again grammar rules for tactics), the rules are repeated but with other non-terminal names, making it harder to verify that these are exactly the same rules. That being said, I think this particular example is a case where you were the one to rename the non-terminal, to avoid duplicate names.

Zimmi48 · 2020-04-13T14:05:36Z

doc/tools/docgram/fullGrammar

 by_tactic: [
 | "by" tactic_expr3
 |
+| "by" tac2expr6


This is an example where it makes sense that it is not exactly the same non-terminal that follows the by clause: in one case it is an Ltac1 expr, whereas in the other it is an Ltac2 expr.

Zimmi48 · 2020-04-13T14:07:48Z

doc/tools/docgram/fullGrammar

 as_name: [
 | "as" ident
 |
+| "as" ident_or_anti
 ]


In this case, Ltac2 adds a second possibility after an as clause.

Zimmi48 · 2020-04-13T14:08:41Z

doc/tools/docgram/fullGrammar

 | "as" or_and_intropattern_loc
 |
+| "as" or_and_intropattern


That's a surprising difference. With the current duplication of code, there is always a risk of divergence between the two grammars.

Zimmi48 · 2020-04-13T14:09:42Z

doc/tools/docgram/fullGrammar

+| Prim.integer
+| Prim.string
+| Prim.qualid
+| "@" Prim.ident
+| "&" lident
+| "'" Constr.constr
+| "constr" ":" "(" Constr.lconstr ")"
+| "open_constr" ":" "(" Constr.lconstr ")"
+| "ident" ":" "(" lident ")"
+| "pattern" ":" "(" Constr.lconstr_pattern ")"
+| "reference" ":" "(" globref ")"
+| "ltac1" ":" "(" ltac1_expr_in_env ")"
+| "ltac1val" ":" "(" ltac1_expr_in_env ")"


It seems likely that these extensions of tactic_atom should have been added to some other non-terminal instead...

IIRC you were eager to get this chapter updated for 8.12 so it doesn't have productionlists. I'm not sure that's really feasible within the next couple weeks. Perhaps it's better to clean up the syntax for other chapters first, in particular doing as much of the tactics chapter as we can for 8.12. And doing much less rewriting.

The issues are:

First, that Ltac2 modifies nonterminals that are documented in other chapters--mostly in the Ltac1 chapter but also things that are elsewhere, e.g. small additions to patterns and intropatterns and tactics that are only available if ltac2 is loaded. Some things are AFAICT fully shared with Ltac1, while tactic_atom has a dozen new productions plus there are other scattered changes. Making the two chapters fully independent would be quite a lot of work. We could include some added productions, such as for patterns and tactics and mark which things are only for ltac2.

Second, it's not really clear where to fit all the Ltac2 productions into the current text. The old grammar is rather different from the current grammar. It seems like there were big changes to the grammar earlier that didn't make it to the doc. Some things don't fit into obvious places in the text.

Third, the current document has very little, if any, explanation on a production-by-production basis.

We could do something much simpler that's not very good but better than nothing, which is just to ensure that all the Ltac2 grammar appears in that chapter without explanation, including in some crude way the additions to nonterminals that apply to things in other chapters. That might be doable by the end of June. And at least we'd be showing the correct grammar.

I'd probably need to extend doc_grammar to get the documented grammar correct and keep the editing/updating sane and maintainable.

I pushed an update that reflects the Ltac1 chapter updates. It doesn't make sense to fix the missing reference warnings from Sphinx until we have a plan.

Let me know your thoughts.

Perhaps it's better to clean up the syntax for other chapters first, in particular doing as much of the tactics chapter as we can for 8.12. And doing much less rewriting.

I insist that there is no rush in fixing the syntax in the tactics chapter. You keep coming back to the idea of fixing the syntax with very little rewriting but experience has shown again and again that updating the syntax without doing the associated rewriting is not possible or would create major regressions in the documentation.

Let me be clear: I'd rather focus on other improvements to the refman for 8.12 and won't review any significant PR about the tactics chapter in the coming weeks. If we don't finish replacing the productionlist for 8.12, fine, but let's then focus on coordinating an effort to improve the pages that are new in 8.12.

If you want to defer reviewing further syntax updates until after 8.12 ships, that's fine. I think we need more discussion before I can do much on Ltac2. We can defer that discussion, too. I think I could make a lot of progress on the tactics chapter in the meantime. If you want my help for other doc improvements for 8.12, let me know what you have in mind.

It will be more a matter of helping the volunteers if we can find some.

Zimmi48

A worry that I have had for quite some time during the syntax revisions and that hits harder now with the Ltac2 chapter question (and that should also appear when attacking the SSR chapter) is that we haven't really managed yet to have a proper way of documenting the grammar of Coq as an extensible grammar (which it fundamentally is). The fact that a plugin may extend the syntax not just by adding new commands, tactics and nonterminals, but even by modifying some parsing rules for existing commands and nonterminals is something that we don't sufficiently acknowledge in the current documentation. The original prodn had support for += which was all about this AFAICT, but it is not really supported by doc_grammar IINM.

Zimmi48 · 2020-06-11T09:13:48Z

doc/sphinx/language/core/variants.rst

@@ -60,7 +60,7 @@ Definition by cases: match
 .. insertprodn term_match pattern0

 .. prodn::
-   term_match ::= match {+, @case_item } {? return @term100 } with {? %| } {*| @eqn } end
+   term_match ::= match {+, @case_item } {? return @term100 } with {? {| {? %| } {*| @eqn } | %| {+| @branch } | {+| @branch } } } end


Ltac2 extends the match syntax on terms!?

Well, yes. There are additions to branches that refer to many other Ltac2-defined nonterminals.

OK, I see the problem: Ltac2 defines its own branches and branch non-terminals, it doesn't extend the existing ones.

Zimmi48 · 2020-06-11T09:15:44Z

doc/sphinx/proof-engine/ltac.rst

+   | @ @ident
+   | & @lident
+   | ' @term
+   | constr : ( @term )
+   | open_constr : ( @term )
+   | ident : ( @lident )
+   | pattern : ( @cpattern )
+   | reference : ( @globref )
+   | ltac1 : ( @ltac1_expr_in_env )
+   | ltac1val : ( @ltac1_expr_in_env )


My suggestion was that this should all be extracted into a single ltac2_atom nonterminal, so that it would be clear when reading the Ltac1 chapter that this is irrelevant, and to document this ltac2_atom in the Ltac2 chapter.

That makes sense.

jfehrle · 2020-06-11T17:45:32Z

A worry that I have had for quite some time during the syntax revisions and that hits harder now with the Ltac2 chapter question (and that should also appear when attacking the SSR chapter) is that we haven't really managed yet to have a proper way of documenting the grammar of Coq as an extensible grammar (which it fundamentally is).

This has always been on my list but so far we haven't had to make a decision. There are only a couple choices:
a) include Ltac2 and SSR nonterminal extensions in other chapters, identifying them as such in the grammar/text. Lengthy descriptions could be hyperlinked to the Ltac2/SSR chapters,
b) list the added productions only in the Ltac2/SSR chapters, perhaps with a single hyperlink through an added nonterminal (like ltac2_atom),
c) repeat some material in 2 places, in particular between Ltac1 and Ltac2 and
d) a case-by-case blend of these.

I prefer "a", I would avoid "c" and I think we'll end up with "d". I think "b" makes sense when there are a bunch of productions added to an existing symbol; if it's only one or two added productions that can be explained succinctly, not so much. The problem with += is that hyperlinks to the extended nonterminal won't take you to the extensions. They become impossible to locate. Better to create new nonterminals to allow hyperlinks to the extensions.

I'm not sure if there are tactics or commands with syntax extensions; if so, we'd need to figure that out, too.

If you prefer, we can continue this discussion some weeks from now.

jfehrle · 2020-06-11T17:49:40Z

PS You may recall that doc_grammar already tracks where productions come from. This info is still printed in fullGrammar. We could tweak prodn to show this somehow and perhaps with a different font.

ring_mod: [
| "decidable" constr      (* setoid_ring plugin *)
| "abstract"      (* setoid_ring plugin *)
| "morphism" constr      (* setoid_ring plugin *)

Zimmi48 · 2020-06-11T18:24:35Z

FWIW I agree with your analysis. And yes, it would probably be useful to show where production comes from.

jfehrle · 2020-06-14T07:55:31Z

I added "Ltac2" tags in prodns. They appear on every production derived from the ltac2 mlg. Examples below. What do you think?

ltac2.rst:

tactics.rst:

variants.rst:

In this case, branch an Ltac2 symbol, the rest is non-Ltac2. There is no tag. I think may not be confusing, since the hyperlink for branch will take you to the Ltac2 chapter where the productions are marked with "Ltac2"

Zimmi48 · 2020-06-15T16:20:04Z

variants.rst:

You probably missed my answer regarding this: there is a confusion because some non-terminal names are reused, but Ltac2 should not and does not modify the (term) match syntax.

Zimmi48 · 2020-06-15T16:21:52Z

ltac2.rst

When it is clear that this is an Ltac2 production, e.g. because the non-terminal itself (and not just the rule) is defined in Ltac2, then I think these annotations are not necessary and may be a bit much.

Zimmi48 · 2020-06-15T16:25:54Z

The case of occs_nums is very likely similar to the case of the match construct: Ltac2 redefines some non-terminals with the same names. If a non-terminal name is the same across several mlg files, but none of these mlg files exports it (as in:

https://github.com/coq/coq/blob/90345eb092f9e3fc7ef1bdfe7f61cb913cb53d18/vernac/g_vernac.mlg#L88

), then these non-terminals should be considered distinct. Maybe that's something that you should consider handling in doc_grammar.

Zimmi48 · 2020-06-15T16:27:35Z

A good example showing these annotations would probably be the term_ltac line in https://coq.github.io/doc/master/refman/language/core/basic.html#grammar-token-term, except in this case we already created an intermediate non-terminal to have it documented in the Ltac chapter.

jfehrle · 2020-06-15T19:55:44Z

OK, I see those symbols are local and independent. The generated code, and occs_nums = Pcoq.Entry.make "occs_nums" gave me the impression that the parser entry name being created is unique and global, which is not the case.

If you think annotations such as "Ltac2" will never be useful, I'll drop that change entirely. What do you think? (If annotations are done on a case-by-case basis, it would need to be revised anyway.)

Zimmi48 · 2020-06-15T19:59:37Z

I think they might be useful, but I would need to see a concrete use case. Keep the code for now, we might end up encountering a good use case.

JasonGross

Not much textual change to this chapter, contrary to the Ltac1 chapter. Is this deliberate?

Makefile.doc

jfehrle · 2020-06-17T05:32:17Z

Not much textual change to this chapter, contrary to the Ltac1 chapter. Is this deliberate?

Well, it's still marked as a draft PR. The real work begins when the previous PR (i.e. Ltac1) is merged.
Usually I make the changes in stages to reduce rework: first address any general concerns (where we are now), then a first cut on the syntax (getting close to pushing that, spent all of yesterday correcting how doc_grammar handles nonterminals that are local to an .mlg), agreeing how to split/organize things, consolidating the cmdv or tacv plus whatever else we deem essential to do. I'll need to learn more specifics along the way just to plan, let alone write.

This chapter is only partially in a reference manual style. I'm not sure how much time I want to spend now in revising. Also some concern that it is still experimental; I'd prefer to focus on the parts that are most likely final. I'm doubtful it will make 8.12.0, but maybe it will be ready for 8.12.1. Inclusion is up to the release managers. It would great if you can review the PR as it evolves, answer questions and help generate examples. As we proceed I'll give some guidance on what to focus on.

JasonGross · 2020-06-17T11:28:15Z

Feel free to mention me with questions, I'll do my best to review as it evolves

jfehrle · 2020-06-19T23:00:10Z

Fully documenting the Ltac2 syntax looks like it could be a big project for which doc_grammar won't provide much help at all. A great deal of the user-visible syntax is defined by 139 notations in Ltac2.Notations.v. This includes 9 basic definitions such as match!, lazymatch! and multimatch! goal, which I can define manually in common.edit_mlg, but for which there would be no automatic detection of changes.

More problematic are the (re)definitions of ~130 tactics and Ltac1 constructs. Determining whether they match the versions hard-wired into the grammar is a non-trivial and unautomated task. Re-documenting any that differ just for Ltac2 is not a happy thought. I would lean toward explaining the redefinitions in general terms without comparing them exhaustively.

jfehrle · 2020-06-20T04:41:07Z

OK, I'm baffled why I get this error every time from Sphinx when CoqIDE 8.12 usually processes this input. (I say "usually" because I think backtracking in CoqIDE may not always fully undo things for Ltac2 (somehow) and I've seen the same error sometimes--but I haven't found a way to reliably repeat it.) So two problems. The Sphinx problem may block creating examples in the doc for Ltac2.

   .. coqtop:: reset all
      
      From Ltac2 Require Import Ltac2.
      From Ltac2 Require Import Message.
      Goal True.
      Ltac2 Notation "ex1" x(constr) := print (of_constr x).
      ex1 (1 + 2).

/mnt/c/proj/coq2/doc/sphinx/proof-engine/ltac2.rst:780: Error while sending the following to coqtop:
    Ltac2 Notation "ex1" x(constr) := print (of_constr x).
  coqtop output:
    Toplevel input, characters 15-20:
    > Ltac2 Notation "ex1" x(constr) := print (of_constr x).
    >                ^^^^^
    Error: Syntax error: [input_fun] expected after [binder] (in [tac2def_body]).

Also on this one:

   .. coqtop:: reset all
      
      From Ltac2 Require Import Ltac2.
      Goal True.
      Ltac2 Notation "ex2" x(list1(constr, ",")) := auto.
      ex2 1, 2, 3.

Extension error:
/mnt/c/proj/coq2/doc/sphinx/proof-engine/ltac2.rst:762: Error while sending the following to coqtop:
    Ltac2 Notation "ex2" x(list1(constr, ",")) := auto.
  coqtop output:
    Toplevel input, characters 15-20:
    > Ltac2 Notation "ex2" x(list1(constr, ",")) := auto.
    >                ^^^^^
    Error: Syntax error: [input_fun] expected after [binder] (in [tac2def_body]).

jfehrle · 2020-06-22T06:21:19Z

I pushed an update. I think most of the syntax is in the right place--would you take a look at that? I'm not ready to deal with a lot of text comments, but if there are typos or grammatical errors feel free to point them out.

I spent a fair bit of time correcting how doc_grammar handles local nonterminals. However, now that I look at result, I think a number of Ltac2 productions should be merged with existing similar nonterminals, tagging the productions that come from Ltac2 (as in my recent experiment) and adding verbiage that explains they're only available with Ltac2. I suppose I could suppress the Ltac2 tags within the Ltac2. The alternative would seem to be the 4 pages of productions at the end of the Notations/Syntactic Classes section. Ugh.

Ltac2 redefines the syntax for a great many tactics in Ltac2/Notations.v (139 "Ltac2 Notation"s) using Syntatic classes. This presents some challenges:

There's no tooling that verify that these definitions are the equivalent (assuming that was the intent). For example, "intros" is redefined, but it seems to omit the | "intros" "until" [ ident | num ] variant. I think the definitions have to be exactly in sync; it would be very confusing for readers/users otherwise.
The definitions in Notations.v rely on 76 external routines corresponding to tactics defined in Std.v.
Seems like this would (eventually) need some doc, but it tend to overlap the material in the tactics chapter.
Some tactics, such as lia (in an optional plugin) are not available at all, and so far I don't see any way to get around that short of code changes in OCaml. This would be a problem for 3rd party plugins!

@JasonGross Do you have any Ltac2 code I can peruse? Also, if faster execution is a benefit of Ltac2, it would be interesting to give an example. Would that fit into you performance evaluations efforts?

I don't know how many examples I'll add. It may be very few or none. As I noted, the coqtop directive fails for the 2 examples I tried. Nor have I considered what non-syntax-related text I'll update, if any. The starting point is far behind the Ltac1 chapter.

Zimmi48 · 2020-06-22T14:42:37Z

More problematic are the (re)definitions of ~130 tactics and Ltac1 constructs. Determining whether they match the versions hard-wired into the grammar is a non-trivial and unautomated task. Re-documenting any that differ just for Ltac2 is not a happy thought. I would lean toward explaining the redefinitions in general terms without comparing them exhaustively.

You can mostly ignore those. It's an implementation detail (that I'd like to get rid of) that the syntax for tactics are defined twice (once in each LtacX plugin).

JasonGross · 2020-06-22T15:25:42Z

Here are some examples of Ltac2 code:

You can also find a great deal of (relatively low-level) Ltac2 in
https://github.com/coq/coq/blob/master/user-contrib/Ltac2/List.v

Here are some Ltac2 examples that probably won't compile on the current version of Ltac2, because they're from an earlier version, but I expect them to be able to compile with only minor changes:

Also, if faster execution is a benefit of Ltac2, it would be interesting to give an example. Would that fit into you performance evaluations efforts?

There's some discussion of performance of Ltac2 in our reification-by-parametricity paper (see especially the graphs on pages 13 and 15, where direct translation from Ltac to Ltac2 (see the "Ltac2" line) seems to incur a slowdown in our particular example (we didn't debug where the slowdown came from; we had to change management of free/fresh variables, management of recurring under binders, and had to move the final term back and forth between Ltac1 and Ltac2, which might have incurred overhead), but where using Ltac2 allowed access to much more low-level term matching and construction primitives (mostly in Constr.Unsafe) which allowed a massive speedup (orders of magnitude, a better asymptotic complexity), and, if I recall correctly, was only about 300x slower than writing the code directly in OCaml (and this gap can presumably be closed by writing a compiler for Ltac2 for Coq, so you can pre-compile the Ltac2 tactics).

So in general I would not expect Ltac2 execution to be faster when just straightforwardly translating from Ltac1, nor when you are just writing your tactic script by hand in the goal. The primary benefits, I believe, are that (a) the language is more principled and not cobbled-together like Ltac1, and (b) it's possible to have much more fine-grained control over constr building and matching, allowing massive performance improvements. I think there'll also be a performance benefit in the future that we can potentially get access to the fast data-structures of OCaml, like array, maps and sets, ref cells, etc.

(Btw, we should make sure we're clear in the documentation how mutation in Ltac2 (of array, ref, etc) interacts with backtracking / exceptions.)

Googling also gives @tchajed 's tutorial at https://github.com/tchajed/ltac2-tutorial

JasonGross · 2020-06-22T15:26:38Z

Some tactics, such as lia (in an optional plugin) are not available at all, and so far I don't see any way to get around that short of code changes in OCaml.

(untested)

Ltac2 lia := ltac1:(lia).

jfehrle · 2020-06-22T18:39:53Z

Ltac2 lia := ltac1:(lia).

I get Tactic definition must be a syntactical value. Let me know if you have another idea. I will mention the workaround or open issue as the case may be.

Separately, I notice that there's no .mlg file for the micromega plugin. lia and nia appear to be defined in .ml files. Seems like we should change this to an .mlg and mandate that as the proper way to add syntax.

UPDATE: lia and nia are defined with Ltac lia := ... in Ztac.v. But I find it hard to believe that micromega doesn't add any syntax.

tchajed · 2020-06-22T19:17:58Z

To make lia available as a tactic, you need to do this trick:

From Ltac2 Require Import Ltac2.
From Coq Require Import Lia.

Local Ltac2 lia_ltac1 () := ltac1:(lia).
Ltac2 Notation "lia" := lia_ltac1 ().

Goal forall n m, n + m = m + n.
Proof.
  lia.
Qed.

tchajed · 2020-06-22T19:24:21Z

@jfehrle I think you might be running into a bug where backtracking across the Require for Ltac2 doesn't work since not all of the syntax extensions are reversed, as @ppedrot acknowledged here: #11549 (comment).

For me the biggest benefit of Ltac2 has been the ability to go back and forth between strings and identifiers, which was not possible in Ltac1 without a plugin. We convert strings to identifiers to support a feature in the Iris Proof Mode; see https://gitlab.mpi-sws.org/iris/string-ident/-/blob/master/theories/ltac2_string_ident.v for the implementation. Koika does the reverse, going from identifiers to strings: https://github.com/mit-plv/koika/blob/master/coq/IdentParsing.v.

jfehrle · 2020-08-21T07:02:52Z

Updated. Jason, would approve this? @Zimmi48 do you want to review it one more time? Will you handle the merge?

coqbot · 2020-08-21T07:09:46Z

For your complete information, the job test-suite:4.11+trunk+dune in allow failure mode has failed for commit eeef3a2: Review #5

jfehrle · 2020-08-24T02:56:52Z

@JasonGross I think @Zimmi48 would like to rely on your approval before merging this. Hope you can do that soon. Maybe will take you less than 5 minutes?

JasonGross · 2020-08-24T16:33:12Z

doc/sphinx/proof-engine/ltac2.rst

+  - A convenient way to build terms with casts through the low-level API because the
+    cast type is opaque.  You can use a variation of this code as a workaround:
+
+    .. coqtop:: none
+
+       From Ltac2 Require Import Ltac2.
+
+    .. coqtop:: in
+
+       Ltac2 get_vm_cast () :=
+         match Constr.Unsafe.kind '(I <: True) with
+         | Constr.Unsafe.Cast _ cst _ => cst
+         | _ => Control.throw Not_found
+         end.
+
+- Missing low-level primitives that are convenient for writing automation, such as:
+
+  - An easy way to get the number of constructors of an inductive type.
+    Currently only way to do this is to destruct a variable of the inductive type
+    and count the number of goals that result.
+
+  - Building terms with casts currently requires an awkward construction like the
+    following, which also incurs extra overhead to repeat typechecking for each
+    call to `get_vm_cast`: `Constr.Unsafe.make (Constr.Unsafe.Cast 'I (get_vm_cast ()) 'True)`


I still think the bullet points should be combined, e.g., like this:

Suggested change

- A convenient way to build terms with casts through the low-level API because the

cast type is opaque. You can use a variation of this code as a workaround:

.. coqtop:: none

From Ltac2 Require Import Ltac2.

.. coqtop:: in

Ltac2 get_vm_cast () :=

match Constr.Unsafe.kind '(I <: True) with

| Constr.Unsafe.Cast _ cst _ => cst

| _ => Control.throw Not_found

end.

- Missing low-level primitives that are convenient for writing automation, such as:

- An easy way to get the number of constructors of an inductive type.

Currently only way to do this is to destruct a variable of the inductive type

and count the number of goals that result.

- Building terms with casts currently requires an awkward construction like the

following, which also incurs extra overhead to repeat typechecking for each

call to `get_vm_cast`: `Constr.Unsafe.make (Constr.Unsafe.Cast 'I (get_vm_cast ()) 'True)`

- A convenient way to build terms with casts through the low-level API. Because the

cast type is opaque, building terms with casts currently requires an awkward construction like the

following, which also incurs extra overhead to repeat typechecking for each

call to `get_vm_cast`: `Constr.Unsafe.make (Constr.Unsafe.Cast 'I (get_vm_cast ()) 'True)`

with:

.. coqtop:: none

From Ltac2 Require Import Ltac2.

.. coqtop:: in

Ltac2 get_vm_cast () :=

match Constr.Unsafe.kind '(I <: True) with

| Constr.Unsafe.Cast _ cst _ => cst

| _ => Control.throw Not_found

end.

- Missing low-level primitives that are convenient for writing automation, such as:

- An easy way to get the number of constructors of an inductive type.

Currently only way to do this is to destruct a variable of the inductive type

and count the number of goals that result.

Feel free to merge with or without this, though.

Got, it thanks.

jfehrle · 2020-08-24T19:01:48Z

Updated. @Zimmi48 time for a final review if you wish and, if ready, a merge.

coqbot-app · 2020-08-24T19:03:22Z

For your complete information, the job test-suite:4.11+trunk+dune in allow failure mode has failed for commit be3da73: Review #6

coqbot-app · 2020-08-24T19:46:26Z

For your complete information, the job test-suite:base+async in allow failure mode has failed for commit be3da73: Review #6

jfehrle · 2020-08-24T21:24:40Z

@JasonGross Thanks for all your help!

@Zimmi48 I believe the failures are unrelated.

Zimmi48

I didn't try to review the Ltac2 chapter changes, only some of the other changes.

Didn't you intend to squash some commits before the merge?

doc/sphinx/changes.rst

Zimmi48 · 2020-08-25T07:52:14Z

doc/sphinx/language/core/basic.rst

@@ -227,6 +227,7 @@ rest of the |Coq| manual: :term:`terms <term>` and :term:`types
        | @term_match
        | @term_record
        | @term_generalizing
+        | [| {*; @term } %| @term {? : @type } |] {? @univ_annot }


What is this supposed to be?

Primitive arrays, added by #11604.

I see. Probably worth refining in a separate PR then. However, this raises the question whether this PR is actually backportable to v8.12. This line should be removed in the backport since it's 8.13-only syntax, but what about the documented features of Ltac2? Is any of what's newly documented in this PR 8.13-specific @JasonGross?

If you copy this PR locally onto 8.12 and run 'make doc_gram_rsts', that would identify and partly reverse 8.13 grammar changes. And then probably a quick review to back out any related textual changes. I can create that if you like after this is merged. I guess just make the new PR go against 8.12 instead of master?

Thanks, I guess I will try following your advice and backporting myself first. And if I don't manage, I'll ask you to do it.

doc/sphinx/language/extensions/match.rst

jfehrle · 2020-08-25T17:49:14Z

Updated. Made 2 small changes and squashed.

doc/sphinx/changes.rst

jfehrle · 2020-08-25T18:37:57Z

Updated.

Zimmi48 · 2020-08-26T12:47:39Z

One last question. The second commit introduces the ability to tag productions coming from plugins (Ltac2 in particular) but in the end, it doesn't look like this is used anywhere. Should we still keep this commit as part of this PR (as opposed to moving it to a new PR) since there isn't really much to test it against (and I can't really review the changes abstractly either)?

jfehrle · 2020-08-26T17:07:09Z

You saw what the output looks like with tags a while ago. We decided to use them sparingly; definitely not showing them for every production in the Ltac2 chapter. It would difficult, I think infeasible, to create an automated test. So I'm not sure what would be gained by making it a separate PR. What else would you do to review it? Splitting it out won't make it any easier to understand the changes. doc_grammar is an internal tool that is still evolving. Its output goes into the .rsts, which have been thoroughly reviewed.

Also, the commit would have to be split. The Makefile.doc change is essential. Some of the changes in coqdomain.py (switching to container and Text) may be needed; using inline and literal was incorrect but I don't recall offhand the exact difference in appearance. It would take some time to recall. doc_grammar.ml may have some small fixes in it that are needed. It would take some time to find those given that I had to reorder a fair bit of the code. (Too bad OCaml doesn't support forward references to functions :-( )

I suggest we keep this as it is.

Zimmi48 · 2020-08-26T17:27:03Z

OK, fine by me.

Zimmi48

@coqbot: merge now

jfehrle · 2020-08-26T17:54:31Z

Thanks for your help, Théo.

Reviewed-by: ejgallego

(cherry picked from commit 461e0d6)

…-prover#12085.

…date syntax

jfehrle requested a review from Zimmi48 April 12, 2020 22:03

Zimmi48 reviewed Apr 13, 2020

View reviewed changes

jfehrle added the kind: documentation Additions or improvement to documentation. label Apr 16, 2020

jfehrle force-pushed the prodn_ltac2 branch from 3c0d2fc to 216207c Compare June 10, 2020 20:02

Zimmi48 reviewed Jun 11, 2020

View reviewed changes

jfehrle force-pushed the prodn_ltac2 branch 2 times, most recently from e874972 to 50afb6a Compare June 14, 2020 07:37

JasonGross reviewed Jun 17, 2020

View reviewed changes

Makefile.doc Outdated Show resolved Hide resolved

jfehrle force-pushed the prodn_ltac2 branch from 50afb6a to 437a192 Compare June 21, 2020 22:00

JasonGross approved these changes Aug 24, 2020

View reviewed changes

Zimmi48 reviewed Aug 25, 2020

View reviewed changes

jfehrle force-pushed the prodn_ltac2 branch from be3da73 to 7b4ee9c Compare August 25, 2020 17:47

Zimmi48 reviewed Aug 25, 2020

View reviewed changes

doc/sphinx/changes.rst Outdated Show resolved Hide resolved

Convert ltac2 chapter to use prodn, update syntax

4a7e393

jfehrle force-pushed the prodn_ltac2 branch from 7b4ee9c to 4a7e393 Compare August 25, 2020 18:37

Zimmi48 self-assigned this Aug 26, 2020

Zimmi48 added this to the 8.12.1 milestone Aug 26, 2020

Zimmi48 approved these changes Aug 26, 2020

View reviewed changes

coqbot-app bot merged commit 748299d into rocq-prover:master Aug 26, 2020

Zimmi48 added a commit to Zimmi48/coq that referenced this pull request Sep 8, 2020

Fix docgram's dune file following rocq-prover#12085.

461e0d6

coqbot-app bot added a commit that referenced this pull request Sep 9, 2020

Merge PR #12994: Fix docgram's dune file following #12085.

cdfe69d

Reviewed-by: ejgallego

Zimmi48 added a commit to Zimmi48/coq that referenced this pull request Sep 10, 2020

Fix docgram's dune file following rocq-prover#12085.

d36d5b1

(cherry picked from commit 461e0d6)

Zimmi48 added a commit to Zimmi48/coq that referenced this pull request Sep 10, 2020

Backport PR rocq-prover#12994: Fix docgram's dune file following rocq…

9f555ce

…-prover#12085.

Zimmi48 added a commit to Zimmi48/coq that referenced this pull request Sep 10, 2020

Backport PR rocq-prover#12085: Convert ltac2 chapter to use prodn, up…

5ca824a

…date syntax

jfehrle mentioned this pull request Mar 12, 2021

Fixed grammar productions for PDF documentations #13935

Merged

Convert ltac2 chapter to use prodn, update syntax #12085

Convert ltac2 chapter to use prodn, update syntax #12085

Uh oh!

Conversation

jfehrle commented Apr 12, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Zimmi48 left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jfehrle Jun 10, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Zimmi48 left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jfehrle commented Jun 11, 2020

Uh oh!

jfehrle commented Jun 11, 2020

Uh oh!

Zimmi48 commented Jun 11, 2020

Uh oh!

jfehrle commented Jun 14, 2020

Uh oh!

Zimmi48 commented Jun 15, 2020

Uh oh!

Zimmi48 commented Jun 15, 2020

Uh oh!

Zimmi48 commented Jun 15, 2020

Uh oh!

Zimmi48 commented Jun 15, 2020

Uh oh!

jfehrle commented Jun 15, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Zimmi48 commented Jun 15, 2020

Uh oh!

JasonGross left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

jfehrle commented Jun 17, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

JasonGross commented Jun 17, 2020

Uh oh!

jfehrle commented Jun 19, 2020

Uh oh!

jfehrle commented Jun 20, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

jfehrle commented Apr 12, 2020 •

edited

Loading

jfehrle Jun 10, 2020 •

edited

Loading

jfehrle commented Jun 15, 2020 •

edited

Loading

jfehrle commented Jun 17, 2020 •

edited

Loading

jfehrle commented Jun 20, 2020 •

edited

Loading

jfehrle commented Jun 22, 2020 •

edited

Loading

Zimmi48 Aug 25, 2020 •

edited

Loading