Re structure

[0art0]

New code for easily modifying parameters.

[siddhartha-gadgil]

I was looking at the code and I see that in some places while reading from Json the kind is hard-wired as "theorem". This is fine but it should be clear when to have this and when to read the kind. Perhaps two different functions, or an argument?

Or is this work in progress?

[0art0]

Thanks. I have modified the code to get the kind to match the one specified in the Request.

[siddhartha-gadgil]

@0art0 Do you handle both these cases (which we need)?

• When reading from safe_prompts.json, the kind is not a field and should be assigned as theorem.
• When reading from withdefs_... we should read the kind.

Which choice is made should be part of the configuration.

[0art0]

I am reading in the kind by default. I have not handled the safe_prompts case, but I am thinking of regenerating the file to add a kind := "theorem" field to keep the Lean4 code more uniform.

[siddhartha-gadgil]

I am reading in the kind by default. I have not handled the safe_prompts case, but I am thinking of regenerating the file to add a kind := "theorem" field to keep the Lean4 code more uniform.

That is a good option too. Do make sure while regenerating that you preserve the unicode (i.e., not escaped) and the lines. Also please regenerate prompts.json as well, so refiltering does not break the code

[0art0]

I have regenerated both sets of prompts with the kind field (the spacing and indentation is a bit distorted, but the content and the Unicode is intact).

[0art0]

I am in the process of making a few more superficial changes to the structures. I will push my code shortly.

[siddhartha-gadgil]

@0art0 I pulled the code and it is repeatedly giving panic messages. This seems to be that in CodeActions.lean there are two instances of .get! which assume that we can get a comment and a theorem. Instead the CodeAction should fail gracefully (maybe go to a default value for now).

[0art0]

I am actually not using CodeActions.lean on this branch. The main file that I am using for testing is StatementAutoformalisation/Experiment.lean (which does not yet have an interface implemented).

[siddhartha-gadgil]

I am actually not using CodeActions.lean on this branch. The main file that I am using for testing is StatementAutoformalisation/Experiment.lean (which does not yet have an interface implemented).

The interface we expect to use in the longer run is CodeActions, so please test the examples in TranslateExamples.lean as you develop.

[siddhartha-gadgil]

@0art0 The errors were due to "informalize", which I have commented out. If it seems fine with you I plan to merge this.

I want to make a "mathlib4" branch getting rid of the binport dependency but for now using the same data for prompting and auto-correction. It is better to merge this first.

[0art0]

I would like to also create an abstract configuration for handling the code action interface for both formalisation and informalisation.

[siddhartha-gadgil]

If you think it is better to do that before mergiing, I can wait. Otherwise I can merge to main and you can continue to use this as a feature branch to develop further and make a fresh PR.

[0art0]

I think merging is fine.