Nightly Build (0ff0741@master)

What's Changed

• [ fix #6976 ] Add constraint for resolving the head of an instance by @jespercockx in #6978
• [ fix #6867 ] Only consider arguments with @0 for forcing if --erasure is on by @jespercockx in #6870
• Delete unused glue1 bindings by @ncfavier in #7021
• User manual: add note about compilation of irrelevant fields by @UlfNorell in #7026
• CI user-manual: bump python to 3.11 and setup-python to v5 by @andreasabel in #7027
• Fix issue 7029 by @jespercockx in #7031
• Break cross-module SCC 4 by @lawcho in #6897
• Recompute blocker in equalSort by @andreasabel in #7039
• update user-manual to stdlib-v2.0 by @jamesmckinna in #7043
• Refactor flake.nix by @lawcho in #7032
• [ fix #7044 ] Serialize defBlocked as neverUnblock by @andreasabel in #7046
• [ fix #7048 ] Only define hcomp constructors when --cubical-compatible. by @andreasabel in #7049
• issue 7050 by @andreasabel in #7051
• [ workflows ] Bump up/download-artifact action to v4 by @andreasabel in #7054
• add --keep-pattern-variables to options that don't require recompilation by @UlfNorell in #7060
• Unspine system projections when they have display forms by @plt-amy in #7055
• [ workflows ] bump GHC 9.6.3 to 9.6.4 by @andreasabel in #7064
• Some documentation fixes by @fredrik-bakke in #7065
• Add 'Inference in Agda' to the list of tutorials by @effectfully in #7072
• [ workflow ] Allow a newer PATCH version for cancel-workflow-action by @L-TChen in #7074
• Provide a .agda-lib for Agda builtins by @ibbem in #6988
• Make tests for #641 less brittle by @UlfNorell in #7075
• Fix #7070: remove built-in max heap setting -M3.5G for Agda by @andreasabel in #7076
• More precise type for Utils.Graph...sccs: every SCC is non-empty by @andreasabel in #7079
• Eta-expand mismatched cubical primitives by @plt-amy in #7071
• Left-hand side let by @UlfNorell in #7078
• Mimer: a drop-in replacement for Agsy by @UlfNorell in #6410
• Fix #7084: Mimer internal error by @UlfNorell in #7087
• #7085: Mimer not recognising qualified hints by @UlfNorell in #7088
• Fix #7086: Mimer crashing if called in type signature by @UlfNorell in #7089
• Add course to “Courses using Agda” by @fmehta in #7091
• Re #7081: add build with debug-{serialisation,parsing} flags to cabal CI by @andreasabel in #7092
• Fix #7095: our cabal build flags are actually all "manual". by @andreasabel in #7096
• Allow zlib-0.7 by @andreasabel in #7098
• Make more flags infective by @jespercockx in #5267
• Float DefP clauses above catch-alls by @plt-amy in #7097
• some preps for 2.6.4.2 by @andreasabel in #7099
• #6972: Also save backcopies in interface file by @plt-amy in #6974
• Bump stack-*.yaml to latest 9.6.4 and 9.8.1 snapshots by @andreasabel in #7102
• Mimer: drop constructor parameters from solutions by @UlfNorell in #7111
• #7105 Do not try to fold let-bindings during printing of the helper function by @knisht in #7106
• Use a separate warning for duplicated interface files by @ibbem in #7112
• Split GenericWarning into individual warnings by @andreasabel in #7119
• Delete Travis CI files by @lawcho in #7129
• Fix for issue #7113 by @jespercockx in #7122
• [ re #5267 ] Add new infective options to user manual by @jespercockx in #7103
• Allow Win32-2.14 by @andreasabel in #7131
• Mimer: fix handling of module parameters by @UlfNorell in #7135
• Janitorial Changes to agda-mode by @phikal in #6536
• Flake improvements by @ncfavier in #7115
• Fix #7136: proper error when pattern definition has unsupported arguments by @andreasabel in #7138
• Cosmetics: remove some unused functions (Parser) by @andreasabel in #7141
• Fix #6783: error for @TactiC on lambda by @andreasabel in #7142
• Fix #7146: printing of cohesion and lock attributes by @andreasabel in #7147
• Fix mutual information not being set properly by the positivity checker by @UlfNorell in #7149
• Fix #7148: restore call to instantiateFull before with-abstraction. by @andreasabel in #7151
• Bump stack*.yaml and submodules (prep 2.6.4.3) by @andreasabel in #7153
• Follow hlint suggestion: move brackets to avoid $. by @philderbeast in #6461
• Update installation.rst by @muchnick0 in #7121
• Fix #7158: Application: check for sufficient arity before checking target by @andreasabel in #7159
• Fix #6667: case not __IMPOSSIBLE__ for nullary syntax by @andreasabel in #7160
• Fix #6945: warn about useless private even in absense of nice decls by @andreasabel in #7161
• Blocks in Concrete syntax: store Range of block keyword by @andreasabel in #7162
• Citation instructions by @L-TChen in #6444
• Fix #7167: type checking underapplied pattern synonyms by @andreasabel in #7168
• Trigger and improve error UnusedVariableInPatternSynonym by @andreasabel in #7169
• Add reference to Cornelis in the documentation by @4e554c4c in #7144
• Part of #2829: Allow instance arguments in pattern synonyms that are such in the pattern already by @andreasabel in #7173
• Discrimination trees for instance search by @plt-amy in #7109
• Bump GHC 9.8.1 to 9.8.2 by @andreasabel in #7175
• Fix #7177: only setScope when scope is not null by @andreasabel in #7179
• Use compareAs for assignE even in compareAtom by @plt-amy in #7180
• Fix #7176: turn absurd pattern in instance position to instance meta by @andreasabel in #7185
• Commenting test for #7180 by @andreasabel in #7184
• Fix Mimer trying bad recursive calls by @UlfNorell in #7195
• HLint list element suggestions by @philderbeast in #7194
• Fix incorrectly quoted sorts by @UlfNorell in #7203
• Re. #7196: Only prune instances in serialised iface by @plt-amy in #7197
• Fix #7202: ModuleDoesntExport: only highlight missing names by @andreasabel in #7204
• Instance overlap pragmas by @plt-amy in #7183
• Various symbol additions to agda-input by @fredrik-bakke in #6769
• Fix #7208: restore missing check for OverlappingProjects by @andreasabel in #7209
• Fix range for deprecated module import warning when applied by @andreasabel in #7210
• Restore agda-input for ordinary backslash (regression in #6769) by @andreasabel in #7213
• Strengthen link between .el files in src/data/emacs and src/agda-mode by @andreasabel in #7216
• Fix #7219: only warn about problems with warning options by @andreasabel in #7222
• GenericError by @andreasabel in #7223
• Bump peaceiris/actions-gh-pages from 3 to 4 by @dependabot in #7224
• Fix #7181: Allow matching to continue when stuck on lazy pattern by @szumixie in #7211
• Follow hlint suggestion: use list comprehension by @philderbeast in #7200
• Follow hlint suggestion: use infix by @philderbeast in #7201
• Coerce unquote applications by @ncfavier in #6570
• Do final checks before freezing metas by @ncfavier in #6569
• Add INJECTIVE_FOR_INFERENCE pragma by @WhatisRT in #6640
• Prevent unintended invoking of stack by @chu-mirror in #7228
• Support GHC 9.6.5 by @andreasabel in #7229
• [ refactor, #7225 ] GenericError to new error EmptyTypeOfSizes by @andreasabel in #7230
• CI cosmetics: keep --dependencies-only step even when cache hit by @andreasabel in #7233
• Remove some GenericErrors by @andreasabel in #7235
• Fix #7236: use context rather than telescope for lambda-bound variables in rewrite patterns by @andreasabel in #7237
• Follow hlint suggestion: use empty by @philderbeast in #7239
• Drop time-compat dependency and Stack LTS for GHC 8.6 by @andreasabel in #7241
• re. 7218: Saturate opaque blocks after Give commands by @plt-amy in #7243
• Build with GHC 9.10 by @andreasabel in #7238
• Refactor: use SmallSet for funFlags, make more boolean fields a FunctionFlag by @andreasabel in #7244
• Follow hlint suggestion: redundant section by @philderbeast in #7246

New Contributors

• @jamesmckinna made their first contribution in #7043
• @fredrik-bakke made their first contribution in #7065
• @effectfully made their first contribution in #7072
• @ibbem made their first contribution in #6988
• @fmehta made their first contribution in #7091
• @phikal made their first contribution in #6536
• @muchnick0 made their first contribution in #7121
• @chu-mirror made their first contribution in #7228

Full Changelog: v2.6.4.3...nightly