Add support for property-based testing #893
Open
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…ng module, along with examples
|
@jiribenes could you review this PR? |
jiribenes
requested changes
Mar 27, 2025
There was a problem hiding this comment.
Thanks for upstreaming, I'm very much looking forward to using the library :)
I have a few comments, mostly about how we can make the stdlib tests pass and how we enable LLVM to also use your testing library.
And I have a few questions — it's completely OK if you aren't sure about your answers to the open-ended questions, but I'm still interested in knowing your thoughts.
Let me know if you have any questions.
| resume(())} | ||
| else { | ||
| val duration = Duration::diff(startTime, bench::relativeTimestamp()) | ||
| do failureForall(name, successCounter, msg ++ "\n failed on input:\n 1. " ++ genericShow(x), duration) |
There was a problem hiding this comment.
This won't work on the LLVM backend because of the genericShow.
Instead, we need to have even more overloads of forall that take a { show: A => String } block parameter, which is later applied at this exact spot.
There was a problem hiding this comment.
I can try to change it, show would be just like in the lowermost assertEqual version, right?
def assertEqual[A](obtained: A, expected: A) { equals: (A, A) => Bool } { show: A => String }: Unit / { Assertion, Formatted } =
do assert(equals(obtained, expected), Formatted::tryEmit(Escape::RESET) ++ "Expected: ".dim ++ show(expected).green ++ "\n Obtained: ".dim ++ show(obtained).red)
Sadly I can only use the JS backend on my laptop, would it be okay for you to check it for the other backends once I committed the changes?
| def assert(condition, msg) = | ||
| if (condition) { | ||
| val duration = Duration::diff(startTime, bench::relativeTimestamp()) | ||
| do successExists(name, triedCounter, " example value:\n 1. " ++ genericShow(x), duration) |
There was a problem hiding this comment.
Same as in forall, in general, this needs to take a show parameter which is then applied on the tested value.
| def generate() = resume { | ||
| //[0, -1, 1, int.minVal, int.maxVal, -2, 2].each // This can reduce the need for shrinking by emitting common edge cases first | ||
| while (true) { | ||
| do emit(randomInt(-50, 50)) |
There was a problem hiding this comment.
This seems too small for "real" uses, can we bump this up to a lot more?
There was a problem hiding this comment.
sure, what would be a good range in your opinion? Is (-10000,10000) okay or still too small?
Comment on lines
+149
to
+157
| def shrink(v: Bool) = resume { | ||
| var out = v | ||
| if(v){ | ||
| out = false | ||
| }else { | ||
| out = true | ||
| } | ||
| do emit(out) | ||
| } |
There was a problem hiding this comment.
I don't get this. Is it just
Suggested change
| def shrink(v: Bool) = resume { | |
| var out = v | |
| if(v){ | |
| out = false | |
| }else { | |
| out = true | |
| } | |
| do emit(out) | |
| } | |
| def shrink(v: Bool) = resume { | |
| do emit(not(out)) | |
| } |
?
There was a problem hiding this comment.
yes it is, I'll change it :D It seems like some leftover code from an experiment, thanks for noticing!
| while (true) { | ||
| val string: String = collectString { | ||
| with boundary; | ||
| with limit[Char](randomInt(1, 20)) |
There was a problem hiding this comment.
Does this mean it never generates an empty string?
Also, this again seems like it generates outputs which are too small?
There was a problem hiding this comment.
That's right, it definitely needs improvements
I think most of the generators do, I'll change all of them with better ranges. Again, what do you think would be good ranges for real uses?
When allowing much bigger inputs it might be even more important to output common edge cases first and continue with the random values afterwards, wdyt?
To realize this it would be great to have an Int max/min value, but Effekt doesn't provide it yet, does it?
| while (true) { | ||
| val list = collectList[T]{ | ||
| with boundary; | ||
| with limit[T](randomInt(1, 10)) |
There was a problem hiding this comment.
see my notes for the string: does this ever generate an empty list? isn't the limit too small?
libraries/common/test.effekt
Outdated
Comment on lines
245
to
260
| def arbitraryList[T](len: Int) { body: => Unit/Generator[List[T]]} : Unit / Generator[T] = { | ||
| try body() with Generator[List[T]]{ | ||
| def generate() = resume { | ||
| while (true) { | ||
| val list = collectList[T]{ | ||
| with boundary; | ||
| with limit[T](len) | ||
| do generate[T]() | ||
| } | ||
| do emit(list) | ||
| } | ||
| } | ||
|
|
||
| def shrink(v: List[T]) = resume { <> } | ||
| } | ||
| } |
There was a problem hiding this comment.
I like the parametric version, but should it take a fixed length len: Int for each generated list or a maximum length max: Int which it then uses to generate a random list of size 0..max?
There was a problem hiding this comment.
It probably depends on the use case, but since the maximum length version provides more randomness I think it's better for the standard version, I'll change it
If users need the fixed length version, they can still make a custom generator
|
Bump @lenakaeufel: thanks again for trying to upstream the code. If needed, we can also take the PR over in order to ensure that it gets merged :) |
Hey, sorry for the silence, I've been quite busy over the past few weeks. I am planning to continue working on it, but sadly haven’t had the time yet :( |
5 tasks
This is a cleaned up version of my [effectful Pi-Day submission](https://gist.github.com/marvinborner/44236c67bbcfdaa184f37bc9b784a73f). Here I've decided to not use the lookup effect boxing for looking up bindings from the environment and used a hashmap instead.
Closes effekt-lang#846 This runs every test without optimization *in addition* to running them with optimization. While this is good for testing, we should change this once it's mergable so our CI doesn't take ~~twice as long~~ much longer. There are many new errors now. I've spent some time investigating and they generally fall into these two categories: - no block info (unsoundness in the optimizer) - unsupported LLVM feature (toplevel object definitions, reached hole (no LLVM FFI for extern definition)), which were somehow optimized away - valgrind error
Free the language server from Kiama and implement a test suite. Found some bugs while reimplementing, and I've confirmed all of them also exist in the old server. It should be on-par with the old implementation in terms of features and bugs. Depends on effekt-lang/kiama#9. **Differences to the old Server:** * Added unit test suite * New server runs single threaded and sequentially * Compile on `didChange`, by default * No Monto anymore, added a custom `$/effekt/publishIR` notification instead. **Implementation status:** * [x] `initialize` * [x] `shutdown` - not covered by unit tests - they cannot handle the process exit * [x] `exit` - not covered by unit tests - they cannot handle the process exit * [x] setTrace * [x] Diagnostics `afterCompilation` * [x] `didChange` * [x] `didOpen` * [x] `didSave` * [x] `didClose` * [ ] `hover` * [x] for symbols * [ ] 🐛 for holes: effekt-lang#549 * [ ] `documentSymbol` * [x] impl & test * [ ] 🐛 Fix spurious symbols at `(0, 0)`: effekt-lang#895 * [ ] `references` * [x] impl & test * [ ] 🐛 Fix not all references being returned (see test case): effekt-lang#896 * [x] `inlayHint` * [x] impl & test * [x] 🐛 inlayHints and hoverInfo sometimes return null (as in old implementation): * [x] inlayHints: effekt-lang#876 (fixed in effekt-lang#894) * [x] hoverInfo: effekt-lang#366 (**can't reproduce**) Note that the timing issue should be gone as we now run on `newSingleThreadExecutor` (which claims "Tasks are guaranteed to execute sequentially"), the caching issues have been fixed in effekt-lang#894. * [ ] `getCodeActions` * [x] port impl from old server * [ ] 🐛 impl doesn't even work in old server: effekt-lang#897 * [x] `definition` * [ ] `notebookDocument/*` * not implemented, student works on another branch * [ ] publish IR (`$/effekt/publishIR`), replacing Monto * [x] impl server and test (this PR) * [x] impl client (effekt-lang/effekt-vscode#63) * [ ] 🐛 many options (e.g. `target`) don't work because the server only runs the compiler frontend - same issue with old server Important questions to reviewers: * [x] `effekt/jvm/src/main/scala/effekt/KiamaUtils.scala` is MPL-licensed code from Kiama - what do we do with this? * I decided to move it to Kiama to be safe. --------- Co-authored-by: Marvin Borner <[email protected]>
…lang#906) Fixes effekt-lang#659, but not effekt-lang#667. I propose deferring fixing effekt-lang#667 to a later point in time, as it requires more design. What this PR does, for now, is to parenthesize boxed types when occurring in parameter or return type positions. For example, `(Int => Int at {}) => Int` instead of `Int => Int at {} => Int`, which, in my opinion, is utterly unreadable.
Fixes effekt-lang#760 by giving a more user-friendly error message like the following: <img width="711" alt="Screenshot 2025-03-28 at 12 02 58" src="https://github.com/user-attachments/assets/72ce83a1-29a0-4309-8718-6d965c74ae22" /> ## How it achieves this In a dynamic variable, it keeps a shadow-stack of what `Namer` is currently processing, checking on insertion. This check is moved into the processing of imports so the positioning information is correct.
We are running into problems where the versions used for development and for the CI are differing so much that we sometimes write code in development that is invalid in the CI. (See effekt-lang#877) I propose upping the Version to 18, which seems to be the Ubuntu standard Edit: the latest release is 20.1.0, so we are also not in unstable territory
Depends on effekt-lang#885 (mostly so we can actually express the unit test). I split `AnnotationsDB` into three separate databases which each tracks its own map. This allows us to properly distinguish types that should be annotated by their object identity (symbols, trees) and those that should be annotated by their value identity (sources). The new types are: * `TreeAnnotations`: key: `source.Tree`, object identity * `SourceAnnotations`: key: `kiama.util.Source`, value identity * `SymbolAnnotations`: key: `symbols.Symbol`, object identity Fixes effekt-lang#876. --------- Co-authored-by: Jonathan Brachthäuser <[email protected]>
Add binary search inspired by Jules Jacobs and Brent Yorgey. The interesting part is the missed optimisations --- if you comment out `150.findSqrtUpTo(100)`, you get _much_ better IR and JS code :) This could be made into a parametric benchmark: given N, search between 0 and N\*N for sqrt(N\*N).
Co-authored-by: Jonathan Brachthäuser <[email protected]>
Resolves effekt-lang#761 by allowing multiple patterns in a lambda case seperated by `,` like: ``` def foo[A,B,C](){ fn: (A, B) => C }: C = ... //... foo(){ case true, y => ... case x, y => ... } ``` ## Implementation This becomes a `Match` with multiple scrutinees, which is resolved in the pattern matching compiler. Typer checks that the clauses have the correct number of patterns (which will be assumed later).
This is a *continuation* of effekt-lang#851. We aim to fix the previously ignored tests that currently fail when being run without optimization. - [x] permute.effekt: segfault in resume->uniqueStack->copyStack since resume is called with an erased resumption stack - apparently from growing the stack via checkLimit - fixed e.g. by initial size = `shl 1, 8` instead of 7 - [x] multiple declarations (in JS) - `ascii_isalphanumeric.effekt`, `ascii_iswhitespace.effekt`, `parser.effekt`, `probabilistic.effekt` - fixed by "Do not contify under reset" (found out via bisect) - is still a problem though - [x] missing block info - [x] generator.effekt: by noting parameters for regions - [x] regions.effekt - [x] selfregion.effekt - [x] typeparametric.effekt: by returning garbage value (`undef`) - [x] issue842.effekt: by effekt-lang#872 - [x] issue861.effekt: by effekt-lang#872 - [x] top-level object definititions - if_control_effect.effekt, toplevel_objects.effekt, type_omission_op.effekt, higherorderobject.effekt, res_obj_boxed.effekt, effectfulobject.effekt --------- Co-authored-by: Philipp Schuster <[email protected]>
Closes effekt-lang#855 --------- Co-authored-by: Marvin Borner <[email protected]>
Fixes effekt-lang#709 by changing `resolveOverloadedFunction` to also check `BlockParam`s in scope. Notably, we only look up the first matching symbol, as we do not (yet?) support overloading on block parameters.
In conjunction with effekt-lang/effekt-website#85, this fixes all invalid URLs and file paths.
Reimplement various C utilities in LLVM and inline the functions inside of common effekt. This should allow LLVM to better optimize code containing these funtions, as the optimizer can see the actual implementation instead of guessing.
Currently, when encountering an error (e.g. through calling `Context.abort`) in the JSWeb backend, all encountered errors are discarded and a JS exception is thrown. All information is lost there, which leads to a singular (unhelpful) error message `Cannot compile interactive.effekt`. It would be more helpful for the user to see the cause. https://github.com/effekt-lang/effekt/blob/8abbff5c34d71f8d3396c9db4b75ad6fdb16a4f5/effekt/js/src/main/scala/effekt/LanguageServer.scala#L101-L112 In line 103 this exception is thrown. Notice that the following line attempt to catch a `FatalPhaseError`, however `mainOutputPath` is a string and thus not lazily evaluated. Furthermore, `Phase.apply` already catches `FatalPhaseError`s and converts them to `None`. Hence, the exception handler is never executed. Instead, we report all collected error messages. Before:  After: <img width="1254" alt="image" src="https://github.com/user-attachments/assets/5fabe8c4-5776-44ba-8fe8-7ecce575184a" /> (the increased resolution is not part of this PR)
General idea: instead of building
`name_123_109238_190238_109283019283_1092830192838019283` chains, what
if we use the automagic `fresh.next` to get just a darn fresh number?
This will limit the identifiers to stuff like `b_k2_123_10928310283`,
which is--at least to me--a pretty big improvement.
We use the full capabilities of a `Symbol`: it has a `name` (which is
really a `String`) and a fresh `id` that gets assigned lazily. Instead
of changing the name to be `${oldName}_${oldId}` and then putting a
fresh `id` on top of that (to get `${oldName}_${oldId}_${newId}`), we
just make a new `Symbol` with the same name, which forces a new,
_fresher_, `id`.
---------
Co-authored-by: Marcial Gaißert <[email protected]>
I think that the allocation here is not needed, so let's avoid it. Also adds more tests for the StringBuffer.
effekt-lang#941) After effekt-lang#938, the `RenamerTests` do not check that the names are actually unique. This adds assertions checking that every `Id` only occurs in one definition-like construct. (note that effekt-lang@4cf2371 is intentionally wrong to show it failing on shadowing :) )
…g#940) I don't know what the nested list is for, but we don't seem to use it anywhere. Therefore I'm removing the nesting and using mutable hashmaps: it's on a hot path! Renamer then goes from 2.4-3.4s to 0.6-0.4s :) [measured a few times via profiling] (for reference, before effekt-lang#938, it was somewhere between 3 and 4 seconds)
IntelliJ has a button for adding `@tailrec` wherever needed. So I clicked it. Let's see what happens now!
Substitutions are used multiple times but computed over and over again. This PR caches them until any modification happens. On my machine, this brings down typer from `1150ms` to `720ms` with ``` effekt --time text examples/casestudies/anf.effekt.md ``` This shaves of 25% of the total compile time, which is reduced from 2.5s to 2s.
…g#956) ## Enhance Reporting for Missing `do` Syntax in Effect Operations This pull request improves error messages for unresolved function calls in the presence of equally named effect operations, addressing issue [effekt-lang#950](effekt-lang#950). --- ## Summary This update enhances the info message in the `Namer` component of Effekt when an equally named effect operation exists but has not been invoked using the `do` syntax. It ensures the user is provided with a more descriptive information message, avoiding the generic `"Cannot find a function named _"`. --- ## Changes ### 1. **Improved Information in `Namer.scala`**: - Removed `lookupOverloaded` and with it the never issued information on fields and added `lookupOperation` to capture equally named effect operations the `resolveFunctionCallTarget` method. - When an equally named effect operation is found, an **information message** is provided to the user with the recommended syntax (`do {operationName}()`). ### 3. **Added Negative Tests**: - Introduced three new tests in `examples/neg/namer/issue950` to verify the following cases: - An info message is displayed when an effect operation is invoked without the `do` syntax. - The generic message is displayed when no valid function or operation matches the call. - Overloaded Effects all get captured by the `foreach` --- ## Example Behavior ### Before the Fix ```scala interface Greet { def sayHello(): Unit } def helloWorld() = try { sayHello() // [error] Cannot find a function named `sayHello`. } with Greet { def sayHello() = { println("Hello!"); resume(()) } } def main() = { helloWorld() // Generic error, not helpful } ``` ### After the Fix ```scala interface Greet { def sayHello(): Unit } def helloWorld() = try { sayHello() // [error] There is an equally named effect operation `sayHello` of interface `Greet`. Use syntax `do sayHello()` to call it. } with Greet { def sayHello() = { println("Hello!"); resume(()) } } def main() = { helloWorld() // Specific error with actionable advice } ``` --- ## Testing - **Negative Test 1**: Missing `do` for effect operation: - Confirms that invoking an effect operation without the `do` syntax triggers the improved error message. - **Negative Test 2**: Unresolved function call: - Ensures that the generic error message appears when no matches (operations, fields, or overloads) are found. - **Negative Test 3**: Overloaded effect operations: - Confirms that overloaded effect operations are all captured by the new foreach --------- Co-authored-by: Jiří Beneš <[email protected]>
Fixes effekt-lang#919 by adding a wellformedness check as suggested [here](effekt-lang#919 (comment)). Resulting error message: <img width="1272" alt="Screenshot 2025-04-25 at 14 27 57" src="https://github.com/user-attachments/assets/e81597a0-602e-4868-a5fd-7ecc1e4e3562" />
I was experimenting with making emitted function definitions `private` by default in llvm. This seemed to only reduce the code size of our *.opt.ll files, which might not even be wanted, because now all the unused/inlined function definitions are gone. Benchmarking this showed no improvement *except* for "examples/benchmarks/are_we_fast_yet/queens.effekt" which unexpectedly got 30% faster. Not sure what is going on
…ers & fix float ops on Chez (effekt-lang#966) Straightforward streaming randomness with an interface supporting both bytes-based PRNG and /dev/urandom.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This pull request is the result of my bachelor thesis, "Property Testing in Effekt". It extends the existing testing module by adding support for property-based testing (PBT), while maintaining full compatibility with the existing functionality.
🔧 Changes to
test.effekt:Generatoreffect to model stream-based generators for PBTInt,Bool)Testeffect with four new operations to capture PBT results:forallandexistsquantifiersforallandexistsin various forms:forall: one with implicit generator passing, and one with explicit🧪 Added PBT Example Files:
list_examples_pbt.effekt: A mixed test suite with unit and property-based tests, showcasing properties of some standard library list functionstree_examples_pbt.effekt: Demonstrates custom generators and property tests for the standard library’s tree-based map📌 Note on Shrinking:
Shrinking is not yet implemented, as it requires further research and design.
However, the thesis repository contains a prototype exploring a potential approach to shrinking.