Stream: Coq users

Topic: pycoq


view this post on Zulip Paolo Giarrusso (Nov 04 2021 at 20:57):

Wait what https://github.com/IBM/pycoq cc @Emilio Jesús Gallego Arias any relation? It is the IBM

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 21:31):

@Paolo Giarrusso I am blind and learned about IBM's pycoq after I sent the mail to coq club

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 21:32):

let's see what happens, tho indeed native pycoq superseedes serapi pycoq

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 21:32):

actually we are in the process of consolidating both

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 21:32):

so only difference for serapi vs pycoq will be the outer outer layer

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 21:33):

that is to say, the "rpc" method used

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 21:33):

once native pycoq exist, there is no reason to go thru serapi

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2021 at 21:33):

and many not to

view this post on Zulip Karl Palmskog (Nov 05 2021 at 07:31):

but one still needs serlib at the Coq level, right?

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 11:31):

If you want to get serialized data yes

view this post on Zulip Emilio Jesús Gallego Arias (Nov 05 2021 at 11:31):

I'd like to have this dep be optional


Last updated: Apr 18 2024 at 01:01 UTC