Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Allow the presence of type casts for return values in Ltac2. #13914

Merged
merged 4 commits into from Mar 23, 2021

Conversation

ppedrot
Copy link
Member

@ppedrot ppedrot commented Mar 8, 2021

Following popular demand from @MSoegtropIMC.

Kind: feature.

@ppedrot ppedrot requested a review from a team as a code owner March 8, 2021 17:55
@ppedrot
Copy link
Member Author

ppedrot commented Mar 8, 2021

I also need to tweak the syntax described in the refman, but I don't remember what's the recommended process for that. Should I regenerate it using the dedicated script? cc @jfehrle

@ppedrot ppedrot added part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge. kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. labels Mar 8, 2021
@ppedrot ppedrot added this to the 8.14+rc1 milestone Mar 8, 2021
Copy link
Contributor

@MSoegtropIMC MSoegtropIMC left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Except for the editorial comment on the change list, this looks good to me! Thanks for looking into it!

@MSoegtropIMC MSoegtropIMC self-assigned this Mar 8, 2021
@jfehrle
Copy link
Member

jfehrle commented Mar 8, 2021

I also need to tweak the syntax described in the refman

type_cast can spliced into the other productions, then add a sentence in the text descriptions below where type_cast is used, e.g. :n:`: @ltac2_type` casts the return value to the specified type.

All you need to do is:

  • Add the middle line shown below to common.edit_mlg
  • Run make doc_gram_rsts.
  • Edit ltac2.rst to add the sentence in two places near where the tool has already modified the file
| conversion
| type_cast
] (* end SPLICE *)

@ppedrot ppedrot requested a review from a team as a code owner March 10, 2021 11:21
@ppedrot
Copy link
Member Author

ppedrot commented Mar 10, 2021

Should be ready.

Copy link
Member

@Zimmi48 Zimmi48 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The doc update looks good. But was the parsing code reorganized recently? I'm surprised to see massive changes in the fullGrammar file.

@ppedrot
Copy link
Member Author

ppedrot commented Mar 10, 2021

This is the bane of autogenerated files not kept in track with the CI. We're bound to lag behind.

@Zimmi48
Copy link
Member

Zimmi48 commented Mar 10, 2021

Yep. I think we'll add this file to CI soon.

@jfehrle
Copy link
Member

jfehrle commented Mar 10, 2021

I'm surprised to see massive changes in the fullGrammar file.

Generally this file has been quite stable. Its order depends on the order in which the mlgs are specified on doc_grammar's command line. It looks like g_constr.mlg was moved to the beginning of the list. Just one block of about 500 lines was moved as a unit. GitHub's diff doesn't recognize that.

I think the underlying cause is that doc/tools/docgram/dune doesn't give the files in the same order that Makefile.doc did. It looks like the latter file was recently removed, exposing the different order.

This seems to be reversing a change that was just committed in #13707.

This is probably a one-time hiccup, but worth looking into if it happens frequently.

@Zimmi48
Copy link
Member

Zimmi48 commented Mar 11, 2021

I think the underlying cause is that doc/tools/docgram/dune doesn't give the files in the same order that Makefile.doc did. It looks like the latter file was recently removed, exposing the different order.

Indeed. Unfortunately, the order in doc/tools/docgram/dune is manually specified, whereas the one in Makefile.doc is automatic. I think we'll get rid of the former as soon as #13617 is in, because then the targets in Makefile.doc will be compatible with Dune.

@Zimmi48
Copy link
Member

Zimmi48 commented Mar 11, 2021

@MSoegtropIMC This is ready to merge from what I can tell.

@Zimmi48
Copy link
Member

Zimmi48 commented Mar 11, 2021

Actually wait a minute. We might want to fix the order in fullGrammar in this PR, considering the automatic order from Makefile.doc to be the correct one.

@Zimmi48
Copy link
Member

Zimmi48 commented Mar 11, 2021

The order I get from Makefile.doc is consistent with the one that I get from Dune. This is what happened in #13707 that is unexplained. Next time, I'll also make sure to review the changes to fullGrammar instead of blindly trusting these.

@jfehrle
Copy link
Member

jfehrle commented Mar 11, 2021

It looks like Makefile.doc was removed before the commit for #13707. I still have that file in my source tree even though it's not in git, so I've been using it for make doc_gram_rsts. If I run make doc_gram_rsts on that commit now, I get only a small update to fullGrammar (moving vernac_toplevel, about 10 lines).

If I hide that file, I can't do a make doc_gram_rsts because AFAIK that's not available without the changes in #13617. Until I have a way to run that and get results consistent with other developers, the best thing to do is to omit the fullGrammar changes from this PR and any other that has these undesired changes (or edit out the undesired changes). Otherwise we may end up with multiple commits that apply and reverse the block move.

I'll also make sure to review the changes to fullGrammar instead of blindly trusting these.

Sanity checking makes sense.

@jfehrle
Copy link
Member

jfehrle commented Mar 11, 2021

Looking into it a bit more, I see that Makefile.doc still exists here, and git log also shows it.
So I don't know what's going on. My IDE is acting as if the file isn't in Git. Not sure if or how that is related.

$ git checkout master
Already on 'master'
Your branch is up to date with 'upstream/master'.
$ git log Makefile.doc
commit 09a2becf1887575976252f5313daba5e2c59a682 (origin/sphinx_clean)
Author: Jim Fehrle <jim.fehrle@gmail.com>
Date:   Thu Dec 24 14:09:03 2020 -0800

    Clean ALL sphinx output files

commit da9fd81c887024e991467d4dd586661c4ca01022 (origin/prodn_logic)
Author: Jim Fehrle <jim.fehrle@gmail.com>
Date:   Sat Sep 12 20:54:22 2020 -0700

    Convert logic.rst to prodn

@Zimmi48
Copy link
Member

Zimmi48 commented Mar 11, 2021

It looks like the issue is on your side only, doesn't it? Then, there's no harm in committing this PR as is, since it only reverts an unwanted change.

@jfehrle
Copy link
Member

jfehrle commented Mar 11, 2021

Perhaps so. We should sanity-check updates to fullGrammar until we figure it out what happened/resolve the issue. At the moment I have no idea about the cause.

@Zimmi48
Copy link
Member

Zimmi48 commented Mar 18, 2021

@MSoegtropIMC I believe this PR is ready to merge. Sorry for the false alarm above but the conclusion was that nothing needed to change in this PR.

@MSoegtropIMC
Copy link
Contributor

Thanks for the reminder - I will likely do it today.

@ppedrot
Copy link
Member Author

ppedrot commented Mar 23, 2021

@MSoegtropIMC ping

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

4 participants