[Agda] [ANNOUNCE] Agda 2.6.1 release candidate 2

mechvel at scico.botik.ru mechvel at scico.botik.ru
Fri Mar 13 11:56:34 CET 2020


On 2020-03-09 04:55, Andrés Sicard-Ramírez wrote:
> Dear all,
> 
> The Agda Team is very pleased to announce the second release candidate
> (RC2) of Agda 2.6.1.
> 
> [..]


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
   
/home/mechvel/.cabal/share/x86_64-linux-ghc-8.8.3/Agda-2.6.0.1.20200307/lib/prim/Codata/Musical/Costring.agda
   
/home/mechvel/.cabal/share/x86_64-linux-ghc-8.8.3/Agda-2.6.0.1.20200307/lib/prim/Codata/Musical/Costring.lagda
when scope checking the declaration
   open import Codata.Musical.Costring using (toCostring)
-----------------------------------------------------------

~/.cabal/share  has
          doc  man  x86_64-linux-ghc-8.8.3

Please, advise,

------
Sergei


More information about the Agda mailing list