load_sorry fails to recognize open statements

[AG161]

In this comment it was suggested that load_sorry can take open statements along with the theorem body. I may have misunderstood something, but I found that not to work in the following MWE:

from pantograph import Server

root = """
open Nat

theorem add_comm_proved_formal_sketch : ∀ n m : Nat, n + m = m + n := sorry
"""
server = Server()
sorries = server.load_sorry(root)
state1 = server.goal_tactic(sorries[1].goal_state, 0, "apply add_comm")
# Traceback (most recent call last):
#   File "<stdin>", line 1, in <module>
#   File "/home/agittis/miniconda3/envs/intern2/lib/python3.10/site-packages/pantograph/utils.py", line 16, in wrapper
#     return asyncio.run(func(*args, **kwargs))
#   File "/home/agittis/miniconda3/envs/intern2/lib/python3.10/asyncio/runners.py", line 44, in run
#     return loop.run_until_complete(main)
#   File "/home/agittis/miniconda3/envs/intern2/lib/python3.10/asyncio/base_events.py", line 649, in run_until_complete
#     return future.result()
#   File "/home/agittis/miniconda3/envs/intern2/lib/python3.10/site-packages/pantograph/server.py", line 279, in goal_tactic_async
#     raise TacticFailure(result)
# pantograph.server.TacticFailure: {'tacticErrors': ["unknown identifier 'add_comm'"]}
state1 = server.goal_tactic(sorries[1].goal_state, 0, "apply Nat.add_comm")
state1
# GoalState(state_id=2, goals=[], _sentinel=[0])

Is there another way to get open statements into pantograph's proof environment for a theorem?

[lenianiva]

Surround it with section ... end

[AG161]

That didn't seem to work. Here is what I tried:

Python 3.10.16 (main, Dec 11 2024, 16:24:50) [GCC 11.2.0] on linux
Type "help", "copyright", "credits" or "license" for more information.
>>> from pantograph import Server
>>> root = """
... section
... 
... open Nat
... 
... theorem add_comm_proved_formal_sketch : ∀ n m : Nat, n + m = m + n := sorry
... 
... end
... """
>>> server = Server()
>>> sorries = server.load_sorry(root)
>>> state1 = server.goal_tactic(sorries[2].goal_state, 0, "apply add_comm")
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "/home/agittis/miniconda3/envs/intern2/lib/python3.10/site-packages/pantograph/utils.py", line 16, in wrapper
    return asyncio.run(func(*args, **kwargs))
  File "/home/agittis/miniconda3/envs/intern2/lib/python3.10/asyncio/runners.py", line 44, in run
    return loop.run_until_complete(main)
  File "/home/agittis/miniconda3/envs/intern2/lib/python3.10/asyncio/base_events.py", line 649, in run_until_complete
    return future.result()
  File "/home/agittis/miniconda3/envs/intern2/lib/python3.10/site-packages/pantograph/server.py", line 279, in goal_tactic_async
    raise TacticFailure(result)
pantograph.server.TacticFailure: {'tacticErrors': ["unknown identifier 'add_comm'"]}
>>> state1 = server.goal_tactic(sorries[2].goal_state, 0, "apply Nat.add_comm")
>>> state1
GoalState(state_id=1, goals=[], _sentinel=[])
>>> 

Naming the section didn't make a difference either.