coq-serapi

coq-serapi copied to clipboard

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

ejgallego

Why don't the responses from coq-serapi corresponds to type definitions on the coq code?

1

I was trying to traverse the s-expressions that coq-serapi gives me. But sometimes there are more arguments than expect. e.g. `GenArg` should have 2 but coq-serapi gives me 3: ```...

brando90

How to have serapi return to me coq human strings from arbitrary subterms in a coq-ast?

4

I want to get the human string after I extract valid sub trees from a coq-serapi ast. e.g. I have ``` (GenArg raw (ExtraArg tactic) (TacArg ((v (TacCall ((v (((v...

brando90

Why does TacArg accepts a value of CAst.t type when it should only accept values of types

1

See the argument for TacArg: https://github.com/ejgallego/coq-serapi/blob/b222c1f821694175273d3a295a04abf9454f6727/serlib/plugins/ltac/ser_tacexpr.ml#L232 but the reply has a type CAst.t as an argument for TacArg: ``` (Parse () "(___hole O).") (Answer 24 Ack) (Answer 24 (ObjList ((CoqAst...

brando90

Querying proof term directly with `Query`

13

I tried this interaction: ``` (Add () "Lemma addn0 n : 0 + n = n. Proof. intros. simpl.") (Exec 5) (Query ((pp ((pp_format PpStr)))) Proof) ``` but I don't...

brando90

Do I always have to wrap anonymous functions in a definition for Coq Serapi to parse it for me?

1

I want to get the "coq ast" for lambda functions in coq. e.g. I did the following but all fail: ``` rlwrap sertop --printer=human (Add () " Theorem add_easy_0: forall...

brando90

This could be useful to some users, as opposed to the previous implementation which was never finished. Closes #270

ejgallego

I wanted to be able to get the entire current proof state (local context and goals) with all the individual terms separated, e.g. each term in a lists/arrays. Pseduocode: ```...

brando90

Fixes ejgallego/coq-serapi#20 This is still experimental, in particular we should maybe provide a better support for handling ejgallego/coq-lsp#332.

ejgallego

Make sertop respond consistently to SIGINT

1

Currently, [these notes](https://github.com/ejgallego/coq-serapi/blob/v8.12/notes/ser-control-protocol.md#interrupting) appear to be the most detailed documentation on interrupting sertop: > ### Interrupting > > 1. The IDE must send an interrupt signal to sertop. > 2....

elidupree