[Agda] [ANNOUNCE] Agda 2.6.0 release candidate 1
Sergei Meshveliani
mechvel at botik.ru
Fri Mar 15 19:09:29 CET 2019
On Fri, 2019-03-15 at 12:41 +0000, Andres Sicard Ramirez wrote:
> Dear all,
>
> The Agda Team is very pleased to announce the first release candidate
> of Agda 2.6.0.
> [..]
I try it on ghc-8.6.3, Ubuntu Linux 18.04.
After installing Agda 2.5.4.2.20190310 and
master lib of March 15, 2019,
I type-check my program with
> agda $agdaOpt +RTS -M7G -RTS Binary.agda
This leads to the report
---------------------------------------------------------------------
Checking Binary (/home/mechvel/inAgda/bfLib/0.01/Binary.agda).
Checking Bin.Bin0 (/home/mechvel/inAgda/bfLib/0.01/Bin/Bin0.agda).
Checking Level
(/home/mechvel/agda/stLib/master-mar15-2019/src/Level.agda).
Checking Function
(/home/mechvel/agda/stLib/master-mar15-2019/src/Function.agda).
Checking Strict
(/home/mechvel/agda/stLib/master-mar15-2019/src/Strict.agda).
Checking Relation.Nullary
(/home/mechvel/agda/stLib/master-mar15-2019/src/Relation/Nullary.agda).
Checking Data.Empty
(/home/mechvel/agda/stLib/master-mar15-2019/src/Data/Empty.agda).
/home/mechvel/agda/stLib/master-mar15-2019/src/Data/Empty.agda:16,1-66
COMPILE pragma not allowed in safe mode.
when scope checking the declaration
open import Data.Empty hiding (⊥-elim)
---------------------------------------------------------------------
Please, how to fix?
------
Sergei
More information about the Agda
mailing list