Accelerated Analysis

[Tragicus]

Motivation for this change

There are a few lines that take a long time to compile (up to 12s). This PR takes every line that takes above 1s to compile and that is not an import or an HB command and rewrites it in less than a second (when I could). This saves overall 7% of the compilation time (with most of the time save (-29%) in lebesgue_integral.v).

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[Tragicus]

@CohenCyril mentioned that integral should probably be locked. I tried something but did not observe any time save on the slow lines a was looking at (the set of which is obviously not empty), so I gave up.
EDIT: I think I am misremembering and it is funpos and funneg that I was supposed to lock, otherwise the unification of \int[mu]_(x in D) f1^\+ x with \int[mu]_(x in D) f1^\- x obviously goes under the lock.

[Tragicus]

I am not convinced that we want all the changes, I can add the time saved be each change if this helps the decision making.

[Tragicus]

Fun fact: ~16% of the total compilation time is spent on HB commands and ~27% is spent importing things.

[zstone1]

Thank you for doing this! Happy to see these improvements