Learning based space formatting of proof assistant code

Stream: Machine Learning for Theorem Proving

[Karl Palmskog]

Dear Lean ML community,

My collaborators and I recently presented our work-in-progress on learning-based space formatting of Coq files at the Coq Workshop (see abstract on arXiv and slides). We used a dataset that was discussed elsewhere on Lean's Zulip.

We believe similar techniques can easily be applicable to Lean files (especially Lean 4, through its accessible ASTs). Our main limitation right now that we don't handle hierarchical formatting of proof scripts. We would welcome any feedback from the Lean ML community on this, in particular how one can define features to expose formatting/indenting based on the proof goal structure.

The best idea I have right now is that one could attach a tuple or list of integers, e.g., "(2, 3)" or "2 3", to tokens inside a tactic expression that is operating on the 3rd subgoal of the 2nd subgoal. But there is likely a general way to handle this, perhaps even across proof assistants like Lean and Coq.

[Gabriel Ebner]

It is not customary to indent tactic scripts in Lean based on the goal structure. If you have multiple goals, then it is common practice to put each of the subgoal into a { ... } block (which ensures that the goal is solved).

example : A ∧ B :=
begin
 split,
 { unfold A, ring },
 { simp only [c, d, e],
   intro n,
   induction n; simp * },
end

[Karl Palmskog]

but you can have nested { ... } though, right? Doesn't that bring "implicit" hierarchical indentation?

[Gabriel Ebner]

Right, but the indentation should always follow the {} blocks.

[Gabriel Ebner]

Maybe I misunderstood your question. I thought this shouldn't be a problem because it is syntactically obvious (and doesn't require any knowledge of the tactic states).

[Karl Palmskog]

so Lean itself enforces that the meaning of the following is always different? (In Coq similar sequences could have the same meaning depending on options)

{  ring, /- subgoal with one subgoal -/
   { ring } }

vs.

{ ring ,  /- two subgoals at the outset -/
  ring }

[Mario Carneiro]

what does /- two subgoals at the top -/ mean? After a { there is always exactly one goal. If the result of running ring produces two goals then it is conventional to put ring, { proof1 }, { proof2 } after it, otherwise (if there is only one goal) we just write ring, proof

[Karl Palmskog]

If the result of running ring produces two goals then it is conventional to put ring, { proof1 }, { proof2 } after it

But this is not mandated by Lean itself, right? You would have to use a linter or similar to enforce this? One goal of our work was to learn (in lieu of specifying precisely) when subgoals should be newlined, e.g., based on discussion here one could either write:

ring, { ring }, { ring }

or

ring,
{ ring },
{ ring }

But I guess you might be already be using linting to get the latter?

[Johan Commelin]

No, we currently have no linter for checking style.

[Johan Commelin]

Usually, { foo, bar, baz } would go on a new line, but if it's really short, sometimes we put it after the tactic that created the multiple goals.

[Johan Commelin]

Example:

induction n, { simp }, -- the case n = 0 is short enough to deal with on this line
-- now there is only one goal left. We sometimes omit the {}
tactic_foo,
bar,
rw IH,
simp

[Karl Palmskog]

thanks, that's very helpful. I guess the only way to figure out if adding the proof goal structure as a feature will actually help Lean formatting is to do a machine learning eval, then. It might go either way here, but for Coq it was very clear that we were missing a lot of indents/newlines

[Johan Commelin]

Of course we could slightly change our style guide, if this means we get an auto-formatter (-;

[Karl Palmskog]

to give you an idea of the current status:

• here is the suggested formatting we got based only on observing Coq token streams, and
• here is the manually formatted file.

Unfortunately, tuning is lacking for things like getting the Qed newlines right.

Since our team doesn't have Lean competence, we are open to working with a Lean (ML) collaborator to do something similar for Lean. In particular, the main limitation may be that we rely on independently readable code with spacing information to learn from (which is very hard to obtain for Lean 3).

[Alex J. Best]

Yeah there are a few things it would be interesting to see if ML would learn, like work_on_goals and all_goals tactics, which are an exception to the "rules".

[Mario Carneiro]

In particular, the main limitation may be that we we rely on independently readable code with spacing information to learn from (which is very hard to obtain for Lean 3).

I'm not sure I understand. Why doesn't mathlib satisfy this requirement?

[Karl Palmskog]

From the dataset topic I referenced at the initial post in this topic:
Jason Rute said:

Karl Palmskog said:

Coq source files are known to be near-impossible to lex/parse accurately by tools external to Coq.

This is definitely the state we are in with Lean 3. I've written some tools, and am writing more, to work with Lean programmatically, but definitely it is not possible to parse a Lean file by itself without recreating Lean. (Lean has an export format, but it throws too much away for machine learning. It's only good for checking proofs with external checkers.) I know Lean 4 is supposed to have an intermediate AST layer. I don't know if that will be easy to access or work with. I've been told it is, but I haven't seen any examples proving it.

[Karl Palmskog]

@Mario Carneiro if there was an independent format of .lean files with their tokens and their locations, we could definitely do it. If there is interest I can give very specific examples of what data we use from serialized Coq code.

[Mario Carneiro]

What tool does this for coq?

[Gabriel Ebner]

Looking at the two Coq files, Lean doesn't have the same issue with indentation in the the tactic scripts. Tactics should be indented if and only if they are in a {} block. But the end still needs to be on a new line with the same indentation as the begin.

[Mario Carneiro]

I think lean tactic fomatting should be about as simple as formatting languages like java, once you get the relevant parsing info

[Karl Palmskog]

We currently use SerAPI to serialize Coq files, to obtain both ASTs and tokens as S-expressions (it uses OCaml PPX metaprogramming): https://github.com/ejgallego/coq-serapi

[Karl Palmskog]

Java was one of the first languages to get a learning-based formatter: http://groups.inf.ed.ac.uk/naturalize/

[Mario Carneiro]

the only thing that might require more intelligence in tactic formatting is determining when to put a newline after a tactic, i.e.

  tac1,
  tac2,

vs

  tac1, tac2,

[Mario Carneiro]

Relevant correlates might include the author, the available line length, as well as the identity of the tactics / whether they "form a unit"

[Mario Carneiro]

which might involve looking at the tactic states

[Mario Carneiro]

however, a decent number of users just put line breaks after every tactic and that's not an unreasonable style (though it is a bit vertically verbose)

[Johan Commelin]

Mario Carneiro said:

Relevant correlates might include the author, the available line length, as well as the identity of the tactics / whether they "form a unit"

If you find stuff that goes on till column 235, it's a safe bet that it was written by Scott.

[Jason Rute]

@Karl Palmskog what specifically do you need from Lean to do this? The lean server can provide some information like which tactic state a character is associated with, but in my experience it is slow and it is not always aligned correctly. Also it can’t handle hierarchical states like tactics inside tactics. Alternately, one can modify the interactive lean code (which governs the behavior of tactics) to record positions. If I recall, you might be able to record the starting and ending positions of tactics using that. This is more accurate but involves a bit of hacking (just the Lean, not the C++). There are probably other approaches as well.