package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

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

Maintainers

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

Sources

rocq-9.0.0.tar.gz
md5=8d522602d23e7a665631826dab9aa92b
sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be

doc/rocq-runtime.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 {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.

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 (8.13) 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