coq-serapi

coq-serapi copied to clipboard

Add a query to perform a diff of terms

6

In my [work-in-progress proof explorer GUI](https://github.com/elidupree/coq_experiments/tree/main/proof_explorer), I currently display diffs of goals by doing a diff on their string representations. It would be better to diff the term structure -...

elidupree

Accessing fully qualified names when printing (for hyperlinking support in Alectryon)

6

Hi Emilio. This is a follow up to https://github.com/coq/coq/issues/4834#issuecomment-655766329 (thanks for the quick response!) One thing Alectryon is missing compared to coqdoc is hyperlinking abilities. I'd like to (1) be...

cpitclaudel

Adding a mode to sercomp to get rid of all notations

13

Hi ! Do you know how complex it would be to extend `sercomp` with a mode that strips a vernacular expression of all notations ? The end goal here is...

vsiles

TypeOf only gives the type of identifiers, not of expressions.

2

For example, `(Query (TypeOf "S"))` returns the correct result, however `(Query (TypeOf "S O"))` results in the error `(CErrors.UserError ("" "Invalid character ' ' in identifier \"S O\".")))`

darbyhaller

Tests for tokenization off-by-one locs

8

Consider the following `sertop` session with the latest SerAPI from the `v8.10` branch (formatted for readability and with unnecessary output removed): ``` (Add () "Notation \"[ 'arg[' ord ]\" :=...

palmskog

Print a sentence with the notation interpretation, scope resolution, and explicit arguments

2

Hi, I would like to be able to print a given input sentence with the notation interpreted, all arguments explicit, and the scopes resolved by Coq's internalization process. For example,...

darbyhaller

Querying module definitions

1

Hi! Is there a way to get sexp-formatted information about modules, like the one acquired by running `Print Coq.Init.Datatypes` in Vernac? I failed to find a way, and running several...

dkhalansky

[protocol] Add `Search` support.

4

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...

ejgallego

[serapi] Add `Init` call to the protocol.

1

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...

ejgallego

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.

ejgallego