Stream: Elpi users & devs

Topic: Hint Resolve


view this post on Zulip Jasper Haag (Feb 01 2022 at 21:10):

Is support for generating [Hint Resolve]s something that you anticipate being relatively easy (like for Hint Opaque)? If so I can open an issue :~)

We would like to generate these registrations to ease the burden on new users involved in properly automating constructs/abstractions which they introduce.

view this post on Zulip Enrico Tassi (Feb 01 2022 at 21:11):

Yes, that should be simple as well. Open an issue please, plz.

view this post on Zulip Jasper Haag (Feb 01 2022 at 21:16):

https://github.com/LPCIC/coq-elpi/issues/337

Thanks for working on all of the issues that Gordon and I have been creating :~) We're having very good results with Elpi so far, and your support has been a big part of that!

view this post on Zulip Enrico Tassi (Feb 01 2022 at 21:33):

OK, now that I'm "done" with https://github.com/LPCIC/coq-elpi/pull/324 I'll try to make a new release with all this little stuff.
@Gordon Stewart do you want me to also finish functors? Or you plan to work on it?

view this post on Zulip Gordon Stewart (Feb 01 2022 at 21:46):

Sorry; I haven't had a chance to finish https://github.com/LPCIC/coq-elpi/pull/332 yet.

What do you think about merging that (just functors, no application, but with the warning fix you mentioned)? Then functor application could perhaps go in a separate MR.

view this post on Zulip Enrico Tassi (Feb 01 2022 at 21:48):

Fine. I just wanted to avoid double work. If you are not working on it, I might. If you do, just tell me.

view this post on Zulip Gordon Stewart (Feb 01 2022 at 21:51):

OK. No, I'm not actively working on it (it turns out I don't need to generate functor applications, then I got sidetracked by other things). For now, I'll fix the warning in https://github.com/LPCIC/coq-elpi/pull/332, then hand the MR over to you.


Last updated: Feb 05 2023 at 13:02 UTC