Fix(typing): mypy errors

[AntiKnot]

Involved Issue

Close #196

Note

• fix some chore typing.
• fix subclass call parent factroy method from_data or from_xml. use Generic[T].
• fix child[x] use cast pass some mypy check if varibale after assert check
• fix cmd call execute if return None, cant slice. raise Error.

Need Discus

• callback node covariant
• is_potential_premise_lean4 node doesn't have name
• is_mutual_lean4 loop on fullname: Optional[str] and set as full_name seams weird.

[yangky11]

Thanks! I'll be able to take a look next week.

[AntiKnot]

Thanks! I'll be able to take a look next week.

Limited understanding of the project, only the type check part, make some review comments.
Any Suggestions are Welcome.

[AntiKnot]

some errors not just about typing.

loop on Optional[str] | List[str]

src/lean_dojo/data_extraction/traced_data.py:897: error: Item "None" of "str | list[str] | None" has no attribute "__iter__" (not iterable)  [union-attr]
                        for s in node.full_name:

LeanDojo/src/lean_dojo/data_extraction/traced_data.py

Lines 872 to 882 in 7f66e93

	if is_mutual_lean4(node):
	for s in node.full_name:
	results.append(
	{
	"full_name": s,
	"code": code,
	"start": list(start),
	"end": list(end),
	"kind": node.kind(),
	}
	)

Node no attribute name

src/lean_dojo/data_extraction/traced_data.py:648: error: Item "IdentNode" of "IdentNode | CommandTheoremNode | StdTacticAliasAliaslrNode" has no attribute "name"  [union-attr]
                        full_name = [_qualify_name(name, prefix) for name in node.name]

LeanDojo/src/lean_dojo/data_extraction/traced_data.py

Lines 632 to 636 in 7f66e93

	full_name = (
	[_qualify_name(name, prefix) for name in node.name]
	if is_mutual_lean4(node)
	else _qualify_name(node.name, prefix)
	)

check instance type IdentNode, CommandTheoremNode, StdTacticAliasAliaslrNode but Node and these SubNode, doesn't has attribute name.

TracedTactic ast node with Optional[Pos]

    # ast: Node = field(repr=False)
    ast: OtherNode | TacticTacticseqbracketedNode = field(repr=False)

but should i check start and end like state_before and state_after assert not None fisrt?

src/lean_dojo/data_extraction/traced_data.py:184: error: Incompatible return value type (got "Pos | None", expected "Pos")  [return-value]
            return self.ast.start
                   ^~~~~~~~~~~~~~
src/lean_dojo/data_extraction/traced_data.py:189: error: Incompatible return value type (got "Pos | None", expected "Pos")  [return-value]
            return self.ast.end

[AntiKnot]

slice not raise error. when index with None, but should not use operator on None

$ a = [1,2,3]
$ a[None:] 
[1,2,3]

src/lean_dojo/data_extraction/traced_data.py:235: error: Unsupported left operand type for <= ("None")  [operator]
                    if cur <= node.start:

check type for node class property. start/end

Generator has incompatible item type "str | None"; expected "str"

src/lean_dojo/data_extraction/traced_data.py:652: error: Generator has incompatible item type "str | None"; expected "str"  [misc]
                        ns.name

".".join([None,None])
Traceback (most recent call last):
  File "/Users/conor/Code/LeanDojo/.venv/lib/python3.10/site-packages/IPython/core/interactiveshell.py", line 3577, in run_code
    exec(code_obj, self.user_global_ns, self.user_ns)
  File "<ipython-input-10-3a6a69d88909>", line 1, in <module>
    ".".join([None,None])
TypeError: sequence item 0: expected str instance, NoneType found

Item "None" of "Any | str | list[str] | None" has no attribute "iter" (not iterable)

src/lean_dojo/data_extraction/traced_data.py:660: error: Item "IdentNode" of "IdentNode | CommandTheoremNode | StdTacticAliasAliaslrNode" has no attribute "name" 
[union-attr]
                        full_name = [_qualify_name(name, prefix) for name in node.name]

def is_mutual_lean4(
    node: Node,
) -> TypeGuard[Union[IdentNode, CommandTheoremNode, StdTacticAliasAliaslrNode]]:
    return (
        isinstance(node, (IdentNode, CommandTheoremNode, StdTacticAliasAliaslrNode))
        and node.is_mutual
    )

is_mutual_type want filter type(full_name) != str so tpye full_name maybe None| List[str],and cant operator loop on None
is_mutual_type want In this judgment, List name is obtained from 3 types, but 3 types are excluded in else.
full_name = [_qualify_name(name, prefix) for name in node.name] node.name can only type List[str]

[AntiKnot]

always use

if is_potential_premise_lean4(node):
    ...
    if is_mutual_lean4(node):
    ...

so node input is_mutual_lean4 always subset of node input is_potential_premise_lean4:

potential_premise ->
CommandDeclarationNode,
LemmaNode,
MathlibTacticLemmaNode,
LeanElabCommandCommandIrreducibleDefNode,
StdTacticAliasAliasNode,
StdTacticAliasAliaslrNode,

subset node type only StdTacticAliasAliaslrNode

change is_mutual_type ,only check isinstance StdTacticAliasAliaslrNode

[AntiKnot]

Thanks! I'll be able to take a look next week.

hi, @yangky11

$ black src/lean_dojo                                 
All done! ✨ 🍰 ✨
10 files left unchanged.

$ mypy src/lean_dojo                                                               
Success: no issues found in 10 source files

[yangky11]

Sorry I've been swamped recently but will take a look when I get a chance!

[AntiKnot]

Sorry I've been swamped recently but will take a look when I get a chance!

It's okay. Related projects are developing rapidly and it works fine now. Type checking is not a priority.
Enjoy the work.