The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Jonathan, Dear Coq Users,

> I tried this typeclasses replacement of axioms in part of a development
> I have that contains its own axiom.  It requires a bit more care and
> feeding than I anticipated, but there do seem to be workarounds for the
> various issues that arise ...

Another issue is that it makes things more complicated, and I am not sure if 
the only purpose of this complexity is compatibility. New users of Coq at 
some point have to understand all this complexity. Some of the complexity is 
inherent and cannot be avoided, but some of the complexities of the Coq 
library are not.

For solving compatibility issues, I would think that at some point it makes 
sense to have major Coq library versions, which are not required to be 
compatible. Most longer living libraries/systems do this, like GTK, Qt, 
Python, .... There is a certain time where both libraries are maintained, but 
at some point the old major versions are deprecated (like GTK 1, Qt 3, Python 
1, ...). Also Coq 8.4 and 8.5 are not fully compatible, and I think these 
incompatibilities result in much more difficulties than manually changing 
Require statements to a scheme which makes Axiom usage more explicit.

Of cause it is work to maintain two versions of a library. But it is also 
work to support legacy in one version - and sometimes and makes it very 
difficult to do improvements. Also I would think that the effort of bug fix 
merging, usually the largest effort in maintaining two versions of a library, 
should be close to zero for Coq libraries ;-)

I still think that usage of axioms should be made visible at Require. This 
could be done by naming conventions or maybe by an extension to Require that 
importing libraries with Axioms requires an additional keyword (Require 
Axioms) and maybe also by some mechanism which forces users of a library to 
confirm that they are requiring certain other modules with a module. This is 
what I meant with the "Require Check" in my previous post, but of cause it 
couldn't work that way. What might work is that Require Check X works like a 
normal Require X, but if a module Y with a Require Check X is required, one 
is forced to write something like "Require Y with X". The "with" part must 
list all "Require Check" modules in Y (recursively). Of cause one can have an 
option to disable this check.

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928