Update syntax in auto.rst chapter by jfehrle · Pull Request #13343 · rocq-prover/rocq

jfehrle · 2020-11-10T19:15:17Z

Convert and refine the chapter.

jfehrle · 2020-11-11T20:34:17Z

Updated.

jfehrle · 2020-11-12T05:13:18Z

I'm wondering what to do about clause_dft_concl. It looks like rewrite would use all the options, but autounfold only a few. It should have a single writeup in one place. Your thoughts?

Zimmi48 · 2020-11-12T08:55:07Z

It belongs here IMHO. If we could keep the nonterminal names as close to what is currently presented as possible, this would be nice BTW (occurrence_clause is a nicer name than clause_dft_concl).

Zimmi48 · 2020-11-12T15:53:34Z

+   :n:`with *`
+     Use the unfolding hints in all existing hint databases.

-   Uses the unfold hints declared in all the hint databases.
+   :n:`with {+ @ident }`
+     Use the unfolding hints in :n:`{+ @ident }` in addition to the database ``core``.
+     Use the fake database `nocore` to omit `core`.


This is basically the same explanation as the previous one of hintbases, so I don't think it is actually worth repeating.

Yeah, we should hyperlink to a common description for commonly used bits of grammar rather than repeating the same text over and over. That may be easier to do as a cleanup once the syntax has been updated everywhere.

Zimmi48 · 2020-11-12T16:03:36Z

+   Unfolds constants that were declared through a :cmd:`Hint Unfold`
+   in the given databases.
+
+.. tacn:: autorewrite {? * } with {+ @ident } {? @clause_dft_concl } {? using @ltac_expr }


@mattam82 (or @JasonGross): can you tell us what this optional * does?

Can you guess from this? The * passes a ~conds:AllMatches to the lower level code. Naive is the default for ~conds.

The options are defined as:

type conditions = | Naive (* Only try the first occurrence of the lemma (default) *) | FirstSolved (* Use the first match whose side-conditions are solved *) | AllMatches (* Rewrite all matches whose side-conditions are solved *)

From this, I would conclude approximately that * means autorewrite will rewrite in all occurrences that match a single rewrite lemma instead of rewriting in only one place at once, and that it may do more progress in some cases because of this.

This seems to be a bit of a mess. Only some parts of the occurrences clause are accepted. I guess the * is a workaround for not supporting the at 1 form. Would you mind turning my last example into something that works and verifying that the occurrence numbers are applied in H?

autorewrite * with True at 1. (* The "at" syntax isn't available yet for the autorewrite tactic. *) autorewrite * with True in |- * at 1. (* The "at" syntax isn't available yet for the autorewrite tactic. *) autorewrite * with True in H at 1. (* Rewriting base True does not exist. *)

See #4976 and #7672

Also #1933 (comment) where @mattam82 seems to have given an explanation (in French)

@JasonGross Thanks for your help. @mattam82's French comment about rewrite* and autorewrite* aligns well with the piece of code found by Jim but the issue opened by Samuel seems to indicate that autorewrite* does not actually work. We need @mattam82 to comment, so I'll ping him by e-mail.

In any case, the current documentation of * added in this PR is probably a bit too simple ("If present, rewrite all occurrences.")

Zimmi48

Here's the rest of my review.

Zimmi48 · 2020-11-13T15:34:30Z

@jfehrle My suggestion to introduce a new syntax bfs eauto and deprecate the syntax eauto natural natural would make the PR go beyond a simple documentation PR, and thus introduces the issue of the upcoming feature freeze (on Monday 16th). Thus, if you agree to follow this suggestion, maybe that should go to a separate PR to guarantee that this can be merged before Monday. I can also open the PR myself actually.

jfehrle · 2020-11-14T03:26:39Z

If we could keep the nonterminal names as close to what is currently presented as possible, this would be nice BTW (occurrence_clause is a nicer name than clause_dft_concl).

occurrence_clause was not used in the chapter. There was a goal_occurrences, but I didn't know what it corresponded to.

jfehrle · 2020-11-14T19:07:15Z

I think this should be changed in the mlgs to OPT "-" LIST1 nat_or_var. Make that a separate PR?

occs_nums: [
| LIST1 nat_or_var
| "-" nat_or_var LIST0 int_or_var
]

jfehrle · 2020-11-15T05:39:06Z

Updated. This took forever to update. Be sure to look at the changes in tactics.rst and in rewriting.rst.

jfehrle · 2020-11-16T02:24:30Z

Updated.

Zimmi48

Great improvement to the occurrence clauses section.

jfehrle · 2020-11-18T00:11:55Z

Updated.

Zimmi48 · 2020-11-19T17:41:38Z

Great improvements to rewriting.rst!

jfehrle · 2020-11-19T23:12:52Z

Updated. Are we getting close to done?

Zimmi48

Only a non-important suggestion but could we introduce more symmetry in the way and the order that the variants and the flags associated to auto, trivial and eauto are presented?

Zimmi48 · 2020-11-20T14:39:24Z

-.. tacv:: autounfold with {+ @ident} in @goal_occurrences
+      Like :tacn:`eauto`, but does a breadth-first search (i.e. the tactic
+      checks all the relevant hints to see if one solves the goal before
+      recurring).


breadth-first search is more than this (it explores all "paths of length 2" before going to "paths of length 3"). Anyway, what about linking to Wikipedia instead of attempting to explain this?

Got it. I had some doubt that this was doing a full bfs. AFAIK, the kernel, monad infrastructure, Ltac, etc. are all designed around dfs and backtracking. For efficiency, you'd want to save the resulting proof state for each successful hint at each level rather than repeating application of the hint (easy to code). I'll have to look at that code sometime.

One thing I'd like to experiment with at some point is guiding the search in part by metrics on the proof such as the length of the goal conclusion(s), keeping only the best N results at any point. That may solve some goals more efficiently and/or make useful progress for the user.

BTW, there are several implementations of proof search and the plan was to get rid of the legacy auto and eauto backend in favor of the most recently written typeclasses eauto which also has a bfs strategy BTW (while keeping the tactics of course). See #721.

Ah, you worked on that! We'll have to chat about it sometime.

Zimmi48

I think we are very close to done.

Zimmi48 · 2020-11-20T17:45:39Z

+| REPLACE "Proof" "using" section_var_expr "with" Pltac.tactic
+| WITH "Proof" "using" section_subset_expr OPT [ "with" ltac_expr5 ]
+| DELETE "Proof" "using" section_var_expr


Instead of making this change in common.edit_mlg, I suggest following more closely the implementation for once. I.e. only document Proof using (without mentioning the with clause) in the proof mode chapter, and put the two forms with the with clause in the auto.rst file.

Note that doc_grammar complains if the same command is shown in more than one :cmd:. I'll use :cmdv: but then doc_grammar won't check or update it. And I'll add a reference from Print using to Print with.

A bit of a weird case. We should start using the pattern LIST0 [ opt1 | opt2 | ... | optn ] in the grammar where needed to accept multiple options in any order.

jfehrle · 2020-11-20T21:51:27Z

Updated.

Zimmi48

Looks very good to me. Only nits remaining, although this will now have to be rebased over #13417 which was just merged.

Zimmi48 · 2020-11-23T09:32:30Z

      | {? @ident } %{ {*; @record_field } {? ; } %}
      constructor ::= @ident {* @binder } {? @of_type }
      cumul_ident_decl ::= @ident {? @cumul_univ_decl }
+      cumul_univ_decl ::= @%{ {* {? {| = | + | * } } @ident } {? + } {| %| {*, @univ_constraint } {? + } %} | {| %} | %|%} } }


I think it's best to leave cumul_univ_decl where it has been put in #12653, i.e. next to univ_decl.

As you wish. That list of productions in the universe chapter is a bit of an anomaly, throwing together several nonterminals that don't all refer to each other.

We should improve this, of course, but there is no point in putting productions very far from the place they are currently documented.

jfehrle · 2020-11-23T22:26:02Z

Rebased and updated.

Zimmi48

Looks good to me. Can you squash at the same time as you address my last comments?

Zimmi48 · 2020-11-24T09:03:12Z

+  Undocumented :n:`eauto @nat_or_var @nat_or_var` syntax in favor of new ``bfs eauto``.
  Also deprecated 2-integer syntax for ``debug eauto`` and ``info_eauto``.
  (Use ``bfs eauto`` with the :flag:`Info Eauto` or :flag:`Debug Eauto` flags instead.)


You could put a few :tacn: in this changelog entry (not an important suggestion).

Zimmi48 · 2020-11-24T09:07:59Z

   | @qualid
   univ_decl ::= @%{ {* @ident } {? + } {? %| {*, @univ_constraint } {? + } } %}
-   cumul_univ_decl ::= @%{ {* {? {| = | + | * } } @ident } {? + } {? %| {*, @univ_constraint } {? + } } %}
+   cumul_univ_decl ::= @%{ {* {? {| = | + | * } } @ident } {? + } {| %| {*, @univ_constraint } {? + } %} | {| %} | %|%} } }


The presentation of this production should not change. This is an implementation detail that we need to take care of the special case where you put no space between the | and the final } (case of an empty list of universe constraints).

It's a new production that needed the same edit that univ_decl has, which I added. They are very similar. It's tempting to deem it a semantic restriction:

jfehrle · 2020-11-24T20:08:51Z

Updated and squashed. Thanks for the review!

Zimmi48 · 2020-11-25T07:51:38Z

@coqbot merge now

jfehrle added kind: documentation Additions or improvement to documentation. needs: merge of dependency This PR depends on another PR being merged first. labels Nov 10, 2020

jfehrle added this to the 8.13+beta1 milestone Nov 10, 2020

jfehrle requested a review from Zimmi48 November 10, 2020 19:15

jfehrle requested review from a team as code owners November 10, 2020 19:15

jfehrle force-pushed the prodn_auto branch 2 times, most recently from 70ef971 to ddcbc27 Compare November 10, 2020 21:26

Zimmi48 reviewed Nov 10, 2020

View reviewed changes

jfehrle force-pushed the prodn_auto branch from ddcbc27 to 1342753 Compare November 10, 2020 22:11

Zimmi48 removed the request for review from a team November 11, 2020 13:50

Zimmi48 removed the needs: merge of dependency This PR depends on another PR being merged first. label Nov 11, 2020

Zimmi48 self-assigned this Nov 12, 2020

Zimmi48 reviewed Nov 12, 2020

View reviewed changes

Zimmi48 reviewed Nov 13, 2020

View reviewed changes

jfehrle requested a review from a team as a code owner November 15, 2020 05:36

Zimmi48 mentioned this pull request Nov 15, 2020

Warn on hints without an explicit locality #13384

Merged

github-actions Bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Nov 15, 2020

jfehrle force-pushed the prodn_auto branch from 68f2f35 to 2b626c7 Compare November 16, 2020 02:24

coqbot-app Bot removed the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Nov 16, 2020

github-actions Bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Nov 16, 2020

Zimmi48 reviewed Nov 16, 2020

View reviewed changes

jfehrle mentioned this pull request Nov 17, 2020

Use only nats for occs_nums rather than ints #13403

Merged

jfehrle force-pushed the prodn_auto branch from 7c9b481 to ab64afe Compare November 17, 2020 06:05

Zimmi48 mentioned this pull request Nov 19, 2020

Use nat_or_var in grammar where negative values don't make sense #13417

Merged

Zimmi48 reviewed Nov 19, 2020

View reviewed changes

github-actions Bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Nov 20, 2020

Zimmi48 reviewed Nov 20, 2020

View reviewed changes

Comment thread doc/sphinx/proofs/automatic-tactics/auto.rst Outdated

Zimmi48 reviewed Nov 20, 2020

View reviewed changes

jfehrle force-pushed the prodn_auto branch from 6abeb4c to 28c8d0f Compare November 20, 2020 21:51

coqbot-app Bot removed the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Nov 20, 2020

github-actions Bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Nov 23, 2020

Zimmi48 reviewed Nov 23, 2020

View reviewed changes

Add COPYALL and APPENDALL edit ops, drop unneeded code

250ffd2

jfehrle force-pushed the prodn_auto branch from 28c8d0f to 5729422 Compare November 23, 2020 22:25

coqbot-app Bot removed the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Nov 23, 2020

Zimmi48 approved these changes Nov 24, 2020

View reviewed changes

Zimmi48 added the needs: squashing Some commits should be squashed together. label Nov 24, 2020

Convert auto chapter to prodn

b1846e8

jfehrle force-pushed the prodn_auto branch from 5729422 to b1846e8 Compare November 24, 2020 20:07

jfehrle removed the needs: squashing Some commits should be squashed together. label Nov 24, 2020

coqbot-app Bot merged commit 6377fbe into rocq-prover:master Nov 25, 2020

Zimmi48 mentioned this pull request Nov 25, 2020

Use nat_or_var for fail/gfail #13469

Merged

gares added a commit to gares/coq that referenced this pull request Nov 25, 2020

Backport PR rocq-prover#13343: Update syntax in auto.rst chapter

688d695

Conversation

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

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

jfehrle commented Nov 11, 2020

Uh oh!

jfehrle commented Nov 12, 2020

Uh oh!

Zimmi48 commented Nov 12, 2020

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

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!

JasonGross Nov 20, 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!

Zimmi48 left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Zimmi48 commented Nov 13, 2020

Uh oh!

jfehrle commented Nov 14, 2020

Uh oh!

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

Uh oh!

Uh oh!

jfehrle commented Nov 15, 2020

Uh oh!

jfehrle commented Nov 16, 2020

Uh oh!

Zimmi48 left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

jfehrle commented Nov 18, 2020

Uh oh!

Zimmi48 commented Nov 19, 2020

Uh oh!

Uh oh!

Uh oh!

jfehrle commented Nov 10, 2020 •

edited

Loading

JasonGross Nov 20, 2020 •

edited

Loading

jfehrle commented Nov 14, 2020 •

edited

Loading