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

[Andrés Sicard-Ramírez]

Post by 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?

Agda 2.5.3 was tested with GHC 7.8.4, 7.10.3, 8.0.2 and 8.2.1. I guess
Agda 2.5.3 also works with GHC 7.10.2.

--
Andrés
La información contenida en este correo electrónico está dirigida únicamente a su destinatario y puede contener información confidencial, material privilegiado o información protegida por derecho de autor. Está prohibida cualquier copia, utilización, indebida retención, modificación, difusión, distribución o reproducción total o parcial. Si usted recibe este mensaje por error, por favor contacte al remitente y elimínelo. La información aquí contenida es responsabilidad exclusiva de su remitente por lo tanto la Universidad EAFIT no se hace responsable de lo que el mensaje contenga. The information contained in this email is addressed to its recipient only and may contain confidential information, privileged material or information protected by copyright. Its prohibited any copy, use, improper retention, modification, dissemination, distribution or total or partial reproduction. If you receive this message by error, please contact the sender and delete it. The information contained herein is the sole responsibility of the sender therefore Universidad EAFIT is not responsible for what the message contains.

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

Post by 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.
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[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

Post by 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)

[Andreas Abel]

Dear James,

Post by James McKinna
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

Post by 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

Post by 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)