The Coq mailing list

["Ade Umut Huxtable" <tkdtezx AT mail.nu>]

Whether the split makes sense for a specific library is up to the maintainer 
to decide, also allocating manpower might stop it from happening (ignorig 
project forks).

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

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.


--- 
jonikelee AT gmail.com
 wrote:

From: Jonathan Leivent 
<jonikelee AT gmail.com>
To: 
tkdtezx AT mail.nu
Cc: 
coq-club AT inria.fr
Subject: Re: [Coq-Club] Axioms reported by coqchk
Date: Fri, 19 Aug 2016 14:46:55 -0400



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





_____________________________________________________________
mail now at http://www.mail.nu