The Coq mailing list

[Jim Fehrle <jim.fehrle AT gmail.com>]

There's already an interface that lets Ltac2 call Ocaml code.  Most of the work would be adapting the current search command core to generate a data structure that you can return rather than printing the info.

I expect this would not be too difficult to prototype.  Ideally the command could be refactored so the printing relies on the data structure generating routine so the command and the Ltac2 routine remain consistent.

Good luck,

Jim

On Fri, May 3, 2024, 3:23 PM Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

Thanks for asking me to clarify. Sorry, the initial message could have been more precise.

I am asking to add a new function, say Ltac2Search, to the ltac2 API, so that it can be used by ltac2 programs. 

It should have signature:

string -> reference list

(I dont know too much about ltac2 but if it already has a type Econstr of terms with holes, the type could instead be Econstr-> reference list)

the string input would precisely be the strings accepted by the Search vernacular command (https://coq.inria.fr/doc/V8.19.0/refman/proof-engine/vernacular-commands.html#grammar-token-search_query)

The output would be the list of references corresponding to what Search would have returned (just the names not the types).

As a fully concrete example, 
Ltac2Search "+" would return [plus_O_n, plus_n_O...]

the items in the list would be concrete references which include fully qualified names of the constants (I am not familiar with the exact representation of the `reference` type of ltac2).

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Fri, May 3, 2024 at 1:50 PM Jim Fehrle <jim.fehrle AT gmail.com> wrote:

Can you be more specific about what you mean by "Search functionality", which is vague?  I don't see how your examples (smart IDEs, serializing for LLMs) fit into search.

Jim

On Fri, May 3, 2024 at 4:55 AM Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

Another use could be to automatically find relevant lemmas to prove a goal, without needing to add to hint dbs, and potentially emit a primitive proof that can be checked faster later.

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Thu, May 2, 2024 at 2:47 PM Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

How hard would it be to add Search functionality to ltac2?
Has somebody already done that?

While developing smart IDEs, this would let us push more functionality to ltac2 rather than having to implement it in elisp (emacs)/typescript (vscode) and have different versions for each IDE.

My concrete usecase is to take an iris separation-logic Coq goal and serialize it for consumption by LLMs.

I would like to implement all of it Ltac2. `Search` API could be useful to feed the LLM relevant lemmas about the constants mentioned in the goal.

In some past projects (e.g. https://sympa.inria.fr/sympa/arc/coq-club/2023-10/msg00026.html),
I found it much easier and less error-prone to write most of the logic in ltac2/ltac rather than in elisp.

-- Abhishek

http://www.cs.cornell.edu/~aa755/