Support multiple :name:s with multiple signatures for .. tacn:: #17507

jfehrle · 2023-04-18T16:44:13Z

Needed for #17503 (See this comment).

@Zimmi48 Can you review/merge this very short PR soon?

Zimmi48

I think that accepting more names than signature lines and silently pointing extra names to the first signature line, but not doing so for the middle names, is a footgun (even more so without any documentation of this behavior). It seems that your suggestion from #17503 (comment) illustrates this, since this should have been :names: lazy cbv weak lazy (and located on the line below).
Since the use case appears valid, a semantic that would look saner to me would simply be to point all the names to the first signature in case there are more names than signatures. This even leads to a simpler implementation:

            if len(names) < len(sigs):
                ERR = ("Expected at least {} semicolon-separated names, got {}.  " +
                       "Please provide at least one name per signature line.")
                raise self.error(ERR.format(len(names), len(sigs)))
            elif len(names) > len(sigs):
                self._sig_names = { sigs[0]: names }
            else:
                self._sig_names = { sig: [name] for (sig, name) in zip(sigs, names) }

Though there might also be valid use cases for providing fewer names than signature lines (in case three signatures start with the same two possible names, but end up with different parsing rules), in which case the code would simply be:

            if len(names) != len(sigs):
                self._sig_names = { sigs[0]: names }
            else:
                self._sig_names = { sig: [name] for (sig, name) in zip(sigs, names) }

Unless @cpitclaudel has a better idea.

Zimmi48 · 2023-04-19T07:52:12Z

doc/tools/coqrst/coqdomain.py

@@ -274,14 +274,16 @@ def _prepare_names(self):
            self._sig_names = {}
        else:
            names = [n.strip() for n in names.split(";")]
-            if len(names) != len(sigs):
+            if len(names) < len(sigs):


This branch was precisely meant for the case where len(names) > len(sigs) = 1.

Huh? What did you mean instead of len(names) > len(sigs) = 1?

What makes you think I meant something else?

Syntax. What do you mean by (simplifying) "A > B = 1"?

Sorry for the delayed answer. I mean A > B /\ B = 1.

Zimmi48 · 2023-04-19T07:52:38Z

doc/tools/coqrst/coqdomain.py

-                    ERR = ("Expected {} semicolon-separated names, got {}.  " +
-                           "Please provide one name per signature line.")
+                    ERR = ("Expected at least {} semicolon-separated names, got {}.  " +
+                           "Please provide at least one name per signature line.")
                    raise self.error(ERR.format(len(names), len(sigs)))
                self._sig_names = { sigs[0]: names }


With your current code, this line becomes unreachable.

It's reachable, but the message needs to be reworded.

jfehrle · 2023-04-19T18:00:22Z

I think that accepting more names than signature lines and silently pointing extra names to the first signature line, but not doing so for the middle names, is a footgun (even more so without any documentation of this behavior).

Colorful, but this seems a minor problem. We're never going to be able to check for every possible doc error. You even suggest pointing all the names to the first signature. I'm OK with changing it so all signatures point to the first entry.

It seems that your suggestion from #17503 (comment) illustrates this, since this should have been :names: lazy cbv weak lazy (and located on the line below).

Not so much, one has to test such changes. Hard to make review comments flawless when you're not actually making the changes. FWIW, I won't mention that you should have said :name: lazy; cbv; weak lazy above.

cpitclaudel · 2023-04-19T21:48:04Z

This looks OK to me, but doesn't sphinx let you add custom index entries with .. index? Maybe that's impler than adding more cases to the already-complicated :name: syntax? Not sure.

jfehrle · 2023-04-19T23:35:20Z

Updated. Hope we can wrap this up very soon.

I simplified the behavior. No need to change ~100 uses of :name: to :index:

I removed some unneeded :name:s.

I couldn't remember how to add text to doc/sphinx/README.rst. I wanted to add "If :name: is specified, the number of names must be >= the number of signatures. The name _ will not appear in indexes." Do you remember?

cpitclaudel · 2023-04-24T17:46:48Z

I simplified the behavior. No need to change ~100 uses of :name: to :index:

I wasn't proposing that, just to handle this additional new case with index instead of making :name: more powerful. (Or did I miss something?)

Zimmi48 · 2023-04-26T12:36:21Z

I couldn't remember how to add text to doc/sphinx/README.rst. I wanted to add "If :name: is specified, the number of names must be >= the number of signatures. The name _ will not appear in indexes." Do you remember?

You need to modify the README.template.rst file and run the build to update README.rst.

Zimmi48

I'm fine with the current version, but maybe we should have kept the ability of linking to each signature when the number of provided names matches exactly with the number of signatures?

I'm also not completely clear on what the alternative proposed by Clément would entail.

BTW, there is a build error that I'm not sure that I understand.

jfehrle · 2023-05-02T03:51:17Z

@cpitclaudel The Coq doc has 7 indexes. I don't see how .. index:: would know which one should get the entry.

Zimmi48 · 2023-05-02T08:29:36Z

Now the build results in:

/builds/coq/coq/_build/default/doc/sphinx/proof-engine/ssreflect-proof-language.rst:2215:Duplicate name first

jfehrle · 2023-05-02T15:41:25Z

That's the same message it was getting before, you just had to look at the full log to see it. I only rebased, no code change, but I think I figured out the cause.

jfehrle · 2023-05-02T21:12:46Z

I still can't get this to work after several hours of trying :-(. Perhaps one of you can figure out how to do this. It does seem like a useful enhancement if it can be made to work.

cpitclaudel · 2023-05-03T04:42:47Z

@cpitclaudel The Coq doc has 7 indexes. I don't see how .. index:: would know which one should get the entry.

See https://www.sphinx-doc.org/en/master/usage/restructuredtext/directives.html#directive-index, you give it the name of the index and what index entry to use.

cpitclaudel · 2023-05-03T04:43:54Z

Perhaps one of you can figure out how to do this.

I would love to help, but I won't have time to write code for this any time soon. If it's critical, I will try to make time. But maybe the .. index:: solution is enough? Let me know

jfehrle · 2023-05-03T20:32:40Z

If it's critical, I will try to make time.

Thanks. The immediate need for this for #17503 has gone away--they'll probably use different syntax that won't need an extra index entry.

But maybe the .. index:: solution is enough?

I looked at the referenced Sphinx doc twice and closely but I don't see how you specify the name of the index. Is it something like :name:??

cpitclaudel · 2023-05-03T23:09:56Z

No, you're right and I was wrong. .. index only inserts entries in the main index...

gares · 2023-06-30T12:05:47Z

Not ready for 8.18, postponing to 8.19

SkySkimmer · 2023-11-22T14:55:13Z

It seems this PR stalled months ago, I'm removing the milestone.

SkySkimmer · 2024-04-17T14:18:39Z

Doesn't work and stalled, reopen if there's progress

jfehrle added the kind: documentation Additions or improvement to documentation. label Apr 18, 2023

jfehrle added this to the 8.18+rc1 milestone Apr 18, 2023

jfehrle requested a review from a team as a code owner April 18, 2023 16:44

coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Apr 18, 2023

jfehrle mentioned this pull request Apr 18, 2023

Add head reduction flags (lazy head beta etc) #17503

Merged

Zimmi48 requested changes Apr 19, 2023

View reviewed changes

jfehrle force-pushed the extend_name_in_doc branch from a3b8296 to c317b58 Compare April 19, 2023 23:28

Zimmi48 approved these changes Apr 26, 2023

View reviewed changes

Zimmi48 added the needs: fixing The proposed code change is broken. label Apr 26, 2023

Support multiple :name:s with multiple signatures for .. tacn::

a583075

jfehrle force-pushed the extend_name_in_doc branch from c317b58 to a583075 Compare May 2, 2023 03:56

jfehrle removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label May 2, 2023

This doesn't work, either

9a26300

coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label May 2, 2023

gares modified the milestones: 8.18+rc1, 8.19+rc1 Jun 30, 2023

SkySkimmer removed this from the 8.19+rc1 milestone Nov 22, 2023

SkySkimmer closed this Apr 17, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Support multiple :name:s with multiple signatures for .. tacn:: #17507

Support multiple :name:s with multiple signatures for .. tacn:: #17507

jfehrle commented Apr 18, 2023 •

edited

Zimmi48 left a comment •

edited

Zimmi48 Apr 19, 2023

jfehrle Apr 19, 2023

Zimmi48 Apr 19, 2023

jfehrle Apr 19, 2023

Zimmi48 Apr 26, 2023

Zimmi48 Apr 19, 2023

jfehrle Apr 19, 2023

jfehrle commented Apr 19, 2023 •

edited

cpitclaudel commented Apr 19, 2023

jfehrle commented Apr 19, 2023

cpitclaudel commented Apr 24, 2023

Zimmi48 commented Apr 26, 2023

Zimmi48 left a comment

jfehrle commented May 2, 2023

Zimmi48 commented May 2, 2023

jfehrle commented May 2, 2023

jfehrle commented May 2, 2023

cpitclaudel commented May 3, 2023

cpitclaudel commented May 3, 2023

jfehrle commented May 3, 2023

cpitclaudel commented May 3, 2023

gares commented Jun 30, 2023

SkySkimmer commented Nov 22, 2023

SkySkimmer commented Apr 17, 2024

Support multiple :name:s with multiple signatures for .. tacn:: #17507

Support multiple :name:s with multiple signatures for .. tacn:: #17507

Conversation

jfehrle commented Apr 18, 2023 • edited

Zimmi48 left a comment • edited

Choose a reason for hiding this comment

Zimmi48 Apr 19, 2023

Choose a reason for hiding this comment

jfehrle Apr 19, 2023

Choose a reason for hiding this comment

Zimmi48 Apr 19, 2023

Choose a reason for hiding this comment

jfehrle Apr 19, 2023

Choose a reason for hiding this comment

Zimmi48 Apr 26, 2023

Choose a reason for hiding this comment

Zimmi48 Apr 19, 2023

Choose a reason for hiding this comment

jfehrle Apr 19, 2023

Choose a reason for hiding this comment

jfehrle commented Apr 19, 2023 • edited

cpitclaudel commented Apr 19, 2023

jfehrle commented Apr 19, 2023

cpitclaudel commented Apr 24, 2023

Zimmi48 commented Apr 26, 2023

Zimmi48 left a comment

Choose a reason for hiding this comment

jfehrle commented May 2, 2023

Zimmi48 commented May 2, 2023

jfehrle commented May 2, 2023

jfehrle commented May 2, 2023

cpitclaudel commented May 3, 2023

cpitclaudel commented May 3, 2023

jfehrle commented May 3, 2023

cpitclaudel commented May 3, 2023

gares commented Jun 30, 2023

SkySkimmer commented Nov 22, 2023

SkySkimmer commented Apr 17, 2024

jfehrle commented Apr 18, 2023 •

edited

Zimmi48 left a comment •

edited

jfehrle commented Apr 19, 2023 •

edited