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.
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.
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.
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 ${Agda_datadir}/${VERSION}
on the first invocation of agda or an invocation ofagda --setup, agda --emacs-mode setup, or agda --emacs-mode compile.
Herein, ${VERSION} is the Agda version and ${Agda_datadir}
the Agda data directory, on Unix-like systems
defaulting to ${HOME}/.local/share/agda.
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 is breaking for packagers of Agda
as the packaging routines might need to be updated
(but should become simpler).
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.
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 anyIrrelevant 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).
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 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 toAbsurdPatternRequiresAbsentRHS.
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.
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 FAdditions 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.
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 ofINLINE 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.
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).
.agda-lib files in the rootAgda'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)
backendInteractTop/backendInteractHole fields for providing backend-specific interaction commands (run with keyboard shortcut C-c C-i).For 2.8.0, the following issues were
closed
(see bug tracker):
Issues for closed for milestone 2.8.0
DISPLAY should be more pragmatic--guardedness warning into an error-hint@tactic arguments visible leads to unsolved constraintsSetup will be phased out in favor of Hookscabal install Agda fails with executable-dynamic{-# CATCHALL #-} pragma--safe misses the pragmasProp <= Set loses canonicityquoteTerm accepts hidden argumentsDISPLAY pragmas should treat any defined name as matchabledeclareDataAgda/TypeChecking/Monad/Context.hs using Mimerwith .. in ..__IMPOSSIBLE__ when Σ and case_of_ are both present♭ produces incorrect projectionnix build skips "generation of Agda core library interface files"toIFile logic from #6988 leads to scattering of .agdai fileslexical-binding directive"withrecord whereopaque and extended lambdas__PRs for closed for milestone 2.8.0
WithClauseProjectionFixityMismatch instead of GenericErrorRecursiveDisplayForm instead of hard errorgive_ and remove PatternErr handler*.lagda.treeCmd_no_metas by Cmd_load_no_metasException, generic errorsInvalidModalTelescopeUse and add reproducer.mdoprimShowNatLevelUniv in Cubical AgdaGenericError is actually __IMPOSSIBLE__BigInt:typeOfunderAbstraction_ for going under lambda in reduceAndEtaContractCOMPILED--local-interfaces and warning DuplicateInterfaceFileswantInterfaces check--build-libraryaddContext when splitting on literals--help, --version etc. if the user requests soagda-mode as agda --emacs-mode__IMPOSSIBLE__private useless in where blocksOpenPublic{Abstract,Private}ConstructorDoesNotFitInDataUselessTactic for tactic attribute on non-hidden binderdroppedPars instead of hand-knitted codemkNotationMissingDefinitions error in --safe until after typecheckingRetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4