[Agda] [ANNOUNCE] Agda 2.6.1 release candidate 1

[Guillaume Allais]

I'll add to that: if you perform all the recursive calls at the
same time as `with comparePP e e'` then you should be able to get
a terminating version of the function.

I am saying "should" because the example is not self-contained and
as such it is impossible to test.

On 31/12/2019 12:23, Jesper Cockx wrote:
> 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
>>
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>