Karl Palmskog (Jun 18 2020 at 20:29): 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.
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:
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.
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?
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.
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.
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: Oct 13 2024 at 01:02 UTC