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

Fix #13739 - disable some warnings when calling Function. #13776

Merged
merged 1 commit into from Feb 3, 2021

Conversation

Matafou
Copy link
Contributor

@Matafou Matafou commented Jan 22, 2021

Kind: bug fix

Fixes / closes #13739 by disabling warnings when calling Function. It also fixes the warning about non truly recursive function.

The fix is not entirely satisfactory since

  1. Function should not build a Fix when the function is not recursive.
  2. Function should raise a warning f the user wrote e useless pattern variable. Only auto generated such variable should be innocuous.

This solution is however acceptable IMHO for the moment.

@Matafou Matafou requested a review from a team as a code owner January 22, 2021 13:51
lib/cWarnings.mli Outdated Show resolved Hide resolved
@Zimmi48 Zimmi48 added this to the 8.13.1 milestone Jan 22, 2021
@Zimmi48 Zimmi48 added kind: fix This fixes a bug or incorrect documentation. part: funind labels Jan 22, 2021
lib/util.mli Outdated Show resolved Hide resolved
@gares
Copy link
Member

gares commented Jan 25, 2021

The patch looks good to me.
I'd only add a test case based on #13739 in the test-suite/output directory to assert the warnings are not actually fired.

@Matafou do you have the time for this last improvement? Otherwise I can take care of it myself.

@Matafou
Copy link
Contributor Author

Matafou commented Jan 25, 2021

I will do it.

@Zimmi48
Copy link
Member

Zimmi48 commented Jan 26, 2021

@liyishuai / @Lysxia: when this PR is merged, you should be able to rely on the new CWarnings.with_warn function instead of the ad hoc code for doing the same thing at https://github.com/QuickChick/QuickChick/blob/56452d27dc978b477e1fc9bae598f1e1560839f1/plugin/quickChick.mlg#L147-L151.

@Matafou
Copy link
Contributor Author

Matafou commented Jan 27, 2021

I will do it.

Not yet done, I need to find some time to reproduce the second warning, to come up with an small example triggering it. see #13739.

@gares
Copy link
Member

gares commented Jan 27, 2021

No problem, but we could also be happy with a test for just one of the 3 warnings you disable (it will test that the whole machinery works).

Also added a generic way of temporarily disabling a warning.
Also added try_finalize un lib/utils.ml.
@Matafou
Copy link
Contributor Author

Matafou commented Feb 3, 2021

No problem, but we could also be happy with a test for just one of the 3 warnings you disable (it will test that the whole machinery works).

Did like this and rebased.

@gares
Copy link
Member

gares commented Feb 3, 2021

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 730e0f4 into coq:master Feb 3, 2021
@coqbot-app coqbot-app bot added this to Request 8.13.1 inclusion in Coq 8.13 Feb 3, 2021
gares added a commit to gares/coq that referenced this pull request Feb 19, 2021
@coqbot-app coqbot-app bot moved this from Request 8.13.1 inclusion to Shipped in 8.13.1 in Coq 8.13 Feb 22, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: fix This fixes a bug or incorrect documentation. part: funind
Projects
No open projects
Coq 8.13
Shipped in 8.13.1
Development

Successfully merging this pull request may close these issues.

Un-removable warning [unused-pattern-matching-variable] for pattern matching when using Functional Induction
4 participants