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

chore: polish bv_bench #844

Merged
merged 9 commits into from
Nov 14, 2024
Merged

chore: polish bv_bench #844

merged 9 commits into from
Nov 14, 2024

Commits on Nov 14, 2024

  1. feat: add bv_bench

    @tobiasgrosser
    tobiasgrosser committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    f5ce558 View commit details
    Browse the repository at this point in the history

  2. run

    @tobiasgrosser
    tobiasgrosser committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    d593e85 View commit details
    Browse the repository at this point in the history

  3. feat: collect data from hacker's delight in symbolic mode, and add da… 

    …ta to paper (#842)

This uses the previously built `tac_bench` infra to create a CSV file of
all the runs, and writes it down into

opencompl/paper-lean-bitvectors@9458bd7

Regrettably, I don't know of any easy way to get the theorem name, and
for whatever reason, the `logInfo` does not seem to prompt lean into
printing the filename / line number. If we want, we can consider using
something like `logWarning` and even more hackery, but I'm totally
unsure this is worth it.
    @bollu @tobiasgrosser
    bollu authored and tobiasgrosser committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    518af3b View commit details
    Browse the repository at this point in the history

  4. WIP

    @tobiasgrosser
    tobiasgrosser committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    04af632 View commit details
    Browse the repository at this point in the history

  5. Set all goals

    @tobiasgrosser
    tobiasgrosser committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    197c149 View commit details
    Browse the repository at this point in the history

  6. WIP

    @tobiasgrosser
    tobiasgrosser committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    d27a489 View commit details
    Browse the repository at this point in the history

  7. measure symbolic data on bitvectors

    @tobiasgrosser
    tobiasgrosser committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    dbcadc2 View commit details
    Browse the repository at this point in the history

  8. update data

    @tobiasgrosser
    tobiasgrosser committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    51f66dc View commit details
    Browse the repository at this point in the history

  9. Update SSA/Projects/InstCombine/HackersDelight/ch2_1DeMorgan.lean

    @tobiasgrosser
    tobiasgrosser authored Nov 14, 2024
    Configuration menu
    Copy the full SHA
    a9eb3ce View commit details
    Browse the repository at this point in the history