Arne Keller

One Step Simplifier: optimizations and new rules

2

This PR fixes #3248 and supersedes #3256 and #3257 by optimizing the One Step Simplifier in several ways. See the commits in this branch for details. Additionally, the following rules...

OSS: extremely bad replaceKnown performance

11

## Description Automated proof search, replaceKnown accounts for 43% of *all* CPU time: (the view below is zoomed in)  As far as I can tell, almost no replace_known_left /...

Origin Tracking slows down proof loading by up to 20%

1

## Description Loading a proof with origin tracking enabled can take up to 20% more time. ## Reproducible Depends on the proof, I guess. ### Steps to reproduce 1. Enable...

Font scaling issues

2

Tracking issue for *all* font scaling bugs. ## Description Changing the global font factor produces some weird artifacts. - [ ] Icon size does not adapt - [ ] Settings...

## Description As far as I can tell, it is not possible to express `int::seqGet` in a specification. `(int) \dl_seqGet` (or `(int)s[i]`) results in a moduloInt:  I have implemented...

StackOverflowError when searching in large sequent

1

## Description When searching in a large sequent, a StackOverflowError is printed to stderr. ``` Exception in thread "AWT-EventQueue-0" java.lang.StackOverflowError at java.base/java.util.regex.Pattern$Slice.match(Pattern.java:4088) at java.base/java.util.regex.Pattern$BmpCharPropertyGreedy.match(Pattern.java:4329) at java.base/java.util.regex.Pattern$Slice.match(Pattern.java:4088) at java.base/java.util.regex.Pattern$BmpCharPropertyGreedy.match(Pattern.java:4329) at java.base/java.util.regex.Pattern$Slice.match(Pattern.java:4088)...