[Agda] [ANNOUNCE] Agda 2.6.1 release candidate 2

[mechvel at scico.botik.ru]

On 2020-03-14 03:00, Andrés Sicard-Ramírez wrote:
> On Fri, 13 Mar 2020 at 05:56, <mechvel at scico.botik.ru> wrote:
>> 
>> I test it on  ghc-8.8.3, Ubuntu Linux 18.04.
>> After installing it and the master lib of March 13, the command
>> 
>>    > agda $agdaLibOpt TypeCheckAll.agda +RTS -M3G -RTS
>> 
>> reports
>> /home/mechvel/inAgda/bfLib/0.3/TypeCheckAll.agda:1,1-55
>> Failed to find source of module Codata.Musical.Costring in any of
>> the following locations:
>>    /home/mechvel/inAgda/bfLib/0.3/Codata/Musical/Costring.agda
>>    /home/mechvel/inAgda/bfLib/0.3/Codata/Musical/Costring.lagda
>>    /home/mechvel/inAgda/bfLib/0.3/Codata/Musical/Costring.agda
>>    /home/mechvel/inAgda/bfLib/0.3/Codata/Musical/Costring.lagda
>>    
>> /home/mechvel/agda/stLib/masterMar13/src/Codata/Musical/Costring.agda
>>    
>> /home/mechvel/agda/stLib/masterMar13/src/Codata/Musical/Costring.lagda
>>    /home/mechvel/inAgda/bfLib/0.3/Codata/Musical/Costring.agda
>>    /home/mechvel/inAgda/bfLib/0.3/Codata/Musical/Costring.lagda
> 
> I couldn't reproduce the problem. I guess the error is not related to
> the release candidate but to the "installation" of the master branch
> of the standard library.
> 
> Which is the output of
> 
> $ ls 
> /home/mechvel/agda/stLib/masterMar13/src/Codata/Musical/Costring.agda
> 
> ?


I am sorry.
I have put it into ..masterMarch13..,
but have set       ..masterMar13..
on the path.


Now, it stops at this point:

   <ℕ-acc {x} =
      Inverse-image.accessible {_} {_} {_} {ℕᵇ} {ℕ} {_<ₙ_} toℕ
                                           (Nat0.<-acc {toℕ x})

Set !=< Level.Level
when checking that the expression ℕᵇ has type Level.Level.
I am trying to find out the source of this.
Probably stdlib has changed the signature for  Inverse-image.accessible 
...

------
Sergei