Clean up, abstract configuration

[siddhartha-gadgil]

Currently the many choices involved in translation are scattered across arguments to many functions and are effectively chosen as default arguments. These should be gathered into a structure and passed as an argument, perhaps with a present configuration stored as an IO.Ref

A (partial) list of the choices made is the following:

• number of sentences based on similarity
• file from which similarity parameters are taken (e.g. safe-prompts).
• field that we look up in the file for similarity.
• function building the prompt statment from the json chosen.
• number based on keywords
• auxiliary keyword parameter choices
• function for string pasted as code, or choices for this (eg example vs theorem)

In the longer run the cleanup will help in allowing the user to configure. In the shorter run it will make experimenting with including definitions, asking for theorem names, using mathlib4 etc easy to try out.

[siddhartha-gadgil]

In the above, we should allow different sources for prompts, including from files and from keywords, and mixing strategies (including append and interleave).

[0art0]

Another abstraction I found useful in the lean3 implementation is the declaration_with_docstring structure (which is similar to the TheoremAndTactic structure).

[siddhartha-gadgil]

Another abstraction I found useful in the lean3 implementation is the declaration_with_docstring structure (which is similar to the TheoremAndTactic structure).

Yes, we can have such a structure and have functions that map to it for the different sources of statements (type only, with name etc).

[0art0]

Rather than using my own custom structure for declaration_with_docstring, I realised that it may be cleaner for me to just extend Lean.Declaration.

[0art0]

I have created some possible structures for holding the prompt building and querying parameters here.

[siddhartha-gadgil]

Looks good. You may need fields to specify the file queried (safe-prompts vs prompts for example) and what is extracted from the response (type vs statement for example). The latter may be a separate structure though (relevant to the prompt construction but not the query).

On Thu, 1 Dec 2022 at 15:36, Anand Rao @.***> wrote:

I have created some possible structures for holding the prompt building and querying parameters here https://github.com/siddhartha-gadgil/LeanAide/blob/re-structure/LeanCodePrompts/Query.lean .

— Reply to this email directly, view it on GitHub https://github.com/siddhartha-gadgil/LeanAide/issues/19#issuecomment-1333520243, or unsubscribe https://github.com/notifications/unsubscribe-auth/AA3K3JDYMTIBYQOGV4VJA5LWLB2CFANCNFSM6AAAAAASQKUNBM . You are receiving this because you authored the thread.Message ID: @.***>

[0art0]

I have written the code for translation with easy configuration. The configuration files are in this folder. An example of loading and using a configuration is here.

There are structures for each set of parameters, and also a structure for Declarations (WithDocstrings). The code is set up so that both informalisation and direct formalisation can be achieved by adjusting the parameters that determine how a DeclarationWithDocstring is displayed in the prompt.