The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi,

> 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.

Right, that's pretty much the question here:  Is it realistic for the
"axiom splitting" of libraries (in particular, everything shipped with
Coq itself, like Program and Psatz) to happen anytime soon or not?  I
agree with the overall tone here that this is the preferred solution,
but I fear that it could take "forever".  Changing coqchk to, for
example, restrict its attention to certain names (with support for
wildcards) is tempting because it would need less changes in the overall
ecosystem -- but it touches and complicates the TCB, and (as you said)
may discourage people from even going with the split.

What are people's feelings about doing such a split in the Coq standard
library?  (By which I mean everything shipped with Coq, including e.g.
Psatz.)  Since this is all about which names are exported where, I would
expect that one could add a compatibility flag which makes "Import
Psatz" turn into "Import PSatzWithAxioms" or so, so that old code
(compiled with the flag) would still work (and porting would be trivial,
just change the name of the module you import).
  I have made very little use of other Coq libraries, so I don't know
how many cases there are out there where axioms could be split.  The one
library using axioms that I checked out (Autosubst) needs these axioms
for pretty much all of its functionality, so there wouldn't be no split
anyway.

Kind regards,
Ralf