Comments (9)
See also this set of notes on the topic; and FYI I have a prospective Honours student looking at working on this 😁
from crosshair.
This so cool. Let me know how I can help.
Starting out with it integrated on the CrossHair side makes sense to me, as it's far more experimental anyway. CrossHair will never detect 100% of cases, so even if we only handle basic cases, I'd be inclined to merge this kind of work :)
from crosshair.
Note: a very basic and slow integration now exists (see this post about it)!
Try it out with crosshair watch --analysis_kind=hypothesis <file.py>
The next steps to make this more effective include some refactoring on the hypothesis side; this issue in particular.
from crosshair.
@JinghanCode is looking at this now, with the work-in-progress over at JinghanCode#1 🎉
Overall plan: start by translating a subset of Hypothesis strategies into CrossHair constraints, in order to get a baseline for the more general "choice sequence"-based approach (see notes, above). It's unclear at this stage whether we'd want to ship this as part of Hypothesis or CrossHair - it's pretty sensitive to unstable/internal implementation details, and there are many many tests it can't handle - but we do expect to learn something useful 😁
from crosshair.
That's likely to consist of me pinging you for code review + advice on how to evaluate it in a few weeks-months, once the basics are working.
Great; reach out anytime, even if it's just for some help along the way. I've also set up regular CrossHair discussion time that's open to the public, here, on calendly. (but don't feel constrained to those days/hours)
My hesitation is because it's depending on the details of actually-for-real unstable implementation details of Hypothesis, which would make for a poor user experience over time. But I'm also keen to ship handling for the cases we can handle somewhere, and with your support a hypothesis[crosshair] extra could be pretty cool - right up to "we proved this always passes, skipping input generation" 😁
Got it. Yeah, it would be amazing to see this as a hypothesis extra. FWIW, if we do end up deciding to put this on the CrossHair side, I'm happy to make sure CrossHair stays compatible.
It makes sense to think about this as an experiment for now, but eventually it might be worth thinking about structuring the bridge logic in a way that is imaginable as part of the strategy interface. For instance, CrossHair would be perfectly happy with an ability to query arbitrary strategies for (1) a (possibly parameterized) type and (2) a post-processing function for mapping/filtering. (though 'm sure my mental model of a strategy is overly naive!)
from crosshair.
https://github.com/JinghanCode/Crosshair-Hypothesis/pull/1/files shows how far we got: based on some runtime introspection, we can analyse @given(...)
tests with st.integers(...)
- as well as one_of()
, .map()
, and .filter()
!
The challenge for future work is to investigate how this scales out to cover more strategies (e.g. st.lists()
), or to try plugging in at the lower-level conjecture
(choice-sequence) interface as we discussed here.
from crosshair.
This so cool. Let me know how I can help.
Will do! That's likely to consist of me pinging you for code review + advice on how to evaluate it in a few weeks-months, once the basics are working.
Starting out with it integrated on the CrossHair side makes sense to me, as it's far more experimental anyway. CrossHair will never detect 100% of cases, so even if we only handle basic cases, I'd be inclined to merge this kind of work :)
My hesitation is because it's depending on the details of actually-for-real unstable implementation details of Hypothesis, which would make for a poor user experience over time. But I'm also keen to ship handling for the cases we can handle somewhere, and with your support a hypothesis[crosshair]
extra could be pretty cool - right up to "we proved this always passes, skipping input generation" 😁
from crosshair.
@JinghanCode and @Zac-HD : how did this investigation go? Looks like you got somewhere with it, and I am very curious about your overall findings!
from crosshair.
Now when CrossHair finds a hypothesis counterexample, it's saved to the hypothesis database. That means even regular runs of hypothesis will try inputs that CrossHair has found! (via #185; thank you @Zac-HD !!)
from crosshair.
Related Issues (20)
- Unexpected counterexample when indexing a symbolic sequence by a object of unknown type
- Support annotated-types HOT 1
- Better error message when a file can't be imported HOT 1
- Check __return__ is not None
- Do not treat KeyboardInterrupt as an exception in code-under-analysis
- Some easy cases cannot be solved HOT 6
- Support atomic grouping and possessive quantifiers
- Support correct and compilable representation of enum values in the cover/pytest mode HOT 7
- Support pytest.raises Assertion / Exception match parameter when there is a message in exception HOT 1
- Produce the correct import statements for pytest output on cover command HOT 1
- CrossHair is missing symbolic support for `str.split` without arguments
- Support Python 3.12 HOT 1
- Implement true floating point semantics
- Unexpected checking results for functions with/without type annotations HOT 4
- Generic objects, when realized to strings, raise TypeError on concatenation.
- CrosshairInternal error raised when attempting to use symbolic integer as a function HOT 1
- Ensure all isinstance checks account for undecided types
- cover command error: (AttributeError("'AlgebraicNumRef' object has no attribute 'as_fraction'") HOT 2
- Unexpectedly long run times on a short example containing floats HOT 2
- Improve premature realization heuristics
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from crosshair.