Agda 2.8.0 → 2.8.0.1
raw patch · 15 files changed
+765/−740 lines, 15 filesdep ~basedep ~containersdep ~template-haskellPVP ok
version bump matches the API change (PVP)
Dependency ranges changed: base, containers, template-haskell, time
API changes (from Hackage documentation)
Files
- Agda.cabal +68/−67
- CHANGELOG.md +4/−637
- LICENSE +16/−15
- doc/release-notes/2.8.0.md +639/−0
- src/data/emacs-mode/agda2-mode-pkg.el +1/−1
- src/data/emacs-mode/agda2-mode.el +4/−4
- src/data/latex/agda.sty +1/−1
- src/full/Agda/TypeChecking/Monad/Base.hs +6/−0
- src/full/Agda/Utils/Map.hs +4/−0
- stack-9.10.2.yaml +0/−7
- stack-9.10.3.yaml +7/−0
- stack-9.12.2.yaml +0/−7
- stack-9.12.4.yaml +7/−0
- stack-9.14.1.yaml +7/−0
- stack-9.8.4.yaml +1/−1
Agda.cabal view
@@ -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
CHANGELOG.md view
@@ -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.
LICENSE view
@@ -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``.
+ doc/release-notes/2.8.0.md view
@@ -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
src/data/emacs-mode/agda2-mode-pkg.el view
@@ -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
src/data/emacs-mode/agda2-mode.el view
@@ -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
src/data/latex/agda.sty view
@@ -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}
src/full/Agda/TypeChecking/Monad/Base.hs view
@@ -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
src/full/Agda/Utils/Map.hs view
@@ -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.
− stack-9.10.2.yaml
@@ -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:-- '.'
+ stack-9.10.3.yaml view
@@ -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:+- '.'
− stack-9.12.2.yaml
@@ -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:-- '.'
+ stack-9.12.4.yaml view
@@ -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:+- '.'
+ stack-9.14.1.yaml view
@@ -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:+- '.'
stack-9.8.4.yaml view
@@ -1,4 +1,4 @@-resolver: lts-23.26+resolver: lts-23.28 compiler: ghc-9.8.4 compiler-check: match-exact