Data Extraction

Data Extraction#

import os
from pathlib import Path
from pantograph.server import Server

Tactic Invocation#

Pantograph can extract tactic invocation data from a Lean file. A tactic invocation is a tuple containing the before and after goal states, and the tactic which converts the “before” state to the “after” state.

To extract tactic invocation data, use server.tactic_invocations(file_name) and supply the file name of the input Lean file.

project_path = Path(os.getcwd()).parent.resolve() / 'examples/Example'
print(f"$PWD: {project_path}")
server = Server(imports=['Example'], project_path=project_path)
units = server.tactic_invocations(project_path / "Example.lean")

$PWD: /home/aniva/Projects/atp/PyPantograph/examples/Example

The function returns a list of CompilationUnit objects, corresponding to each compilation unit in the input Lean file. For performance reasons only the text boundaries are loaded into CompilationUnits.

with open(project_path / "Example.lean", 'rb') as f:
    content = f.read()
    for i, unit in enumerate(units):
        print(f"#{i}: [{unit.i_begin},{unit.i_end}]")
        unit_text = content[unit.i_begin:unit.i_end].decode('utf-8')
        print(unit_text)

#0: [14,85]
/-- Ensure that Aesop is running -/
example : α → α :=
  by aesop


#1: [85,254]
example : ∀ (p q: Prop), p ∨ q → q ∨ p := by
  intro p q h
  -- Here are some comments
  cases h
  . apply Or.inr
    assumption
  . apply Or.inl
    assumption

Each CompilationUnit includes a list of TacticInvocations, which contains the .before (corresponding to the state before the tactic), .after (corresponding to the state after the tactic), and .tactic (tactic executed) fields.

for i in units[0].invocations:
    print(f"[Before]\n{i.before}")
    print(f"[Tactic]\n{i.tactic} (using {i.used_constants})")
    print(f"[After]\n{i.after}")

[Before]
α : Sort ?u.7
⊢ α → α
[Tactic]
aesop (using [])
[After]

for i in units[1].invocations:
    print(f"[Before]\n{i.before}")
    print(f"[Tactic]\n{i.tactic} (using {i.used_constants})")
    print(f"[After]\n{i.after}")

[Before]
⊢ ∀ (p q : Prop), p ∨ q → q ∨ p
[Tactic]
intro p q h (using [])
[After]
p q : Prop
h : p ∨ q
⊢ q ∨ p
[Before]
p q : Prop
h : p ∨ q
⊢ q ∨ p
[Tactic]
cases h (using ['Eq.refl', 'Or'])
[After]
case inl
p q : Prop
h✝ : p
⊢ q ∨ p
case inr p q : Prop h✝ : q ⊢ q ∨ p
[Before]
case inl
p q : Prop
h✝ : p
⊢ q ∨ p
[Tactic]
apply Or.inr (using ['Or.inr'])
[After]
case inl.h
p q : Prop
h✝ : p
⊢ p
[Before]
case inl.h
p q : Prop
h✝ : p
⊢ p
[Tactic]
assumption (using [])
[After]

[Before]
case inr
p q : Prop
h✝ : q
⊢ q ∨ p
[Tactic]
apply Or.inl (using ['Or.inl'])
[After]
case inr.h
p q : Prop
h✝ : q
⊢ q
[Before]
case inr.h
p q : Prop
h✝ : q
⊢ q
[Tactic]
assumption (using [])
[After]
Contents