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

[James McKinna]

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.