Convert misc chapters to prodn, update syntax #12936

jfehrle · 2020-08-29T00:44:15Z

This seems to be pretty straightforward. Some questions embedded in the .rst files.

After this, there's just SSR and the tactics chapters to do. Then there will be some cleanup at the end.

doc/sphinx/addendum/extraction.rst

Zimmi48

This might take a while for me to review all this PR because it modifies chapters on topics which I know less about.

doc/sphinx/addendum/extraction.rst

Zimmi48 · 2020-09-08T09:33:39Z

doc/sphinx/addendum/extraction.rst

+     If the type scheme axiom is an arity (a sequence of products followed
+     by a sort), the then some type
+     variables have to be given (as quoted strings). The syntax is then:


I personally don't understand any of this but it should clearly be rewritten, maybe with help from @coq/extraction-maintainers.

Note the left-over "The syntax is then:" from the previous version.

Zimmi48 · 2020-09-08T09:40:04Z

doc/sphinx/addendum/generalized-rewriting.rst

+   .. todo PR needs more work.  The first @one_term maps to :g:`relation (A t1 ... tn)`.
+      I guess the second maps to :g:`Aeq: forall (y1 : β1 ... ym : βm)`, but that
+      doesn't match the (Aeq t′1 ... t′m) in the cmd syntax before my changes.
+      And then not sure how :g:`(A : αi -> ... αn -> Type)` fits in at all, e.g.
+      what is α?


@mattam82 Can you help (or designate someone that could help)?

The first term should be a Type (the carrier of the relation), say T, while the second should be a relation on T, i.e. of type (T -> T -> Prop). As written before, we had A and Aeq applied to some terms built from the binders. So A: forall x1 ... x2, Type and Aeq : forall x1 .. x2, (A x1 ... xn) -> A (x1 ... xn) -> Prop), or equivalently, Aeq : forall x1 ... xn, relation (A x1 ... xn).

Here's my best shot:

How do the binders relate to the alphas? Or are they unrelated?

The binders are usually the same as the alphas, but there is no strict relationship. Maybe rather say that one_termA and one_term_Aeq should be typeable under the context binders instead.

doc/sphinx/addendum/generalized-rewriting.rst

jfehrle · 2020-09-14T22:25:03Z

Let me know when you're done with a first pass review--I assume you're not because of the small number of comments you've made.

Zimmi48

Review still not complete.

doc/sphinx/addendum/implicit-coercions.rst

doc/sphinx/addendum/micromega.rst

Zimmi48 · 2020-09-22T13:08:00Z

doc/sphinx/addendum/micromega.rst

+      show_zify ::= {| InjTyp | BinOp | UnOp | CstOp | BinRel | UnOpSpec | BinOpSpec | Spec }
+
+   .. todo PR: should there be Show Zify {| PropBinOp | PropOp | PropUOp | Saturate } options?
+      to match Add Zify ...   An oversight or not?


What do you mean by options? Things you can set?
Show Zify bla does not enable printing. It prints information when invoked.

I hope it answers the question.

Perhaps I should have said "commands" instead of "options". For symmetry with Add Zify, should Show Zify also support PropOp | PropBinOp | PropUOp | Saturate? If so, I will add them in another PR.

@fajb says:

As the set of such operators looks fixed to me.
I'll rather remove the Add PropOp PropBinOp et PropUOp.
That is convenient for implementation but the user probably does not
care.

doc/sphinx/addendum/program.rst

Zimmi48 · 2020-09-22T13:47:46Z

doc/sphinx/addendum/program.rst


-   The optional order annotation follows the grammar:
+   .. todo PR: move measure and wf info to inductive.html#recursive-functions-fix?


I think there is a different meaning to these annotations depending on whether you use them with Function or Program (and possibly with Equations). @mattam82?

The wf annotation is treated the same but for measures Program differs indeed.

@mattam82 Can you elaborate on what the difference is here? Just a few lines below, I have text that says ":g:wf R x which is equivalent to :g:measure x R." which seems inconsistent with you statement (that wf is the same but measure is difterent).

What @mattam82 said is that wf annotation is treated the same way in Function and Program and that measure means something different in Function and Program. In Program, wf means the same up to the order of the arguments. This is not inconsistent with the fact that measure means something else in Function.

BTW @mattam82, this is kind of confusing, so don't you think that measure should be disallowed with Program?

measure is nicer in Program as it allows the user not to pack the arguments in a tuple but can mention all of them.
One can write Program Fixpoint foo (l l' : list nat) {measure (length l + length l')} not having to mention that the relation should be Nat.lt.

I need a bit more explanation of measure, wf and struct (not described in the doc) before I can say how they're different with or without Program. I don't have a clear grasp on their meaning. I take it measure has to decrease for each recursion in the definition (maybe not the best words), but I have no clue how that differs from the other two. struct means the number of symbols in the specified variable must decrease for each recursion? No idea how tuples fit into this. A couple very simple examples would help.

wf means the same up to the order of the arguments

Meaning ignoring the order of the arguments? Not so familiar with the "up to" idiom.

struct is for structural recursion. It means you can only call the recursive function on strict subterms (obtained by pattern-matching) of your initial argument. This is the simplest form of recursion, the only one accepted by the kernel.

Meaning ignoring the order of the arguments?

In this case, I mean that the order of arguments is inverted between the two syntax.

doc/sphinx/addendum/program.rst

doc/sphinx/addendum/nsatz.rst

Zimmi48 · 2020-09-23T13:17:47Z

doc/sphinx/addendum/nsatz.rst

+       * strategy = 0: reverse lexicographic order and newest s-polynomial.
+       * strategy = 1: reverse lexicographic order and sugar strategy.
+       * strategy = 2: pure lexicographic order and newest s-polynomial.
+       * strategy = 3: pure lexicographic order and sugar strategy.


Suggested change

* strategy = 0: reverse lexicographic order and newest s-polynomial.

* strategy = 1: reverse lexicographic order and sugar strategy.

* strategy = 2: pure lexicographic order and newest s-polynomial.

* strategy = 3: pure lexicographic order and sugar strategy.

* `strategy := 0%Z`: reverse lexicographic order and newest s-polynomial.

* `strategy := 1%Z`: reverse lexicographic order and sugar strategy.

* `strategy := 2%Z`: pure lexicographic order and newest s-polynomial.

* `strategy := 3%Z`: pure lexicographic order and sugar strategy.

Got it. Kind of weird you have to put "%Z" after something that's not even used as a number.

Yes. We are just documenting this but honestly, I'm seriously scared by the way this tactic is taking its arguments.

Something more high-level could indeed be done. I don't know how much these arguments are used though in practise and whether a change could be done without too much worries. Cc @thery

doc/sphinx/addendum/nsatz.rst

jfehrle · 2020-09-28T05:16:19Z

Updated, please take a look.

jfehrle · 2020-09-29T19:58:55Z

Rebased.

doc/sphinx/addendum/generalized-rewriting.rst

doc/sphinx/addendum/implicit-coercions.rst

doc/sphinx/conf.py

doc/sphinx/language/core/assumptions.rst

doc/sphinx/language/core/definitions.rst

doc/sphinx/language/core/inductive.rst

doc/sphinx/language/core/records.rst

doc/sphinx/proof-engine/vernacular-commands.rst

jfehrle · 2020-10-02T20:26:25Z

Updated.

jfehrle · 2020-10-20T01:22:55Z

Updated.

mattam82 · 2020-10-20T08:49:44Z

doc/sphinx/addendum/generalized-rewriting.rst

+      And then not sure how :g:`(A : αi -> ... αn -> Type)` fits in at all, e.g.
+      what is α?
+
+   Declares a parametric relation :g:`Aeq: forall (y1 : β1 ... ym : βm)`,
   :g:`relation (A t1 ... tn)` over :g:`(A : αi -> ... αn -> Type)`.



I think that's correct, although it's a bit strange to separate the Aeq : forall ... from the relation part.

Well, except that \beta1 ... \betan should be \alpha1 ... \alphan here.

jfehrle · 2020-10-21T05:59:41Z

Updated.

doc/sphinx/user-extensions/proof-schemes.rst

doc/sphinx/using/libraries/funind.rst

Zimmi48 · 2020-10-22T13:40:54Z

We're going to release 8.12.1 soon but given how close to ready this PR is, I'd appreciate being able to include it. Feel free to squash your last changes to spare a cycle.

jfehrle · 2020-10-22T23:17:08Z

Updated. Still need some help with measure/wf/struct, so not quite done.

Always generate prodn* files if edits succeed

Zimmi48 · 2020-10-23T08:31:36Z

We are getting blocked on some detail which is already written well enough for the manual (doesn't introduce any regression). Of course, its presentation could be improved further, but this is also the case of many other things in the manual, and in the meantime, this delays the integration of a PR which contains huge improvements. Furthermore, it would be easier to have this kind of detailed discussion on a specific aspect in a smaller PR which is only focused on this.

jfehrle · 2020-10-23T21:14:32Z

If you're satisfied that works for me. So I squashed this without further changes. We can come back to struct, wf and measure sometime in the future. Thanks for all your help reviewing this.

Zimmi48 · 2020-10-24T20:31:29Z

Thanks! Though, there is just one regression in the description of the record declaration that we would need to fix before merging this PR.

Formerly, the text said "If type is omitted, the default type is Type."

In the new version, it should say "If sort is omitted, the default sort is Type."

However, the following (which is currently written in this PR) is wrong:

If present, field_body gives the type of the field name. Otherwise, the field type defaults to Type.

There is no default field type. As I said before, field types are inferred if there is sufficient information to do so.

jfehrle · 2020-10-24T22:39:03Z

Updated.

I replaced If present, field_body gives the type of the field name. Otherwise, the field type defaults to Type.
with If :token:`sort` is omitted, the default sort is Type."

jfehrle · 2020-10-25T02:59:24Z

All the refman jobs built, so I think it's good to go.

Zimmi48

@coqbot: merge now

jfehrle · 2020-10-25T20:35:03Z

Awesome!

jfehrle added the kind: documentation Additions or improvement to documentation. label Aug 29, 2020

jfehrle added this to the 8.12.1 milestone Aug 29, 2020

jfehrle requested a review from Zimmi48 August 29, 2020 00:44

jfehrle requested a review from a team as a code owner August 29, 2020 00:44

proux01 reviewed Sep 1, 2020

View reviewed changes

doc/sphinx/addendum/extraction.rst Outdated Show resolved Hide resolved

Zimmi48 reviewed Sep 8, 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 Sep 8, 2020

Zimmi48 mentioned this pull request Sep 11, 2020

Minimal changes to make the refman compatible with Sphinx 3. #13011

Merged

2 tasks

jfehrle mentioned this pull request Sep 13, 2020

Convert SSR chapter to use prodn, update syntax #13019

Closed

1 task

This comment has been minimized.

Sign in to view

Zimmi48 reviewed Sep 22, 2020

View reviewed changes

Zimmi48 reviewed Sep 23, 2020

View reviewed changes

doc/sphinx/addendum/nsatz.rst Outdated Show resolved Hide resolved

Zimmi48 reviewed Sep 23, 2020

View reviewed changes

jfehrle force-pushed the prodn_misc_chapts branch from c73f919 to ad41653 Compare September 28, 2020 05:15

coqbot-app bot removed the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Sep 28, 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 Sep 29, 2020

This comment has been minimized.

Sign in to view

Zimmi48 mentioned this pull request Sep 29, 2020

coqbot did not push to GitLab (or rather GitLab didn't answer to git push). coq/bot#111

Open

jfehrle force-pushed the prodn_misc_chapts branch from ad41653 to f116a15 Compare September 29, 2020 19:53

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

jfehrle force-pushed the prodn_misc_chapts branch from f116a15 to 75a2695 Compare September 29, 2020 21:35

This comment has been minimized.

Sign in to view

Zimmi48 reviewed Oct 1, 2020

View reviewed changes

mattam82 reviewed Oct 20, 2020

View reviewed changes

Zimmi48 reviewed Oct 22, 2020

View reviewed changes

doc/sphinx/user-extensions/proof-schemes.rst Outdated Show resolved Hide resolved

Zimmi48 reviewed Oct 22, 2020

View reviewed changes

doc/sphinx/using/libraries/funind.rst Outdated Show resolved Hide resolved

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

jfehrle force-pushed the prodn_misc_chapts branch from 8fc29d7 to 3e77f1b Compare October 22, 2020 23:15

jfehrle force-pushed the prodn_misc_chapts branch from 3e77f1b to 9656b72 Compare October 22, 2020 23:21

Make no match/multiple match for tacn/cmd an error

703d2c9

Always generate prodn* files if edits succeed

jfehrle force-pushed the prodn_misc_chapts branch from 9656b72 to e911332 Compare October 22, 2020 23:26

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

jfehrle force-pushed the prodn_misc_chapts branch from e911332 to eae30c6 Compare October 23, 2020 21:10

jfehrle force-pushed the prodn_misc_chapts branch from eae30c6 to e2fcc74 Compare October 24, 2020 22:35

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

Convert misc chapters to prodn

7a57a23

jfehrle force-pushed the prodn_misc_chapts branch from e2fcc74 to 7a57a23 Compare October 24, 2020 22:38

Zimmi48 approved these changes Oct 25, 2020

View reviewed changes

coqbot-app bot merged commit a12112c into coq:master Oct 25, 2020

coqbot-app bot added this to Request 8.12.1 inclusion in Coq 8.12 Oct 25, 2020

jfehrle mentioned this pull request Oct 26, 2020

Correct "typeclasses eauto" syntax #13272

Closed

Zimmi48 added a commit to Zimmi48/coq that referenced this pull request Oct 26, 2020

Backport PR coq#12936: Convert misc chapters to prodn, update syntax

19bf55b

coqbot-app bot moved this from Request 8.12.1 inclusion to Shipped in 8.12.1 in Coq 8.12 Oct 27, 2020


		The optional order annotation follows the grammar:
		.. todo PR: move measure and wf info to inductive.html#recursive-functions-fix?

Convert misc chapters to prodn, update syntax #12936

Convert misc chapters to prodn, update syntax #12936

Conversation

jfehrle commented Aug 29, 2020 • edited

Zimmi48 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jfehrle commented Sep 14, 2020

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

Zimmi48 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

mattam82 Oct 22, 2020 • edited

Choose a reason for hiding this comment

jfehrle Oct 22, 2020 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jfehrle commented Sep 28, 2020

This comment has been minimized.

jfehrle commented Sep 29, 2020

This comment has been minimized.

jfehrle commented Oct 2, 2020

jfehrle commented Oct 20, 2020

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jfehrle commented Oct 21, 2020

Zimmi48 commented Oct 22, 2020

jfehrle commented Oct 22, 2020

Zimmi48 commented Oct 23, 2020

jfehrle commented Oct 23, 2020

Zimmi48 commented Oct 24, 2020

jfehrle commented Oct 24, 2020 • edited

jfehrle commented Oct 25, 2020

Zimmi48 left a comment

Choose a reason for hiding this comment

jfehrle commented Oct 25, 2020

jfehrle commented Aug 29, 2020 •

edited

mattam82 Oct 22, 2020 •

edited

jfehrle Oct 22, 2020 •

edited

jfehrle commented Oct 24, 2020 •

edited