Update pull_request_template.md

[mattulbrich]

Intended Change

Updated and improved the pull request template.

Removing the checkboxes which always (if unticked) indicated that the PR is only partially finished in the overview. Replaced by item list from which items can be deleted.

Refining the structure. Adding a new subsection "Plan".

Type of pull request

• There are changes to the deployment/CI infrastructure (gradle, github, ...)

Ensuring quality

n/a

Additional information and contact(s)

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

[codecov]

Codecov Report

All modified and coverable lines are covered by tests ✅

Project coverage is 37.85%. Comparing base (fb58c33) to head (bac61ee).

Additional details and impacted files

@@             Coverage Diff              @@
##               main    #3446      +/-   ##
============================================
- Coverage     37.85%   37.85%   -0.01%     
  Complexity    17042    17042              
============================================
  Files          2082     2082              
  Lines        127290   127290              
  Branches      21441    21441              
============================================
- Hits          48184    48183       -1     
  Misses        73194    73194              
- Partials       5912     5913       +1     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[wadoon]

Can we get rid of the not semantically-correctly used todo items?

• Yes
• No
• Maybe?

I find it very annoying if you look on a PR and Github says "5 out of 10 tasks done".

[WolframPfeifer]

Can we get rid of the not semantically-correctly used todo items?

* [ ]  Yes

* [ ]  No

* [ ]  Maybe?

I find it very annoying if you look on a PR and Github says "5 out of 10 tasks done".

Is this not exactly what the PR does?

[WolframPfeifer]

Thanks, I also find this very annoying. Unfortunately, checkboxes that are not task lists are not really supported by GitHub at the moment, even though this feature that was requested multiple times. One of these feature requests also mentioned a workaround: You can wrap checkboxes in a list, then they are not counted as tasks:

• • option 1
• • option 2
• • option 3
    While this may mess up the spacing a bit (conceptually, this is a list of lists then), we could also use this. However, I am also quite happy with the template suggested in this PR.

[mattulbrich]

I find it very annoying if you look on a PR and Github says "5 out of 10 tasks done".

That's the reason for the PR. If we have checkboxes than we should have them for things were 10/10 is the desired goal, and fewer should not be merged.