Proof Assistants Stack Exchange is a question and answer site for mathematicians and computer scientists who develop and use proof assistants. It only takes a minute to sign up.
Sign up to join this community
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?
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.
