[Agda] [ANNOUNCE] Agda 2.6.1 release candidate 1

[mechvel at scico.botik.ru]

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

There are two large files in my program where this candidate Agda acts a 
bit strangely.
When it finds in such a file a termination checking problem, it hangs 
for long
(I do not know, may be loops infinitely).
Then I interrupt it and comment out somewhat the trailing half of the 
file.
And then, it reports fast "Termination checking failed", and I proceed 
with fixing the
source by reducing the part commented out.

In many places it forced me to add values for implicits (where Agda 
2.6.0.1 did not).
Like this:
    +ms-step> {a} {b} {e} {e'} {_} {mons'} e>e'
instead of
    +ms-step> e>e'.

These two features are not of so a great importance.

I continue testing.

--
SM