The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Don't forget about the order of non-definition objects.  Definitions may be reorderable with each other, but they cannot be reordered across `Strategy` / `Opaque` / `Transparent` commands without potentially changing the performance of coqchk on the file from "instantaneous" to "longer than the lifetime of the universe".  Technically the order only matters when the opacity command is about a constant in the recursive dependencies of the constant being reordered, so you could still have a topological sort, but the computation may require arbitrary amounts of unfolding (a la Print Assumptions, though thankfully opaque proofs bodies wouldn't need to be fetched from disk), and this may be slow on large constants.

This is further complicated by the fact that modules must group not only their constants but also Ltac, notations, etc.  And furthermore plugins can declare arbitrary serializable data to be stored in the vo file, I believe, and can declare arbitrary code to be run on deserialization, IIRC.  And there's no way, AFAIK, to inspect the dependences of this data.  (Consider what would happen if a declared number notation were to be loaded before the constants it uses exist.). So probably any plug-in data objects would act as a reordering boundary.

Additionally, the nuances of what is and is not a reordering boundary could impact the correctness of the kernel, which seems like a recipe for worrisome complexity.

On Sun, Nov 27, 2022, 04:21 Clément Pit-Claudel <cpitclaudel AT gmail.com> wrote:

On 11/23/22 16:15, Abhishek Anand wrote:
> AFAIK, there is no way to distinguish the 2 versions via coqtop/coqc when the .vo file is imported in other files.

It probably doesn't matter, but…

   Print Module original.
   (* Module original := Struct Definition xx : nat. Definition yy : nat. End *)
   Print Module reversed.
   (* Module reversed := Struct Definition yy : nat. Definition xx : nat. End *)