Maxime Dénès (Jan 20 2023 at 20:19): Maxime Dénès (Jan 20 2023 at 20:19):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?
Maxime Dénès (Jan 20 2023 at 20:19):I don't mean an implementation schedule of course, but at least the current team view on what should be done.
Karl Palmskog (Jan 20 2023 at 20:24):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:?
Michael Soegtrop (Jan 21 2023 at 09:20):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.
Paolo Giarrusso (Jan 21 2023 at 14:51):I think we've been over this, and automation are needs that are out of scope for your prototype (reducing user-defined functions).
Michael Soegtrop (Jan 22 2023 at 09:57):@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.
Michael Soegtrop (Jan 22 2023 at 09:58):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.
Paolo Giarrusso (Jan 22 2023 at 09:59):Ack :grinning:
Michael Soegtrop (Jan 22 2023 at 10:03):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.
Karl Palmskog (Jan 22 2023 at 10:31):that sounds a lot like HOL4 simpsets...
Last updated: Dec 05 2023 at 04:01 UTC