[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