package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

coq.inria.fr Readme Edit opam file Versions (11)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.19.2.tar.gz
md5=5d1187d5e44ed0163f76fb12dabf012e
sha512=91bc81530fa4f6498961583ad51eac5001f139881788b88e360a866ad8e2a6e2c5bce86d1a580ab4cd4782bf49d48318767df82471ce33ba3ac143e5569ad33c

doc/coq-core.interp/Dumpglob/index.html

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

Sourceval start_dump_glob : vfile:string -> vofile:string -> unit
Sourceval end_dump_glob : unit -> unit
Sourceval dump : unit -> bool
Sourcetype glob_output =
  1. | NoGlob
  2. | Feedback
  3. | MultFiles
  4. | File of string
Sourceval push_output : glob_output -> unit

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

Sourceval pop_output : unit -> unit

Restores the original output that was overridden by push_output

Sourceval pause : unit -> unit

Alias for push_output NoGlob

Sourceval continue : unit -> unit

Deprecated alias for pop_output

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

Registration of constant information