Stream: coq-community devs & users

Topic: Removing omega from RegLang


view this post on Zulip Karl Palmskog (Jun 18 2020 at 20:29):

@Christian Doczkal what are your thoughts on this being merged: https://github.com/coq-community/reglang/compare/shepherdson-zify

This removes use of omega in favor of lia via zify. However, this can currently only be done in a way that supports either:

The branch takes the first option, but the diff needed for the second is quite simple.

view this post on Zulip Christian Doczkal (Jun 18 2020 at 20:53):

Hmm, my thought would be to wait for Coq-8.13 which should (fingers crossed) include a variant of lia that can deal natively with boolean relations. See Issue #14, which I created a mere 7h ago :laughter_tears:

view this post on Zulip Karl Palmskog (Jun 18 2020 at 20:54):

well, I had the branch lying around since February, and also 8.13 might be a 6-9 months away.

view this post on Zulip Christian Doczkal (Jun 18 2020 at 21:08):

Yes, but I also don't see a reason to rush to remove omega, in particular if it requires adding a new file (zify.v) that's a trimmed down version of a file from mathcomp if I understand correctly. What's your rationale for this?

view this post on Zulip Karl Palmskog (Jun 18 2020 at 21:09):

it doesn't live in MathComp currently, but here: https://github.com/pi8027/mczify --- it's trimmed down because I don't want it to depend on mathcomp-algebra, etc.

view this post on Zulip Karl Palmskog (Jun 18 2020 at 21:10):

in any case, this was an experiment mainly to investigate whether I could easily switch to just lia everywhere in my projects, so not a big deal for me to wait for 8.13 w.r.t. RegLang.

view this post on Zulip Karl Palmskog (Jun 18 2020 at 21:12):

also, I think sauto/scrush from CoqHammer (seemingly current top dog of Coq FOL-oriented automation) could now work quite well in MC projects via zify in this way


Last updated: Feb 05 2023 at 13:02 UTC