How to compile modules using Creusot contracts?

[Lysxia]

Following the Quickstart in the Creusot guide, I created a src/lib.rs file with some Creusot contracts. cargo creusot succeeds, but cargo build fails because some features are not enabled (which cargo creusot enabled implicitly to succeed). If I enable the features explicitly:

#![feature(stmt_expr_attributes,proc_macro_hygiene)]

Then cargo creusot complains because the features are enabled twice.

One workaround is to enable the feature conditionally:

#![cfg_attr(not(creusot),feature(stmt_expr_attributes,proc_macro_hygiene))]

Am I missing something? Could Creusot not enable those features, or enable them only if they are not already enabled?

[xldenis]

Unfortunately, that's the best way I know of doing things, I suppose the alternative would be for creusot to not enable these features and instead just require all client projects to unconditionally enable them? I'm open to suggestions on this.

[Lysxia]

Yes, I think creusot should let users enable those features unconditionally.

#![feature(stmt_expr_attributes,proc_macro_hygiene)]

[jhjourdan]

I'd like a macro to generate these automatically each time we are using Creusot.

But here it is said that this is impossible:

https://users.rust-lang.org/t/how-to-generate-top-level-macro-calls-with-a-proc-macro/51142

Sad :'(

[xldenis]

The real solution is to just work to stablize these features :P

[jhjourdan]

I'm not confident that we will never use another unstable feature in the future.

[xldenis]

I'm not confident that we will never use another unstable feature in the future.

In our macros? That seems easier to guarantee, in the creusot compiler / contracts sure.