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.

Sign up for GitHub

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

Jump to bottom

Add dfs flag for typeclasses eauto #14693

Merged
merged 5 commits into from Jul 23, 2021
Merged

Add dfs flag for typeclasses eauto #14693

merged 5 commits into from Jul 23, 2021

Conversation

Alizter
Copy link
Contributor

@Alizter Alizter commented Jul 21, 2021 •
edited

Fixes / closes #13859

  • Added / updated test-suite.
  • Added changelog.
  • Added / updated documentation.
    • Updated documented syntax by running make -f Makefile.make doc_gram_rsts.

@Alizter Alizter added part: typeclasses The typeclass mechanism. kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. labels Jul 21, 2021
@Alizter Alizter requested review from a team July 21, 2021 17:58
@Alizter Alizter requested a review from a team as a code owner July 21, 2021 18:00
@Alizter Alizter requested review from a team and removed request for a team July 21, 2021 18:03
@Alizter
Copy link
Contributor Author

Alizter commented Jul 21, 2021

Should I update the documentation to talk about the new syntax?

@Alizter Alizter requested a review from cpitclaudel July 21, 2021 18:04
jfehrle
jfehrle requested changes Jul 21, 2021
View reviewed changes
Copy link
Member

@jfehrle jfehrle left a comment

Choose a reason for hiding this comment

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

Please update as described. The wording is a suggestion.

doc/changelog/04-tactics/14693-alizter+typeclasses-eauto-dfs-flag.rst Outdated Show resolved Hide resolved
doc/tools/docgram/orderedGrammar Outdated Show resolved Hide resolved
@Alizter Alizter force-pushed the alizter+typeclasses-eauto-dfs-flag branch 2 times, most recently from 74731fe to 3e69ce5 Compare July 21, 2021 20:01
@Alizter Alizter requested a review from jfehrle July 21, 2021 20:11
jfehrle
jfehrle reviewed Jul 21, 2021
View reviewed changes
Copy link
Member

@jfehrle jfehrle left a comment

Choose a reason for hiding this comment

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

Better, a few more nits.

doc/sphinx/addendum/type-classes.rst Outdated Show resolved Hide resolved
doc/sphinx/addendum/type-classes.rst Outdated Show resolved Hide resolved
@Alizter Alizter force-pushed the alizter+typeclasses-eauto-dfs-flag branch from b24f7d2 to 8376bfb Compare July 21, 2021 20:39
@Alizter Alizter requested a review from jfehrle July 21, 2021 20:39
jfehrle
jfehrle reviewed Jul 21, 2021
View reviewed changes
Copy link
Member

@jfehrle jfehrle left a comment

Choose a reason for hiding this comment

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

2 more small tweaks.

doc/sphinx/addendum/type-classes.rst Outdated Show resolved Hide resolved
doc/sphinx/addendum/type-classes.rst Outdated Show resolved Hide resolved
@Alizter Alizter force-pushed the alizter+typeclasses-eauto-dfs-flag branch from 8376bfb to 9fba97f Compare July 21, 2021 22:30
jfehrle
jfehrle approved these changes Jul 21, 2021
View reviewed changes
Copy link
Member

@jfehrle jfehrle 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 looks good

Zimmi48
Zimmi48 reviewed Jul 22, 2021
View reviewed changes
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.

It's great to include a test case, but ideally, this test case would check that the two modes actually do something different (right now, you can only manually inspect the debug output). The idea would be to choose goals which fail when run with the wrong mode (dfs or bfs) and succeed with the other. Then you could insert Fail 1: typeclasses eauto ... to assert this.

Otherwise, LGTM 😄

plugins/ltac/g_class.mlg Outdated Show resolved Hide resolved
@Alizter
Copy link
Contributor Author

Alizter commented Jul 22, 2021 •
edited

@Zimmi48 They shouldn't succeed on the wrong modes in the test case. The classes and values were picked carefully so that they fail when the wrong mode is given. Should I add a comment to the case making this clearer?

@Zimmi48
Copy link
Member

Zimmi48 commented Jul 22, 2021

That's what I expected when looking at the test case, so I wanted to suggest inserting the appropriate Fail statements. But when testing locally (with Coq 8.13.2), I was surprised to discover that the other mode also succeeded in these cases.

@Alizter
Copy link
Contributor Author

Alizter commented Jul 22, 2021

Oh, that's not supposed to happen. Let me take a look.

@Alizter
Copy link
Contributor Author

Alizter commented Jul 22, 2021

@Zimmi48 I'm confused, how are you testing this on 8.13? Could you give me something that doesn't work? I am unable to break it.

Alizter and others added 5 commits July 22, 2021 10:10
@Alizter
Added dfs option for typeclasses eauto.
c5d0179 
We allow passing a dfs flag to `typeclasses eauto`. Previously only
bfs could be passed which meant that if the global enviornment had dfs
set, there was no way to do `typeclasses eauto` using dfs locally.
@Alizter
Add test for typeclasses eauto {dfs|bfs}
f62b1ca 
We test `typeclasses eauto dfs` and `typeclasses eauto bfs` in both
global dfs or bfs environments.
@Alizter
Added to documented syntax.
a818067
@Alizter
Added description of bfs and dfs flags to doc of typeclasses eauto.
8322fdf
@Alizter @jfehrle
Updated changelog.
ca35997 
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
@Alizter Alizter force-pushed the alizter+typeclasses-eauto-dfs-flag branch from 9fba97f to ca35997 Compare July 22, 2021 09:10
@Alizter
Copy link
Contributor Author

Alizter commented Jul 22, 2021

In the test, typeclasses eauto will always succeed, its the following reflexivity that checks if it is correct. I've added some comments to the test to make it a bit clearer.

@Zimmi48
Copy link
Member

Zimmi48 commented Jul 22, 2021

how are you testing this on 8.13?

I was testing without the new syntax. But indeed, I hadn't really read the test precisely and I had missed that the reflexivity tactic was the one that should fail. Your added explanations are great!

Zimmi48
Zimmi48 approved these changes Jul 22, 2021
View reviewed changes
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.

I'll merge this PR tomorrow.

@Zimmi48 Zimmi48 self-assigned this Jul 22, 2021
@Zimmi48 Zimmi48 added this to the 8.15+rc1 milestone Jul 22, 2021
@Zimmi48
Copy link
Member

Zimmi48 commented Jul 23, 2021

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 22ee3a5 into coq:master Jul 23, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Zimmi48 Zimmi48 Zimmi48 approved these changes

@jfehrle jfehrle jfehrle approved these changes

@cpitclaudel cpitclaudel Awaiting requested review from cpitclaudel

Assignees

@Zimmi48 Zimmi48

Labels
kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. part: typeclasses The typeclass mechanism.
Projects
None yet
Milestone
8.15+rc1
Development

Successfully merging this pull request may close these issues.

Feature request: dfs flag for the typeclasses eauto tactic
3 participants
@Alizter @Zimmi48 @jfehrle