[Agda] [ANNOUNCE] Agda 2.6.1 release candidate 1

[Jesper Cockx]

>From the changelog:

The "with inlining" feature of the termination checker has been removed. As
> a consequence, some functions defined using with are no longer accepted as
> terminating. See Issue #59 for why this feature was originally introduced
> and #3604 for why it had to be removed.
>

It is likely that your function no longer passes the termination checker
because this feature was removed. There were several issues with the
implementation of this feature and no-one was willing to maintain it, so
unfortunately it had to be removed.

-- Jesper

On Tue, Dec 31, 2019 at 12:32 PM <mechvel at scico.botik.ru> wrote:

> The below function _+ms_ satisfies the following property.
>
> For each pattern in the third clause for +ms there exists a nonempty
> subset js
> in the argument position set {1, 2} such that
> (for all i <- js,  argument(i)  is structurally greater than
> argument(i)-on-RHS,
>   while the arguments at all other positions do not change
> syntactically).
>
> And by this rule, +ms is terminating.
> And a generalization of this rule is implemented in Agda.
>
> Am I missing something?
>
> If it is all right, then Agda-2.6.1 needs to follow Agda-2.6.0.1 at this
> point.
>
> ?
>
> --
> SM
>
>
> On 2019-12-30 21:36, mechvel at scico.botik.ru wrote:
> > On 2019-12-22 14:41, Andres Sicard Ramirez wrote:
> >> Dear all,
> >>
> >> The Agda Team is very pleased to announce the first release candidate
> >> of Agda 2.6.1. We plan to release 2.6.1 in three weeks.
> >> [..]
> >
> > This Agda-2.6.0.1.20191219 reports "Termination checking failed ..."
> > for
> >
> > --------------------------------
> > _+ms_ :  Op₂ (List Mon)
> > []                  +ms mons'                  =  mons'
> > mons                +ms []                     =  mons
> > ((monᶜ a e) ∷ mons) +ms ((monᶜ b e') ∷ mons')  with comparePP e e'
> > ...
> >     | tri> _ _ _ =  (monᶜ a e)  ∷ (mons +ms ((monᶜ b e') ∷ mons'))
> > ... | tri< _ _ _ =  (monᶜ b e') ∷ (((monᶜ a e) ∷ mons) +ms mons')
> > ... | tri≈ _ _ _ =  (monᶜ (a + b)  e) ∷ (mons +ms mons')
> > --------------------------------
> >
> > while Agda-2.6.0.1 type-checks this.
> > Which one is more correct?
> >
> > Among the arguments for +ms on RHS the first one is smaller by
> > construction than in LHS
> > (for tri>), or the second is smaller by construction than in LHS (for
> > tri<),
> > or each is smaller by construction than in LHS (for tri≈).
> >
> > --
> > SM
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20191231/d18dbebf/attachment.html>