diff --git a/Agda.cabal b/Agda.cabal --- a/Agda.cabal +++ b/Agda.cabal @@ -1,6 +1,6 @@ cabal-version: 2.4 name: Agda -version: 2.8.0 +version: 2.8.0.1 build-type: Simple license: MIT license-file: LICENSE @@ -30,8 +30,9 @@ Emacs mode. tested-with: - GHC == 9.12.2 - GHC == 9.10.2 + GHC == 9.14.1 + GHC == 9.12.4 + GHC == 9.10.3 GHC == 9.8.4 GHC == 9.6.7 GHC == 9.4.8 @@ -44,6 +45,7 @@ CHANGELOG.md README.md doc/user-manual/agda.svg + doc/release-notes/2.8.0.md doc/release-notes/2.7.0.1.md doc/release-notes/2.7.0.md doc/release-notes/2.6.4.3.md @@ -89,8 +91,9 @@ doc/release-notes/2.2.0.md extra-source-files: - stack-9.12.2.yaml - stack-9.10.2.yaml + stack-9.14.1.yaml + stack-9.12.4.yaml + stack-9.10.3.yaml stack-9.8.4.yaml stack-9.6.7.yaml stack-9.4.8.yaml @@ -221,7 +224,7 @@ source-repository this type: git location: https://github.com/agda/agda.git - tag: v2.8.0 + tag: v2.8.0.1 -- Build flags --------------------------------------------------------------------------- @@ -295,48 +298,46 @@ -dsuppress-module-prefixes -ddump-to-file ghc-options: - -- ASR (2022-05-31). Workaround to Issue #5932. - -Wwarn - -Wwarn=cpp-undef - -Wwarn=deprecated-flags - -Wwarn=deriving-typeable - -Wwarn=dodgy-exports - -Wwarn=dodgy-foreign-imports - -Wwarn=dodgy-imports - -Wwarn=duplicate-exports - -Wwarn=empty-enumerations - -Wwarn=identities - -Wwarn=inaccessible-code - -Wwarn=inline-rule-shadowing - -Wwarn=missed-extra-shared-lib - -Wwarn=missing-fields - -Wwarn=missing-home-modules - -Wwarn=missing-methods - -Wwarn=missing-pattern-synonym-signatures - -Wwarn=missing-signatures - -Wwarn=noncanonical-monad-instances - -Wwarn=noncanonical-monoid-instances - -Wwarn=overflowed-literals - -Wwarn=overlapping-patterns --- -Wwarn=redundant-constraints - -Wwarn=simplifiable-class-constraints - -Wwarn=star-binder - -Wwarn=star-is-type - -Wwarn=tabs - -Wwarn=typed-holes - -Wwarn=unbanged-strict-patterns - -Wwarn=unrecognised-pragmas - -Wwarn=unrecognised-warning-flags - -Wwarn=unticked-promoted-constructors - -Wwarn=unused-do-bind - -Wwarn=unused-foralls - -Wwarn=warnings-deprecations - -Wwarn=wrong-do-bind + -Wcpp-undef + -Wdeprecated-flags + -Wderiving-typeable + -Wdodgy-exports + -Wdodgy-foreign-imports + -Wdodgy-imports + -Wduplicate-exports + -Wempty-enumerations + -Widentities + -Winaccessible-code + -Winline-rule-shadowing + -Wmissed-extra-shared-lib + -Wmissing-fields + -Wmissing-home-modules + -Wmissing-methods + -Wmissing-pattern-synonym-signatures + -Wmissing-signatures + -Wnoncanonical-monad-instances + -Wnoncanonical-monoid-instances + -Woverflowed-literals + -Woverlapping-patterns +-- -Wredundant-constraints + -Wsimplifiable-class-constraints + -Wstar-binder + -Wstar-is-type + -Wtabs + -Wtyped-holes + -Wunbanged-strict-patterns + -Wunrecognised-pragmas + -Wunrecognised-warning-flags + -Wunticked-promoted-constructors + -Wunused-do-bind + -Wunused-foralls + -Wwarnings-deprecations + -Wwrong-do-bind -- The following warning is an error in GHC >= 8.10. if impl(ghc < 8.10) ghc-options: - -Wwarn=implicit-kind-vars + -Wimplicit-kind-vars -- #6623: Turn off this (nameless) warning: -- "Pattern match checker exceeded (2000000) iterations in a case alternative." -- See: https://gitlab.haskell.org/ghc/ghc/-/issues/13464 @@ -345,42 +346,42 @@ if impl(ghc < 9.10) ghc-options: - -Wwarn=semigroup + -Wsemigroup -- The semigroup warning is deprecated in GHC 9.10 if impl(ghc >= 8.10) ghc-options: - -Wwarn=deriving-defaults - -Wwarn=redundant-record-wildcards - -Wwarn=unused-packages - -Wwarn=unused-record-wildcards + -Wderiving-defaults + -Wredundant-record-wildcards + -Wunused-packages + -Wunused-record-wildcards if impl(ghc >= 9.0) ghc-options: - -Wwarn=invalid-haddock + -Winvalid-haddock -- #6137: coverage checker works only sufficiently well from GHC 9.0 - -Wwarn=incomplete-patterns - -Wwarn=incomplete-record-updates - -Wwarn=overlapping-patterns + -Wincomplete-patterns + -Wincomplete-record-updates + -Woverlapping-patterns -- ASR (2022-04-27). This warning was added in GHC 9.0.2, removed -- from 9.2.1 and added back in 9.2.2. if impl(ghc == 9.0.2 || >= 9.2.2) ghc-options: - -Wwarn=unicode-bidirectional-format-characters + -Wunicode-bidirectional-format-characters if impl(ghc >= 9.2) ghc-options: - -Wwarn=operator-whitespace - -Wwarn=redundant-bang-patterns + -Woperator-whitespace + -Wredundant-bang-patterns if impl(ghc >= 9.4) ghc-options: - -Wwarn=type-equality-out-of-scope + -Wtype-equality-out-of-scope if impl(ghc >= 9.4 && < 9.10) ghc-options: - -Wwarn=forall-identifier + -Wforall-identifier -- The forall-identifier warning is deprecated in GHC 9.10 default-language: Haskell2010 @@ -497,17 +498,17 @@ -- This is currently LTS 16.31 (last for GHC 8.8.4). build-depends: -- Please keep in alphabetical order! - , aeson >= 1.4.7.1 && < 2.3 + , aeson >= 1.4.7.1 && < 2.4 , ansi-terminal >= 0.10.3 && < 1.2 , array >= 0.5.4.0 && < 0.6 , async >= 2.2.2 && < 2.3 - , base >= 4.13.0.0 && < 4.22 + , base >= 4.13.0.0 && < 4.23 , binary >= 0.8.7.0 && < 0.9 , blaze-html >= 0.9.1.2 && < 0.10 , boxes >= 0.1.5 && < 0.2 , bytestring >= 0.10.10.1 && < 0.13 , case-insensitive >= 1.2.1.0 && < 1.3 - , containers >= 0.6.2.1 && < 0.8 + , containers >= 0.6.2.1 && < 0.9 -- containers-0.6.3.1 adds IntSet.mapMonotonic, but its too young for GHC 8.8 , data-hash >= 0.2.0.1 && < 0.3 , deepseq >= 1.4.4.0 && < 1.6 @@ -530,9 +531,9 @@ , mtl >= 2.2.2 && < 2.4 , murmur-hash >= 0.1.0.9 && < 0.2 , nonempty-containers >= 0.3.4.1 && < 0.4 - , parallel >= 3.2.2.0 && < 3.3 + , parallel >= 3.2.2.0 && < 3.4 , peano >= 0.1.0.1 && < 0.2 - , pqueue >= 1.4.1.3 && < 1.6 + , pqueue >= 1.4.1.3 && < 1.8 , pretty >= 1.1.3.6 && < 1.2 , process >= 1.6.9.0 && < 1.7 , process-extras >= 0.7.4 && < 0.8 @@ -542,9 +543,9 @@ , STMonadTrans >= 0.4.5 && < 0.5 , strict >= 0.4.0.1 && < 0.6 -- module Data.Strict.Classes entered in strict-0.4 - , template-haskell >= 2.15.0.0 && < 2.24 + , template-haskell >= 2.15.0.0 && < 2.25 , text >= 1.2.4.0 && < 2.2 - , time >= 1.9.3 && < 1.15 + , time >= 1.9.3 && < 1.16 , transformers >= 0.5.6.2 && < 0.7 , unordered-containers >= 0.2.10.0 && < 0.3 , uri-encode >= 1.5.0.7 && < 1.6 @@ -1011,11 +1012,11 @@ th-lift-instances >= 0.1.18 && < 0.1.21 build-depends: - , base >= 4.13.0.0 && < 4.22 + , base >= 4.13.0.0 && < 4.23 , bytestring >= 0.10.10.1 && < 0.13 , directory >= 1.3.6.0 && < 1.4 , filelock >= 0.1.1.5 && < 0.2 , filepath >= 1.4.2.1 && < 1.6 , gitrev >= 1.3.1 && < 2 , process >= 1.6.9.0 && < 1.7 - , template-haskell >= 2.15.0.0 && < 2.24 + , template-haskell >= 2.15.0.0 && < 2.25 diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,639 +1,6 @@ -Release notes for Agda version 2.8.0 -==================================== - -Highlights ----------- - -* Agda is now a self-contained single binary. - -* Build all Agda files reachable from paths in the `.agda-lib` file with new flag `--build-library`. - -* Experimental support for polarity annotations with new flag `--polarity`. - -* Compile to JavaScript with ES6 module syntax with new flag `--js-es6`. - -* Errors now have an identifier and follow the GNU standard. - -Installation ------------- - -* Dropped support for GHC 8.6, added support for GHC 9.12. - -* Agda supports GHC versions 8.8.4 to 9.12.2. - -* The `agda` binary now contains everything to set itself up, - it need not be shipped with additional files. - - 1. The functionality of the `agda-mode` executable has been replicated - under the new option `--emacs-mode`. - The `agda-mode` executable is now deprecated. - References to `agda-mode` in your `.emacs` file should be replaced - by `agda --emacs-mode`. - - 2. Agda now contains all its data files, - like primitive and builtin modules, - supplements for the HTML and LaTeX backends, - the runtimes for the `JS` and `GHC` backends, - and the emacs mode. - - These will be written to the data directory - on the first invocation of `agda` or an invocation of - `agda --setup`, `agda --emacs-mode setup`, or `agda --emacs-mode compile`. - - The location of the data directory can be printed using - `agda --print-agda-data-dir` and can be controlled by the `use-xdg-data-home` - flag at build time and the `Agda_datadir` environment variable at runtime; see the - documentation for more information. - -* The Cabal/Stack custom installation `Setup.hs` has been removed - that previously generated the `.agdai` files for the builtin and primitive modules. - These will now be generated by Agda whenever they are needed, - just as for ordinary modules. - - This change might be **breaking** for packagers of Agda - as the packaging routines might need to be updated: in particular, - declarative build systems like Nix or Guix should generate the `.agdai` files - by invoking Agda at build time. - -* Pre-built binaries are available as release assets for the following platforms - - * Windows (x86-64) - * Linux (x86-64) - * macOS (x86-64) - * macOS (arm64) - - Installation instructions are provided in the Agda user manual. - -* The `optimise-heavily` build flag is now turned on by default. - - This requires more resources when building Agda, but leads to a faster Agda binary. - Should GHC run out of memory when building Agda, turn this flag off. - -* Added cabal build flag `dump-core` to save the optimised GHC Core code during - compilation of Agda. This can be useful for people working on improving the - performance of the Agda implementation. - -Pragmas and options -------------------- - -* **BREAKING**: Abbreviation of options, such as `--warning` to `--warn`, is no longer supported. - -* New main mode of operation `--build-library` (issue [#4338](https://github.com/agda/agda/issues/4338)). - Invoking `agda --build-library` will look for an `.agda-lib` file starting in the current directory. - It will then extract the `include` directories of this library, - collect all Agda files in these directories and their subdirectories, - and check all these files. - -* New option `--setup` that writes out the Agda data files (see above) - and can be used to regenerate them. - -* New option `--emacs-mode` to administer the Emacs mode - as previously done by the `agda-mode` executable. - -* Option `--local-interfaces` and warning `DuplicateInterfaceFiles` have been removed. - -* New option `--js-es6` for generating JavaScript with ES6 module syntax. - -* `DISPLAY` pragmas can now define display forms that match on defined names - beyond constructors ([issue #7533](https://github.com/agda/agda/issues/7533)). - Example: - ```agda - {-# DISPLAY Irrelevant Empty = ⊥ #-} - ``` - `Empty` used to be interpreted as a pattern variable, effectively installing - the display form `Irrelevant _ = ⊥`. - Now `Empty` is treated as a matchable name, as one would intuitively expect - from a display form. - As a consequence, only `Irrelevant Empty` is displayed as `⊥`, not just any - `Irrelevant A`. - -* A new **experimental** flag `--experimental-lazy-instances` causes - instance selection to be deferred until the type of the instance - constraint is determined enough to make an unamibiguous decision at - the discrimination tree level. This significantly improves performance - for cases where instances can be distinguished by rigid data. - - This flag will become the default in the future, but it is currently - **disabled by default** because it has unexpected interactions with - parts of the codebase (and macros) which rely on constraint solving - order (see e.g. [issue #7882](https://github.com/agda/agda/issues/7883) - and [issue #7847](https://github.com/agda/agda/issues/7847)). - -Warnings --------- - -* New warning `RewritesNothing` if a `rewrite` clause did not fire. - -* New deadcode warnings `FixingCohesion`, `FixingPolarity` and `FixingRelevance` - when wrong user-written attribute was corrected automatically by Agda. - -* New deadcode warning `InvalidDisplayForm` instead of hard error - when a display form is illegal (and thus ignored). - -* New warning `UnusedVariablesInDisplayForm` when DISPLAY pragma - binds variables that are not used. - Example: - ```agda - {-# DISPLAY List (Fin n) = ListFin #-} - ``` - Since pattern variable `n` is not used on the right hand side `ListFin`, - Agda throws a warning and recommeds to rewrite it as: - ```agda - {-# DISPLAY List (Fin _) = ListFin #-} - ``` - -* Unused `CATCHALL` pragmas now trigger `UselessPragma` warnings. - -* New deadcode warning `EmptyPolarityPragma` for POLARITY pragma without polarities. - E.g. triggered by `{-# POLARITY F #-}`. - -* New parser warnings `MisplacedAttributes`, `UnknownAttribute`, and `UnknownPolarity` - instead of hard parser errors. - -* New deadcode warning `TooManyPolarities` instead of hard error - when a POLARITY pragma gives polarities that exceed the known - arity of the postulate. - -* New deadcode warning `UselessTactic` when a `@tactic` attribute has no effect, - typically when it is attached to a non-hidden or instance argument. - -* New warning `WithClauseProjectionFixityMismatch` instead of hard error - when in a with-clause a projection is used in a different fixity - (prefix vs. postfix) than in its parent clause. - -* New error warning `TooManyArgumentsToSort` instead of hard error. - -* Warning `AbsurdPatternRequiresNoRHS` has been renamed to - `AbsurdPatternRequiresAbsentRHS`. - -* Warnings `OpenPublicAbstract` and `OpenPublicPrivate` have been replaced - by new warnings `OpenImportAbstract` and `OpenImportPrivate`. - -* Warning `NoGuardednessFlag` has been removed. - Instead Agda gives a hint when `--guardedness` would help with termination checking, - unless options `--sized-types` or `--no-guardedness` are set. - - -Polarity --------- - -* Support for polarity annotations can be enabled by the feature flag - `--polarity`. - - This flag is infective. - - Uses of variables bound with polarity annotations are checked through modal - typing rules, and the positivity checker has been expanded to take annotations - into account. This means that the following is now definable: - - ```agda - {-# OPTIONS --polarity #-} - - data Mu (F : @++ Set → Set) : Set where - fix : F (Mu F) → Mu F - ``` - -Syntax ------- - -Additions to the Agda syntax. - -* Add new literate agda: forester, see [#7403](https://github.com/agda/agda/pull/7403). - You will need the postprocessor [`agda-tree`](https://github.com/dannypsnl/agda-tree), - see Agda user manual on literate programming for more information. - -* It is now always possible to refer to the name of a record type's - constructor, even if a name was not explicitly specified. This is done - using the new `(Record name).constructor` syntax; - see [issue #6964](https://github.com/agda/agda/issues/6964) for the motivation. - -* The *left-hand-sides* of functions bound in a `let` expression can now - contain the same types of patterns that are allowed in lambda - expressions, in dependent function types, and in other `let` bindings. - - This means that - - ```agda - let - f : A → B → C - f p1 p2 = ... - in ... - ``` - - should be accepted exactly when, and have the same meaning as, - - ```agda - let - f : A → B → C - f = λ p1 p2 → ... - ``` - - See [#7572](https://github.com/agda/agda/pull/7572). - -Language --------- - -Changes to type checker and other components defining the Agda language. - -* **BREAKING**: The primitive "cubical identity type", previously - exported from `Agda.Builtin.Cubical.Id`, has been removed. Its - computational behaviour is exactly replicated by the user-definable - identity type, which is also exported from `Agda.Builtin.Equality`. - - See [agda/cubical#1005](https://github.com/agda/cubical/pull/1005) for - the PR removing it from the library, and - [#7652](https://github.com/agda/agda/pull/7652) for the compiler. - -* Inlining constructors no longer happens on the right-hand-sides of - `INLINE` functions. This allows using `INLINE` functions to define - "smart constructors" for record types which have the same reduction - behaviour as using the actual constructor would. Small example: - - ```agda - triple : Nat → Nat → Nat → Nat × Nat × Nat - {-# INLINE triple #-} - triple x y z = record { fst = x ; snd = y , z } - - ex = triple 1 2 3 - ``` - - Here, constructor inlining happens on the right hand side *of `ex`* - rather than of `triple`. - -Reflection ----------- - -Changes to the meta-programming facilities. - -* New reflection primitive: `checkFromStringTC : String → Type → TC Term` - - Parse and type check the given string against the given type, returning - the resulting term (when successful). - - -Library management ------------------- - -* **BREAKING**: Agda no longer accepts several `.agda-lib` files in the root - of an Agda project. - (Previously, it allowed this and took the union of their contents.) - - -Interaction and emacs mode --------------------------- - -* Agda's error messages now follow the [GNU standard](https://www.gnu.org/prep/standards/html_node/Errors.html). - To comply with this policy, line and column are now separated by a dot instead of comma. - The format of regular errors and error warnings follows this template: - - > _sourcefile_:_line1_._column1_-_line2_._column2_: error: [_ErrorName_] - > ... - > _error message_ - > ... - > when _error context_ - - _line2_ or even _column2_ can be missing, in some cases even the entire error location. - Internal errors might follow a different format. - - Warnings are printed in a similar format: - - > _sourcefile_:_line1_._column1_-_line2_._column2_: warning: -W[no]_WarningName_ - > ... - > _warning text_ - > ... - > when _warning context_ - -* Emacs: new face `agda2-highlight-cosmetic-problem-face` - for highlighting the new aspect `CosmeticProblem`. - -* Emacs: new face `agda2-highlight-instance-problem-face` - for highlighting the new aspect `InstanceProblem`. - -* When generating clauses after case splitting on a datatype defined in a parameterised module, - Agda now prints constructor names without a module prefix rather than fully qualified (see issue #3209). - This is only a surface-level fix, since Agda might still fail to find the properly qualified name for - the constructor in scope, but should at least make more sense in most situations. - -* New bindings for unicode 'tacks' (⟘⟙⟛⟝⟞⫫⫪) via \tack (as well as specialised names for each of them) - -Backends --------- - -* New `backendInteractTop/backendInteractHole` fields for providing backend-specific interaction commands - (run with keyboard shortcut `C-c C-i`). - -* Buggy unused argument optimization removed from the JavaScript backend - ([PR #7509](https://github.com/agda/agda/pull/7509)). - -Issues closed -------------- - -For 2.8.0, the following issues were -[closed](https://github.com/agda/agda/issues?q=is%3Aissue+milestone%3A2.8.0+is%3Aclosed) -(see [bug tracker](https://github.com/agda/agda/issues)): - -Issues for closed for milestone 2.8.0 -- [Issue #570](https://github.com/agda/agda/issues/570): Explicit polarity annotation -- [Issue #2004](https://github.com/agda/agda/issues/2004): `DISPLAY` should be more pragmatic -- [Issue #4100](https://github.com/agda/agda/issues/4100): GHC backend produces code that is wrongly compiled by GHC 8.4.* and 8.6.* -- [Issue #4338](https://github.com/agda/agda/issues/4338): Add mechanism to type check entire Agda libraries -- [Issue #4343](https://github.com/agda/agda/issues/4343): File order of checking matters (rewrite rules) -- [Issue #5299](https://github.com/agda/agda/issues/5299): Postfix projections are not documented -- [Issue #5865](https://github.com/agda/agda/issues/5865): Non Pattern Match Lambdas Missing From Docs -- [Issue #6111](https://github.com/agda/agda/issues/6111): Is compile-time irrelevance supposed to be erased with `COMPILE` pragmas? -- [Issue #6320](https://github.com/agda/agda/issues/6320): Parse strings to terms as reflection operation -- [Issue #6657](https://github.com/agda/agda/issues/6657): Turn `--guardedness` warning into an error-hint -- [Issue #6781](https://github.com/agda/agda/issues/6781): Making `@tactic` arguments visible leads to unsolved constraints -- [Issue #6916](https://github.com/agda/agda/issues/6916): Internal error at Agda/TypeChecking/Sort.hs:224:21 -- [Issue #6964](https://github.com/agda/agda/issues/6964): Allow referring to unnamed record constructors -- [Issue #6994](https://github.com/agda/agda/issues/6994): Warnings are turned off, but code is still highlighted -- [Issue #7057](https://github.com/agda/agda/issues/7057): Document let-bindings in telescopes -- [Issue #7066](https://github.com/agda/agda/issues/7066): Documentation for anonymous modules -- [Issue #7157](https://github.com/agda/agda/issues/7157): Future: cabal build-type `Setup` will be phased out in favor of `Hooks` -- [Issue #7163](https://github.com/agda/agda/issues/7163): `cabal install Agda` fails with executable-dynamic -- [Issue #7321](https://github.com/agda/agda/issues/7321): No warning about useless `{-# CATCHALL #-}` pragma -- [Issue #7324](https://github.com/agda/agda/issues/7324): HTML backend: inconsistent highlighting for macro names -- [Issue #7375](https://github.com/agda/agda/issues/7375): The specification of `--safe` misses the pragmas -- [Issue #7381](https://github.com/agda/agda/issues/7381): Our error messages do not follow the GNU standard -- [Issue #7392](https://github.com/agda/agda/issues/7392): Pattern matching unifier does not preserve instances -- [Issue #7434](https://github.com/agda/agda/issues/7434): Range printed twice for "Parse error" -- [Issue #7440](https://github.com/agda/agda/issues/7440): Unexpected hidden argument in nested records/modules -- [Issue #7495](https://github.com/agda/agda/issues/7495): Catchall clauses with less arguments are considered exact -- [Issue #7503](https://github.com/agda/agda/issues/7503): Cumulativity `Prop <= Set` loses canonicity -- [Issue #7507](https://github.com/agda/agda/issues/7507): Broken CI/haskell installation on GitHub? -- [Issue #7508](https://github.com/agda/agda/issues/7508): Unused-arg optimization breaks function call -- [Issue #7517](https://github.com/agda/agda/issues/7517): `quoteTerm` accepts hidden arguments -- [Issue #7529](https://github.com/agda/agda/issues/7529): Strange problem with --level-universe and --cubical -- [Issue #7530](https://github.com/agda/agda/issues/7530): Generalized variable blocks projection-likeness -- [Issue #7531](https://github.com/agda/agda/issues/7531): JS backend crashes on big case split -- [Issue #7533](https://github.com/agda/agda/issues/7533): `DISPLAY` pragmas should treat any defined name as matchable -- [Issue #7535](https://github.com/agda/agda/issues/7535): Regression in 2.6.4: Agda thinks large propositions can be transported -- [Issue #7537](https://github.com/agda/agda/issues/7537): Type checking a definition with higher inductive type fails to terminate -- [Issue #7546](https://github.com/agda/agda/issues/7546): Why do we allow empty POLARITY pragmas? -- [Issue #7573](https://github.com/agda/agda/issues/7573): `primFloatRound` broken in JS -- [Issue #7574](https://github.com/agda/agda/issues/7574): Support GHC 9.12 -- [Issue #7575](https://github.com/agda/agda/issues/7575): impossible error: `variable` in `BUILTIN` -- [Issue #7576](https://github.com/agda/agda/issues/7576): impossible error: parameter overflow in `declareData` -- [Issue #7580](https://github.com/agda/agda/issues/7580): Our Setup.hs does not build with Cabal-3.14 -- [Issue #7585](https://github.com/agda/agda/issues/7585): Happy-2.1.1 causes Agda build to fail -- [Issue #7587](https://github.com/agda/agda/issues/7587): Mimer takes an absurd lambda as the solution of the original goal rather than the current (sub)goal -- [Issue #7588](https://github.com/agda/agda/issues/7588): __IMPOSSIBLE__, called at src/full/Agda/Compiler/JS/Compiler.hs:596:45 -- [Issue #7590](https://github.com/agda/agda/issues/7590): Internal error with interaction point in a shared type signature -- [Issue #7618](https://github.com/agda/agda/issues/7618): De Bruijn index out of scope in the presence of rewrite rules and records -- [Issue #7624](https://github.com/agda/agda/issues/7624): Internal error when interactively checking expression with new meta-variables -- [Issue #7639](https://github.com/agda/agda/issues/7639): Internal error in `Agda/TypeChecking/Monad/Context.hs` using Mimer -- [Issue #7641](https://github.com/agda/agda/issues/7641): No error highlighting when "fits in" test fails -- [Issue #7642](https://github.com/agda/agda/issues/7642): Better not claim "Level should be a function type" -- [Issue #7643](https://github.com/agda/agda/issues/7643): Panic: uncaught pattern violation -- [Issue #7650](https://github.com/agda/agda/issues/7650): Internal error when utilizing Emacs case splits and `with .. in ..` -- [Issue #7655](https://github.com/agda/agda/issues/7655): haskell/cabal#10235 can still occur with Agda-2.7.0.1 -- [Issue #7659](https://github.com/agda/agda/issues/7659): Using auto leads to `__IMPOSSIBLE__` when Σ and case_of_ are both present -- [Issue #7660](https://github.com/agda/agda/issues/7660): Add a warning for unresolved constructor name -- [Issue #7662](https://github.com/agda/agda/issues/7662): Using Auto with a goal involving musical coinduction `♭` produces incorrect projection -- [Issue #7668](https://github.com/agda/agda/issues/7668): Inductive identity allowed in negative position, inconsistent in Cubical Agda -- [Issue #7669](https://github.com/agda/agda/issues/7669): Positivity checker doesn't respect definitional equality -- [Issue #7673](https://github.com/agda/agda/issues/7673): `nix build` skips "generation of Agda core library interface files" -- [Issue #7675](https://github.com/agda/agda/issues/7675): `toIFile` logic from #6988 leads to scattering of `.agdai` files -- [Issue #7678](https://github.com/agda/agda/issues/7678): Order of agda-lib files in a directory affects flag settings -- [Issue #7692](https://github.com/agda/agda/issues/7692): Option to completely disable generation of dot patterns -- [Issue #7696](https://github.com/agda/agda/issues/7696): Panic: de Bruijn index out of scope -- [Issue #7707](https://github.com/agda/agda/issues/7707): ConstructorDoesNotFitInData error for record in Prop with Set fields -- [Issue #7709](https://github.com/agda/agda/issues/7709): Slow typecheck when importing a module with instances -- [Issue #7710](https://github.com/agda/agda/issues/7710): Forcing evaluation can give incorrect results in ghc compiled code -- [Issue #7712](https://github.com/agda/agda/issues/7712): Embed data files using file-embed -- [Issue #7722](https://github.com/agda/agda/issues/7722): Exponential behavior in pattern operator parser -- [Issue #7730](https://github.com/agda/agda/issues/7730): emacs-mode files fail to build with "file has no `lexical-binding` directive" -- [Issue #7738](https://github.com/agda/agda/issues/7738): Rewriting by a constructor -- [Issue #7751](https://github.com/agda/agda/issues/7751): Application of module with datatype fools the termination checker -- [Issue #7753](https://github.com/agda/agda/issues/7753): Coverage checker internal error with copatterns and dot patterns -- [Issue #7759](https://github.com/agda/agda/issues/7759): Internal error for ellipsis without with-patterns -- [Issue #7761](https://github.com/agda/agda/issues/7761): Propω is not actually proof irrelevant -- [Issue #7765](https://github.com/agda/agda/issues/7765): Supply reason with UselessPublic warning -- [Issue #7766](https://github.com/agda/agda/issues/7766): .lagda.org: {-1} outside agda code block messes up hole detection -- [Issue #7769](https://github.com/agda/agda/issues/7769): The warning OpenPublicAbstract is wrongly formulated -- [Issue #7777](https://github.com/agda/agda/issues/7777): Parse error when using tactic and irrelevance -- [Issue #7788](https://github.com/agda/agda/issues/7788): TooManyPatternsInWithClause when nesting hidden `with` -- [Issue #7792](https://github.com/agda/agda/issues/7792): Inlining happens at most twice -- [Issue #7795](https://github.com/agda/agda/issues/7795): Polarity annotation ignored by positivity checker? -- [Issue #7796](https://github.com/agda/agda/issues/7796): Distinguish --no-guardedness from default value in termination hints? -- [Issue #7799](https://github.com/agda/agda/issues/7799): Potential regression related to instance resolution -- [Issue #7811](https://github.com/agda/agda/issues/7811): Internal error with Path and with-abstraction II -- [Issue #7815](https://github.com/agda/agda/issues/7815): Missing highlighting in module telescopes -- [Issue #7823](https://github.com/agda/agda/issues/7823): DISPLAY matches pattern with wrong amount of arguments -- [Issue #7825](https://github.com/agda/agda/issues/7825): DISPLAY form on irrelevant projection drops arguments -- [Issue #7832](https://github.com/agda/agda/issues/7832): Recursive function over inductive record treats arguments as irrelevant -- [Issue #7851](https://github.com/agda/agda/issues/7851): Error TooManyPolarities is too eager -- [Issue #7853](https://github.com/agda/agda/issues/7853): Subject reduction failure with instance constructors in parameterised modules -- [Issue #7856](https://github.com/agda/agda/issues/7856): Strange interaction between `opaque` and extended lambdas -- [Issue #7863](https://github.com/agda/agda/issues/7863): Internal error when calling MakeCase on target `__` -- [Issue #7878](https://github.com/agda/agda/issues/7878): Impossible with malformed notation RHS -- [Issue #7884](https://github.com/agda/agda/issues/7884): Better documentation of forester backend in CHANGELOG -- [Issue #7898](https://github.com/agda/agda/issues/7898): Solving with auto doesn't update constraints -- [Issue #7903](https://github.com/agda/agda/issues/7903): Constructor inlining defeated by moving binders -- [Issue #7911](https://github.com/agda/agda/issues/7911): `UnsolvedConstraints` error should reference location even when all metas were solved -- [Issue #7912](https://github.com/agda/agda/issues/7912): Missing error location for error: [ModuleNameDoesntMatchFileName] -- [Issue #7916](https://github.com/agda/agda/issues/7916): Make `-f optimise-heavily` default -- [Issue #7935](https://github.com/agda/agda/issues/7935): Document scoping rules for rewrite rules -- [Issue #7938](https://github.com/agda/agda/issues/7938): Request: Expose backend-internal modules as part of the library -- [Issue #7943](https://github.com/agda/agda/issues/7943): Local erased definition remains in compiled code -- [Issue #7944](https://github.com/agda/agda/issues/7944): Local erased modules break erasure analysis -- [Issue #7952](https://github.com/agda/agda/issues/7952): Primitive root example in docs -- [Issue #7953](https://github.com/agda/agda/issues/7953): Confusing error in case of illegal declaration before top-level module in a nested file -- [Issue #7966](https://github.com/agda/agda/issues/7966): Disallow option abbreviation -- [Issue #7973](https://github.com/agda/agda/issues/7973): If rewrite does not rewrite anything, give a warning -- [Issue #7977](https://github.com/agda/agda/issues/7977): Soft error for unknown attributes +Release notes for Agda version 2.8.0.1 +====================================== -PRs for closed for milestone 2.8.0 +* Added support for GHC 9.14.1 -- [PR #6629](https://github.com/agda/agda/issues/6629): Reflection primitive for parsing surface level syntax from string. -- [PR #7010](https://github.com/agda/agda/issues/7010): [new] backend-end specific interaction -- [PR #7023](https://github.com/agda/agda/issues/7023): Add ⧺ in agda-input.el -- [PR #7287](https://github.com/agda/agda/issues/7287): Temporary fix for reflection of partial elements. -- [PR #7366](https://github.com/agda/agda/issues/7366): Handle symlinks correctly when computing interface file locations -- [PR #7374](https://github.com/agda/agda/issues/7374): New warning `WithClauseProjectionFixityMismatch` instead of GenericError -- [PR #7377](https://github.com/agda/agda/issues/7377): New warning `RecursiveDisplayForm` instead of hard error -- [PR #7379](https://github.com/agda/agda/issues/7379): Print error name with error message -- [PR #7385](https://github.com/agda/agda/issues/7385): New error group GHCBackendError instead of GenericError -- [PR #7387](https://github.com/agda/agda/issues/7387): Factor out `give_` and remove PatternErr handler -- [PR #7388](https://github.com/agda/agda/issues/7388): GenericError crusade, continued -- [PR #7391](https://github.com/agda/agda/issues/7391): New error NeedOptionAllowExec etc. instead of GenericError -- [PR #7394](https://github.com/agda/agda/issues/7394): New error group InteractionError -- [PR #7395](https://github.com/agda/agda/issues/7395): Get rid of some MonadFail in favor of __IMPOSSIBLE__ -- [PR #7396](https://github.com/agda/agda/issues/7396): instance warning -- [PR #7403](https://github.com/agda/agda/issues/7403): New literate programming backend forester, `*.lagda.tree` -- [PR #7409](https://github.com/agda/agda/issues/7409): GenericError crusade goes on: NeedOptionSizedTypes etc. -- [PR #7412](https://github.com/agda/agda/issues/7412): pattern in path lambda -- [PR #7414](https://github.com/agda/agda/issues/7414): Replace interaction `Cmd_no_metas` by `Cmd_load_no_metas` -- [PR #7415](https://github.com/agda/agda/issues/7415): Error refactoring: use of `Exception`, generic errors -- [PR #7418](https://github.com/agda/agda/issues/7418): New errors CannotGenerate{HComp,Transport}Clause -- [PR #7425](https://github.com/agda/agda/issues/7425): GenericError replacements -- [PR #7426](https://github.com/agda/agda/issues/7426): #7371: add Mimer tests for -s and -l -- [PR #7430](https://github.com/agda/agda/issues/7430): Warnings instead of GenericError for ill-formed pragmas -- [PR #7435](https://github.com/agda/agda/issues/7435): Print warning name on same line as location -- [PR #7437](https://github.com/agda/agda/issues/7437): Reform printing of parse error -- [PR #7447](https://github.com/agda/agda/issues/7447): Add new error `InvalidModalTelescopeUse` and add reproducer. -- [PR #7451](https://github.com/agda/agda/issues/7451): New warning FixingRelevance instead of GenericError -- [PR #7453](https://github.com/agda/agda/issues/7453): New error NotAllowedInDotPatterns instead of GenericError -- [PR #7458](https://github.com/agda/agda/issues/7458): Add ZuriHac Video to tutorial-list -- [PR #7459](https://github.com/agda/agda/issues/7459): NotAValidLet{Expression,Binding} instead of GenericError -- [PR #7462](https://github.com/agda/agda/issues/7462): Naming generic syntax errors (GenericError quest) -- [PR #7473](https://github.com/agda/agda/issues/7473): Re #6919: also separate compilation warnings by newlines -- [PR #7478](https://github.com/agda/agda/issues/7478): Store warnings in a set rather than a list -- [PR #7481](https://github.com/agda/agda/issues/7481): Named Backend errors instead of GenericError -- [PR #7483](https://github.com/agda/agda/issues/7483): Some named scope errors replacing GenericError -- [PR #7488](https://github.com/agda/agda/issues/7488): Named scope errors instead of GenericError -- [PR #7491](https://github.com/agda/agda/issues/7491): ES6 modules -- [PR #7492](https://github.com/agda/agda/issues/7492): Correctly print ParserWarning range, remove `mdo` -- [PR #7496](https://github.com/agda/agda/issues/7496): Fix #7495: Check extra split clause patterns are trivial for exactness -- [PR #7498](https://github.com/agda/agda/issues/7498): Add Left Multimap (⟜) to agda-input.el -- [PR #7500](https://github.com/agda/agda/issues/7500): Fix & test `primShowNat` -- [PR #7501](https://github.com/agda/agda/issues/7501): handle ProjPs in DISPLAY pragmas -- [PR #7502](https://github.com/agda/agda/issues/7502): Make termination checking more permissive wrt non-exact clause reduction -- [PR #7504](https://github.com/agda/agda/issues/7504): [ fix #7503 ] Use principal sort of datatype for checking if split is ok -- [PR #7509](https://github.com/agda/agda/issues/7509): Fix #7508: remove unused-arg optimization from the JS backend -- [PR #7510](https://github.com/agda/agda/issues/7510): Expose the names of generated record constructors (reopen #6975) -- [PR #7511](https://github.com/agda/agda/issues/7511): Fix #7381: comply to GNU error standard: use dot instead of comma in ranges -- [PR #7512](https://github.com/agda/agda/issues/7512): GenericError crusade -- [PR #7513](https://github.com/agda/agda/issues/7513): Reconcile PR #7510 with commit ac2888a7ad: add Maybe Induction to scopeRecords -- [PR #7516](https://github.com/agda/agda/issues/7516): New error CannotQuote instead of GenericError -- [PR #7518](https://github.com/agda/agda/issues/7518): OccursCheckErrors -- [PR #7520](https://github.com/agda/agda/issues/7520): Drop GHC 8.6 -- [PR #7534](https://github.com/agda/agda/issues/7534): Fix #7529: treat `LevelUniv` in Cubical Agda -- [PR #7536](https://github.com/agda/agda/issues/7536): Re #7533: warn when DISPLAY form binds variables unused on the rhs -- [PR #7539](https://github.com/agda/agda/issues/7539): Fix #7413: Cubical: a `GenericError` is actually `__IMPOSSIBLE__` -- [PR #7543](https://github.com/agda/agda/issues/7543): DISPLAY: match on defined names -- [PR #7545](https://github.com/agda/agda/issues/7545): Fix #7531: Preserve let bindings in the JS backend -- [PR #7550](https://github.com/agda/agda/issues/7550): Fix #7546: warn about empty POLARITY pragmas -- [PR #7555](https://github.com/agda/agda/issues/7555): Some error housekeeping -- [PR #7556](https://github.com/agda/agda/issues/7556): unquote errors -- [PR #7557](https://github.com/agda/agda/issues/7557): kill GenericError in instance search -- [PR #7559](https://github.com/agda/agda/issues/7559): Fix compilation of serialisation code on 32 bit platforms -- [PR #7566](https://github.com/agda/agda/issues/7566): Make dangling hidden/instance args into a warning -- [PR #7570](https://github.com/agda/agda/issues/7570): Optimize concrete name scopeLookup -- [PR #7572](https://github.com/agda/agda/issues/7572): Improvements to let desugaring -- [PR #7577](https://github.com/agda/agda/issues/7577): chore: remove uses of genericError -- [PR #7581](https://github.com/agda/agda/issues/7581): don't add generalizedTel definitions to mutual blocks -- [PR #7583](https://github.com/agda/agda/issues/7583): Implement conversion to JS `BigInt` -- [PR #7586](https://github.com/agda/agda/issues/7586): Support Happy 2.1.1 -- [PR #7589](https://github.com/agda/agda/issues/7589): Fix #7575: Check if variables are generalizable in builtin pragmas -- [PR #7591](https://github.com/agda/agda/issues/7591): Fix #7588: Remove overlapping branches when simplifying chained cases -- [PR #7593](https://github.com/agda/agda/issues/7593): Fix #7576 -- [PR #7604](https://github.com/agda/agda/issues/7604): REPL: fix printing of result of `:typeOf` -- [PR #7613](https://github.com/agda/agda/issues/7613): Correct parameters to wrapper modules created in module telescopes -- [PR #7617](https://github.com/agda/agda/issues/7617): Fix de Bruijn indices in Treeless primitive translation -- [PR #7622](https://github.com/agda/agda/issues/7622): [ fix #7618 ] Use `underAbstraction_` for going under lambda in `reduceAndEtaContract` -- [PR #7640](https://github.com/agda/agda/issues/7640): [ emacs ] adding su(b/p)(sim/approx) to input method -- [PR #7645](https://github.com/agda/agda/issues/7645): Fix #7642: new error CannotApply that mentions also term, not only type -- [PR #7648](https://github.com/agda/agda/issues/7648): Fix #7641: Range for ConstructorDoesNotFit warning (anon. rec. con.) -- [PR #7651](https://github.com/agda/agda/issues/7651): Fix #7650: Throw CaseSplitError when splitting on with-abstraction equality -- [PR #7652](https://github.com/agda/agda/issues/7652): remove the cubical identity type -- [PR #7653](https://github.com/agda/agda/issues/7653): Print point-ranges as such (line.col rather than line:col-col) -- [PR #7657](https://github.com/agda/agda/issues/7657): Setup: unconditionally check if we want interfaces -- [PR #7670](https://github.com/agda/agda/issues/7670): Fix typo `COMPILED` -- [PR #7672](https://github.com/agda/agda/issues/7672): Fix #7643: coverage: handle blocked sort in isFibrant -- [PR #7674](https://github.com/agda/agda/issues/7674): Fix #7669: positivity checker: compute function arity up to def. eq. -- [PR #7676](https://github.com/agda/agda/issues/7676): Remove `--local-interfaces` and warning `DuplicateInterfaceFiles` -- [PR #7677](https://github.com/agda/agda/issues/7677): Setup: fix `wantInterfaces` check -- [PR #7679](https://github.com/agda/agda/issues/7679): Disallow several .agda-lib files in the project root (#7678) -- [PR #7682](https://github.com/agda/agda/issues/7682): New main mode `--build-library` -- [PR #7685](https://github.com/agda/agda/issues/7685): Add dump-core cabal flag -- [PR #7686](https://github.com/agda/agda/issues/7686): Monomorphise unifyIndices -- [PR #7687](https://github.com/agda/agda/issues/7687): Make toTerm return a monadic function -- [PR #7688](https://github.com/agda/agda/issues/7688): Add some links to lecture notes and videos on Agda -- [PR #7697](https://github.com/agda/agda/issues/7697): Fix #7696: Add missing `addContext` when splitting on literals -- [PR #7699](https://github.com/agda/agda/issues/7699): Remove custom Setup.hs -- [PR #7700](https://github.com/agda/agda/issues/7700): Never generate dot patterns under --keep-pattern-variables -- [PR #7704](https://github.com/agda/agda/issues/7704): Speed up nix build -- [PR #7719](https://github.com/agda/agda/issues/7719): Embed data files into Agda binary -- [PR #7726](https://github.com/agda/agda/issues/7726): Compare overlapping instances in the right context -- [PR #7727](https://github.com/agda/agda/issues/7727): Fix #7722: in pattern parser only consider pattern-relevant operators -- [PR #7728](https://github.com/agda/agda/issues/7728): Improvements to instance search performance -- [PR #7729](https://github.com/agda/agda/issues/7729): Let Agda perform several of `--help`, `--version` etc. if the user requests so -- [PR #7732](https://github.com/agda/agda/issues/7732): Duplicate `agda-mode` as `agda --emacs-mode` -- [PR #7734](https://github.com/agda/agda/issues/7734): Doc: executable-dynamic no longer a problem on Linux -- [PR #7739](https://github.com/agda/agda/issues/7739): Fix #7738: Allow rewrite rule defined with constructor or primitive -- [PR #7742](https://github.com/agda/agda/issues/7742): Fix #7741: Fix printing inserted binder from operator section -- [PR #7743](https://github.com/agda/agda/issues/7743): Re-enable dot-pattern termination for Cubical Agda -- [PR #7745](https://github.com/agda/agda/issues/7745): Limit depth of constructed discrimination tree -- [PR #7746](https://github.com/agda/agda/issues/7746): Compute occurrences in trX “constructors” -- [PR #7750](https://github.com/agda/agda/issues/7750): Support GHC 9.12.2 -- [PR #7752](https://github.com/agda/agda/issues/7752): Fix #7751: Consider datatype clauses generated from module application in recursion checker -- [PR #7758](https://github.com/agda/agda/issues/7758): Fix #7753: a possible `__IMPOSSIBLE__` -- [PR #7763](https://github.com/agda/agda/issues/7763): Fix #7761: Include large Prop in checks whether something is a Prop -- [PR #7764](https://github.com/agda/agda/issues/7764): Fixed #7730 -- [PR #7767](https://github.com/agda/agda/issues/7767): Fix #7766: emacs org mode: fix code block end detection -- [PR #7768](https://github.com/agda/agda/issues/7768): Reason for UselessPublic; `private` useless in `where` blocks -- [PR #7771](https://github.com/agda/agda/issues/7771): Fix #7769: replace warning `OpenPublic{Abstract,Private}` -- [PR #7772](https://github.com/agda/agda/issues/7772): Fix #7707: wording of warning `ConstructorDoesNotFitInData` -- [PR #7773](https://github.com/agda/agda/issues/7773): Fix #7662: Mimer: special case for printing ♭ -- [PR #7774](https://github.com/agda/agda/issues/7774): Fix #7321: warn about unused CATCHALL pragmas -- [PR #7775](https://github.com/agda/agda/issues/7775): Fix #6994: highlighting only for enabled warnings -- [PR #7776](https://github.com/agda/agda/issues/7776): Fix #7624 by reifying Term before wrapping it in GoalAndElaboration -- [PR #7778](https://github.com/agda/agda/issues/7778): Fix #6657: termination checker hints at missing --guardedness flag -- [PR #7782](https://github.com/agda/agda/issues/7782): re #3209: print out-of-scope names unqualified in case splits -- [PR #7783](https://github.com/agda/agda/issues/7783): Don't inline constructors into inline functions -- [PR #7785](https://github.com/agda/agda/issues/7785): Fix #7777: parse both attributes and irrelevance markers -- [PR #7786](https://github.com/agda/agda/issues/7786): New warning `UselessTactic` for `tactic` attribute on non-hidden binder -- [PR #7787](https://github.com/agda/agda/issues/7787): Small fixes for parsing and printing attributes -- [PR #7789](https://github.com/agda/agda/issues/7789): Fix issues #7759 and #7788: wrong counting of with-patterns in nested with -- [PR #7791](https://github.com/agda/agda/issues/7791): [ new ] unicode symbols for various 'tacks' -- [PR #7793](https://github.com/agda/agda/issues/7793): re #7792: keep inlining after inlining a copy -- [PR #7800](https://github.com/agda/agda/issues/7800): Fix #7796: don't hint towards --guardedness when --no-guardedness -- [PR #7802](https://github.com/agda/agda/issues/7802): Remove broken AbsurdLam heuristics from Mimer -- [PR #7804](https://github.com/agda/agda/issues/7804): re #7799: add instance hack to checkSectionApplication -- [PR #7812](https://github.com/agda/agda/issues/7812): Fix #7803 fix #7811: new error PathAbstractionFailed instead of crash -- [PR #7814](https://github.com/agda/agda/issues/7814): Fix #7660: new DisambiguateConstructor postponed tc problem -- [PR #7816](https://github.com/agda/agda/issues/7816): re #7815: propagate range into wrapper modules -- [PR #7817](https://github.com/agda/agda/issues/7817): Add documentation for telescopes and some related things -- [PR #7818](https://github.com/agda/agda/issues/7818): Make data directory overridable, default to XDG_DATA_HOME -- [PR #7819](https://github.com/agda/agda/issues/7819): [ fix #7392 ] Ensure wildcards and variable instances are kept -- [PR #7822](https://github.com/agda/agda/issues/7822): Fix issue #7537 -- [PR #7824](https://github.com/agda/agda/issues/7824): Fix #7823: Compare number of arguments when matching on DISPLAY pragma -- [PR #7826](https://github.com/agda/agda/issues/7826): Fix #7825 by using `droppedPars` instead of hand-knitted code -- [PR #7830](https://github.com/agda/agda/issues/7830): Disregard qualified names when assigning clauses to functions in the nicifier -- [PR #7831](https://github.com/agda/agda/issues/7831): Fix #7829 by reactivating my own fix of #1618 -- [PR #7834](https://github.com/agda/agda/issues/7834): fix #7795: Use occurrences from type for defs -- [PR #7840](https://github.com/agda/agda/issues/7840): Document which pragmas are unsafe -- [PR #7848](https://github.com/agda/agda/issues/7848): fix #7846: instance hack in abstract axioms -- [PR #7849](https://github.com/agda/agda/issues/7849): Fix for #7639 -- [PR #7850](https://github.com/agda/agda/issues/7850): Re #7225: new error DatatypeIndexPolarity instead of GenericError -- [PR #7852](https://github.com/agda/agda/issues/7852): Turn TooManyPolarities error into warning (fixes #7851) -- [PR #7854](https://github.com/agda/agda/issues/7854): Modality warnings for constructors and fields -- [PR #7855](https://github.com/agda/agda/issues/7855): Re #7225 name error CubicalNotErasure -- [PR #7857](https://github.com/agda/agda/issues/7857): Forget opacity when checking signatures -- [PR #7858](https://github.com/agda/agda/issues/7858): Fix for #7659 -- [PR #7859](https://github.com/agda/agda/issues/7859): Fix #7853: don't drop parameters of constructor in the same module -- [PR #7860](https://github.com/agda/agda/issues/7860): [ re #7587 ] Properly reintroduce absurd lambdas to Mimer -- [PR #7865](https://github.com/agda/agda/issues/7865): Fix #7863: properly parse names before case-splitting -- [PR #7867](https://github.com/agda/agda/issues/7867): Fix #7832 by placing properlyMatching in monad to have isEtaRecordConstructor -- [PR #7879](https://github.com/agda/agda/issues/7879): Fix #7878: reorder checks in `mkNotation` -- [PR #7880](https://github.com/agda/agda/issues/7880): Defer `MissingDefinitions` error in `--safe` until after typechecking -- [PR #7885](https://github.com/agda/agda/issues/7885): disable discrim-based instance deferral by default -- [PR #7886](https://github.com/agda/agda/issues/7886): [doc] explain how to do postprocessing for literate forester -- [PR #7891](https://github.com/agda/agda/issues/7891): Remove duplicate inverse scope computation. -- [PR #7895](https://github.com/agda/agda/issues/7895): Fix #7590 -- [PR #7896](https://github.com/agda/agda/issues/7896): Fix #7324: highlighting of macro names in their definition -- [PR #7900](https://github.com/agda/agda/issues/7900): intro: filter (higher) constructors based on dimension -- [PR #7901](https://github.com/agda/agda/issues/7901): Properly update interaction points when solving with Mimer -- [PR #7904](https://github.com/agda/agda/issues/7904): Fix lexical-scope issue in emacs mode -- [PR #7907](https://github.com/agda/agda/issues/7907): Fix issue #7903: etaExpandClause before constructor inlining -- [PR #7913](https://github.com/agda/agda/issues/7913): Range information for unsolved instance constraints -- [PR #7920](https://github.com/agda/agda/issues/7920): Fix #7916: make optimise-heavily the default -- [PR #7924](https://github.com/agda/agda/issues/7924): Add a few notes on irrelevance -- [PR #7925](https://github.com/agda/agda/issues/7925): Add documentation for lambda expressions and absurd lambdas -- [PR #7931](https://github.com/agda/agda/issues/7931): Hint towards --guardedness even when --sized-types is on -- [PR #7932](https://github.com/agda/agda/issues/7932): Add `use-xdg-data-home` -- [PR #7934](https://github.com/agda/agda/issues/7934): Hygienic import of rewrite rules -- [PR #7936](https://github.com/agda/agda/issues/7936): Highlight only record keyword when fields are missing -- [PR #7939](https://github.com/agda/agda/issues/7939): Fix #7938: API: export Agda Highlighting Backend modules -- [PR #7942](https://github.com/agda/agda/issues/7942): [ doc ] remove reference to Cubical.Core.Everything -- [PR #7945](https://github.com/agda/agda/issues/7945): Fix #7944: do not apply `@0` from where-module to clause rhs -- [PR #7946](https://github.com/agda/agda/issues/7946): Fix #7943: propagate erasure status to `where` blocks. -- [PR #7956](https://github.com/agda/agda/issues/7956): Fix #7955: replace impossible with syntax error -- [PR #7957](https://github.com/agda/agda/issues/7957): Doc: replace PrimRoot by PrimeFactor in introductory text -- [PR #7958](https://github.com/agda/agda/issues/7958): Fix #7953: remember whether top-level module name was inferred -- [PR #7965](https://github.com/agda/agda/issues/7965): Re #7932: restore data-files in Agda.cabal and default data-dir -- [PR #7967](https://github.com/agda/agda/issues/7967): Fix #7966: fork GetOpt to disallow long option abbreviations -- [PR #7971](https://github.com/agda/agda/issues/7971): flake: use --build-library to build the builtins -- [PR #7978](https://github.com/agda/agda/issues/7978): Fix #7973: print warning if `rewrite` does not fire -- [PR #7981](https://github.com/agda/agda/issues/7981): Parse warning instead of error on unknown attributes and polarities +* Agda supports GHC versions 8.8.4 to 9.14.1. diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -5,26 +5,27 @@ Cubical Agda was originally contributed by Andrea Vezzosi. Agda 2 is currently actively developed mainly by Andreas Abel, -Liang-Ting Chen, Lawrence Chonavel, Jesper Cockx, -Nils Anders Danielsson, Amélia Liao, Ulf Norell, and Szumi Xie. +Nathaniel Burke, Lawrence Chonavel, Jesper Cockx, +Nils Anders Danielsson, and András Kovács. Further, Agda 2 has received contributions by, amongst others, -Arthur Adjedj, Guillaume Allais, Malin Altenmüller, Stevan Andjelkovic, +Arthur Adjedj, Guillaume Allais, Malin Altenmüller, Stevan Andjelkovic, Marcin Benke, Jean-Philippe Bernardy, Guillaume Brunerie, -James Chapman, Joris Ceulemans, Jonathan Coates, -Matthew Daggitt, Dominique Devriese, Péter Diviánszky, +James Chapman, Liang-Ting Chen, Joris Ceulemans, Jonathan Coates, +Matthew Daggitt, Dominique Devriese, Marko Dimjašević, Péter Diviánszky, Lucas Escot, Robert Estelle, -Naïm Favier, Kuen-Bang Hou (Favonia), Olle Fredriksson, -Adam Gundry, Daniel Gustafsson, +Naïm Camille Favier, Kuen-Bang Hou (Favonia), Olle Fredriksson, +Paolo G. Giarrusso, Adam Gundry, Daniel Gustafsson, Philipp Hausmann, Alex Haršáni, -Alan Jeffrey, Phil de Joux, -Wolfram Kahl, Andre Knispel, Wen Kokke, András Kovács, -John Leo, Fredrik Lindblad, Víctor López Juan, Ting-Gan Lua, -Francesco Mazzoli, Stefan Monnier, Guilhem Moulin, -Konstantin Nisht, Fredrik Nordvall Forsberg, Andreas Nuyts, -Josselin Poiret, Nicolas Pouillard, Jonathan Prieto, -Christian Sattler, Michael Shulman, Andrés Sicard-Ramírez, -Makoto Takeyama, Andrea Vezzosi, Noam Zeilberger, and Tesla Ice Zhang. +Patrik Jansson, Alan Jeffrey, Phil de Joux, +Wolfram Kahl, Philip Kaludercic, Andre Knispel, Wen Kokke, +John Leo, Amélia Liao, Ziyang Liu, Fredrik Lindblad, Víctor López Juan, Ting-Gan Lua, +Francesco Mazzoli, Stefan Monnier, Guilhem Moulin, Reed Mullanix, +Konstantin Nisht, Fredrik Nordvall Forsberg, Ulf Norell, Andreas Nuyts, +Herminie Pagel, Josselin Poiret, Nicolas Pouillard, Jonathan Prieto, +Christian Sattler, Artem Shinkarov, Michael Shulman, Andrés Sicard-Ramírez, Nate Soares, +Makoto Takeyama, Andrea Vezzosi, Szumi Xie, Nobuo Yamashita, +Noam Zeilberger, and Tesla Ice Zhang. The full list of contributors is available at https://github.com/agda/agda/graphs/contributors or from the git repository via ``git shortlog -sne``. diff --git a/doc/release-notes/2.8.0.md b/doc/release-notes/2.8.0.md new file mode 100644 --- /dev/null +++ b/doc/release-notes/2.8.0.md @@ -0,0 +1,639 @@ +Release notes for Agda version 2.8.0 +==================================== + +Highlights +---------- + +* Agda is now a self-contained single binary. + +* Build all Agda files reachable from paths in the `.agda-lib` file with new flag `--build-library`. + +* Experimental support for polarity annotations with new flag `--polarity`. + +* Compile to JavaScript with ES6 module syntax with new flag `--js-es6`. + +* Errors now have an identifier and follow the GNU standard. + +Installation +------------ + +* Dropped support for GHC 8.6, added support for GHC 9.12. + +* Agda supports GHC versions 8.8.4 to 9.12.2. + +* The `agda` binary now contains everything to set itself up, + it need not be shipped with additional files. + + 1. The functionality of the `agda-mode` executable has been replicated + under the new option `--emacs-mode`. + The `agda-mode` executable is now deprecated. + References to `agda-mode` in your `.emacs` file should be replaced + by `agda --emacs-mode`. + + 2. Agda now contains all its data files, + like primitive and builtin modules, + supplements for the HTML and LaTeX backends, + the runtimes for the `JS` and `GHC` backends, + and the emacs mode. + + These will be written to the data directory + on the first invocation of `agda` or an invocation of + `agda --setup`, `agda --emacs-mode setup`, or `agda --emacs-mode compile`. + + The location of the data directory can be printed using + `agda --print-agda-data-dir` and can be controlled by the `use-xdg-data-home` + flag at build time and the `Agda_datadir` environment variable at runtime; see the + documentation for more information. + +* The Cabal/Stack custom installation `Setup.hs` has been removed + that previously generated the `.agdai` files for the builtin and primitive modules. + These will now be generated by Agda whenever they are needed, + just as for ordinary modules. + + This change might be **breaking** for packagers of Agda + as the packaging routines might need to be updated: in particular, + declarative build systems like Nix or Guix should generate the `.agdai` files + by invoking Agda at build time. + +* Pre-built binaries are available as release assets for the following platforms + + * Windows (x86-64) + * Linux (x86-64) + * macOS (x86-64) + * macOS (arm64) + + Installation instructions are provided in the Agda user manual. + +* The `optimise-heavily` build flag is now turned on by default. + + This requires more resources when building Agda, but leads to a faster Agda binary. + Should GHC run out of memory when building Agda, turn this flag off. + +* Added cabal build flag `dump-core` to save the optimised GHC Core code during + compilation of Agda. This can be useful for people working on improving the + performance of the Agda implementation. + +Pragmas and options +------------------- + +* **BREAKING**: Abbreviation of options, such as `--warning` to `--warn`, is no longer supported. + +* New main mode of operation `--build-library` (issue [#4338](https://github.com/agda/agda/issues/4338)). + Invoking `agda --build-library` will look for an `.agda-lib` file starting in the current directory. + It will then extract the `include` directories of this library, + collect all Agda files in these directories and their subdirectories, + and check all these files. + +* New option `--setup` that writes out the Agda data files (see above) + and can be used to regenerate them. + +* New option `--emacs-mode` to administer the Emacs mode + as previously done by the `agda-mode` executable. + +* Option `--local-interfaces` and warning `DuplicateInterfaceFiles` have been removed. + +* New option `--js-es6` for generating JavaScript with ES6 module syntax. + +* `DISPLAY` pragmas can now define display forms that match on defined names + beyond constructors ([issue #7533](https://github.com/agda/agda/issues/7533)). + Example: + ```agda + {-# DISPLAY Irrelevant Empty = ⊥ #-} + ``` + `Empty` used to be interpreted as a pattern variable, effectively installing + the display form `Irrelevant _ = ⊥`. + Now `Empty` is treated as a matchable name, as one would intuitively expect + from a display form. + As a consequence, only `Irrelevant Empty` is displayed as `⊥`, not just any + `Irrelevant A`. + +* A new **experimental** flag `--experimental-lazy-instances` causes + instance selection to be deferred until the type of the instance + constraint is determined enough to make an unamibiguous decision at + the discrimination tree level. This significantly improves performance + for cases where instances can be distinguished by rigid data. + + This flag will become the default in the future, but it is currently + **disabled by default** because it has unexpected interactions with + parts of the codebase (and macros) which rely on constraint solving + order (see e.g. [issue #7882](https://github.com/agda/agda/issues/7883) + and [issue #7847](https://github.com/agda/agda/issues/7847)). + +Warnings +-------- + +* New warning `RewritesNothing` if a `rewrite` clause did not fire. + +* New deadcode warnings `FixingCohesion`, `FixingPolarity` and `FixingRelevance` + when wrong user-written attribute was corrected automatically by Agda. + +* New deadcode warning `InvalidDisplayForm` instead of hard error + when a display form is illegal (and thus ignored). + +* New warning `UnusedVariablesInDisplayForm` when DISPLAY pragma + binds variables that are not used. + Example: + ```agda + {-# DISPLAY List (Fin n) = ListFin #-} + ``` + Since pattern variable `n` is not used on the right hand side `ListFin`, + Agda throws a warning and recommeds to rewrite it as: + ```agda + {-# DISPLAY List (Fin _) = ListFin #-} + ``` + +* Unused `CATCHALL` pragmas now trigger `UselessPragma` warnings. + +* New deadcode warning `EmptyPolarityPragma` for POLARITY pragma without polarities. + E.g. triggered by `{-# POLARITY F #-}`. + +* New parser warnings `MisplacedAttributes`, `UnknownAttribute`, and `UnknownPolarity` + instead of hard parser errors. + +* New deadcode warning `TooManyPolarities` instead of hard error + when a POLARITY pragma gives polarities that exceed the known + arity of the postulate. + +* New deadcode warning `UselessTactic` when a `@tactic` attribute has no effect, + typically when it is attached to a non-hidden or instance argument. + +* New warning `WithClauseProjectionFixityMismatch` instead of hard error + when in a with-clause a projection is used in a different fixity + (prefix vs. postfix) than in its parent clause. + +* New error warning `TooManyArgumentsToSort` instead of hard error. + +* Warning `AbsurdPatternRequiresNoRHS` has been renamed to + `AbsurdPatternRequiresAbsentRHS`. + +* Warnings `OpenPublicAbstract` and `OpenPublicPrivate` have been replaced + by new warnings `OpenImportAbstract` and `OpenImportPrivate`. + +* Warning `NoGuardednessFlag` has been removed. + Instead Agda gives a hint when `--guardedness` would help with termination checking, + unless options `--sized-types` or `--no-guardedness` are set. + + +Polarity +-------- + +* Support for polarity annotations can be enabled by the feature flag + `--polarity`. + + This flag is infective. + + Uses of variables bound with polarity annotations are checked through modal + typing rules, and the positivity checker has been expanded to take annotations + into account. This means that the following is now definable: + + ```agda + {-# OPTIONS --polarity #-} + + data Mu (F : @++ Set → Set) : Set where + fix : F (Mu F) → Mu F + ``` + +Syntax +------ + +Additions to the Agda syntax. + +* Add new literate agda: forester, see [#7403](https://github.com/agda/agda/pull/7403). + You will need the postprocessor [`agda-tree`](https://github.com/dannypsnl/agda-tree), + see Agda user manual on literate programming for more information. + +* It is now always possible to refer to the name of a record type's + constructor, even if a name was not explicitly specified. This is done + using the new `(Record name).constructor` syntax; + see [issue #6964](https://github.com/agda/agda/issues/6964) for the motivation. + +* The *left-hand-sides* of functions bound in a `let` expression can now + contain the same types of patterns that are allowed in lambda + expressions, in dependent function types, and in other `let` bindings. + + This means that + + ```agda + let + f : A → B → C + f p1 p2 = ... + in ... + ``` + + should be accepted exactly when, and have the same meaning as, + + ```agda + let + f : A → B → C + f = λ p1 p2 → ... + ``` + + See [#7572](https://github.com/agda/agda/pull/7572). + +Language +-------- + +Changes to type checker and other components defining the Agda language. + +* **BREAKING**: The primitive "cubical identity type", previously + exported from `Agda.Builtin.Cubical.Id`, has been removed. Its + computational behaviour is exactly replicated by the user-definable + identity type, which is also exported from `Agda.Builtin.Equality`. + + See [agda/cubical#1005](https://github.com/agda/cubical/pull/1005) for + the PR removing it from the library, and + [#7652](https://github.com/agda/agda/pull/7652) for the compiler. + +* Inlining constructors no longer happens on the right-hand-sides of + `INLINE` functions. This allows using `INLINE` functions to define + "smart constructors" for record types which have the same reduction + behaviour as using the actual constructor would. Small example: + + ```agda + triple : Nat → Nat → Nat → Nat × Nat × Nat + {-# INLINE triple #-} + triple x y z = record { fst = x ; snd = y , z } + + ex = triple 1 2 3 + ``` + + Here, constructor inlining happens on the right hand side *of `ex`* + rather than of `triple`. + +Reflection +---------- + +Changes to the meta-programming facilities. + +* New reflection primitive: `checkFromStringTC : String → Type → TC Term` + + Parse and type check the given string against the given type, returning + the resulting term (when successful). + + +Library management +------------------ + +* **BREAKING**: Agda no longer accepts several `.agda-lib` files in the root + of an Agda project. + (Previously, it allowed this and took the union of their contents.) + + +Interaction and emacs mode +-------------------------- + +* Agda's error messages now follow the [GNU standard](https://www.gnu.org/prep/standards/html_node/Errors.html). + To comply with this policy, line and column are now separated by a dot instead of comma. + The format of regular errors and error warnings follows this template: + + > _sourcefile_:_line1_._column1_-_line2_._column2_: error: [_ErrorName_] + > ... + > _error message_ + > ... + > when _error context_ + + _line2_ or even _column2_ can be missing, in some cases even the entire error location. + Internal errors might follow a different format. + + Warnings are printed in a similar format: + + > _sourcefile_:_line1_._column1_-_line2_._column2_: warning: -W[no]_WarningName_ + > ... + > _warning text_ + > ... + > when _warning context_ + +* Emacs: new face `agda2-highlight-cosmetic-problem-face` + for highlighting the new aspect `CosmeticProblem`. + +* Emacs: new face `agda2-highlight-instance-problem-face` + for highlighting the new aspect `InstanceProblem`. + +* When generating clauses after case splitting on a datatype defined in a parameterised module, + Agda now prints constructor names without a module prefix rather than fully qualified (see issue #3209). + This is only a surface-level fix, since Agda might still fail to find the properly qualified name for + the constructor in scope, but should at least make more sense in most situations. + +* New bindings for unicode 'tacks' (⟘⟙⟛⟝⟞⫫⫪) via \tack (as well as specialised names for each of them) + +Backends +-------- + +* New `backendInteractTop/backendInteractHole` fields for providing backend-specific interaction commands + (run with keyboard shortcut `C-c C-i`). + +* Buggy unused argument optimization removed from the JavaScript backend + ([PR #7509](https://github.com/agda/agda/pull/7509)). + +Issues closed +------------- + +For 2.8.0, the following issues were +[closed](https://github.com/agda/agda/issues?q=is%3Aissue+milestone%3A2.8.0+is%3Aclosed) +(see [bug tracker](https://github.com/agda/agda/issues)): + +Issues for closed for milestone 2.8.0 +- [Issue #570](https://github.com/agda/agda/issues/570): Explicit polarity annotation +- [Issue #2004](https://github.com/agda/agda/issues/2004): `DISPLAY` should be more pragmatic +- [Issue #4100](https://github.com/agda/agda/issues/4100): GHC backend produces code that is wrongly compiled by GHC 8.4.* and 8.6.* +- [Issue #4338](https://github.com/agda/agda/issues/4338): Add mechanism to type check entire Agda libraries +- [Issue #4343](https://github.com/agda/agda/issues/4343): File order of checking matters (rewrite rules) +- [Issue #5299](https://github.com/agda/agda/issues/5299): Postfix projections are not documented +- [Issue #5865](https://github.com/agda/agda/issues/5865): Non Pattern Match Lambdas Missing From Docs +- [Issue #6111](https://github.com/agda/agda/issues/6111): Is compile-time irrelevance supposed to be erased with `COMPILE` pragmas? +- [Issue #6320](https://github.com/agda/agda/issues/6320): Parse strings to terms as reflection operation +- [Issue #6657](https://github.com/agda/agda/issues/6657): Turn `--guardedness` warning into an error-hint +- [Issue #6781](https://github.com/agda/agda/issues/6781): Making `@tactic` arguments visible leads to unsolved constraints +- [Issue #6916](https://github.com/agda/agda/issues/6916): Internal error at Agda/TypeChecking/Sort.hs:224:21 +- [Issue #6964](https://github.com/agda/agda/issues/6964): Allow referring to unnamed record constructors +- [Issue #6994](https://github.com/agda/agda/issues/6994): Warnings are turned off, but code is still highlighted +- [Issue #7057](https://github.com/agda/agda/issues/7057): Document let-bindings in telescopes +- [Issue #7066](https://github.com/agda/agda/issues/7066): Documentation for anonymous modules +- [Issue #7157](https://github.com/agda/agda/issues/7157): Future: cabal build-type `Setup` will be phased out in favor of `Hooks` +- [Issue #7163](https://github.com/agda/agda/issues/7163): `cabal install Agda` fails with executable-dynamic +- [Issue #7321](https://github.com/agda/agda/issues/7321): No warning about useless `{-# CATCHALL #-}` pragma +- [Issue #7324](https://github.com/agda/agda/issues/7324): HTML backend: inconsistent highlighting for macro names +- [Issue #7375](https://github.com/agda/agda/issues/7375): The specification of `--safe` misses the pragmas +- [Issue #7381](https://github.com/agda/agda/issues/7381): Our error messages do not follow the GNU standard +- [Issue #7392](https://github.com/agda/agda/issues/7392): Pattern matching unifier does not preserve instances +- [Issue #7434](https://github.com/agda/agda/issues/7434): Range printed twice for "Parse error" +- [Issue #7440](https://github.com/agda/agda/issues/7440): Unexpected hidden argument in nested records/modules +- [Issue #7495](https://github.com/agda/agda/issues/7495): Catchall clauses with less arguments are considered exact +- [Issue #7503](https://github.com/agda/agda/issues/7503): Cumulativity `Prop <= Set` loses canonicity +- [Issue #7507](https://github.com/agda/agda/issues/7507): Broken CI/haskell installation on GitHub? +- [Issue #7508](https://github.com/agda/agda/issues/7508): Unused-arg optimization breaks function call +- [Issue #7517](https://github.com/agda/agda/issues/7517): `quoteTerm` accepts hidden arguments +- [Issue #7529](https://github.com/agda/agda/issues/7529): Strange problem with --level-universe and --cubical +- [Issue #7530](https://github.com/agda/agda/issues/7530): Generalized variable blocks projection-likeness +- [Issue #7531](https://github.com/agda/agda/issues/7531): JS backend crashes on big case split +- [Issue #7533](https://github.com/agda/agda/issues/7533): `DISPLAY` pragmas should treat any defined name as matchable +- [Issue #7535](https://github.com/agda/agda/issues/7535): Regression in 2.6.4: Agda thinks large propositions can be transported +- [Issue #7537](https://github.com/agda/agda/issues/7537): Type checking a definition with higher inductive type fails to terminate +- [Issue #7546](https://github.com/agda/agda/issues/7546): Why do we allow empty POLARITY pragmas? +- [Issue #7573](https://github.com/agda/agda/issues/7573): `primFloatRound` broken in JS +- [Issue #7574](https://github.com/agda/agda/issues/7574): Support GHC 9.12 +- [Issue #7575](https://github.com/agda/agda/issues/7575): impossible error: `variable` in `BUILTIN` +- [Issue #7576](https://github.com/agda/agda/issues/7576): impossible error: parameter overflow in `declareData` +- [Issue #7580](https://github.com/agda/agda/issues/7580): Our Setup.hs does not build with Cabal-3.14 +- [Issue #7585](https://github.com/agda/agda/issues/7585): Happy-2.1.1 causes Agda build to fail +- [Issue #7587](https://github.com/agda/agda/issues/7587): Mimer takes an absurd lambda as the solution of the original goal rather than the current (sub)goal +- [Issue #7588](https://github.com/agda/agda/issues/7588): __IMPOSSIBLE__, called at src/full/Agda/Compiler/JS/Compiler.hs:596:45 +- [Issue #7590](https://github.com/agda/agda/issues/7590): Internal error with interaction point in a shared type signature +- [Issue #7618](https://github.com/agda/agda/issues/7618): De Bruijn index out of scope in the presence of rewrite rules and records +- [Issue #7624](https://github.com/agda/agda/issues/7624): Internal error when interactively checking expression with new meta-variables +- [Issue #7639](https://github.com/agda/agda/issues/7639): Internal error in `Agda/TypeChecking/Monad/Context.hs` using Mimer +- [Issue #7641](https://github.com/agda/agda/issues/7641): No error highlighting when "fits in" test fails +- [Issue #7642](https://github.com/agda/agda/issues/7642): Better not claim "Level should be a function type" +- [Issue #7643](https://github.com/agda/agda/issues/7643): Panic: uncaught pattern violation +- [Issue #7650](https://github.com/agda/agda/issues/7650): Internal error when utilizing Emacs case splits and `with .. in ..` +- [Issue #7655](https://github.com/agda/agda/issues/7655): haskell/cabal#10235 can still occur with Agda-2.7.0.1 +- [Issue #7659](https://github.com/agda/agda/issues/7659): Using auto leads to `__IMPOSSIBLE__` when Σ and case_of_ are both present +- [Issue #7660](https://github.com/agda/agda/issues/7660): Add a warning for unresolved constructor name +- [Issue #7662](https://github.com/agda/agda/issues/7662): Using Auto with a goal involving musical coinduction `♭` produces incorrect projection +- [Issue #7668](https://github.com/agda/agda/issues/7668): Inductive identity allowed in negative position, inconsistent in Cubical Agda +- [Issue #7669](https://github.com/agda/agda/issues/7669): Positivity checker doesn't respect definitional equality +- [Issue #7673](https://github.com/agda/agda/issues/7673): `nix build` skips "generation of Agda core library interface files" +- [Issue #7675](https://github.com/agda/agda/issues/7675): `toIFile` logic from #6988 leads to scattering of `.agdai` files +- [Issue #7678](https://github.com/agda/agda/issues/7678): Order of agda-lib files in a directory affects flag settings +- [Issue #7692](https://github.com/agda/agda/issues/7692): Option to completely disable generation of dot patterns +- [Issue #7696](https://github.com/agda/agda/issues/7696): Panic: de Bruijn index out of scope +- [Issue #7707](https://github.com/agda/agda/issues/7707): ConstructorDoesNotFitInData error for record in Prop with Set fields +- [Issue #7709](https://github.com/agda/agda/issues/7709): Slow typecheck when importing a module with instances +- [Issue #7710](https://github.com/agda/agda/issues/7710): Forcing evaluation can give incorrect results in ghc compiled code +- [Issue #7712](https://github.com/agda/agda/issues/7712): Embed data files using file-embed +- [Issue #7722](https://github.com/agda/agda/issues/7722): Exponential behavior in pattern operator parser +- [Issue #7730](https://github.com/agda/agda/issues/7730): emacs-mode files fail to build with "file has no `lexical-binding` directive" +- [Issue #7738](https://github.com/agda/agda/issues/7738): Rewriting by a constructor +- [Issue #7751](https://github.com/agda/agda/issues/7751): Application of module with datatype fools the termination checker +- [Issue #7753](https://github.com/agda/agda/issues/7753): Coverage checker internal error with copatterns and dot patterns +- [Issue #7759](https://github.com/agda/agda/issues/7759): Internal error for ellipsis without with-patterns +- [Issue #7761](https://github.com/agda/agda/issues/7761): Propω is not actually proof irrelevant +- [Issue #7765](https://github.com/agda/agda/issues/7765): Supply reason with UselessPublic warning +- [Issue #7766](https://github.com/agda/agda/issues/7766): .lagda.org: {-1} outside agda code block messes up hole detection +- [Issue #7769](https://github.com/agda/agda/issues/7769): The warning OpenPublicAbstract is wrongly formulated +- [Issue #7777](https://github.com/agda/agda/issues/7777): Parse error when using tactic and irrelevance +- [Issue #7788](https://github.com/agda/agda/issues/7788): TooManyPatternsInWithClause when nesting hidden `with` +- [Issue #7792](https://github.com/agda/agda/issues/7792): Inlining happens at most twice +- [Issue #7795](https://github.com/agda/agda/issues/7795): Polarity annotation ignored by positivity checker? +- [Issue #7796](https://github.com/agda/agda/issues/7796): Distinguish --no-guardedness from default value in termination hints? +- [Issue #7799](https://github.com/agda/agda/issues/7799): Potential regression related to instance resolution +- [Issue #7811](https://github.com/agda/agda/issues/7811): Internal error with Path and with-abstraction II +- [Issue #7815](https://github.com/agda/agda/issues/7815): Missing highlighting in module telescopes +- [Issue #7823](https://github.com/agda/agda/issues/7823): DISPLAY matches pattern with wrong amount of arguments +- [Issue #7825](https://github.com/agda/agda/issues/7825): DISPLAY form on irrelevant projection drops arguments +- [Issue #7832](https://github.com/agda/agda/issues/7832): Recursive function over inductive record treats arguments as irrelevant +- [Issue #7851](https://github.com/agda/agda/issues/7851): Error TooManyPolarities is too eager +- [Issue #7853](https://github.com/agda/agda/issues/7853): Subject reduction failure with instance constructors in parameterised modules +- [Issue #7856](https://github.com/agda/agda/issues/7856): Strange interaction between `opaque` and extended lambdas +- [Issue #7863](https://github.com/agda/agda/issues/7863): Internal error when calling MakeCase on target `__` +- [Issue #7878](https://github.com/agda/agda/issues/7878): Impossible with malformed notation RHS +- [Issue #7884](https://github.com/agda/agda/issues/7884): Better documentation of forester backend in CHANGELOG +- [Issue #7898](https://github.com/agda/agda/issues/7898): Solving with auto doesn't update constraints +- [Issue #7903](https://github.com/agda/agda/issues/7903): Constructor inlining defeated by moving binders +- [Issue #7911](https://github.com/agda/agda/issues/7911): `UnsolvedConstraints` error should reference location even when all metas were solved +- [Issue #7912](https://github.com/agda/agda/issues/7912): Missing error location for error: [ModuleNameDoesntMatchFileName] +- [Issue #7916](https://github.com/agda/agda/issues/7916): Make `-f optimise-heavily` default +- [Issue #7935](https://github.com/agda/agda/issues/7935): Document scoping rules for rewrite rules +- [Issue #7938](https://github.com/agda/agda/issues/7938): Request: Expose backend-internal modules as part of the library +- [Issue #7943](https://github.com/agda/agda/issues/7943): Local erased definition remains in compiled code +- [Issue #7944](https://github.com/agda/agda/issues/7944): Local erased modules break erasure analysis +- [Issue #7952](https://github.com/agda/agda/issues/7952): Primitive root example in docs +- [Issue #7953](https://github.com/agda/agda/issues/7953): Confusing error in case of illegal declaration before top-level module in a nested file +- [Issue #7966](https://github.com/agda/agda/issues/7966): Disallow option abbreviation +- [Issue #7973](https://github.com/agda/agda/issues/7973): If rewrite does not rewrite anything, give a warning +- [Issue #7977](https://github.com/agda/agda/issues/7977): Soft error for unknown attributes + +PRs for closed for milestone 2.8.0 + +- [PR #6629](https://github.com/agda/agda/issues/6629): Reflection primitive for parsing surface level syntax from string. +- [PR #7010](https://github.com/agda/agda/issues/7010): [new] backend-end specific interaction +- [PR #7023](https://github.com/agda/agda/issues/7023): Add ⧺ in agda-input.el +- [PR #7287](https://github.com/agda/agda/issues/7287): Temporary fix for reflection of partial elements. +- [PR #7366](https://github.com/agda/agda/issues/7366): Handle symlinks correctly when computing interface file locations +- [PR #7374](https://github.com/agda/agda/issues/7374): New warning `WithClauseProjectionFixityMismatch` instead of GenericError +- [PR #7377](https://github.com/agda/agda/issues/7377): New warning `RecursiveDisplayForm` instead of hard error +- [PR #7379](https://github.com/agda/agda/issues/7379): Print error name with error message +- [PR #7385](https://github.com/agda/agda/issues/7385): New error group GHCBackendError instead of GenericError +- [PR #7387](https://github.com/agda/agda/issues/7387): Factor out `give_` and remove PatternErr handler +- [PR #7388](https://github.com/agda/agda/issues/7388): GenericError crusade, continued +- [PR #7391](https://github.com/agda/agda/issues/7391): New error NeedOptionAllowExec etc. instead of GenericError +- [PR #7394](https://github.com/agda/agda/issues/7394): New error group InteractionError +- [PR #7395](https://github.com/agda/agda/issues/7395): Get rid of some MonadFail in favor of __IMPOSSIBLE__ +- [PR #7396](https://github.com/agda/agda/issues/7396): instance warning +- [PR #7403](https://github.com/agda/agda/issues/7403): New literate programming backend forester, `*.lagda.tree` +- [PR #7409](https://github.com/agda/agda/issues/7409): GenericError crusade goes on: NeedOptionSizedTypes etc. +- [PR #7412](https://github.com/agda/agda/issues/7412): pattern in path lambda +- [PR #7414](https://github.com/agda/agda/issues/7414): Replace interaction `Cmd_no_metas` by `Cmd_load_no_metas` +- [PR #7415](https://github.com/agda/agda/issues/7415): Error refactoring: use of `Exception`, generic errors +- [PR #7418](https://github.com/agda/agda/issues/7418): New errors CannotGenerate{HComp,Transport}Clause +- [PR #7425](https://github.com/agda/agda/issues/7425): GenericError replacements +- [PR #7426](https://github.com/agda/agda/issues/7426): #7371: add Mimer tests for -s and -l +- [PR #7430](https://github.com/agda/agda/issues/7430): Warnings instead of GenericError for ill-formed pragmas +- [PR #7435](https://github.com/agda/agda/issues/7435): Print warning name on same line as location +- [PR #7437](https://github.com/agda/agda/issues/7437): Reform printing of parse error +- [PR #7447](https://github.com/agda/agda/issues/7447): Add new error `InvalidModalTelescopeUse` and add reproducer. +- [PR #7451](https://github.com/agda/agda/issues/7451): New warning FixingRelevance instead of GenericError +- [PR #7453](https://github.com/agda/agda/issues/7453): New error NotAllowedInDotPatterns instead of GenericError +- [PR #7458](https://github.com/agda/agda/issues/7458): Add ZuriHac Video to tutorial-list +- [PR #7459](https://github.com/agda/agda/issues/7459): NotAValidLet{Expression,Binding} instead of GenericError +- [PR #7462](https://github.com/agda/agda/issues/7462): Naming generic syntax errors (GenericError quest) +- [PR #7473](https://github.com/agda/agda/issues/7473): Re #6919: also separate compilation warnings by newlines +- [PR #7478](https://github.com/agda/agda/issues/7478): Store warnings in a set rather than a list +- [PR #7481](https://github.com/agda/agda/issues/7481): Named Backend errors instead of GenericError +- [PR #7483](https://github.com/agda/agda/issues/7483): Some named scope errors replacing GenericError +- [PR #7488](https://github.com/agda/agda/issues/7488): Named scope errors instead of GenericError +- [PR #7491](https://github.com/agda/agda/issues/7491): ES6 modules +- [PR #7492](https://github.com/agda/agda/issues/7492): Correctly print ParserWarning range, remove `mdo` +- [PR #7496](https://github.com/agda/agda/issues/7496): Fix #7495: Check extra split clause patterns are trivial for exactness +- [PR #7498](https://github.com/agda/agda/issues/7498): Add Left Multimap (⟜) to agda-input.el +- [PR #7500](https://github.com/agda/agda/issues/7500): Fix & test `primShowNat` +- [PR #7501](https://github.com/agda/agda/issues/7501): handle ProjPs in DISPLAY pragmas +- [PR #7502](https://github.com/agda/agda/issues/7502): Make termination checking more permissive wrt non-exact clause reduction +- [PR #7504](https://github.com/agda/agda/issues/7504): [ fix #7503 ] Use principal sort of datatype for checking if split is ok +- [PR #7509](https://github.com/agda/agda/issues/7509): Fix #7508: remove unused-arg optimization from the JS backend +- [PR #7510](https://github.com/agda/agda/issues/7510): Expose the names of generated record constructors (reopen #6975) +- [PR #7511](https://github.com/agda/agda/issues/7511): Fix #7381: comply to GNU error standard: use dot instead of comma in ranges +- [PR #7512](https://github.com/agda/agda/issues/7512): GenericError crusade +- [PR #7513](https://github.com/agda/agda/issues/7513): Reconcile PR #7510 with commit ac2888a7ad: add Maybe Induction to scopeRecords +- [PR #7516](https://github.com/agda/agda/issues/7516): New error CannotQuote instead of GenericError +- [PR #7518](https://github.com/agda/agda/issues/7518): OccursCheckErrors +- [PR #7520](https://github.com/agda/agda/issues/7520): Drop GHC 8.6 +- [PR #7534](https://github.com/agda/agda/issues/7534): Fix #7529: treat `LevelUniv` in Cubical Agda +- [PR #7536](https://github.com/agda/agda/issues/7536): Re #7533: warn when DISPLAY form binds variables unused on the rhs +- [PR #7539](https://github.com/agda/agda/issues/7539): Fix #7413: Cubical: a `GenericError` is actually `__IMPOSSIBLE__` +- [PR #7543](https://github.com/agda/agda/issues/7543): DISPLAY: match on defined names +- [PR #7545](https://github.com/agda/agda/issues/7545): Fix #7531: Preserve let bindings in the JS backend +- [PR #7550](https://github.com/agda/agda/issues/7550): Fix #7546: warn about empty POLARITY pragmas +- [PR #7555](https://github.com/agda/agda/issues/7555): Some error housekeeping +- [PR #7556](https://github.com/agda/agda/issues/7556): unquote errors +- [PR #7557](https://github.com/agda/agda/issues/7557): kill GenericError in instance search +- [PR #7559](https://github.com/agda/agda/issues/7559): Fix compilation of serialisation code on 32 bit platforms +- [PR #7566](https://github.com/agda/agda/issues/7566): Make dangling hidden/instance args into a warning +- [PR #7570](https://github.com/agda/agda/issues/7570): Optimize concrete name scopeLookup +- [PR #7572](https://github.com/agda/agda/issues/7572): Improvements to let desugaring +- [PR #7577](https://github.com/agda/agda/issues/7577): chore: remove uses of genericError +- [PR #7581](https://github.com/agda/agda/issues/7581): don't add generalizedTel definitions to mutual blocks +- [PR #7583](https://github.com/agda/agda/issues/7583): Implement conversion to JS `BigInt` +- [PR #7586](https://github.com/agda/agda/issues/7586): Support Happy 2.1.1 +- [PR #7589](https://github.com/agda/agda/issues/7589): Fix #7575: Check if variables are generalizable in builtin pragmas +- [PR #7591](https://github.com/agda/agda/issues/7591): Fix #7588: Remove overlapping branches when simplifying chained cases +- [PR #7593](https://github.com/agda/agda/issues/7593): Fix #7576 +- [PR #7604](https://github.com/agda/agda/issues/7604): REPL: fix printing of result of `:typeOf` +- [PR #7613](https://github.com/agda/agda/issues/7613): Correct parameters to wrapper modules created in module telescopes +- [PR #7617](https://github.com/agda/agda/issues/7617): Fix de Bruijn indices in Treeless primitive translation +- [PR #7622](https://github.com/agda/agda/issues/7622): [ fix #7618 ] Use `underAbstraction_` for going under lambda in `reduceAndEtaContract` +- [PR #7640](https://github.com/agda/agda/issues/7640): [ emacs ] adding su(b/p)(sim/approx) to input method +- [PR #7645](https://github.com/agda/agda/issues/7645): Fix #7642: new error CannotApply that mentions also term, not only type +- [PR #7648](https://github.com/agda/agda/issues/7648): Fix #7641: Range for ConstructorDoesNotFit warning (anon. rec. con.) +- [PR #7651](https://github.com/agda/agda/issues/7651): Fix #7650: Throw CaseSplitError when splitting on with-abstraction equality +- [PR #7652](https://github.com/agda/agda/issues/7652): remove the cubical identity type +- [PR #7653](https://github.com/agda/agda/issues/7653): Print point-ranges as such (line.col rather than line:col-col) +- [PR #7657](https://github.com/agda/agda/issues/7657): Setup: unconditionally check if we want interfaces +- [PR #7670](https://github.com/agda/agda/issues/7670): Fix typo `COMPILED` +- [PR #7672](https://github.com/agda/agda/issues/7672): Fix #7643: coverage: handle blocked sort in isFibrant +- [PR #7674](https://github.com/agda/agda/issues/7674): Fix #7669: positivity checker: compute function arity up to def. eq. +- [PR #7676](https://github.com/agda/agda/issues/7676): Remove `--local-interfaces` and warning `DuplicateInterfaceFiles` +- [PR #7677](https://github.com/agda/agda/issues/7677): Setup: fix `wantInterfaces` check +- [PR #7679](https://github.com/agda/agda/issues/7679): Disallow several .agda-lib files in the project root (#7678) +- [PR #7682](https://github.com/agda/agda/issues/7682): New main mode `--build-library` +- [PR #7685](https://github.com/agda/agda/issues/7685): Add dump-core cabal flag +- [PR #7686](https://github.com/agda/agda/issues/7686): Monomorphise unifyIndices +- [PR #7687](https://github.com/agda/agda/issues/7687): Make toTerm return a monadic function +- [PR #7688](https://github.com/agda/agda/issues/7688): Add some links to lecture notes and videos on Agda +- [PR #7697](https://github.com/agda/agda/issues/7697): Fix #7696: Add missing `addContext` when splitting on literals +- [PR #7699](https://github.com/agda/agda/issues/7699): Remove custom Setup.hs +- [PR #7700](https://github.com/agda/agda/issues/7700): Never generate dot patterns under --keep-pattern-variables +- [PR #7704](https://github.com/agda/agda/issues/7704): Speed up nix build +- [PR #7719](https://github.com/agda/agda/issues/7719): Embed data files into Agda binary +- [PR #7726](https://github.com/agda/agda/issues/7726): Compare overlapping instances in the right context +- [PR #7727](https://github.com/agda/agda/issues/7727): Fix #7722: in pattern parser only consider pattern-relevant operators +- [PR #7728](https://github.com/agda/agda/issues/7728): Improvements to instance search performance +- [PR #7729](https://github.com/agda/agda/issues/7729): Let Agda perform several of `--help`, `--version` etc. if the user requests so +- [PR #7732](https://github.com/agda/agda/issues/7732): Duplicate `agda-mode` as `agda --emacs-mode` +- [PR #7734](https://github.com/agda/agda/issues/7734): Doc: executable-dynamic no longer a problem on Linux +- [PR #7739](https://github.com/agda/agda/issues/7739): Fix #7738: Allow rewrite rule defined with constructor or primitive +- [PR #7742](https://github.com/agda/agda/issues/7742): Fix #7741: Fix printing inserted binder from operator section +- [PR #7743](https://github.com/agda/agda/issues/7743): Re-enable dot-pattern termination for Cubical Agda +- [PR #7745](https://github.com/agda/agda/issues/7745): Limit depth of constructed discrimination tree +- [PR #7746](https://github.com/agda/agda/issues/7746): Compute occurrences in trX “constructors” +- [PR #7750](https://github.com/agda/agda/issues/7750): Support GHC 9.12.2 +- [PR #7752](https://github.com/agda/agda/issues/7752): Fix #7751: Consider datatype clauses generated from module application in recursion checker +- [PR #7758](https://github.com/agda/agda/issues/7758): Fix #7753: a possible `__IMPOSSIBLE__` +- [PR #7763](https://github.com/agda/agda/issues/7763): Fix #7761: Include large Prop in checks whether something is a Prop +- [PR #7764](https://github.com/agda/agda/issues/7764): Fixed #7730 +- [PR #7767](https://github.com/agda/agda/issues/7767): Fix #7766: emacs org mode: fix code block end detection +- [PR #7768](https://github.com/agda/agda/issues/7768): Reason for UselessPublic; `private` useless in `where` blocks +- [PR #7771](https://github.com/agda/agda/issues/7771): Fix #7769: replace warning `OpenPublic{Abstract,Private}` +- [PR #7772](https://github.com/agda/agda/issues/7772): Fix #7707: wording of warning `ConstructorDoesNotFitInData` +- [PR #7773](https://github.com/agda/agda/issues/7773): Fix #7662: Mimer: special case for printing ♭ +- [PR #7774](https://github.com/agda/agda/issues/7774): Fix #7321: warn about unused CATCHALL pragmas +- [PR #7775](https://github.com/agda/agda/issues/7775): Fix #6994: highlighting only for enabled warnings +- [PR #7776](https://github.com/agda/agda/issues/7776): Fix #7624 by reifying Term before wrapping it in GoalAndElaboration +- [PR #7778](https://github.com/agda/agda/issues/7778): Fix #6657: termination checker hints at missing --guardedness flag +- [PR #7782](https://github.com/agda/agda/issues/7782): re #3209: print out-of-scope names unqualified in case splits +- [PR #7783](https://github.com/agda/agda/issues/7783): Don't inline constructors into inline functions +- [PR #7785](https://github.com/agda/agda/issues/7785): Fix #7777: parse both attributes and irrelevance markers +- [PR #7786](https://github.com/agda/agda/issues/7786): New warning `UselessTactic` for `tactic` attribute on non-hidden binder +- [PR #7787](https://github.com/agda/agda/issues/7787): Small fixes for parsing and printing attributes +- [PR #7789](https://github.com/agda/agda/issues/7789): Fix issues #7759 and #7788: wrong counting of with-patterns in nested with +- [PR #7791](https://github.com/agda/agda/issues/7791): [ new ] unicode symbols for various 'tacks' +- [PR #7793](https://github.com/agda/agda/issues/7793): re #7792: keep inlining after inlining a copy +- [PR #7800](https://github.com/agda/agda/issues/7800): Fix #7796: don't hint towards --guardedness when --no-guardedness +- [PR #7802](https://github.com/agda/agda/issues/7802): Remove broken AbsurdLam heuristics from Mimer +- [PR #7804](https://github.com/agda/agda/issues/7804): re #7799: add instance hack to checkSectionApplication +- [PR #7812](https://github.com/agda/agda/issues/7812): Fix #7803 fix #7811: new error PathAbstractionFailed instead of crash +- [PR #7814](https://github.com/agda/agda/issues/7814): Fix #7660: new DisambiguateConstructor postponed tc problem +- [PR #7816](https://github.com/agda/agda/issues/7816): re #7815: propagate range into wrapper modules +- [PR #7817](https://github.com/agda/agda/issues/7817): Add documentation for telescopes and some related things +- [PR #7818](https://github.com/agda/agda/issues/7818): Make data directory overridable, default to XDG_DATA_HOME +- [PR #7819](https://github.com/agda/agda/issues/7819): [ fix #7392 ] Ensure wildcards and variable instances are kept +- [PR #7822](https://github.com/agda/agda/issues/7822): Fix issue #7537 +- [PR #7824](https://github.com/agda/agda/issues/7824): Fix #7823: Compare number of arguments when matching on DISPLAY pragma +- [PR #7826](https://github.com/agda/agda/issues/7826): Fix #7825 by using `droppedPars` instead of hand-knitted code +- [PR #7830](https://github.com/agda/agda/issues/7830): Disregard qualified names when assigning clauses to functions in the nicifier +- [PR #7831](https://github.com/agda/agda/issues/7831): Fix #7829 by reactivating my own fix of #1618 +- [PR #7834](https://github.com/agda/agda/issues/7834): fix #7795: Use occurrences from type for defs +- [PR #7840](https://github.com/agda/agda/issues/7840): Document which pragmas are unsafe +- [PR #7848](https://github.com/agda/agda/issues/7848): fix #7846: instance hack in abstract axioms +- [PR #7849](https://github.com/agda/agda/issues/7849): Fix for #7639 +- [PR #7850](https://github.com/agda/agda/issues/7850): Re #7225: new error DatatypeIndexPolarity instead of GenericError +- [PR #7852](https://github.com/agda/agda/issues/7852): Turn TooManyPolarities error into warning (fixes #7851) +- [PR #7854](https://github.com/agda/agda/issues/7854): Modality warnings for constructors and fields +- [PR #7855](https://github.com/agda/agda/issues/7855): Re #7225 name error CubicalNotErasure +- [PR #7857](https://github.com/agda/agda/issues/7857): Forget opacity when checking signatures +- [PR #7858](https://github.com/agda/agda/issues/7858): Fix for #7659 +- [PR #7859](https://github.com/agda/agda/issues/7859): Fix #7853: don't drop parameters of constructor in the same module +- [PR #7860](https://github.com/agda/agda/issues/7860): [ re #7587 ] Properly reintroduce absurd lambdas to Mimer +- [PR #7865](https://github.com/agda/agda/issues/7865): Fix #7863: properly parse names before case-splitting +- [PR #7867](https://github.com/agda/agda/issues/7867): Fix #7832 by placing properlyMatching in monad to have isEtaRecordConstructor +- [PR #7879](https://github.com/agda/agda/issues/7879): Fix #7878: reorder checks in `mkNotation` +- [PR #7880](https://github.com/agda/agda/issues/7880): Defer `MissingDefinitions` error in `--safe` until after typechecking +- [PR #7885](https://github.com/agda/agda/issues/7885): disable discrim-based instance deferral by default +- [PR #7886](https://github.com/agda/agda/issues/7886): [doc] explain how to do postprocessing for literate forester +- [PR #7891](https://github.com/agda/agda/issues/7891): Remove duplicate inverse scope computation. +- [PR #7895](https://github.com/agda/agda/issues/7895): Fix #7590 +- [PR #7896](https://github.com/agda/agda/issues/7896): Fix #7324: highlighting of macro names in their definition +- [PR #7900](https://github.com/agda/agda/issues/7900): intro: filter (higher) constructors based on dimension +- [PR #7901](https://github.com/agda/agda/issues/7901): Properly update interaction points when solving with Mimer +- [PR #7904](https://github.com/agda/agda/issues/7904): Fix lexical-scope issue in emacs mode +- [PR #7907](https://github.com/agda/agda/issues/7907): Fix issue #7903: etaExpandClause before constructor inlining +- [PR #7913](https://github.com/agda/agda/issues/7913): Range information for unsolved instance constraints +- [PR #7920](https://github.com/agda/agda/issues/7920): Fix #7916: make optimise-heavily the default +- [PR #7924](https://github.com/agda/agda/issues/7924): Add a few notes on irrelevance +- [PR #7925](https://github.com/agda/agda/issues/7925): Add documentation for lambda expressions and absurd lambdas +- [PR #7931](https://github.com/agda/agda/issues/7931): Hint towards --guardedness even when --sized-types is on +- [PR #7932](https://github.com/agda/agda/issues/7932): Add `use-xdg-data-home` +- [PR #7934](https://github.com/agda/agda/issues/7934): Hygienic import of rewrite rules +- [PR #7936](https://github.com/agda/agda/issues/7936): Highlight only record keyword when fields are missing +- [PR #7939](https://github.com/agda/agda/issues/7939): Fix #7938: API: export Agda Highlighting Backend modules +- [PR #7942](https://github.com/agda/agda/issues/7942): [ doc ] remove reference to Cubical.Core.Everything +- [PR #7945](https://github.com/agda/agda/issues/7945): Fix #7944: do not apply `@0` from where-module to clause rhs +- [PR #7946](https://github.com/agda/agda/issues/7946): Fix #7943: propagate erasure status to `where` blocks. +- [PR #7956](https://github.com/agda/agda/issues/7956): Fix #7955: replace impossible with syntax error +- [PR #7957](https://github.com/agda/agda/issues/7957): Doc: replace PrimRoot by PrimeFactor in introductory text +- [PR #7958](https://github.com/agda/agda/issues/7958): Fix #7953: remember whether top-level module name was inferred +- [PR #7965](https://github.com/agda/agda/issues/7965): Re #7932: restore data-files in Agda.cabal and default data-dir +- [PR #7967](https://github.com/agda/agda/issues/7967): Fix #7966: fork GetOpt to disallow long option abbreviations +- [PR #7971](https://github.com/agda/agda/issues/7971): flake: use --build-library to build the builtins +- [PR #7978](https://github.com/agda/agda/issues/7978): Fix #7973: print warning if `rewrite` does not fire +- [PR #7981](https://github.com/agda/agda/issues/7981): Parse warning instead of error on unknown attributes and polarities diff --git a/src/data/emacs-mode/agda2-mode-pkg.el b/src/data/emacs-mode/agda2-mode-pkg.el --- a/src/data/emacs-mode/agda2-mode-pkg.el +++ b/src/data/emacs-mode/agda2-mode-pkg.el @@ -1,3 +1,3 @@ -(define-package "agda2-mode" "2.8.0" +(define-package "agda2-mode" "2.8.0.1" "interactive development for Agda, a dependently typed functional programming language" '((emacs "24.3"))) ;; dep defs for `annotation.el` and `eri.el` are not required if they are packaged together diff --git a/src/data/emacs-mode/agda2-mode.el b/src/data/emacs-mode/agda2-mode.el --- a/src/data/emacs-mode/agda2-mode.el +++ b/src/data/emacs-mode/agda2-mode.el @@ -29,7 +29,7 @@ ;;; Code: -(defvar agda2-version "2.8.0" +(defvar agda2-version "2.8.0.1" "The version of the Agda mode. Note that the same version of the Agda executable must be used.") @@ -2002,7 +2002,7 @@ If the version cannot be parsed, the answer is no. So e.g. agda-fast would be interpreted as not older than -agda-2.8.0" +agda-2.8.0.1" ;; If the given string does not have a numeric prefix, we answer no. (and (string-match "^[0-9][0-9.]*" version) (version< (match-string 0 version) "2.8"))) @@ -2026,7 +2026,7 @@ If VERSION is empty or \"agda\", then agda is used. A prefix \"agda-\" is stripped from VERSION, so one can invoke this function e.g. with -\"agda-2.8.0\" instead of \"2.8.0\". +\"agda-2.8.0.1\" instead of \"2.8.0.1\". An attempt is made to preserve the default value of `agda2-mode-hook'." (interactive @@ -2047,7 +2047,7 @@ ;; * Replace version "agda" by just "". ;; ;; Rationale: - ;; The user might by accident enter "agda-2.8.0" instead of "2.8.0", + ;; The user might by accident enter "agda-2.8.0.1" instead of "2.8.0.1", ;; or "agda" instead of "". (version (cond diff --git a/src/data/latex/agda.sty b/src/data/latex/agda.sty --- a/src/data/latex/agda.sty +++ b/src/data/latex/agda.sty @@ -6,7 +6,7 @@ % !!! NOTE: when you make changes to this file, bump the date. !!! % !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! \ProvidesPackage{agda} - [2021/07/14 version 2.8.0 Formatting LaTeX generated by Agda] + [2021/07/14 version 2.8.0.1 Formatting LaTeX generated by Agda] \RequirePackage{ifxetex, ifluatex, xifthen, xcolor, polytable, etoolbox, calc, environ, xparse, xkeyval} diff --git a/src/full/Agda/TypeChecking/Monad/Base.hs b/src/full/Agda/TypeChecking/Monad/Base.hs --- a/src/full/Agda/TypeChecking/Monad/Base.hs +++ b/src/full/Agda/TypeChecking/Monad/Base.hs @@ -1,5 +1,11 @@ {-# LANGUAGE CPP #-} -- {-# LANGUAGE UndecidableInstances #-} -- ghc >= 8.2, GeneralizedNewtypeDeriving MonadTransControl BlockT +-- Turning off DeepSubsumption for +-- SPECIALIZE mapTCMT :: (forall a. IO a -> IO a) -> TCM a -> TCM a +-- with GHC 9.14 +#if __GLASGOW_HASKELL__ >= 914 +{-# LANGUAGE NoDeepSubsumption #-} +#endif module Agda.TypeChecking.Monad.Base ( module Agda.TypeChecking.Monad.Base diff --git a/src/full/Agda/Utils/Map.hs b/src/full/Agda/Utils/Map.hs --- a/src/full/Agda/Utils/Map.hs +++ b/src/full/Agda/Utils/Map.hs @@ -1,3 +1,5 @@ +{-# LANGUAGE CPP #-} + module Agda.Utils.Map where import Data.Functor.Compose @@ -53,9 +55,11 @@ -- allWithKey :: (k -> a -> Bool) -> Map k a -> Bool -- allWithKey f = Map.foldrWithKey (\ k a b -> f k a && b) True +#if !MIN_VERSION_containers(0,8,0) -- | Filter a map based on the keys. filterKeys :: (k -> Bool) -> Map k a -> Map k a filterKeys p = Map.filterWithKey (const . p) +#endif -- UNUSED Andreas (2021-08-19) -- -- | O(n log n). Rebuilds the map from scratch. diff --git a/stack-9.10.2.yaml b/stack-9.10.2.yaml deleted file mode 100644 --- a/stack-9.10.2.yaml +++ /dev/null @@ -1,7 +0,0 @@ -resolver: nightly-2025-07-01 -compiler: ghc-9.10.2 -compiler-check: match-exact - -# Local packages specified by relative directory name. -packages: -- '.' diff --git a/stack-9.10.3.yaml b/stack-9.10.3.yaml new file mode 100644 --- /dev/null +++ b/stack-9.10.3.yaml @@ -0,0 +1,7 @@ +resolver: lts-24.55 +compiler: ghc-9.10.3 +compiler-check: match-exact + +# Local packages specified by relative directory name. +packages: +- '.' diff --git a/stack-9.12.2.yaml b/stack-9.12.2.yaml deleted file mode 100644 --- a/stack-9.12.2.yaml +++ /dev/null @@ -1,7 +0,0 @@ -resolver: nightly-2025-07-01 -compiler: ghc-9.12.2 -compiler-check: match-exact - -# Local packages specified by relative directory name. -packages: -- '.' diff --git a/stack-9.12.4.yaml b/stack-9.12.4.yaml new file mode 100644 --- /dev/null +++ b/stack-9.12.4.yaml @@ -0,0 +1,7 @@ +resolver: nightly-2026-08-16 +compiler: ghc-9.12.4 +compiler-check: match-exact + +# Local packages specified by relative directory name. +packages: +- '.' diff --git a/stack-9.14.1.yaml b/stack-9.14.1.yaml new file mode 100644 --- /dev/null +++ b/stack-9.14.1.yaml @@ -0,0 +1,7 @@ +resolver: nightly-2026-08-16 +compiler: ghc-9.14.1 +compiler-check: match-exact + +# Local packages specified by relative directory name. +packages: +- '.' diff --git a/stack-9.8.4.yaml b/stack-9.8.4.yaml --- a/stack-9.8.4.yaml +++ b/stack-9.8.4.yaml @@ -1,4 +1,4 @@ -resolver: lts-23.26 +resolver: lts-23.28 compiler: ghc-9.8.4 compiler-check: match-exact