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.

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

Cache invariants, color PASS/FAIL/[assumed], & syntax definitions #64

Open
wants to merge 9 commits into
base: master
Choose a base branch
from

Conversation

maxvonhippel
Copy link

@maxvonhippel maxvonhippel commented Jun 17, 2022

This pull request makes the following changes.

  1. Adds an optional database parameter. Setting database=my-file.txt tells the code to use my-file.txt as a data-base. The database works like a cache of failed SMT formulae, namely, failed negations of invariants or assertions. The idea is to achieve a speed-up by caching computations done when checking the model before you added or removed an invariant, sort of like how in Coq some portion of your proof will be green and won't need to be re-evaluated just to check the next portion you write.
  2. Colors PASS green, FAIL red, and [assumed] blue (will behave slightly differently depending on your terminal theme). This improves overall legibility.

found-in-db

  1. Includes some minor linting in setup.py, as well as the requirement that you use Python 2.x as the code simply is not Python 3 compatible.
  2. Rolls in changes from another PR to add some syntax highlighting, in addition to syntax highlighting for sublime text that I authored.

@maxvonhippel
Copy link
Author

Here is how [assumed] looks:
assumed

@maxvonhippel
Copy link
Author

Example contents of my-database-file.txt:

-1622833400573599434
-5789786322462225471
-2650329083325368840
2711453712209863790
-4444313916419122133
-7296276615417619981
4881745331986217060
6250922562833032095
-254541914791903277

@maxvonhippel
Copy link
Author

Orthogonally, I'd like to mention that the setup.py does not correctly install the scripts on my machine (Linux Mint Debian, XPS 13 with Intel CPU). It defaults to the wrong Python. But if I create aliases, e.g.

alias ivy_check="python2 ~/projects/research/open-source-contributions/ivy/ivy/ivy_check.py"

... then everything works correctly.

@maxvonhippel
Copy link
Author

maxvonhippel commented Jun 17, 2022

Here is how FAIL looks.

FAIL

@maxvonhippel
Copy link
Author

I've rolled this other PR into mine, per our conversation @kenmcmil , so all these changes can be accepted at once. I'll make a few more changes that we discussed before this PR should be merged.

@maxvonhippel
Copy link
Author

The "PASS PASS" issue we observed wasn't a bug, I just pasted the word PASS again on accident, so we can ignore that.

@maxvonhippel
Copy link
Author

@kenmcmil you also mentioned maybe we should lock the file before writing/reading and unlock after. I'm not sure how best to do this, but will look into it some more.

@maxvonhippel maxvonhippel changed the title Cache invariants & color PASS/FAIL/[assumed] Cache invariants, color PASS/FAIL/[assumed], & syntax definitions Jun 23, 2022
@maxvonhippel
Copy link
Author

To be clear the lock feature is implemented. This is ready to be merged.

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.

1 participant