Emilio Jesús Gallego Arias (Apr 15 2021 at 20:51): Emilio Jesús Gallego Arias (Apr 15 2021 at 20:51):Hi folks, thanks for all the feedback; I got distracted with other stuff today so I didn't manage to push the changes but I hope I will do ASAP.
I'd like to mention that the Python bindings for SerAPI are actually quite ready I think as a prototype, so this could save some people a bit of plumbing work I think; they were blocked by a problem with ppx_python but I think that's solved now.
So if you plan to interact with SerAPI from Python you should be able to give the branch a go soon [current branch on github I think is broken due to the ppx problem so I need to update it]
Clément Pit-Claudel (Apr 15 2021 at 22:33):Oh, that's very exciting! Does this save on serialization/deserialization time? In the Alectryon paper I measured that about 1/3 of the runtime was spend parsing and unparsing sexps.
Emilio Jesús Gallego Arias (Apr 15 2021 at 23:43):Good question, should be faster but I dunno how much, as still we have the OCaml -> Python conversion and vice-versa; I am not very familiar with the internals of ppx_python .
Emilio Jesús Gallego Arias (Apr 15 2021 at 23:44):There are still a few issues to be solved, in particular w.r.t. how to best map some notions / Coq APIs to Python, but the basic things should work.
Clément Pit-Claudel (Apr 16 2021 at 04:44):Sweet. Let me know when I should give it a spin (though it'll take me a few weeks to catch up with my current stuff)
Emilio Jesús Gallego Arias (Apr 17 2021 at 19:01):Ok, got it working https://github.com/ejgallego/coq-serapi/blob/v8.13%2Bpyml/test.py
Emilio Jesús Gallego Arias (Apr 17 2021 at 19:01):[('ObjList', ([('CoqAst', ({'v': {'control': [], 'attrs': [], 'expr': ('VernacDefinition', ((('NoDischarge', None), ('Definition', None)), ({'v': ('Name', (('Id', ('b',)),)), 'loc': {'fname': ('ToplevelInput', None), 'line_nb': 1, 'bol_pos': 0, 'line_nb_last': 1, 'bol_pos_last': 0, 'bp': 11, 'ep': 12}}, None), ('DefineBody', ([], None, {'v': ('CPrim', (('Number', ((('SPlus', None), {'int': '2', 'frac': '', 'exp': ''}),)),)), 'loc': {'fname': ('ToplevelInput', None), 'line_nb': 1, 'bol_pos': 0, 'line_nb_last': 1, 'bol_pos_last': 0, 'bp': 16, 'ep': 17}}, None))))}, 'loc': {'fname': ('ToplevelInput', None), 'line_nb': 1, 'bol_pos': 0, 'line_nb_last': 1, 'bol_pos_last': 0, 'bp': 0, 'ep': 18}},))],)), ('Completed', None)]
Still many things to improve, and I have 0 Python knowledge so indeed you folks who are Python experts should help to frame the API as you would like it
Emilio Jesús Gallego Arias (Apr 17 2021 at 19:03):Will post instructions in the corresponding issue https://github.com/ejgallego/coq-serapi/issues/48
Emilio Jesús Gallego Arias (Apr 18 2021 at 23:30):Ok I put the instructions on a draft PR https://github.com/ejgallego/coq-serapi/pull/240
Emilio Jesús Gallego Arias (Apr 22 2021 at 22:38):Hi folks, something I'll need help here is with regards to Python packaging; the way I will proceed is that once the required deps for coq-serapi + python is ready, the opam package will install the corresponding .so that can be loaded by python, but no idea how to sync that to the particular python code that I'd assume grow large over time.
Brando Miranda (Jun 10 2022 at 18:34):I'm curious, what is the differences between emilio's PyCoq and Proverbot's coq_serapy interface https://github.com/HazardousPeach/coq_serapy/tree/main ?
Brando Miranda (Jun 23 2022 at 20:38):How will the interface to python interface to coq (https://github.com/ejgallego/pycoq) change when a language server is used? asking due to following line:
Note: In future versions, sentence id will be deprecated, and instead we will use Language Server Protocol-style locations inside the document to identify sentences.
from http://ejgallego.github.io/coq-serapi/coq-serapi/Serapi/Serapi_protocol/
Brando Miranda (Jun 23 2022 at 20:39):(I assume this will change the interface to SerAPI and not only PyCoq-SerApi? Since we won't be able to send documents seperated by dots etc anymore?)
Last updated: May 31 2023 at 03:30 UTC