[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,

Many thanks to Andrea Vezzosi and Andrés Sicard-Ramírez, for their 
speedy replies addressing points 0) and 1). That just leaves 2), which 
is still giving us problems, effectively limiting our development to 
v2.5.2.

Apologies in adavance for not being able to follow the list's customary 
request for a minimal failing example, but it's far from obvious (to us, 
at least) how to construct one. It remains the case that the unfolding 
behaviour of definitions in one module, both in interactive proof 
construction, and in subsequent typechecking/reloading, appears to have 
changed, such that agda2.5.3 rejects terms which previously typechecked, 
having failed to validate equations/coercions between types.

AFAICT, this is due to unfolding behaviour which is less strict in 2.5.3 
than previously in 2.5.1/2 (Andrea's suggestion concerning the {- 
TERMINATING -} pragma wrt point 2) does not seem relevant here; all our 
definitions are terminating). Is it possible to describe how Agda's 
reduction behaviour has changed, and how it might be to force evaluation 
in the relevant places to allow checking to proceed?

Thanks in advance,

James


Previously, I 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.