[ admin ] first steps towards leaving CHANGELOG hell (re #521)

[gallais]

I currently only support some basic functionalities. If we are happy with the design I'll add all of the categories we are currently using. I am open to renaming the directories (it's a matter of changing a variable):

• each PR is associated to a directory PRDIR in changes/
• each PR may declare:
  • deprecations for module M.N.P in changes/PRDIR/deprecated/M.N.P (two names per line, meaning the first got renamed to the second)
  • additions in module M.N.P in changes/PRDIR/new/M.N.P (one declaration per line)
  • highlights in changes/PRDIR/highlights (paragraphs are separated by empty lines)
  • bug fixes in changes/PRDIR/bugfixes/FILE each FILE contains a section for the bugfix part of the changelog; the others file is special: each paragraph (separated by empty lines) is an item and these get grouped across PRs under the #### Others section header.
  • breaking changes in changes/PRDIR/breaking/FILE with the same special treatment of the file others described for bugfixes

The main function explores all of the changes/PRDIR directories and merges the contributions of each PR, outputting something like this (based on the current content of the changes/testN/ directories I have added as illustrations):

Highlights
----------
* A highlight

* My super cool shiny feature

* Btw, did you know that you can
  have highlights
  spanning multiple lines?
  As long as you are not skipping lines,
  it's all good.

* Otherwise It'll start a new one.

Bug fixes
---------

#### `_<_` in `Data.Integer`

* The definition of `_<_` in `Data.Integer` often resulted in unsolved metas
  when Agda had to infer the first argument. This was because it was
  previously implemented in terms of `suc` -> `_+_` -> `_⊖_`.

* To fix this problem the implementation has therefore changed to:
  ```agda
  data _<_ : ℤ → ℤ → Set where
    -<+ : ∀ {m n} → -[1+ m ] < + n
    -<- : ∀ {m n} → (n<m : n ℕ.< m) → -[1+ m ] < -[1+ n ]
    +<+ : ∀ {m n} → (m<n : m ℕ.< n) → + m < + n
  ```
  which should allow many implicit parameters which previously had
  to be given explicitly to be removed.

* All proofs involving `_<_` have been updated correspondingly

* For backwards compatibility the old relations still exist as primed versions
  `_<′_` as do all the old proofs, e.g. `+-monoˡ-<` has become `+-monoˡ-<′`,
  but these have all been deprecated and may be removed in some future version.

* Migrating code might require lemmas relating `m < n` and `m <′ n`/`suc m ≤ n`;
  such lemmas have unfortunately only been added in 1.3.


#### Other

* Changed the definition of `_⊓_` for `Codata.Conat`; it was mistakenly using
  `_⊔_` in a recursive call.

* Changed the type of `max≈v⁺` in `Data.List.Extrema`; it was mistakenly talking
  about `min` rather than `max`.

Non-backwards compatible changes
--------------------------------

* Version 1.1 in the library added irrelevance to various places in the library.
  Unfortunately this exposed the library to several irrelevance-related bugs.
  The decision has therefore been taken to roll-back these additions until
  irrelevance is more stable. In particular it has been removed from
  `_%_`, `_/_`, `_div_`, `_mod_` in `Data.Nat.DivMod` and from `fromℕ≤`,
  `inject≤` in `Data.Fin.Base`.

* The proofs `isPreorder` and `preorder` have been moved from the `Setoid`
  record to the module `Relation.Binary.Properties.Setoid`.

* The function `normalize` in `Data.Rational.Base` has been reimplemented
  in terms of a direct division of the numerator and denominator by their
  GCD. Although less elegant than the previous implementation, it's
  reduction behaviour is much easier to reason about.

Deprecated names
----------------

The following deprecations have occurred as part of a drive to improve
consistency across the library. The deprecated names still exist and
therefore all existing code should still work, however use of the new
names is encouraged. Although not anticipated any time soon, they may
eventually be removed in some future release of the library. Automated
warnings are attached to all deprecated names to discourage their use.

* In `Data.List.Relation.Unary.All.Properties`:
  ```agda
  Any¬→¬All ↦ Any¬⇒¬All
  ```

New modules
-----------

* Added a formalisation of fresh lists and their operations


  ```agda
  Data.List.Fresh
  Data.List.Fresh.Properties
  Data.List.Fresh.Relation.Unary.All
  ```

* Added new modules to produce textual
  representations
  of common data
  structures.


  ```agda
  Text.Tabular.Core
  Text.Tabular.Vec
  Text.Tabular.List
  
  Text.Pretty.Core
  Text.Pretty
  
  Text.Tree.Linear
  ```


#### Other

  ```agda
  Data.Tree.Rose
  Data.Tree.Rose.Properties
  ```

Other minor additions
---------------------

* New definitions in `Data.List.Base`:
  ```agda
  _?∷_  : Maybe A → List A → List A
  _∷ʳ?_ : List A → Maybe A → List A
  ```

* New definitions in `Data.String.Base`:
  ```agda
  padLeft  : Char → ℕ → String → String
  padRight : Char → ℕ → String → String
  padBoth  : Char → Char → ℕ → String → String
  
  data Alignment : Set where Left Center Right : Alignment
  fromAlignment  : Alignment → ℕ → String → String
  
  rectangle  : Vec (ℕ → String → String) n → Vec String n → Vec String n
  rectangleˡ : Char → Vec String n → Vec String n
  rectangleʳ : Char → Vec String n → Vec String n
  rectangleᶜ : Char → Char → Vec String n → Vec String n
  ```

[MatthewDaggitt]

Thanks so much for putting it together. Although it looks great, I guess I have a slight concern about how difficult are new contributors going to find it to use? Currently not only are there a list of magic directory names they have to learn, it looks like the files in each directory type have their own associated special syntax.

I think some of my concerns might be ameliorated by not having a directory per PR. If we just had:

• changes/deprecated
• changes/new
• changes/highlights
• etc.

and contributors just added new files in the relevant folders, then: a) they would no longer be responsible for knowing the magic folder names b) it would be easy to find the required syntax just by looking at other entries in that folder

It should be easy enough to recover which PR the file originated from by looking at the git history of the files? Maybe I'm missing something though :smile:

[gallais]

Good idea. I was planning to write a small tool generating a changes/PRDIR with sample files but this will be much more easy to explore.

[MatthewDaggitt]

Thanks :+1: Other minor thoughts:

• we might need a folder name a little more descriptive than new for minor additions as we will also want a section for new sets of modules right? Perhaps something like minor_additions and new_modules?
• I'm imagining that upon release we'll generate the final changelog then commit it into the CHANGELOG/ folder and then delete all the individual entries rather than keeping them around?

[gallais]

Re new, that was a first draft but I am going to go through the last 2 or 3 changelogs, see what the structure is and try to get as close to it as possible.

Re CHANGELOG itself, I agree that it's not worth keeping the files once the file for the released version has been generated.

[JacquesCarette]

[Catching up on backlog of things]. This looks really great - and should really help with the merge problems with CHANGELOG. And, with the latest changes, seems quite straightforward too.

[MatthewDaggitt]

Yup it's looking good. I suggest that we should adopt it once v1.3 has been released.

[MatthewDaggitt]

Right, now that v1.3 is out the way we should merge this in and start using it as soon possible. @gallais any chance you could add some instructions in HACKING.md and then merge this in?

[MatthewDaggitt]

@gallais I appreciate you have a ton of other things on your place right now 😄 In the meantime would you mind me merging some of the other PRs in using the old system?

[gallais]

Go for it. I should have shipped my thesis by Monday so my evenings will soon again be available.

[MatthewDaggitt]

Go for it. I should have shipped my thesis by Monday so my evenings will soon again be available.

Haha, you haven't exactly been inactive for these past couple of weeks! I think I was at my most productive for other things in the final few weeks of mine 😉

[MatthewDaggitt]

Having muddled along for three years without any additional complaints of people pushing for this to be merged, I think evidence suggests that maybe this piece of infrastructure is over-complicating things.

I'm therefore going to close this. If there are any objections then please feel free to re-open.