The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 08/19/2016 03:44 PM, Ade Umut Huxtable wrote:
> Whether the split makes sense for a specific library is up to the maintainer 
> to decide,

But, when talking about the standard library and standard plugins, it 
seems like the user base should have considerable say in this regard.

> also allocating manpower might stop it from happening (ignorig project forks).

I don't understand what you mean there.

> Without the library commiting to the axiomless subset, an update is more 
> likely to introduce actually used axioms in a user's development.

In the case when a lemma uses an axiom when there is an alternative 
axiom-less proof (say by using UIP when UIP_dec would suffice), I think 
such an unnecessary dependency on an axiom is a bug. Furthermore...

> It might be unrealistic to expect libraries to perform the split though, 
> since apparently not even the standard library follows this suggestion...
>
> So: adding the feature "Print Module Assumptons X." to coqchk (or another 
> tool) would be nice, but without library owner cooperation, users are at risk of 
> suprise axioming. Also, having such a tool further lowers the motivation on libraries 
> to actually bother with splitting.

... having the Print Module Assumptions X - or a checked variant that 
would be something like Assert Module Assumptions X [assump1, assump2 
...], or via a coqchk-like utility - when used by the standard library 
itself would ease the maintenance of any such segregation of axioms.  
The Assert mechanism would also provide users with an easy way to view 
the assumption dependencies.

Still, despite your argument, it seems that the difficulties of dealing 
with compatibility weigh quite heavily on Coq developers to the point 
that such module splitting seems unlikely.

However, at least with the standard library, since all of the Coq script 
source is available and should be understandable to Coq users, the users 
that really care about segregating axioms can do so by making their own 
copies of the standard library modules impacted.  This is less true of 
plugins like Program mode and Psatz, where Coq users that depend on 
those plugins are far less likely to understand their implementation to 
the point of being able to do the segregation (and subsequent 
maintenance) themselves.

-- Jonathan