search

MetaCoq / metacoq

Metaprogramming, verified meta-theory and implementation of Coq in Coq
https://metacoq.github.io
MIT License
379 stars 81 forks source link

Reasoning about TemplateMonad commands? #753

Open jsarracino opened 2 years ago

jsarracino commented 2 years ago

Hello,

This is more of a question than a real issue, but I wasn't sure how best to reach folks, so I'm putting it here. I've been using MetaCoq and TemplateMonad for developing a plugin (it's really usable and slick, great job!) and it would be great to reason about the result of running TemplateMonad programs (even axiomatically).

Is there currently a way to do this, or plans (even tentative) to implement something like it? For example, it would be nice to reason about the effect of tmMkDefinition on the global environment, or the behavior of tmLocate, etc.

Thanks, John

TheoWinterhalter commented 2 years ago

The best way to reach us is probably on the Metacoq zulip stream of the Coq zulip: https://coq.zulipchat.com/

For now we have no specifications for these operations. I guess it could be interesting but I'm not sure anyone is working on it.