Romain Ruetschi comments

Results 161 comments of


                                            Romain Ruetschi

Add clippy to Travis and remove unnecessary code

@nvesely Agreed.

Make gf256 it's own crate

We discussed that with @FredericJacobs, but IIRC we decided against it because we felt it would be hard to provide an implementation which would suit most use cases, and didn't...

Release version 0.3.0

Could someone look into build/CI issues with #74? I won't have time to get to it this week myself, but can take care of releasing 0.3.0 once it's merged. Otherwise...

Build failure when added as a dependency

Ouch, sorry about that, and thanks for the report! I have just released version 0.2.2 which restricts `protobuf` to >=1.4 and

Crash and failure to infer measure for type class

@rjraya Output when `MeasureInference` crashes: https://gist.github.com/romac/19223f12275e3efdd675f861d6ca90a9#file-crash-txt Output when `MeasureInference` passes: https://gist.github.com/romac/19223f12275e3efdd675f861d6ca90a9#file-pass-txt

Mutable fields in traits cannot have a default value when using var inside @extern class

You can use `@ignore` to leave out a definition (class, object, method, function) entirely.

ListSet implementation.

Looks like the build is stuck even though all tests passed.

Support for breakable and break (Was: Missing dependencies for breakable, break)

I am afraid I don't see a way to support such code without rewriting it at the moment. There might be a way to define alternatives to `breakable` and `break`...

Replace VC cache backend with embedded database

For large projects, where the cache can easily grow over 2GB, the performance of the current caching backend really suffers and has quite an impact on overall verification time (5-10s...

Replace VC cache backend with embedded database

We won't go with SwayDB [because of its license](https://github.com/epfl-lara/stainless/pull/1071#issuecomment-848619933), so we need to find another embedded database with support for persistent sets.