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

Changelog should identify changes that impact user developments #15012

Open
ejgallego opened this issue Oct 10, 2021 · 4 comments
Open

Changelog should identify changes that impact user developments #15012

ejgallego opened this issue Oct 10, 2021 · 4 comments
Labels
kind: documentation Additions or improvement to documentation. kind: meta About the process of developing Coq.

Comments

@ejgallego
Copy link
Member

As of today, the Coq changelog doesn't distinguish between changes that impact compatibility at the .v file level, and those that don't.

This makes hard for users to analyze and identify possible compatibility impact when upgrading to a Coq version.

Other systems [for example OCaml] special mark those changes, and IMHO it would useful to do so for Coq too.

@ejgallego ejgallego added kind: documentation Additions or improvement to documentation. kind: meta About the process of developing Coq. labels Oct 10, 2021
@Zimmi48
Copy link
Member

Zimmi48 commented Oct 10, 2021

Could you be more specific on what you mean by impact (e.g. with examples)? We do already have a Changed category and we only include user-visible changes in the changelog.

@ejgallego
Copy link
Member Author

The wording used by OCaml is "changes that can break existing programs", for example see https://ocaml.org/releases/4.12.0.html#Changes

Our changes category seems more general, doesn't it?

@Zimmi48
Copy link
Member

Zimmi48 commented Oct 11, 2021

Yes, but I'm curious how frequently they are used for other purposes in practice. Skimming through the list of Changed entries, it seems to me that almost all the occurrences that I've looked can be qualified as "changes that can break existing programs" and the rare exceptions are mostly changelog items that were miscategorified (e.g. "Changed: Added the ability for coq_makefile to directly set the installation folders, through the COQLIBINSTALL and COQDOCINSTALL variables" which should have been "Added: Ability for coq_makefile to directly set the installation folders, through the COQLIBINSTALL and COQDOCINSTALL variables").

@Zimmi48
Copy link
Member

Zimmi48 commented Oct 11, 2021

FTR our types of changelog entries are taken from https://keepachangelog.com/en/1.0.0/.

@ejgallego ejgallego added this to Forward to Dune in Dune Jan 27, 2022
@Alizter Alizter added this to Infrastructure in User documentation May 17, 2022
@ejgallego ejgallego moved this from Forward to Dune to Ready to address in Dune Jul 7, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: documentation Additions or improvement to documentation. kind: meta About the process of developing Coq.
Projects
Dune
  
Ready to address
Status: Infrastructure
User documentation
  
Infrastructure
Development

No branches or pull requests

2 participants