Stream: Coq devs & plugin devs

Topic: CClosure.whd_stack as a tactic?


view this post on Zulip Janno (Oct 30 2020 at 12:29):

Does Coq expose CClosure.whd_stack as a reduction/tactic? I only realized just now that hnf is not the right thing because it does too much.

view this post on Zulip Gaëtan Gilbert (Oct 30 2020 at 12:31):

only full reduction afaik

view this post on Zulip Janno (Oct 30 2020 at 12:32):

That's too bad. It's very useful :)

view this post on Zulip Gaëtan Gilbert (Oct 30 2020 at 12:40):

make a PR to expose it

view this post on Zulip Pierre-Marie Pédrot (Oct 30 2020 at 12:43):

in master it does

view this post on Zulip Pierre-Marie Pédrot (Oct 30 2020 at 12:44):

ah, sorry, misunderstood what you meant, I thought you talked about the ML tactic api

view this post on Zulip Janno (Oct 30 2020 at 12:48):

What I really want is to have it in ltac2. Pretyping and hnf are the main source of slowdown in my experiments right now :)

view this post on Zulip Janno (Oct 30 2020 at 12:48):

I suppose this is a good opportunity to try to write a plugin that exposes this function

view this post on Zulip Pierre-Marie Pédrot (Oct 30 2020 at 12:49):

FTR hnf is the dreaded whd-something-something-but-fix function we discussed about

view this post on Zulip Pierre-Marie Pédrot (Oct 30 2020 at 12:49):

at least the ML API is truthful, which is not the case of the user-facing reduction function name

view this post on Zulip Janno (Oct 30 2020 at 12:52):

Yes, I noticed that in the perf profile.. the name really is quite misleading

view this post on Zulip Janno (Oct 30 2020 at 12:53):

The user-facing name, that is

view this post on Zulip Pierre-Marie Pédrot (Oct 30 2020 at 12:53):

IIRC it goes back to the prehistory of Coq


Last updated: Oct 16 2021 at 02:03 UTC