Skip to content

Enable link-time optimisation for release builds - #1009

Merged
MichaelRawson merged 2 commits into
vprover:masterfrom
Dragon-Hatcher:lto-release
Oct 6, 2026
Merged

MichaelRawson merged 2 commits into
vprover:masterfrom
Dragon-Hatcher:lto-release

Conversation

@Dragon-Hatcher

@Dragon-Hatcher Dragon-Hatcher commented Oct 4, 2026 •

Copy link
Copy Markdown
Contributor

Release builds now use link-time optimisation when the toolchain supports it, checked with CMake's check_ipo_supported.

Results

master (af03e15) built with -DCMAKE_BUILD_TYPE=Release, with and without this change, measured with -sa discount -p off -t 30 on Apple clang, arm64:

instructions, median instructions, total memory, median
133 random TPTP problems −7.5% −5.2% −3%

Release builds use link-time optimisation where the toolchain supports it
(check_ipo_supported); elsewhere the build is unchanged.

Co-Authored-By: Claude Opus 5.5 (1M context) <[email protected]>
@MichaelRawson

Copy link
Copy Markdown
Contributor

It used to be that this took forever to link on Linux, which was why we didn't have it. I'll check on my machine again...

@MichaelRawson

Copy link
Copy Markdown
Contributor

Alright, the future is now! My (relatively ancient Debian) clang++ can IPO-link Vampire reasonably quickly.

Comment thread CMakeLists.txt Outdated
@MichaelRawson
MichaelRawson merged commit f2291d1 into vprover:master Oct 6, 2026
1 check passed
@MichaelRawson

Copy link
Copy Markdown
Contributor

I believe that IPO is doing something positive. However, it's worth noting (thanks to @quickbeam123) that "fewer instructions" could mean:

  • We needed fewer instructions to solve a problem (good).
  • On problems which timeout, we burned fewer instructions per unit time (bad).

🤷

@Dragon-Hatcher

Copy link
Copy Markdown
Contributor Author

Good to keep in mind, but these were all problems Vampire solves.

@easychair

easychair commented Oct 6, 2026 via email

Copy link
Copy Markdown
Contributor

@MichaelRawson

Copy link
Copy Markdown
Contributor

DISCOUNT.

@easychair

easychair commented Oct 6, 2026 via email

Copy link
Copy Markdown
Contributor

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