Questions: What is purposes of file_path and full_name in LeanGitRepo, and what is the pp in TacticState?

[irene622]

Hi, I try to experiment a small test.

My code to run is the below.

from pathlib import Path

# pp = 'α : Type u_1,\nβ : Type u_3,\nf : α → β → β,\na : α,\nh : ∀ (b : β), f a b = b,\nt : set β\n⊢ image2 f {a} t = t'
my_ts = TacticState(pp="\u03b1\u0020\u003a\u0020\u0054\u0079\u0070\u0065\u0020\u0075\u005f\u0031\u002c\u005c\u006e\u03b2\u0020\u003a\u0020\u0054\u0079\u0070\u0065\u0020\u0075\u005f\u0033\u002c\u005c\u006e\u0066\u0020\u003a\u0020\u03b1\u0020\u2192\u0020\u03b2\u0020\u2192\u0020\u03b2\u002c\u005c\u006e\u0061\u0020\u003a\u0020\u03b1\u002c\u005c\u006e\u0068\u0020\u003a\u0020\u2200\u0020\u0028\u0062\u0020\u003a\u0020\u03b2\u0029\u002c\u0020\u0066\u0020\u0061\u0020\u0062\u0020\u003d\u0020\u0062\u002c\u005c\u006e\u0074\u0020\u003a\u0020\u0073\u0065\u0074\u0020\u03b2\u005c\u006e\u22a2\u0020\u0069\u006d\u0061\u0067\u0065\u0032\u0020\u0066\u0020\u007b\u0061\u007d\u0020\u0074\u0020\u003d\u0020\u0074", id=0)

my_thm = Theorem(repo=LeanGitRepo(url='https://github.com/leanprover-community/mathlib', 
                               commit='8c1b484d6a214e059531e22f1be9898ed6c1fd47'),
            file_path=Path('src/data/set/n_ary.lean'), 
            full_name='set.image2_left_identity')

with Dojo(my_thm) as (my_dojo, my_init_state) :
    response = my_dojo.run_tac(my_init_state, "exact set.image_id")
    print(response)

The code prints LeanError() as response and do not show any errors.

I have three ambiguous points.

1. What is the pp in TacticState? I guess that put the hypothesis and conclusion in pp. What is the pp meaning?
2. I wonder the purpose of id in TacticState,,,

3. I don't know the purpose of file_path and full_name in LeanGitRepo. file_path is the relative file path which contains pp and full_name is the name of pp. Then, why file_path and full_name do need?

   Please answer... I can not find in any information in Lean-Dojo document...