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

Add FEATURE_IDEAS.md #6284

Merged
merged 3 commits into from
Sep 1, 2021
Merged

Add FEATURE_IDEAS.md #6284

merged 3 commits into from
Sep 1, 2021

Conversation

TGWDB
Copy link
Contributor

@TGWDB TGWDB commented Aug 10, 2021

This adds FEATURE_IDEAS.md to gather together new features and research ideas
that otherwise would fill the issues/PR backlog. Also provide a simple
reference point for finding feature ideas or projects.

This now also combines the MINI_PROJECTS.md file into this one so there is a single location for all these kinds of ideas and projects.

Note that this would replace/close #28 #29 #40 #218 #265 #618 (and others as they are transitioned here).

  • Each commit message has a non-empty body, explaining why the change was made.
  • Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@TGWDB TGWDB added cleanup RFC Request for comment feature request labels Aug 10, 2021
Copy link
Member

@peterschrammel peterschrammel left a comment

Choose a reason for hiding this comment

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

I'd suggest to call the file FEATURE_IDEAS.md to make it clearer what its content is.

@codecov
Copy link

codecov bot commented Aug 10, 2021

Codecov Report

Merging #6284 (b8487d4) into develop (f8cca6c) will not change coverage.
The diff coverage is n/a.

Impacted file tree graph

@@           Coverage Diff            @@
##           develop    #6284   +/-   ##
========================================
  Coverage    75.91%   75.91%           
========================================
  Files         1514     1514           
  Lines       163984   163984           
========================================
  Hits        124485   124485           
  Misses       39499    39499           

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 2b3c737...b8487d4. Read the comment docs.

Copy link
Collaborator

@martin-cs martin-cs left a comment

Choose a reason for hiding this comment

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

I would rather not do things this way. There is already a mini-projects list:

#3930

which does get occasional updates:

#4119

It would be better to add to that than start a new file. However despite being the original author of many of these I think that issues are a much better way of tracking this sort of thing. They can be cross-referenced, have clearer updates from multiple people, integrate with the rest of how we work and have a much lower barrier to entry.

If this is a "number of open issues" issue then ... maybe a tag for "feature ideas" which can be excluded from the count?

@martin-cs
Copy link
Collaborator

( The content is good though, as is making this sort of thing better recorded. )

TGWDB added 3 commits August 29, 2021 12:07
This adds FEATURES.md to gather together new features and research ideas
that otherwise would fill the issues/PR backlog. Also provide a simple
reference point for finding feature ideas or projects.
This removes the two files for FEATURES and MINI_PROJECTS and
combines them into a single FEATURE_IDEAS file.
@TGWDB TGWDB marked this pull request as ready for review September 1, 2021 09:01
@TGWDB TGWDB changed the title Add FEATURES.md Add FEATURE_IDEAS.md Sep 1, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Refinement-based slicing
4 participants