Stream: Coq users

Topic: Unqualified names and order of Imports

Pierre Rousselin (Oct 31 2023 at 09:13):

Sometimes the order of the Imports matters a lot (the latest Import takes precedence if there are conflicts between unqualified names). This makes things very hard to debug. Is there a Warning one can set to detect these situations?

Pierre Roux (Oct 31 2023 at 10:23):

No warning but maybe some good practices:

• always load your own code (the library you are currently developping) last, so that none of your dependency can shadow one of your own definition if they happen to add one with the same name
• always load things in the same order (and I tend to use something close from a topological order of the file dependencies)

Karl Palmskog (Oct 31 2023 at 10:29):

I also think library authors should provide explicit recommended "export files" that Require Export all reasonable things in the right order. The canonical example is all_ssreflect (and friends) in MathComp, and another example is Stdpp's prelude.

Karl Palmskog (Oct 31 2023 at 10:31):

... and users obviously need to know they should use these "export files" whenever possible

Last updated: Oct 13 2024 at 01:02 UTC