search

dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.93k stars 262 forks source link

Find a way for DafnyWrittenCodeGenerators to report unsupported features from the Dafny side #5714

Open robin-aws opened 3 months ago

robin-aws commented 3 months ago

The DafnyCodeGenerator class will throw UnsupportedFeatureExceptions when it hits Features it doesn't support, which lets it opt out of certain tests in the suite as long as those unsupported features are documented. The Dafny code implementing the rest of the compilation, however, can't throw such exceptions, and the RustCodeGenerator (i.e. Dafny-compiler-rust.dfy) currently inserts code comments for unsupported things instead.

It looks like if the errors use the UnsupportedFeatureException.MessagePrefix this should just work, but I haven't tried it.

MikaelMayer commented 2 months ago

The Rust code generator wrapping the dafny code will throw an exception if an error is detected in Dafny, and the option --emit-uncompilable-code is not set

https://github.com/dafny-lang/dafny/pull/5613/files#diff-f5f8b8bdbe3722e2a630eeb3d23bc1580913068b49bff942cae2223ee846029dR21

Does that solve the issue?

MikaelMayer commented 2 months ago

Is the message above sufficient to consider the issue as already solved?