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). 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). Example:

  {-# 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 and issue #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:

  {-# 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:

  {-# 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:

  {-# 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. You will need the postprocessor 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 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

  let
    f : A → B → C
    f p1 p2 = ...
  in ...
  

  should be accepted exactly when, and have the same meaning as,

  let
    f : A → B → C
    f = λ p1 p2 → ...
  

  See #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 for the PR removing it from the library, and #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:

  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. 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).

Issues closed

For 2.8.0, the following issues were closed (see bug tracker):

Issues for closed for milestone 2.8.0

• Issue #570: Explicit polarity annotation
• Issue #2004: DISPLAY should be more pragmatic
• Issue #4100: GHC backend produces code that is wrongly compiled by GHC 8.4.* and 8.6.*
• Issue #4338: Add mechanism to type check entire Agda libraries
• Issue #4343: File order of checking matters (rewrite rules)
• Issue #5299: Postfix projections are not documented
• Issue #5865: Non Pattern Match Lambdas Missing From Docs
• Issue #6111: Is compile-time irrelevance supposed to be erased with COMPILE pragmas?
• Issue #6320: Parse strings to terms as reflection operation
• Issue #6657: Turn --guardedness warning into an error-hint
• Issue #6781: Making @tactic arguments visible leads to unsolved constraints
• Issue #6916: Internal error at Agda/TypeChecking/Sort.hs:224:21
• Issue #6964: Allow referring to unnamed record constructors
• Issue #6994: Warnings are turned off, but code is still highlighted
• Issue #7057: Document let-bindings in telescopes
• Issue #7066: Documentation for anonymous modules
• Issue #7157: Future: cabal build-type Setup will be phased out in favor of Hooks
• Issue #7163: cabal install Agda fails with executable-dynamic
• Issue #7321: No warning about useless {-# CATCHALL #-} pragma
• Issue #7324: HTML backend: inconsistent highlighting for macro names
• Issue #7375: The specification of --safe misses the pragmas
• Issue #7381: Our error messages do not follow the GNU standard
• Issue #7392: Pattern matching unifier does not preserve instances
• Issue #7434: Range printed twice for “Parse error”
• Issue #7440: Unexpected hidden argument in nested records/modules
• Issue #7495: Catchall clauses with less arguments are considered exact
• Issue #7503: Cumulativity Prop <= Set loses canonicity
• Issue #7507: Broken CI/haskell installation on GitHub?
• Issue #7508: Unused-arg optimization breaks function call
• Issue #7517: quoteTerm accepts hidden arguments
• Issue #7529: Strange problem with –level-universe and –cubical
• Issue #7530: Generalized variable blocks projection-likeness
• Issue #7531: JS backend crashes on big case split
• Issue #7533: DISPLAY pragmas should treat any defined name as matchable
• Issue #7535: Regression in 2.6.4: Agda thinks large propositions can be transported
• Issue #7537: Type checking a definition with higher inductive type fails to terminate
• Issue #7546: Why do we allow empty POLARITY pragmas?
• Issue #7573: primFloatRound broken in JS
• Issue #7574: Support GHC 9.12
• Issue #7575: impossible error: variable in BUILTIN
• Issue #7576: impossible error: parameter overflow in declareData
• Issue #7580: Our Setup.hs does not build with Cabal-3.14
• Issue #7585: Happy-2.1.1 causes Agda build to fail
• Issue #7587: Mimer takes an absurd lambda as the solution of the original goal rather than the current (sub)goal
• Issue #7588: IMPOSSIBLE, called at src/full/Agda/Compiler/JS/Compiler.hs:596:45
• Issue #7590: Internal error with interaction point in a shared type signature
• Issue #7618: De Bruijn index out of scope in the presence of rewrite rules and records
• Issue #7624: Internal error when interactively checking expression with new meta-variables
• Issue #7639: Internal error in Agda/TypeChecking/Monad/Context.hs using Mimer
• Issue #7641: No error highlighting when “fits in” test fails
• Issue #7642: Better not claim “Level should be a function type”
• Issue #7643: Panic: uncaught pattern violation
• Issue #7650: Internal error when utilizing Emacs case splits and with .. in ..
• Issue #7655: haskell/cabal#10235 can still occur with Agda-2.7.0.1
• Issue #7659: Using auto leads to __IMPOSSIBLE__ when Σ and case_of_ are both present
• Issue #7660: Add a warning for unresolved constructor name
• Issue #7662: Using Auto with a goal involving musical coinduction ♭ produces incorrect projection
• Issue #7668: Inductive identity allowed in negative position, inconsistent in Cubical Agda
• Issue #7669: Positivity checker doesn’t respect definitional equality
• Issue #7673: nix build skips “generation of Agda core library interface files”
• Issue #7675: toIFile logic from #6988 leads to scattering of .agdai files
• Issue #7678: Order of agda-lib files in a directory affects flag settings
• Issue #7692: Option to completely disable generation of dot patterns
• Issue #7696: Panic: de Bruijn index out of scope
• Issue #7707: ConstructorDoesNotFitInData error for record in Prop with Set fields
• Issue #7709: Slow typecheck when importing a module with instances
• Issue #7710: Forcing evaluation can give incorrect results in ghc compiled code
• Issue #7712: Embed data files using file-embed
• Issue #7722: Exponential behavior in pattern operator parser
• Issue #7730: emacs-mode files fail to build with “file has no lexical-binding directive”
• Issue #7738: Rewriting by a constructor
• Issue #7751: Application of module with datatype fools the termination checker
• Issue #7753: Coverage checker internal error with copatterns and dot patterns
• Issue #7759: Internal error for ellipsis without with-patterns
• Issue #7761: Propω is not actually proof irrelevant
• Issue #7765: Supply reason with UselessPublic warning
• Issue #7766: .lagda.org: {-1} outside agda code block messes up hole detection
• Issue #7769: The warning OpenPublicAbstract is wrongly formulated
• Issue #7777: Parse error when using tactic and irrelevance
• Issue #7788: TooManyPatternsInWithClause when nesting hidden with
• Issue #7792: Inlining happens at most twice
• Issue #7795: Polarity annotation ignored by positivity checker?
• Issue #7796: Distinguish –no-guardedness from default value in termination hints?
• Issue #7799: Potential regression related to instance resolution
• Issue #7811: Internal error with Path and with-abstraction II
• Issue #7815: Missing highlighting in module telescopes
• Issue #7823: DISPLAY matches pattern with wrong amount of arguments
• Issue #7825: DISPLAY form on irrelevant projection drops arguments
• Issue #7832: Recursive function over inductive record treats arguments as irrelevant
• Issue #7851: Error TooManyPolarities is too eager
• Issue #7853: Subject reduction failure with instance constructors in parameterised modules
• Issue #7856: Strange interaction between opaque and extended lambdas
• Issue #7863: Internal error when calling MakeCase on target __
• Issue #7878: Impossible with malformed notation RHS
• Issue #7884: Better documentation of forester backend in CHANGELOG
• Issue #7898: Solving with auto doesn’t update constraints
• Issue #7903: Constructor inlining defeated by moving binders
• Issue #7911: UnsolvedConstraints error should reference location even when all metas were solved
• Issue #7912: Missing error location for error: [ModuleNameDoesntMatchFileName]
• Issue #7916: Make -f optimise-heavily default
• Issue #7935: Document scoping rules for rewrite rules
• Issue #7938: Request: Expose backend-internal modules as part of the library
• Issue #7943: Local erased definition remains in compiled code
• Issue #7944: Local erased modules break erasure analysis
• Issue #7952: Primitive root example in docs
• Issue #7953: Confusing error in case of illegal declaration before top-level module in a nested file
• Issue #7966: Disallow option abbreviation
• Issue #7973: If rewrite does not rewrite anything, give a warning
• Issue #7977: Soft error for unknown attributes

PRs for closed for milestone 2.8.0

• PR #6629: Reflection primitive for parsing surface level syntax from string.
• PR #7010: [new] backend-end specific interaction
• PR #7023: Add ⧺ in agda-input.el
• PR #7287: Temporary fix for reflection of partial elements.
• PR #7366: Handle symlinks correctly when computing interface file locations
• PR #7374: New warning WithClauseProjectionFixityMismatch instead of GenericError
• PR #7377: New warning RecursiveDisplayForm instead of hard error
• PR #7379: Print error name with error message
• PR #7385: New error group GHCBackendError instead of GenericError
• PR #7387: Factor out give_ and remove PatternErr handler
• PR #7388: GenericError crusade, continued
• PR #7391: New error NeedOptionAllowExec etc. instead of GenericError
• PR #7394: New error group InteractionError
• PR #7395: Get rid of some MonadFail in favor of IMPOSSIBLE
• PR #7396: instance warning
• PR #7403: New literate programming backend forester, *.lagda.tree
• PR #7409: GenericError crusade goes on: NeedOptionSizedTypes etc.
• PR #7412: pattern in path lambda
• PR #7414: Replace interaction Cmd_no_metas by Cmd_load_no_metas
• PR #7415: Error refactoring: use of Exception, generic errors
• PR #7418: New errors CannotGenerate{HComp,Transport}Clause
• PR #7425: GenericError replacements
• PR #7426: #7371: add Mimer tests for -s and -l
• PR #7430: Warnings instead of GenericError for ill-formed pragmas
• PR #7435: Print warning name on same line as location
• PR #7437: Reform printing of parse error
• PR #7447: Add new error InvalidModalTelescopeUse and add reproducer.
• PR #7451: New warning FixingRelevance instead of GenericError
• PR #7453: New error NotAllowedInDotPatterns instead of GenericError
• PR #7458: Add ZuriHac Video to tutorial-list
• PR #7459: NotAValidLet{Expression,Binding} instead of GenericError
• PR #7462: Naming generic syntax errors (GenericError quest)
• PR #7473: Re #6919: also separate compilation warnings by newlines
• PR #7478: Store warnings in a set rather than a list
• PR #7481: Named Backend errors instead of GenericError
• PR #7483: Some named scope errors replacing GenericError
• PR #7488: Named scope errors instead of GenericError
• PR #7491: ES6 modules
• PR #7492: Correctly print ParserWarning range, remove mdo
• PR #7496: Fix #7495: Check extra split clause patterns are trivial for exactness
• PR #7498: Add Left Multimap (⟜) to agda-input.el
• PR #7500: Fix & test primShowNat
• PR #7501: handle ProjPs in DISPLAY pragmas
• PR #7502: Make termination checking more permissive wrt non-exact clause reduction
• PR #7504: [ fix #7503 ] Use principal sort of datatype for checking if split is ok
• PR #7509: Fix #7508: remove unused-arg optimization from the JS backend
• PR #7510: Expose the names of generated record constructors (reopen #6975)
• PR #7511: Fix #7381: comply to GNU error standard: use dot instead of comma in ranges
• PR #7512: GenericError crusade
• PR #7513: Reconcile PR #7510 with commit ac2888a7ad: add Maybe Induction to scopeRecords
• PR #7516: New error CannotQuote instead of GenericError
• PR #7518: OccursCheckErrors
• PR #7520: Drop GHC 8.6
• PR #7534: Fix #7529: treat LevelUniv in Cubical Agda
• PR #7536: Re #7533: warn when DISPLAY form binds variables unused on the rhs
• PR #7539: Fix #7413: Cubical: a GenericError is actually __IMPOSSIBLE__
• PR #7543: DISPLAY: match on defined names
• PR #7545: Fix #7531: Preserve let bindings in the JS backend
• PR #7550: Fix #7546: warn about empty POLARITY pragmas
• PR #7555: Some error housekeeping
• PR #7556: unquote errors
• PR #7557: kill GenericError in instance search
• PR #7559: Fix compilation of serialisation code on 32 bit platforms
• PR #7566: Make dangling hidden/instance args into a warning
• PR #7570: Optimize concrete name scopeLookup
• PR #7572: Improvements to let desugaring
• PR #7577: chore: remove uses of genericError
• PR #7581: don’t add generalizedTel definitions to mutual blocks
• PR #7583: Implement conversion to JS BigInt
• PR #7586: Support Happy 2.1.1
• PR #7589: Fix #7575: Check if variables are generalizable in builtin pragmas
• PR #7591: Fix #7588: Remove overlapping branches when simplifying chained cases
• PR #7593: Fix #7576
• PR #7604: REPL: fix printing of result of :typeOf
• PR #7613: Correct parameters to wrapper modules created in module telescopes
• PR #7617: Fix de Bruijn indices in Treeless primitive translation
• PR #7622: [ fix #7618 ] Use underAbstraction_ for going under lambda in reduceAndEtaContract
• PR #7640: [ emacs ] adding su(b/p)(sim/approx) to input method
• PR #7645: Fix #7642: new error CannotApply that mentions also term, not only type
• PR #7648: Fix #7641: Range for ConstructorDoesNotFit warning (anon. rec. con.)
• PR #7651: Fix #7650: Throw CaseSplitError when splitting on with-abstraction equality
• PR #7652: remove the cubical identity type
• PR #7653: Print point-ranges as such (line.col rather than line:col-col)
• PR #7657: Setup: unconditionally check if we want interfaces
• PR #7670: Fix typo COMPILED
• PR #7672: Fix #7643: coverage: handle blocked sort in isFibrant
• PR #7674: Fix #7669: positivity checker: compute function arity up to def. eq.
• PR #7676: Remove --local-interfaces and warning DuplicateInterfaceFiles
• PR #7677: Setup: fix wantInterfaces check
• PR #7679: Disallow several .agda-lib files in the project root (#7678)
• PR #7682: New main mode --build-library
• PR #7685: Add dump-core cabal flag
• PR #7686: Monomorphise unifyIndices
• PR #7687: Make toTerm return a monadic function
• PR #7688: Add some links to lecture notes and videos on Agda
• PR #7697: Fix #7696: Add missing addContext when splitting on literals
• PR #7699: Remove custom Setup.hs
• PR #7700: Never generate dot patterns under –keep-pattern-variables
• PR #7704: Speed up nix build
• PR #7719: Embed data files into Agda binary
• PR #7726: Compare overlapping instances in the right context
• PR #7727: Fix #7722: in pattern parser only consider pattern-relevant operators
• PR #7728: Improvements to instance search performance
• PR #7729: Let Agda perform several of --help, --version etc. if the user requests so
• PR #7732: Duplicate agda-mode as agda --emacs-mode
• PR #7734: Doc: executable-dynamic no longer a problem on Linux
• PR #7739: Fix #7738: Allow rewrite rule defined with constructor or primitive
• PR #7742: Fix #7741: Fix printing inserted binder from operator section
• PR #7743: Re-enable dot-pattern termination for Cubical Agda
• PR #7745: Limit depth of constructed discrimination tree
• PR #7746: Compute occurrences in trX “constructors”
• PR #7750: Support GHC 9.12.2
• PR #7752: Fix #7751: Consider datatype clauses generated from module application in recursion checker
• PR #7758: Fix #7753: a possible __IMPOSSIBLE__
• PR #7763: Fix #7761: Include large Prop in checks whether something is a Prop
• PR #7764: Fixed #7730
• PR #7767: Fix #7766: emacs org mode: fix code block end detection
• PR #7768: Reason for UselessPublic; private useless in where blocks
• PR #7771: Fix #7769: replace warning OpenPublic{Abstract,Private}
• PR #7772: Fix #7707: wording of warning ConstructorDoesNotFitInData
• PR #7773: Fix #7662: Mimer: special case for printing ♭
• PR #7774: Fix #7321: warn about unused CATCHALL pragmas
• PR #7775: Fix #6994: highlighting only for enabled warnings
• PR #7776: Fix #7624 by reifying Term before wrapping it in GoalAndElaboration
• PR #7778: Fix #6657: termination checker hints at missing –guardedness flag
• PR #7782: re #3209: print out-of-scope names unqualified in case splits
• PR #7783: Don’t inline constructors into inline functions
• PR #7785: Fix #7777: parse both attributes and irrelevance markers
• PR #7786: New warning UselessTactic for tactic attribute on non-hidden binder
• PR #7787: Small fixes for parsing and printing attributes
• PR #7789: Fix issues #7759 and #7788: wrong counting of with-patterns in nested with
• PR #7791: [ new ] unicode symbols for various ‘tacks’
• PR #7793: re #7792: keep inlining after inlining a copy
• PR #7800: Fix #7796: don’t hint towards –guardedness when –no-guardedness
• PR #7802: Remove broken AbsurdLam heuristics from Mimer
• PR #7804: re #7799: add instance hack to checkSectionApplication
• PR #7812: Fix #7803 fix #7811: new error PathAbstractionFailed instead of crash
• PR #7814: Fix #7660: new DisambiguateConstructor postponed tc problem
• PR #7816: re #7815: propagate range into wrapper modules
• PR #7817: Add documentation for telescopes and some related things
• PR #7818: Make data directory overridable, default to XDG_DATA_HOME
• PR #7819: [ fix #7392 ] Ensure wildcards and variable instances are kept
• PR #7822: Fix issue #7537
• PR #7824: Fix #7823: Compare number of arguments when matching on DISPLAY pragma
• PR #7826: Fix #7825 by using droppedPars instead of hand-knitted code
• PR #7830: Disregard qualified names when assigning clauses to functions in the nicifier
• PR #7831: Fix #7829 by reactivating my own fix of #1618
• PR #7834: fix #7795: Use occurrences from type for defs
• PR #7840: Document which pragmas are unsafe
• PR #7848: fix #7846: instance hack in abstract axioms
• PR #7849: Fix for #7639
• PR #7850: Re #7225: new error DatatypeIndexPolarity instead of GenericError
• PR #7852: Turn TooManyPolarities error into warning (fixes #7851)
• PR #7854: Modality warnings for constructors and fields
• PR #7855: Re #7225 name error CubicalNotErasure
• PR #7857: Forget opacity when checking signatures
• PR #7858: Fix for #7659
• PR #7859: Fix #7853: don’t drop parameters of constructor in the same module
• PR #7860: [ re #7587 ] Properly reintroduce absurd lambdas to Mimer
• PR #7865: Fix #7863: properly parse names before case-splitting
• PR #7867: Fix #7832 by placing properlyMatching in monad to have isEtaRecordConstructor
• PR #7879: Fix #7878: reorder checks in mkNotation
• PR #7880: Defer MissingDefinitions error in --safe until after typechecking
• PR #7885: disable discrim-based instance deferral by default
• PR #7886: [doc] explain how to do postprocessing for literate forester
• PR #7891: Remove duplicate inverse scope computation.
• PR #7895: Fix #7590
• PR #7896: Fix #7324: highlighting of macro names in their definition
• PR #7900: intro: filter (higher) constructors based on dimension
• PR #7901: Properly update interaction points when solving with Mimer
• PR #7904: Fix lexical-scope issue in emacs mode
• PR #7907: Fix issue #7903: etaExpandClause before constructor inlining
• PR #7913: Range information for unsolved instance constraints
• PR #7920: Fix #7916: make optimise-heavily the default
• PR #7924: Add a few notes on irrelevance
• PR #7925: Add documentation for lambda expressions and absurd lambdas
• PR #7931: Hint towards –guardedness even when –sized-types is on
• PR #7932: Add use-xdg-data-home
• PR #7934: Hygienic import of rewrite rules
• PR #7936: Highlight only record keyword when fields are missing
• PR #7939: Fix #7938: API: export Agda Highlighting Backend modules
• PR #7942: [ doc ] remove reference to Cubical.Core.Everything
• PR #7945: Fix #7944: do not apply @0 from where-module to clause rhs
• PR #7946: Fix #7943: propagate erasure status to where blocks.
• PR #7956: Fix #7955: replace impossible with syntax error
• PR #7957: Doc: replace PrimRoot by PrimeFactor in introductory text
• PR #7958: Fix #7953: remember whether top-level module name was inferred
• PR #7965: Re #7932: restore data-files in Agda.cabal and default data-dir
• PR #7967: Fix #7966: fork GetOpt to disallow long option abbreviations
• PR #7971: flake: use –build-library to build the builtins
• PR #7978: Fix #7973: print warning if rewrite does not fire
• PR #7981: Parse warning instead of error on unknown attributes and polarities