Module DumpglobSource

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

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