Compilation warning

[WojciechKarpiel]

Hello!
(disclamer: I'm new to both HoTT and Agda)

I use current (git) version of Agda (Agda version 2.6.0-dc58db0) and HoTT (commit 831dcfc), both pulled 1st July

When I try to compile the library itself it gives warning:

/home/wojciech/Kod/HoTT-Agda/core/lib/Base.agda:70,1-25
Builtin REFL does no longer exist. It is now bound by BUILTIN
EQUALITY
when checking the pragma BUILTIN REFL idp

It's following piece of code:

infix 30 _==_
data _==_ {i} {A : Type i} (a : A) : A → Type i where
  idp : a == a

Path = _==_

{-# BUILTIN EQUALITY _==_ #-}
{-# BUILTIN REFL idp #-}

Simply commenting out the BUILTIN REFL line fixes the problem.

Last changes to these lines are from 2013. Has anyone had similar issue and knows how to fix it?

[favonia]

@WojciechKarpiel Hello! Thanks for reporting the issue. I was aware of this issue, but it is required by the current stable version (2.5.2) of Agda and its next (stable) version has not been released yet. :-( Due to this I am a little bit reluctant to remove it even though I am also using the unstable (git) version. You can track issue #27 for future updates on this library, or downgrade your Agda back to 2.5.2 for the moment. Does that sound reasonable to you?

[favonia]

By the way, technically speaking this is a warning not an error, and your development should still work.

[WojciechKarpiel]

Does that sound reasonable to you?

Sure, thanks for clarification!

Also: I changed 'Error' to 'Warning' in issue title

[favonia]

@WojciechKarpiel Thanks. However, let me close this because it is already on the to-do list #27.