NES in HB

[CohenCyril]

No description provided.

[gares]

Please open an issue saying to remove this when we decide to require a more recent coq-elpi

[CohenCyril]

It's not about upgrading to a more recent coq-elpi (yet), it's about adding the NES.Snapshot (I did not manage to re-import NES.db nor did I manage to import nes.elpi to hotfix it)...

[CohenCyril]

I need to make a PR in coq-elpi to add this feature though, and you will be right ;)

[CohenCyril]

Done cf LPCIC/coq-elpi#212

[gares]

Another problem I have with this is that "logging" is something I'm implementing in HB. And we definitely want calls to NES to be replaced by vernacular commands in plan-B, so I think we should Accumulate this file together with hb.elpi and hook into the logging infrastructure (in the other PR)

[CohenCyril]

Another problem I have with this is that "logging" is something I'm implementing in HB. And we definitely want calls to NES to be replaced by vernacular commands in plan-B, so I think we should Accumulate this file together with hb.elpi and hook into the logging infrastructure (in the other PR)

I do not understand completely, shouldn't NES have its own logging infrastructure and incorporated in LPCIC/coq-elpi#212?

[gares]

It could, but I did deliberately not put the logging code in coq-elpi because it is too experimental. You are right that its place is there, but it is not ready. The plan was to let it mature inside HB and only then move it back to coq-elpi.