Skip to content

Conversation

@augustepoiroux
Copy link
Contributor

@augustepoiroux augustepoiroux commented Apr 22, 2025

Extend all commands with a timeout attribute.
When the timeout is reached, the REPL attempts to cancel the command and returns a timeout error. Interaction with the REPL can be resumed with new commands.

@augustepoiroux augustepoiroux changed the title Implement timeout option Implement soft timeout option Apr 24, 2025
@kim-em
Copy link
Contributor

kim-em commented May 1, 2025

Let's check that the test suite passes with the default timeout set to some long value.

@kim-em kim-em marked this pull request as draft May 1, 2025 15:31
@augustepoiroux augustepoiroux force-pushed the timeout branch 2 times, most recently from b6b6514 to 5abeb58 Compare July 4, 2025 10:22
@Kripner
Copy link

Kripner commented Dec 17, 2025

This feature is critical for automated theorem proving. Is there anything blocking the merge?
The test outputs are expired, so I can't see them now, but I tested the timeout logic and it seems to work.

@augustepoiroux
Copy link
Contributor Author

augustepoiroux commented Dec 18, 2025

Hey @Kripner!
I rebased the code on the latest main changes.
From what I remember, I was facing the following issues:

  • I am using a task with IO.sleep for timeout measurement. It seems that they are not cancelled until IO.sleep terminates. This has the side effect of accumulating memory overhead when sending lots of requests in a short amount of time.
  • The long_kernel_check.in test does not pass, i.e. my implementation of timeout is not working in that case.

I don't have enough bandwidth to work on this at the moment, but if you want to look into that, feel free to update this PR!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants