search

adampetcher / fcf

Foundational Cryptography Framework for machine-checked proofs of cryptography.
Other
48 stars 23 forks source link

#[export] instances and Hints #38

Closed andrew-appel closed 2 years ago

andrew-appel commented 2 years ago

Since Coq 8.13 (plus or minus), the Instance and Hint Resolve require a locality annotation, such as Global or Local or #[export]. Without the annotation, one gets a deprecation warning message. Here's an example from compiling FCF in Coq 8.15.1:

File ".\fcf/src/FCF/EqDec.v", line 387, characters 0-62:
Warning: The default value for instance locality is currently "local" in a      
section and "global" otherwise, but is scheduled to change in a future
release. For the time being, adding instances outside of sections without       
specifying an explicit locality attribute is therefore deprecated. It is        
recommended to use "export" whenever possible. Use the attributes #[local],     
#[global] and #[export] depending on your choice. For example: "#[export]       
Instance Foo : Bar := baz." [deprecated-instance-without-locality,deprecated]

For strict compatibility with previous FCF behavior, you would add Global before each such Instance or Hint. But I would suggest instead using #[export]. For clients that do Require Import, there will be no difference. Clients that do Require without Import will be affected. Anyway, one way or another I would like to stop seeing these deprecation messages.

adampetcher commented 2 years ago

Fixed in the latest commit. I set them all as #[export]. Anyone that runs into compatibility issues can use the coq_8_13 tag.