Skip to content

Conversation

@tanyongkiam
Copy link
Contributor

Work done by @dnezam

@dnezam
Copy link
Contributor

dnezam commented Oct 23, 2025

The harder fixes are courteousy of @tanyongkiam :)

Judging by #345 , we already suspected that the simplifier could cause bad performance. What I observed in TextIOProof was that some CFML tactic invocations spent an overwhelming amount of time in the simplifier. The "fix" was to use a "weaker" simplifier (e.g., something like srw_ss() or std_ss, or just rewrite_tac) and to tweak other parts of the tactics to get closer to the original result.

I sadly didn't record a before and after, but I think the speed up is something like going 30min to 10min for TextIOProof.

@ordinarymath
Copy link
Contributor

I think it was 30 mins roughly before I did the lift out REWR_CONV _ calls in the arith decision procedures and it got to slightly more than 20 mins.

@tanyongkiam tanyongkiam merged commit 1efe1f5 into master Oct 24, 2025
1 check passed
@tanyongkiam tanyongkiam deleted the faster-textioproof branch October 24, 2025 02:59
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