Bas Spitters (Jun 04 2020 at 10:51): Bas Spitters (Jun 04 2020 at 10:51):Any plans about https://github.com/smtcoq/smtcoq ?
Karl Palmskog (Jun 04 2020 at 11:11):@Bas Spitters as per discussion here, SMTCoq isn't yet compatible with 8.12/master, only 8.9. (Although there seems to be some recent activity on the "standard" (non-native) version and and 8.11)
Bas Spitters (Jun 04 2020 at 11:19):Thanks. That's a pity.
Michael Soegtrop (Jun 04 2020 at 11:26):Thanks. That's a pity.
Indeed - SMTCoq seems to have a nice and clean interface.
Karl Palmskog (Jun 04 2020 at 11:39):it would seem that the native version of SMTCoq (as opposed to the standard version which has an 8.11 branch) is the key to performance:
If you want to use SMTCoq with high performance to check large proof certificates, you need to use the version of Coq with native data-structures
and I think this is some way off, or perhaps Maxime will know more (it's based on his native-coq fork)
Karl Palmskog (Jun 04 2020 at 11:41):ping @Maxime Dénès just to check if there is some update on the native-coq features used by SMTCoq (e.g., if this is planned for 8.13?)
Maxime Dénès (Jun 04 2020 at 11:43):ah ah, your timing is good: https://github.com/coq/coq/pull/11604 just marked as ready for review
Karl Palmskog (Jun 04 2020 at 11:53):Maxime Dénès said:
ah ah, your timing is good: https://github.com/coq/coq/pull/11604 just marked as ready for review
Let's assume we are in an ideal world and this gets merged relatively promptly. Would it then be considered for backporting to v8.12 @Théo Zimmermann? I'm just asking since native SMTCoq could be a valuable tool to many users, and official support late 2020 (or early 2021) would be a bit unfortunate.
Pierre-Marie Pédrot (Jun 04 2020 at 11:54):This is a major kernel feature, no way this would get backported into 8.12...
Karl Palmskog (Jun 04 2020 at 11:54):OK, thanks for clarifying.
Maxime Dénès (Jun 04 2020 at 11:55):I don't think it can be backported indeed. I was planning to have it ready earlier, but as you know 2020 didn't really go according to plan so far.
Karl Palmskog (Jun 04 2020 at 11:57):@Bas Spitters I guess we have the answer then: native SMTCoq in 8.13 and next iteration of Coq Platform (hopefully). I guess the "standard" SMTCoq could still happen along the way.
Théo Zimmermann (Sep 14 2022 at 16:28):I'm a bit worried by the way SMTCoq is maintained with respect to its dependencies. It's currently still stuck at Coq 8.13, but this is not the only problem. Apparently, it requires CVC4 1.6 (from 4 years ago). It is not compatible with CVC4 1.8 (from last year), which I'm guessing is what the Coq Platform packages for CoqHammer, and even CVC4 is discontinued now in favor of CVC5... In nixpkgs, we keep getting build issues because of this (see https://github.com/coq-community/coq-nix-toolbox/pull/121, https://github.com/NixOS/nixpkgs/pull/176321, https://github.com/NixOS/nixpkgs/pull/183084).
Karl Palmskog (Sep 14 2022 at 16:30):have also been worried about this, maybe one core aspect is the usage of Coq native arrays? Or has this been addressed?
Karl Palmskog (Sep 14 2022 at 16:31):or maybe the lack of CVC4 support is due to problems unrelated to Coq itself (e.g., dev resources)
Karl Palmskog (Sep 14 2022 at 16:33):some discussion on the arrays thing here: https://github.com/coq-community/manifesto/issues/91
Théo Zimmermann (Sep 14 2022 at 16:34):Karl Palmskog said:
have also been worried about this, maybe one core aspect is the usage of Coq native arrays? Or has this been addressed?
Since it is now using a standard Coq version, I'm not getting why the use of a feature would make migrating to new versions much harder. Anyway, it's unfortunate that the port to master did not happen because it would have permitted to put it in Coq's CI.
Théo Zimmermann (Sep 14 2022 at 16:34):Karl Palmskog said:
or maybe the lack of CVC4 support is due to problems unrelated to Coq itself (e.g., dev resources)
That's my guess, and also for Coq.
Karl Palmskog (Sep 14 2022 at 16:42):unfortunately this will likely lead to a large number of ad-hoc Coq/SMT integrations in the future (just one recent example: https://dl.acm.org/doi/abs/10.1145/3519939.3523715)
Théo Zimmermann (Sep 14 2022 at 17:16):You mean the fact that SMTCoq is not part of the Coq Platform?
Michael Soegtrop (Sep 14 2022 at 17:26):@Chantal Keller : could you tell us what your plans are? I would really like to see SMTCoq in Coq Platform - it is really a pity that it bit rots.
Karl Palmskog (Sep 14 2022 at 17:34):I mean that if there isn't any SMT-for-Coq compatible with latest-ish Coq (which most people use) to converge on, lots of people will likely spend lots of time doing the "same" work of integrating Coq with SMT again and again going forward.
Karl Palmskog (Sep 14 2022 at 17:35):being in the Platform is of course even better, then we broadcast that "this is the SMT-for-Coq you should use", but not a requirement in itself
Chantal Keller (Sep 15 2022 at 07:45):Hi
It always take time to port SMTCoq to new versions of Coq because it contains a large amount of OCaml code. It does not mean that it is stuck; I do port every time I can but I also want to spend time improving it. A port is planned for after the deadline of CPP.
Regarding the supported versions of the provers: a collegue from Iowa is working on porting to CVC5 and the last version of veriT.
I appreciate the support; I do as much as I can with the means and time I have... I always find time to discuss with people who want to use it some way or another.
Chantal Keller (Sep 15 2022 at 07:49):And in my opinion, porting is not only having things compile, but also benefit from new features. For instance, I would like to use native arrays, but I have been struggling with them due to the fact that there are universe polymorphic, which forces me to change a lot of the OCaml code. A branch is under progress...
Michael Soegtrop (Sep 15 2022 at 08:16):@Chantal Keller : would it make sense to have a "compatibility branch" where just the necessary things are done to make it compatible to the latest Coq version and to do the development of new / improved features in a separate feature branch - possibly even several for separate features - which are merged when ready?
It would involve a bit of additional merging effort, but if the compatibility branch would be in Coq CI, quite a few things will likely get fixed the moment compatibility breaks, so under the line it might save you time by merging over such changes to the feature branch.
I don't see another way to have your work in Coq Platform, because this essentially means that a compatible release shall usually be available 6..8 weeks after the Coq release candidate release. From what you wrote above I would say this is not manageable as is.
I am sure a lot of users would profit from your work being in Coq Platform.
Théo Zimmermann (Sep 15 2022 at 08:16):@Chantal Keller This is good to hear. And I can understand that porting is not just having things compile. But wouldn't being in Coq's CI still save you a significant part of the time that you spend on porting from one Coq version to the next? This requires pushing up to Coq master (currently 8.17+alpha) at one point, so it's an investment, but it should be worthwhile in the long run. Furthermore, this would enable releasing new SMTCoq versions compatible with new Coq versions with a smaller delay (even if they do not yet take advantages of all the new features) and reach more users through the Platform.
EDIT: posted in parallel to Michael's message above.
Chantal Keller (Sep 15 2022 at 08:18):@Michael Soegtrop @Théo Zimmermann This is the way I proceed. It is also that the last two times I did such a "compatibality" port, a new release of Coq happened soon after. It is very fast...
I will let you know when I do the next push.
Théo Zimmermann (Sep 15 2022 at 08:20):To reach Coq's CI, you need anyway to target Coq's master, not the latest Coq release, so whether the next Coq release is expected soon or further away doesn't change much.
Chantal Keller (Sep 15 2022 at 08:20):I mean, I am closer to master right after a release than right before ;-)
Théo Zimmermann (Sep 15 2022 at 08:21):Sure, if you focus on releases.
Chantal Keller (Sep 15 2022 at 08:21):Anyway, I got it, and my next focus will be on pushing towards master ;-)
Théo Zimmermann (Sep 15 2022 at 08:21):I believe that SMTCoq is anyway considered important enough that you could request some help from Coq consortium's engineers to reach this objective. But @Maxime Dénès could say more.
Michael Soegtrop (Sep 15 2022 at 08:23):@Chantal Keller : the main question is: do you think it is feasible to have SMTCoq in Coq Platform (with the 6..8 weeks in mind)? If not, what would be required to get there?
EDIT: posted in parallel with Théo.
Chantal Keller (Sep 15 2022 at 08:24):@Michael Soegtrop Yes, in particular if it is in Coq CI.
Michael Soegtrop (Sep 15 2022 at 08:25):Perfect - I am looking forward to it!
Gaëtan Gilbert (Sep 15 2022 at 08:25):Théo Zimmermann said:
I believe that SMTCoq is anyway considered important enough that you could request some help from Coq consortium's engineers to reach this objective. But Maxime Dénès could say more.
in a less formal way we are generally willing to help with just about any plugin development problem ;)
Maxime Dénès (Sep 16 2022 at 13:00):Indeed. And yes, it is easy to argue that SMTCoq is of general interest and hence provide some support.
Chantal Keller (Oct 12 2022 at 15:59):Hi
SMTCoq now compiles with master, and I have just made a pull request to integrate the CI: https://github.com/coq/coq/pull/16649
Michael Soegtrop (Oct 12 2022 at 17:57):@Chantal Keller : very well! Do you think we should start the Coq Platform inclusion process now? I would target Coq 8.17 / Coq Platform 2023.03 which leaves some time to sort out OS dependency issues. If the answer is yes, please create a corresponding issue at https://github.com/coq/platform/issues.
Last updated: Jun 03 2023 at 03:01 UTC