Since Agda is software and sometimes software has breaking changes, e.g. Python 2 vs Python 3 (ref), does Agda have any significant breaking changes that one would need to be concerned about?

Also see related question:

When installing Agda does one have to be attentive to a version?


1 Answer 1


It has tons of breaking changes. For example, if they've found an inconsistency, they'll try to restrict some features, so code surely breaks.

For instance, they used to have a special treatment for with-abstraction when checking termination, but the feature is abused and nobody's maintaining this part of the code, so it gets removed completely.

As another example, guardedness flag used to be enabled by default, but people found that it's incompatible with sized types, so it gets turned off by default. If you want to use it, you'll need to add the flag manually.

AFAIK they try their best to keep compatibility, but things go wrong.

  • $\begingroup$ Yesh sure why not. Fyi you may specify agda version for installed libraries agda.readthedocs.io/en/latest/tools/… so I guess it's less likely to be a problem $\endgroup$
    – ice1000
    Commented Feb 9, 2022 at 2:26

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.