The two most common questions I got here at POPL so far were: what is the plan w.r.t. universes (dropping template poly or not,...) and what is the plan w.r.t. simpl
vs cbn
. Do we have material somewhere that we can point people to?
I don't mean an implementation schedule of course, but at least the current team view on what should be done.
not able to answer the question, but related to this topic: I'd be interested in hearing general gist of what POPL people think about the Coq ecosystem these days (Coq Platform, many packages joining the Platform and getting releases, etc.). Is it :thumbs_up:, :thumbs_down: or :meh:?
IMHO one should recommend to use simpl
and cbn
only in manual proofs and use something entirely different in automation (I have a prototype in Elpi). For manual proofs it shouldn't matter much if one uses simpl
or cbn
.
I think we've been over this, and automation are needs that are out of scope for your prototype (reducing user-defined functions).
@Paolo Giarrusso : sure there are different kinds of automation with different needs. May main point was that if this is a major question on POPL this discussion should be deepened and IMHO at least part of the solution would be good support for a simplifier along the lines of my prototype.
It can btw. also help in manual applications - say as an extension of simpl - to say that certain classes of symbols should be or shouldn't be expanded.
Ack :grinning:
What I want is mainly a flexible and efficient way to define "largish sets of symbols" which can then be used as delta argument to reduction function or as specification of what symbols one wants to see/ not to see in the result of a simplification. I think a major problem with simpl is that it is hard to specify what one means by "simple". If one could easily define sets of symbols, one could easily define "domains" one wants to present to or hide from the user. As an example you could say that you want to see results in Z and never ever see any details of the positive based implementation of Z. In complex developments the number of levels one might want to hide or show is much larger.
that sounds a lot like HOL4 simpsets...
Last updated: Dec 05 2023 at 04:01 UTC