coq-serapi
coq-serapi copied to clipboard
ejgallego
Coq Protocol Playground with Se(xp)rialization of Internal Structures.
We'd like to do correct location reporting for UTF-8 scripts. See https://coq.inria.fr/bugs/show_bug.cgi?id=4965 for more details.
From the example on the docs the format of the proof state should be something like: ``` ((CoqString "\ \n local context\ \n============================\ \ngoals... ``` but in induction the goals...
@ejgallego : I have an issue with serapi on MacOS: serapi wants to load Coq .vo files from a compile time path. On Windows, when running serapi from a binary...
The max file name length of a serapi build with Coq Platform standards path is beyond the 259 char Windows limit again and is now: ``` C:\bin\cygwin64_coq_platform\home\Michael\.opam\CP.2023.11.0~8.18~2023.11\.opam-switch\build\coq-serapi.8.18.0+0.18.1\_build\default\serlib\plugins\syntax\.serlib_number_string_notation_plugin.objs\serlib_number_string_notation_plugin__Ser_number.impl.all-deps ``` The breakdown...
Should hopefully close #266 , thanks to Julien Puydt and Karl Palmskog for helping with this. - Fix LICENSE and opam file discrepancies - Update LICENSE from `debian/copyright` work by...
Fixes: #371
Hi. While I was viewing serlib's document, I noticed that functions for converting between types for the extraction plugin (e.g., [lang](https://coq.inria.fr/doc/V8.18+rc1/api/coq-core/Extraction_plugin/Table/index.html#type-lang)) and SExp were missing. Is it okay to send...