Is Agda Holes still being maintained?

Open scmu opened this issue 5 years ago • 1 comments

Sorry that I sent this as an issue, since I don't know of other ways to contact you. Thank you for creating Agda.Holes! I am wondering whether it is still being maintained ?

I tried to use it with a newer version of Agda (2.6.1). I needed some small changes to get it to work, namely,

quantify over Set levels in two places in Holes.Prelude;
adding a pragma {-# NOINLINE ⌞_⌟ #-} in Holes.Term.

Afterwards the examples seem to work, but my own equational proof still didn't go through, for reasons I don't understand.

Anyway, are you still maintaining this library?

Aug 31 '20 14:08 scmu

Hi! I think sending this as an issue is perfectly fine. I have not been actively maintaining this library for a while, but I am happy to help you make it work for you. Please could you submit the changes you made to make it compile as a PR? Also if you show me your own proof I can help you figure out why it doesn't work.

Aug 31 '20 20:08 bch29