[Agda] [REQUEST] Help with transition from 2.5.1/2 (std-lib 0.12) to 2.5.3 (std-lib 0.14)

[Andrea Vezzosi]

1) You would have to edit the sources themselves
2) Are you disabling termination checking in any way? {-# TERMINATING
#-} is how you promise that the definition is terminating so that Agda
will reduce it at compile time.



On Thu, Oct 26, 2017 at 6:42 PM, James McKinna <James.McKinna at ed.ac.uk> wrote:
> Dear List,
>
> in response to a reviewer's request for the upcoming CPP, we are attempting
> to migrate proofs which previously typechecked under 2.5.1/2, with stdlib
> 0.12 to 2.5.3 with stdlib 0.14.
>
> This has revealed some (very!) unpleasant backwards incompatibilities, so
> this is a request for assistance/insight into how to deal with them.
>
> Hoping to hear from experts on some or all of the following points!
>
> Cheers,
>
> James McKinna
> =====================================================================
> 0) dependency on ghc
>
> Previously, and for institutional reasons, we've been building/running Agda
> under ghc-7.10.2/3
>
> What is the most recent agda version which builds under ghc-7.x.y?
>
> 1) stdlib 0.14 dependency on agda
>
> Many things in stdlib 0.14 appear to depend on having agda version 2.5.3 or
> above. In particular, the language pragmas FOREIGN and COMPILE in Data.Empty
> seem to make 2.5.1/2 fall over. Is there a sensible way to disable such
> pragmas without editing the stdlib, for developments which make *no use* of
> compilation to haskell?
>
> 2) reduction behaviour of functions/compile-time conversion checking
>
> Lots of things we rely on in our proofs seem now no longer to typecheck.
>
> Agda seems no longer to be unfolding definitions, or at least not in the
> ways we expect, during proof construction or re-checking, as previously in
> 2.5.1/2. There's no easy way to phrase this question, but how are we
> supposed to understand the change, and rework our codebase so that old
> proofs still check? For the time being, no minimal failing example is easy
> to provide. Is it possible to explain at least what has changed, and better
> still, to restore the old reduction/unification behaviour? The CHANGELOG
> gives no clues (at least that I could understand)
>
>
>
> --
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda