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

[DRAFT] Automatic tracking of statistics after each commit #479

Draft
wants to merge 1 commit into
base: main
Choose a base branch
from
Draft

[DRAFT] Automatic tracking of statistics after each commit #479

wants to merge 1 commit into from

Conversation

carlini
Copy link
Contributor

@carlini carlini commented Oct 9, 2024

This PR is the first step to log data about how far the project has progressed over time. Right now I've run the extract_implications --hist tool for every commit from when the tool was created until this morning. I'll start back-filling the remaining commits by cherry-picking the extraction tool into the past.

Once I've completed the backfill, I'll try to get the CI to automatically add one of these files with each PR. I have an idea for how to do this but it'll take a bit of work. and will discuss this on issue #171.

@carlini carlini marked this pull request as draft October 9, 2024 23:47
@carlini carlini mentioned this pull request Oct 9, 2024
Open
@avi-levy
Copy link
Contributor

Out of curiosity I went through the stats files checked in on the PR and I noticed that 20 of them showed a usage message rather than displaying statistics, is this behavior intentional?

  • data/stat_history/12ceca3.txt
  • data/stat_history/16ecfa0.txt
  • data/stat_history/216d377.txt
  • data/stat_history/2ddfb96.txt
  • data/stat_history/3294f5e.txt
  • data/stat_history/551d1ac.txt
  • data/stat_history/55fd2de.txt
  • data/stat_history/858d43a.txt
  • data/stat_history/8b4ecbd.txt
  • data/stat_history/8bed986.txt
  • data/stat_history/9b898f5.txt
  • data/stat_history/a06c30b.txt
  • data/stat_history/b8efafa.txt
  • data/stat_history/bf6c691.txt
  • data/stat_history/c3bf4ac.txt
  • data/stat_history/c5a903f.txt
  • data/stat_history/f5378ff.txt
  • data/stat_history/f91b4f2.txt
  • data/stat_history/fe88e4f.txt
  • data/stat_history/fe8966e.txt

@carlini
Copy link
Contributor Author

carlini commented Oct 10, 2024

Ah no. It looks the file existed at that point, but didn't support --hist. I'll backport that too.

@euprunin
Copy link
Contributor

This looks excellent!

I wrote a parser and got the following numbers:

% scripts/explore_magma_history.py
2024-10-02  Dashboard status (3b11388): 27,803 explicitly proven, 5,294,943 implicitly proven, 829,607 explicitly disproven, 12,994,633 implicitly disproven, 1,625,249 open
2024-10-03  Dashboard status (a03ffcb): 28,263 explicitly proven, 5,457,962 implicitly proven, 13,842,866 explicitly disproven, 3,522 implicitly disproven, 2,729,196 open
2024-10-04  Dashboard status (dac82d9): 31,023 explicitly proven, 8,151,818 implicitly proven, 605,854 explicitly disproven, 13,243,426 implicitly disproven, 29,688 open
2024-10-05  Dashboard status (6b0de50): 31,023 explicitly proven, 8,151,818 implicitly proven, 581,647 explicitly disproven, 13,275,912 implicitly disproven, 21,409 open
2024-10-06  Dashboard status (679a681): 31,019 explicitly proven, 8,147,260 implicitly proven, 582,094 explicitly disproven, 13,272,262 implicitly disproven, 1,001 open
2024-10-07  Dashboard status (851d3ec): 31,019 explicitly proven, 8,147,260 implicitly proven, 582,096 explicitly disproven, 13,272,262 implicitly disproven, 999 open

Does everything look accurate?

@teorth
Copy link
Owner

teorth commented Oct 11, 2024

It's strange that the number of open problems increased from 10-02 to 10-03... possibly some flaw in the transitive closure algorithm?

@euprunin
Copy link
Contributor

euprunin commented Oct 12, 2024 •
edited
Loading

Yes, something seems off with the first entries.

Here is the underlying data for the corresponding commits:

% cat data/stat_history/3b11388.txt | tr "\n" " "
{"explicit_proof_true": 27803, "implicit_proof_true": 5294943, "explicit_conjecture_true": 38938, "implicit_conjecture_true": 1222463, "unknown": 2826, "implicit_conjecture_false": 1542808, "explicit_conjecture_false": 79615, "implicit_proof_false": 12994633, "explicit_proof_false": 829607 }
% cat data/stat_history/a03ffcb.txt | tr "\n" " "
{"explicit_proof_true": 28263, "implicit_proof_true": 5457962, "unknown": 2729196, "implicit_proof_false": 3522, "explicit_proof_false": 13842866
% cat data/stat_history/dac82d9.txt | tr "\n" " "
{"unknown": 29688,  "implicit_proof_true": 8151818,  "implicit_proof_false": 13243426,  "explicit_proof_true": 31023,  "explicit_proof_false": 605854}

The later entries -- such as 2024-10-06 Dashboard status (679a681): 31,019 explicitly proven, 8,147,260 implicitly proven, 582,094 explicitly disproven, 13,272,262 implicitly disproven, 1,001 open -- seem to align with the manually recorded numbers, correct?

@euprunin
Copy link
Contributor

I'm really excited about this PR, and I’d love to build tooling on top of it. What’s still left to be done?

@euprunin
Copy link
Contributor

Hey @carlini, feel free to reach out if you'd like any help getting this PR ready for merging! I'd like to see it in main.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@carlini @avi-levy @euprunin @teorth