KeyError when raising ServerError

[sorgfresser]

It seems that there is not always a desc key present if the result from Pantograph is an error.
For example I managed to produce the following json

{'error': 'timeout',
'message': "Timeout exceeded.\n<pexpect.pty_spawn.spawn object at 0x154b25f72390>\ncommand: PyPantograph/pantograph/pantograph-repl\nargs: [b'PyPantograph/pantograph/pantograph-repl', b'Mathlib', b'--maxHeartbeats=0', b'--maxRecDepth=100000']\nbuffer (last 100 chars): ''\nbefore (last 100 chars): ''\nafter: <class 'pexpect.exceptions.TIMEOUT'>\nmatch: None\nmatch_index: None\nexitstatus: None\nflag_eof: False\npid: 1032192\nchild_fd: 5\nclosed: False\ntimeout: 120\ndelimiter: <class 'pexpect.exceptions.EOF'>\nlogfile: None\nlogfile_read: None\nlogfile_send: None\nmaxread: 1000000\nignorecase: False\nsearchwindowsize: None\ndelaybeforesend: 0.05\ndelayafterclose: 0.1\ndelayafterterminate: 0.1\nsearcher: searcher_re:\n    0: re.compile('\\r\\n')\n    1: EOF"}

which raised a KeyError when trying to raise the ServerError in tactic_invocations because the desc key is missing.

[lenianiva]

This seems to be a problem of pexpect

[lenianiva]

Should we lengthen the timeout?

[sorgfresser]

Increasing the timeout was my workaround so far, yes.
Though I am not sure there is a perfect solution for the timeout. Parametrizing the timeout might be useful.

[lenianiva]

Increasing the timeout was my workaround so far, yes. Though I am not sure there is a perfect solution for the timeout. Parametrizing the timeout might be useful.

The timeout's already parameterized https://github.com/lenianiva/PyPantograph/blob/309975657a1abef2b7a8a4e901da8874ed5ddd43/pantograph/server.py#L105

I don't want the timeout to be endless since if there's some bug or malformed tactic in Lean that hangs the system (nothing's preventing someone from writing one), then we must terminate the server process, but on the other hand not being able to run a IO-like monad with a timeout is a known limitation in Lean 4

[sorgfresser]

Increasing the timeout was my workaround so far, yes. Though I am not sure there is a perfect solution for the timeout. Parametrizing the timeout might be useful.

The timeout's already parameterized

https://github.com/lenianiva/PyPantograph/blob/309975657a1abef2b7a8a4e901da8874ed5ddd43/pantograph/server.py#L105

I don't want the timeout to be endless since if there's some bug or malformed tactic in Lean that hangs the system (nothing's preventing someone from writing one), then we must terminate the server process, but on the other hand not being able to run a IO-like monad with a timeout is a known limitation in Lean 4

There are many reasons why the timeout shouldn't be endless. Since it is already parametrized, I'll close this issue for now. Simply increasing the timeout works. Nonetheless, the underlying KeyError raised within PyPantograph because the desc key was missing might not be ideal, but is certainly not a major issue.