[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