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:

  • *definitions*: these entries correspond to definitions of inductives, functions, binders, notations. They are written as:

%kind %bc:%ec %secpath %name

where %kind is one of {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. def Definition
  2. coe Coertion
  3. thm Theorem
  4. subclass Sub Class
  5. canonstruc Canonical Declaration
  6. ex Example
  7. scheme Scheme
  8. class Class declaration
  9. proj Projection from a structure
  10. inst Instance
  11. meth Class Method
  12. defax Definitional assumption
  13. prfax Logical assumption
  14. prim Primitive
  15. var Variable reference
  16. indrec Inductive
  17. rec Inductive (variant)
  18. corec Coinductive
  19. ind Record
  20. variant Record (variant)
  21. coind Coinductive Record
  22. constr Constructor
  23. not Notation
  24. binder Binder
  25. lib Require
  26. mod Module Reference (Import, Module start / end)
  27. modtype Module Type

%bc and %ec are respectively the start and end byte locations in the file (0-indexed) %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.
  • *references*: which identify the object a particular document piece of text points to; their format is:

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