Is it possible to run on a Lean 3 file which doesn't compile (i.e., valid syntax, unknown references)

[offendo]

Hi there, I'm trying to run mathport on an incomplete Lean 3 file and not sure if that's even possible. For example if I just have the following lemma:

-- example.lean

lemma (x : X) : x > 5 
  := sorry

Synport seems like what I want, but not totally sure. Is it possible to run only synport on the file?

[digama0]

Yes. sorry or other semantic errors are okay, but syntax errors are not and will cause a panic in mathport. By default, only synport runs (more or less) so you should not have to do anything special for that.

[offendo]

Much appreciated! I'm running oneshot and it seems like it errors if I don't at least have definitions with sorrys, e.g., the following snippet errors out:

lemma beta
  (n : ℕ) (hn : n ≥ 1) :
  β α n = abs ((q α n) * x - (p α n))
  := sorry

But just adding sorrys and/or variables makes it work:

def β := sorry
def q := sorry
def p := sorry

variables (A : Type*) (α : A) (x : A)

lemma beta
  (n : ℕ) (hn : n ≥ 1) :
  β α n = abs ((q α n) * x - (p α n))
  := sorry

[digama0]

Yes, those are name resolution errors and they mess up the syntax tree. As a rule of thumb you should try to get rid of anything that would be a red squiggle in lean, use sorry as needed.