Emilio Jesús Gallego Arias
Emilio Jesús Gallego Arias
We would like to have binary builds [at least for Windows] so `coq-lsp` can be installed from the market easily. A possible roadmap would be to use Github Actions on...
We perform a very large refactoring of `serlib`, moving all the `Obj.magic` hacks to a more principled solution based on interfaces, mainly exported by `SerType`. Moreover, we use a similar...
This could be useful to some users, as opposed to the previous implementation which was never finished. Closes #270
Fixes ejgallego/coq-serapi#20 This is still experimental, in particular we should maybe provide a better support for handling ejgallego/coq-lsp#332.
Right now, the code for search reads: ``` | Search -> [CoqString "Not Implemented"] ``` `Names` provides a very restricted subset of `Search`, however we should unify A question is...
As of today, SerAPI creates a new document by default, with standard loadpaths, libraries, etc... This can be overridden to some point using cmdline parameters, but we would like to...
We'd like to add support for evar querying. The XML protocol already provides some support, see https://github.com/coq/coq/blob/trunk/ide/ide_slave.ml#L223 Also, https://coq.inria.fr/bugs/show_bug.cgi?id=4504 seems very relevant.
[serlib] Add ppx_python serialization. We add Python serialization for the complete protocol, modulo the existing issues the current setup seems to work well! Main hiccup was the lack of variants...
We should provide a Python binding for SerAPI as this is what many people actually use. In principle, we should have a `doc` object, with `add` and `cancel` methods, as...
This is a frequent request by for example @cpitclaudel or @JasonGross ; I already have something in my document manager implementation that does exactly this [so incremental checking can have...