The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 08/19/2016 02:11 PM, Ade Umut Huxtable wrote:
> I agree with Pierre-Marie Pédrot, it's not a tooling problem.
>
> Libraries should make an effort to offer (if that at all makes sense) an 
> axiom free subset of their features.
>
> Ade

How difficult would this be?  For instance, how difficult would it be 
for plugins like Psatz to do this?  Such a plugin may depend on the 
existence of axioms that it doesn't always use.  The issue is also with 
tactics - currently, it isn't possible to write a tactic that will use 
an axiom if it is Required, but still work in some cases otherwise.  The 
definition of the tactic will fail to compile merely because it mentions 
the axiom, regardless of the fact that it mentions the axiom on a branch 
that isn't always executed.  I've been playing with a workaround, but it 
requires that the module user to redefine some Ltac definitions at the 
point of use.

Alternatively, all axioms could be defined to be typeclass instances 
such that their conditional usage by tactics and plugins doesn't need to 
depend on their symbolic names (which was mentioned on another thread).  
Such a typeclass-based technique may be the best way to deal with 
modularity issues...

But, just in terms of compatibility and in the kinds and extent of 
rewritings of existing standard libraries and plugins one could expect 
in a reasonable time horizon from Coq developers and plugin developers, 
as well as the effect of the resulting changes on users - does asking 
for per-module axiom segregation make pragmatic sense?

-- Jonathan