Module Dumpglob

This file implements the Coq's .glob file format, which provides information about the objects that are defined and referenced from a Coq file.

The .glob file format is notably used by coqdoc and coq2html to generate links and other documentation meta-data.

Note that we consider this format a legacy one, and no stability guarantees are provided as of today, as we search to replace this format with a more structured and strongly-typed API.

However, we do provide up to date documentation about the format of .glob files below.

The .glob file format

.glob files contain a header, and then a list of entries, with one line per entry.

.glob header

The header consists of two lines:

DIGEST: %md5sum_of_file F%modpath

where %modpath is the fully-qualified module name of the library that the .glob file refers to. %md5sum_of_file may be NO if -dump-glob file was used.

.glob entries

There are 2 kinds of .glob entries:

%kind %bc:%ec %secpath %name

where %kind is one of {ax,def,coe,subclass,canonstruc,ex,scheme,proj,inst,meth,defax,prfax,thm,prim,class,var,indrec,rec,corec,ind,variant,coind,constr,not,binder,lib,mod,modtype}, meaning:

  1. ax Axiom, Parameter or Variable(s), Hypothes,es, Context outside any section
  2. def Definition
  3. coe Coertion
  4. thm Theorem
  5. subclass Sub Class
  6. canonstruc Canonical Declaration
  7. ex Example
  8. scheme Scheme
  9. class Class declaration
  10. proj Projection from a structure
  11. inst Instance
  12. meth Class Method
  13. defax Definitional assumption
  14. prfax Logical assumption
  15. prim Primitive
  16. var section Variable reference (Variable,s, Hypothes,es, Context)
  17. indrec Inductive
  18. rec Inductive (variant)
  19. corec Coinductive
  20. ind Record
  21. variant Record (variant)
  22. coind Coinductive Record
  23. constr Constructor
  24. not Notation
  25. binder Binder
  26. lib Require
  27. mod Module Reference (Import, Module start / end)
  28. modtype Module Type

%bc and %ec are respectively the start and end byte locations in the file (0-indexed), multiple entries can share the same %bc and %ec %secpath the section path (or <> if no section path) and %name the name of the defined object, or also <> in where no name applies.

Section paths are ...

  1. In the case of notations, %name is encoded as :entry:scope:notation_key where _ is used to replace spaces in the notation key, %entry is left empty if the notation entry is constr, and similarly %scope is empty if the corresponding notation has no associated scope.
  1. For binding variables, :number is added to distinguish uniquely different binding variables of the same name in a file.

R%bc:%ec %filepath %secpath %name %kind

where %bc, %ec, %name, and %kind are as the above; %filepath contains the file module path the object that the references lives in, whereas %name may contain non-file non-directory module names.

val start_dump_glob : vfile:string -> vofile:string -> unit
val end_dump_glob : unit -> unit
val dump : unit -> bool
type glob_output =
| NoGlob
| Feedback
| MultFiles
| File of string
val push_output : glob_output -> unit

push_output o temporarily overrides the output location to o. The original output can be restored using pop_output

val pop_output : unit -> unit

Restores the original output that was overridden by push_output

val pause : unit -> unit

Alias for push_output NoGlob

val continue : unit -> unit

Deprecated alias for pop_output

val with_glob_output : glob_output -> (unit -> 'a) -> unit -> 'a
val add_glob : ?loc:Loc.t -> Names.GlobRef.t -> unit
val add_glob_kn : ?loc:Loc.t -> Names.KerName.t -> unit
val dump_definition : Names.lident -> bool -> string -> unit
val dump_moddef : ?loc:Loc.t -> Names.ModPath.t -> string -> unit
val dump_modref : ?loc:Loc.t -> Names.ModPath.t -> string -> unit
val dump_reference : ?loc:Loc.t -> string -> string -> string -> unit
val dump_secvar : ?loc:Loc.t -> Names.Id.t -> unit
val dump_libref : ?loc:Loc.t -> Names.DirPath.t -> string -> unit
val dump_notation_location : (int * int) list -> Constrexpr.notation -> (Notation.notation_location * Notation_term.scope_name option) -> unit
val dump_binding : ?loc:Loc.t -> string -> unit
val dump_notation : Constrexpr.notation CAst.t -> Notation_term.scope_name option -> bool -> unit
val dump_constraint : Names.lname -> bool -> string -> unit
val dump_string : string -> unit
val type_of_global_ref : Names.GlobRef.t -> string
val add_constant_kind : Names.Constant.t -> Decls.logical_kind -> unit

Registration of constant information

val constant_kind : Names.Constant.t -> Decls.logical_kind