search

EasyCrypt / easycrypt

EasyCrypt: Computer-Aided Cryptographic Proofs
MIT License
319 stars 49 forks source link

Add a deprecation mechanism #236

Open strub opened 2 years ago

chdoc commented 2 years ago

I would like to have at least two places to trigger a deprecation warning:

strub commented 2 years ago

For lemmas, operators, internal theories, it would be easy to add a deprecated keyword. For top-level theories, I am not sure what to do so that a user can mark the while file as deprecated.

chdoc commented 2 years ago

Would it be possible to add a command to mark the enclosing theory as deprecated and make deprecated theory ... (or whatever you envisioned) just syntax for opening a theory and invoking the deprecate command right after?

strub commented 2 years ago

Would it be possible to add a command to mark the enclosing theory as deprecated and make deprecated theory ... (or whatever you envisioned) just syntax for opening a theory and invoking the deprecate command right after?

Yes, this makes sense.

fdupress commented 2 years ago

For deprecating a whole file, an extension change could also do? .ecd

The warning part of the mechanism could also be used to deprecate tactics. (We don't need a source-level mechanism to mark tactics as deprecated.)

Do we want to support deprecating a particular clone of a non-deprecated theory? (In which case, we'll want deprecated clone ....)