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

[Andreas Abel]

Dear James,

 > 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.

You also send a link to e.g. a github commit to one of us developers so 
that we can investigate the failure further...

--Andreas

On 01.11.2017 20:09, James McKinna wrote:
> 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)
>>
>>
>>
> 


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/