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

Release Agda 2.6.3 #6055

Closed
jespercockx opened this issue Aug 27, 2022 · 114 comments
Closed

Release Agda 2.6.3 #6055

jespercockx opened this issue Aug 27, 2022 · 114 comments
Labels
not-in-changelog This issue should not be listed in the changelog. release Concerning the release process and releases (not in changelog)
Milestone

Comments

@jespercockx
Copy link
Member

It would be good to work towards a release of 2.6.3 before the next Agda meeting, i.e. by the end of October.

To get us started, I went through all the issues with milestone 2.6.3 and moved many of them to either the icebox or the (newly created) "later" milestone, which is intended for issues that we are planning to fix in an upcoming release but not the next one. If you can, please take a look at the issues with that new milestone and comment or reassign the milestone if you disagree.

This currently leaves us with 39 issues that still have the 2.6.3 milestone, perhaps it would be good to restart the weekly online developer meetings to discuss who can work on which of these issues and which ones could be postponed. @UlfNorell @andreasabel @nad @plt-amy @Saizan since you are currently assigned to one or more of the issues with milestone 2.6.3, would you be available for a meeting in the coming week, perhaps Wednesday afternoon? (What time zone are you in @plt-amy ?)

@jespercockx jespercockx added not-in-changelog This issue should not be listed in the changelog. release Concerning the release process and releases (not in changelog) labels Aug 27, 2022
@jespercockx jespercockx added this to the 2.6.3 milestone Aug 27, 2022
@plt-amy
Copy link
Member

plt-amy commented Aug 27, 2022

I'm in GMT-3 (America/Sao_Paulo), and Wednesday works for me 🙂

@jespercockx
Copy link
Member Author

Let's have a meeting on Wednesday at 15:00 (GMT+2) / 10:00 (GMT-3) then. I'll send you the details in private.

@jespercockx
Copy link
Member Author

Next meeting: October 5th

@jespercockx
Copy link
Member Author

There are just three open issues left (#5702 #6047 and #6220) so we could start to prepare a release candidate. @asr do you perhaps have time this week to assist with the release?

@andreasabel
Copy link
Member

There is lots of closed issues without milestone which should potentially be added to 2.6.3, so that they appear in the changelog. I get started on this.

@andreasabel
Copy link
Member

There is lots of closed issues without milestone which should potentially be added to 2.6.3, so that they appear in the changelog. I get started on this.

I am done going through the relevant issues without a milestone and assigned these. Fingers crossed, we should now not have any issue closed by 2.6.3 which is not on the milestone.

@andreasabel
Copy link
Member

There are just three open issues left (#5702 #6047 and #6220) so we could start to prepare a release candidate.

Now there is only #6220 left from this list. We could start a release candidate as soon as @nad 's PR #6221 has landed in master, and the other hot PRs have cooled. Once we forked a release branch, adding stuff is extra work, so I'd do the fork not too early.

@andreasabel
Copy link
Member

andreasabel commented Oct 24, 2022

This is the list of closed issues currently computed by closed-issues-for-milestone 2.6.3. We should check for correct issue descriptions, whether these issues should appear in the changelog, and whether the changelog contains more detailed information when necessary:

  • #394: Syntax binders with multi-argument lambdas
    (has changelog)
  • #957: Auto missing support for Copatterns
    (has changelog)
  • #1625: Remove "--experimental" from "--experimental-lossy-unification"
    (has changelog)
  • #3714: Rename inc/ouc everywhere
    (changelog: 091fdf5163) @plt-amy
  • #4103: Rewrite rule rejected because of projection likeness
  • #4384: Rewrite rules with interval arguments are not supported
    (has changelog)
  • #4506: Lack of unicode support in locale may result in uncaught IOException
    needs changelog: new option --transliterate @nad
  • #4701: A compiler for Cubical Agda programs where all cubical parts have been marked as erased
    (has changelog)
  • #4725: Program rejected due to moved dot pattern
  • #4755: Rewrite rule on constructor uses wrong type for matching
  • #4763: Unquote anonymous copattern involving path
  • #4778: Expansion of ellipsis no longer faithful to what the user wrote
  • #4786: Should the parameters be marked as erased in the types of constructors and projections?
    (has changelog)
  • #5191: Unifier can use erased variables in non-erased data parameters
  • #5293: C-c C-s (solve constraints) infers the incorrect module to project from
  • #5378: Internal error with tactic on record field
  • #5427: Remove support for subtyping for erasure and irrelevance
    (has changelog)
  • #5448: Should the predicate be erasable in the subst rule (without-K)
  • #5462: Internal error caused by a REWRITE
  • #5468: Disallow certain forms of pattern matching when an index is erased
  • #5525: Duplicate entries in executables file lead to undefined behavior
  • #5551: Panic when showing module contents with pattern synonym
  • #5563: Allow erased names in the type signatures of let-bound definitions
  • #5581: Lexical error with tab character in literate Agda text
  • #5589: Internal error with REWRITE of function from path
  • #5634: Restricting the DOT backend to specific libraries
    (has changelog)
  • #5644: One can override .agda-lib files in "sneaky" ways
  • #5661: Cubical does not ensure EQUIVFUN has left inverse
  • #5681: "Panic: uncaught pattern violation" on record with hole sort
  • #5702: Can't case split an HitInt with some already existing cases
  • #5715: Proposal: Use Telescope for getContext, inContext, and extendContext
  • #5727: Reducing universe levels before checking is not sufficient
  • #5728: Internal error when pattern matching on ... in with statement without providing a pattern match
  • #5731: Instantiated meta-variables in interfaces?
    (has changelog)
  • #5734: Relevance check in reflection
  • #5751: json interaction produces Haskell output for SolveAll
  • #5760: Some code related to Cubical Agda runs also when the K rule is on
  • #5763: Internal parser error using syntax rules
  • #5765: Erasure check failure when pattern matching on refl in erased definition
  • #5769: Parameter arguments of projections of instance-opened record type are not erased
  • #5770: Option to erase record parameters in record module without erasing them as arguments to the type
    (has changelog)
  • #5775: JSON interaction produces fully qualified terms
  • #5781: No information about modules in output for -vprofile.modules:10
    (has changelog)
  • #5794: Prelude.!!: index too large
  • #5801: Make it possible to limit how many times the syntactic equality shortcut is allowed to fail
  • #5823: Loop on eta record
  • #5828: Panic when trying to automatically fill a hole with -r in the presence of a pattern synonym.
    - #5843: Proposal: new flag --cubical-compatible replacing --without-K
  • #5845: Internal error caused by abstracting variables
  • #5848: Internal error with --confluence-check
  • #5850: Warn about useless hiding in variable declaration
  • #5856: Lambda with irrefutable pattern is not rejected when used on Path
  • #5875: Instance Search breaks Termination Highlighting
  • #5876: GHC 9.0.2 missing warning: -Wunicode-bidirectional-format-characters
  • #5891: SizeUniv : SizeUniv is inconsistent
  • #5901: Use emacs --batch mode in agda-mode setup
  • #5920: Erased constructors are not treated correctly
  • #5922: Unexpected failure of termination checking for reflection-generated code
  • #5923: Internal error in rewriting
  • #5930: Support GHC 9.2.3
  • #5932: The flag Werror=unrecognised-warning-flags does not turn unrecognised warnings on fatal errors
  • #5944: Internal error in rewriting with --two-level
  • #5953: Recursor of inductive-inductive type does not pass termination check in Cubical Agda
  • #5955: Composition of Glue Type (Seemingly) Causes Infinite Loop
  • #5956: Cubical Agda crashes when interactively normalizing J for equivalences
  • #5966: Performance issues/opportunities involving hash tables
  • #5989: Internal error when using function whose type contains private tactic
  • #6003: de Bruijn index out of scope when rewriting
  • #6006: Internal error rewriting with holes
  • #6015: Pi types with different domain finiteness should not be equal
  • #6019: Support GHC 9.2.4
  • #6022: Private bindings in imported modules defeat check for binding of primIdFace/primIdPath
  • #6042: De Bruijn index out of scope when rewriting without-K
  • #6043: de Bruijn error on unexpected implicit argument
  • #6049: Separate flags for "compatible with univalence" and "compatible with Cubical Agda"
  • #6059: Strange code in the termination checker
  • #6066: The meaning of pattern without no-eta-equality shoud be documented
  • #6067: Another de Bruijn error in rewriting
  • #6073: Constraint solving does not honour singleton types
  • #6074: piSort/funSort of IUniv should be blocked on the codomain
  • #6076: Minibuffer display for \; is strange
  • #6080: A space leak due to absName
  • #6082: Elaborate-and-give does not respect --postfix-projections
  • #6093: Different NaN on M1 mac
  • #6095: Duplicated pattern causes error only when defining an unnamed module
  • #6096: Should n be size tel?
  • #6108: Higher constructors can trick the productivity checker
    (has changelog)
  • #6112: Internal error: non-confluent rewriting to singletons
  • #6128: Stack CI times out for Windows
  • #6145: Avoid recomputing SourceToModule maps
  • #6205: Internal error with withReconstructed
  • #6220: Should README modules still be supported?

Issues that get removed from the changelog by adding suitable not-in-changelog tags are striked out.
After finalizing this list, I'd like to structure it into features, regression fixes (grouped by Agda version that introduced the regression), and other bug fixes.

@plt-amy
Copy link
Member

plt-amy commented Oct 24, 2022

@andreasabel What needs to be done re.

We should check for correct issue descriptions

this?

@andreasabel
Copy link
Member

andreasabel commented Oct 24, 2022

@plt-amy : I meant that if an issue has a non-descriptive title, go there and edit it (don't edit it in the list above).
And then, some issues that add new features to Agda (rather than being mere bug fixes) need a changelog entry explaining the new feature and how to use it (or link to the docs).

@nad
Copy link
Contributor

nad commented Oct 24, 2022

  • #4506: Lack of unicode support in locale may result in uncaught IOException
    needs changelog: new option --transliterate @nad

Do you really want to advertise this hack (which is documented in the user manual)? The option is included as a (not very good) workaround for those who encounter error messages like "commitBuffer: invalid argument (invalid character)". If that error message is printed, then Agda will hopefully inform the user about possible workarounds, including the use of --transliterate:

agda/src/full/Agda/Main.hs

Lines 337 to 355 in 1a89181

, "This error may be due to the use of a locale or code page that does not"
, "support some character used in the program being type-checked."
, ""
, "If it is, then one option is to use the option --transliterate, in which"
, "case unsupported characters are (hopefully) replaced with something else,"
, "perhaps question marks. However, that could make the output harder to"
, "read."
, ""
, "If you want to fix the problem \"properly\", then you could try one of the"
, "following suggestions:"
, ""
, "* If you are using Windows, try switching to a different code page (for"
, " instance by running the command 'CHCP 65001')."
, ""
, "* If you are using a Unix-like system, try using a different locale. The"
, " installed locales are perhaps printed by the command 'locale -a'. If"
, " you have a UTF-8 locale installed (for instance sv_SE.UTF-8), then you"
, " can perhaps make Agda use this locale by running something like"
, " 'LC_ALL=sv_SE.UTF-8 agda <...>'."

@andreasabel
Copy link
Member

Do you really want to advertise this hack (which is documented in the user manual)?

Fine with me if you want to keep it under the radar.

plt-amy added a commit that referenced this issue Oct 24, 2022
Also removes the mention of copatterns not being supported from the Agsy
docs
@asr
Copy link
Member

asr commented Oct 25, 2022

@asr do you perhaps have time this week to assist with the release?

Yes. I'll prepare the RC.

@asr
Copy link
Member

asr commented Oct 25, 2022

In the CHANGELOG for 2.6.2.2 (and other versions too) we included a section with highlights. Could someone add some highlights for 2.6.3?

@asr
Copy link
Member

asr commented Oct 25, 2022

Now there is only #6220 left from this list. We could start a release candidate as soon as @nad 's PR #6221 has landed in master, and the other hot PRs have cooled. Once we forked a release branch, adding stuff is extra work, so I'd do the fork not too early.

It seems we are ready for creating the release branch. Right?

@andreasabel
Copy link
Member

andreasabel commented Oct 25, 2022

It seems we are ready for creating the release branch. Right?

There are some PRs left with milestone 2.6.3 which I expect to land very soon. You could wait for these to save you some cherry-picking and keep a simpler commit history.

There are also

@nad
Copy link
Contributor

nad commented Oct 25, 2022

I just moved issue #5577 to the 2.6.3 milestone.

@andreasabel
Copy link
Member

Updated list of currently closed issues in for the 2.6.3 changelog (doesn't include #5577 and other to-be-closed issues):

Regressions in Agda 2.6.0

  • #5875: Instance Search breaks Termination Highlighting
  • #6095: Ambiguous pattern synonyms broken with anonymous module

Regressions in Agda 2.6.1

Internal errors triggered by rewriting:

  • #5923: Internal error in rewriting
  • #6003: de Bruijn index out of scope when rewriting
  • #6006: Internal error rewriting with holes
  • #6042: De Bruijn index out of scope when rewriting without-K
  • #6043: de Bruijn error on unexpected implicit argument
  • #6067: Another de Bruijn error in rewriting

Regressions in Agda 2.6.2

  • #4725: Cubical Agda: Program rejected by termination checker due to moved dot pattern
  • #5681: Panic on record declaration with unknown sort
  • #5727: Reducing universe levels before checking is not sufficient
  • #5728: Internal error when pattern matching on ... in with statement without providing a pattern match
  • #5845: Internal error caused by abstracting variables
  • #5922: Failure of termination checking for reflection-generated code due to data projections
  • #5953: Recursor of inductive-inductive type does not pass termination check in Cubical Agda
  • #5955: Composition of Glue Type Causes Infinite Loop

Other bug fixes and new features

  • #394: Syntax binders with multi-argument lambdas
  • #957: Auto missing support for Copatterns
  • #1625: Remove "--experimental" from "--experimental-lossy-unification"
  • #3714: Rename inc/ouc everywhere
  • #4103: Rewrite rule rejected because of projection likeness
  • #4384: Rewrite rules with interval arguments are not supported
  • #4506: Lack of unicode support in locale may result in uncaught IOException
  • #4701: A compiler for Cubical Agda programs where all cubical parts have been marked as erased
  • #4755: Rewrite rule on constructor uses wrong type for matching
  • #4763: Cubical Agda: Unquote anonymous copattern involving path
  • #4786: Should the parameters be marked as erased in the types of constructors and projections?
  • #5191: Unifier can use erased variables in non-erased data parameters
  • #5378: Internal error with tactic on record field
  • #5427: Remove support for subtyping for erasure and irrelevance
  • #5448: Should the predicate be erasable in the subst rule (without-K)
  • #5462: Internal error caused by a REWRITE on a projection-like function
  • #5468: Disallow certain forms of pattern matching when an index is erased
  • #5525: Duplicate entries in executables file lead to undefined behavior
  • #5551: Panic when showing module contents with pattern synonym
  • #5563: Allow erased names in the type signatures of let-bound definitions
  • #5581: Lexical error with tab character in literate Agda text
  • #5589: Internal error with REWRITE of function from path
  • #5634: Restricting the DOT backend to specific libraries
  • #5644: Library (.agda-lib) files below the project root
  • #5661: Cubical does not ensure EQUIVFUN has left inverse
  • #5702: Can't case split an HitInt with some already existing cases
  • #5715: Reflection: Use Telescope for getContext, inContext, and extendContext
  • #5731: Performance: Instantiated meta-variables in interface files
  • #5734: Relevance check in reflection
  • #5751: json interaction produces Haskell output for SolveAll
  • #5760: Some code related to Cubical Agda runs also when the K rule is on
  • #5763: Internal parser error using syntax rules
  • #5765: Erasure check failure when pattern matching on refl in erased definition
  • #5769: Parameter arguments of projections of instance-opened record type are not erased
  • #5770: Option to erase record parameters in record module without erasing them as arguments to the type
  • #5775: JSON interaction produces fully qualified terms
  • #5781: New flag --profile replaces verbosity option -vprofile
  • #5794: Agsy/Auto crashes with Prelude.!!: index too large
  • #5801: Make it possible to limit how many times the syntactic equality shortcut is allowed to fail
  • #5823: Singleton check loops on recursive eta record
  • #5828: Agsy/Auto panics with -r in the presence of a pattern synonym
  • #5848: Internal error with --confluence-check
  • #5850: Warn about useless hiding in variable declaration
  • #5856: Lambda with irrefutable pattern is not rejected when used on Path
  • #5891: SizeUniv : SizeUniv is inconsistent
  • #5901: Use emacs --batch mode in agda-mode setup
  • #5920: Erased constructors skipped in modality check
  • #5944: Internal error in rewriting with --two-level
  • #5956: Cubical Agda crashes when printing empty system
  • #5966: Performance enhancement: switching to vector-hashtables library
  • #5989: Dead-code elimination crashes function with private tactic argument
  • #6015: Pi types and Partial types should not be considered inter-convertible
  • #6022: Private bindings in imported modules defeat check for binding of primIdFace/primIdPath
  • #6049: Separate flags for "compatible with univalence" and "compatible with Cubical Agda"
  • #6059: Non-terminating function over tuples passed with --termination-depth=2
  • #6066: Document the meaning of pattern without no-eta-equality
  • #6073: Constraint solving does not honour singleton types
  • #6074: piSort/funSort of IUniv should be blocked on the codomain
  • #6076: Agda input mode (emacs): Minibuffer display for \; is strange
  • #6080: A space leak due to absName
  • #6082: Elaborate-and-give does not respect --postfix-projections
  • #6093: Different NaN on M1 mac
  • #6108: Higher constructors can trick the productivity checker
  • #6112: Internal error: non-confluent rewriting to singletons
  • #6145: Preformance enhancement for large projects: Avoid recomputing SourceToModule maps
  • #6194: The GHC backend sometimes compiles the wrong modules when --interaction is used
  • #6205: Internal error with withReconstructed

@nad
Copy link
Contributor

nad commented Oct 25, 2022

Should issues that are mentioned explicitly in the changelog be included in the list that is added during the release process?

@jespercockx
Copy link
Member Author

Usually we apply the label documented-in-changelog to them, which implies that they are not listed in the issue list.

@andreasabel
Copy link
Member

andreasabel commented Oct 25, 2022

Usually we apply the label documented-in-changelog to them, which implies that they are not listed in the issue list.

Ok, didn't remember this trick. I can apply this label accordingly to the issues with (has changelog).
EDIT: seems like someone else is already at it. That someone else, please also strike them out in #6055 (comment).

@nad
Copy link
Contributor

nad commented Oct 25, 2022

Usually we apply the label documented-in-changelog to them, which implies that they are not listed in the issue list.

I thought that enhancements were not part of the list, because enhancements are typically documented in the changelog.

Anyway, I've added documented-in-changelog too all issues that were documented in the changelog.

That someone else, please also strike them out in #6055 (comment).

Isn't that list automatically generated? I don't see the point of that exercise.

@andreasabel
Copy link
Member

Anyway, I've added documented-in-changelog too all issues that were documented in the changelog.

Thanks.

That someone else, please also strike them out in #6055 (comment).

Isn't that list automatically generated? I don't see the point of that exercise.

That list was originally automatically generated, but now is a manually maintained worklist.
The point of the exercise is to show in one glance that nothing was forgotten. E.g. you forgot to apply documented-in-changelog to #3714.

@nad
Copy link
Contributor

nad commented Oct 25, 2022

Issue #3714 is not mentioned in the changelog.

@andreasabel
Copy link
Member

Here:

agda/CHANGELOG.md

Lines 216 to 218 in 6b55111

* The builtin `SUBIN` is now exported from `Agda.Builtin.Cubical.Sub` as
**`inS`** rather than `inc`. Similarly, the internal modules refer to
`primSubOut` as `outS`. ([#6032](https://github.com/agda/agda/pull/6032))

asr added a commit that referenced this issue Jan 30, 2023
asr added a commit that referenced this issue Jan 30, 2023
asr added a commit that referenced this issue Jan 30, 2023
@asr
Copy link
Member

asr commented Jan 30, 2023

Agda 2.6.3 has been released. Great job every one!

@asr asr closed this as completed Jan 30, 2023
@nad
Copy link
Contributor

nad commented Jan 30, 2023

Is this not the experimental branch you're after?

Yes, more or less. The question is if the std-lib test should use this branch, or something like "v1.7.3".

JobPetrovcic pushed a commit to JobPetrovcic/agda that referenced this issue Apr 5, 2024
* Removed Cabal test-suite
* Removed -Werror
* Cleaning stack-XYZ.yaml files
  + Removed QuickCheck dependency
  + Removed tasty-* dependencies
  + Removed local package (src/size-solver)
JobPetrovcic pushed a commit to JobPetrovcic/agda that referenced this issue Apr 5, 2024
JobPetrovcic pushed a commit to JobPetrovcic/agda that referenced this issue Apr 5, 2024
JobPetrovcic pushed a commit to JobPetrovcic/agda that referenced this issue Apr 5, 2024
* Removed Cabal test-suite
* Removed -Werror
* Cleaning stack-XYZ.yaml files
  + Removed QuickCheck dependency
  + Removed tasty-* dependencies
  + Removed local package (src/size-solver)
JobPetrovcic pushed a commit to JobPetrovcic/agda that referenced this issue Apr 5, 2024
JobPetrovcic pushed a commit to JobPetrovcic/agda that referenced this issue Apr 5, 2024
JobPetrovcic pushed a commit to JobPetrovcic/agda that referenced this issue Apr 5, 2024
JobPetrovcic pushed a commit to JobPetrovcic/agda that referenced this issue Apr 5, 2024
* Removed Cabal test-suite
* Removed -Werror
* Cleaning stack-XYZ.yaml files
  + Removed QuickCheck dependency
  + Removed tasty-* dependencies
  + Removed local package (src/size-solver)

[ci skip]
JobPetrovcic pushed a commit to JobPetrovcic/agda that referenced this issue Apr 5, 2024
JobPetrovcic pushed a commit to JobPetrovcic/agda that referenced this issue Apr 5, 2024
JobPetrovcic pushed a commit to JobPetrovcic/agda that referenced this issue Apr 5, 2024
JobPetrovcic pushed a commit to JobPetrovcic/agda that referenced this issue Apr 5, 2024
* Removed Cabal test-suite
* Removed -Werror
* Cleaning stack-XYZ.yaml files
  + Removed QuickCheck dependency
  + Removed tasty-* dependencies
  + Removed package section

[ci skip]
JobPetrovcic pushed a commit to JobPetrovcic/agda that referenced this issue Apr 5, 2024
JobPetrovcic pushed a commit to JobPetrovcic/agda that referenced this issue Apr 5, 2024
JobPetrovcic pushed a commit to JobPetrovcic/agda that referenced this issue Apr 5, 2024
JobPetrovcic pushed a commit to JobPetrovcic/agda that referenced this issue Apr 5, 2024
    * Removed Cabal test-suite
    * Removed -Werror
    * Cleaning stack-XYZ.yaml files
      + Removed QuickCheck dependency
      + Removed tasty-* dependencies
      + Removed package section

[ci skip]
JobPetrovcic pushed a commit to JobPetrovcic/agda that referenced this issue Apr 5, 2024
JobPetrovcic pushed a commit to JobPetrovcic/agda that referenced this issue Apr 10, 2024
JobPetrovcic pushed a commit to JobPetrovcic/agda that referenced this issue Apr 10, 2024
JobPetrovcic pushed a commit to JobPetrovcic/agda that referenced this issue Apr 10, 2024
@andreasabel
Copy link
Member

andreasabel commented Oct 27, 2024

I just realized 2.6.3 was released with -Werror.
Not sure how this happened, I thought hackage would reject such a package.
But apparently, cabal check is happy with 2.6.3's Agda.cabal, so maybe it only complains if one has a global -Werror.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
not-in-changelog This issue should not be listed in the changelog. release Concerning the release process and releases (not in changelog)
Projects
None yet
Development

No branches or pull requests

8 participants