Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Better factoring of the search procedure #30

Open
5 tasks
LasseBlaauwbroek opened this issue Aug 5, 2021 · 0 comments
Open
5 tasks

Better factoring of the search procedure #30

LasseBlaauwbroek opened this issue Aug 5, 2021 · 0 comments

Comments

@LasseBlaauwbroek
Copy link
Member

  • Module to check for cycles and tactics doing the same thing (this will probably require hash-consing proof states)
  • Add a variable timeout for tactics (the timeout can be learned
  • Port the search procedure to Ltac2, so that it can be modified by end-users
  • Fix iterative deepening for cases where very few tactics apply
  • Attempt to make a more fail-safe contract for search procedure plugins. Possibly use msplit if this is fast enough.
LasseBlaauwbroek added a commit that referenced this issue Jan 27, 2022
@LasseBlaauwbroek
Make iterative deepening depend on number of tactics processed
6ae4ae7 
This instead of the previous behavior of depth, which could lead to quadratic
behavior for simple but long proofs.

This solves point 4 of issue #30
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@LasseBlaauwbroek