(************************************************************************) (* * The Rocq Prover / The Rocq Development Team *) (* v * Copyright INRIA, CNRS and contributors *) (* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************)
(** 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.
*)
(** {2 The [.glob] file format}
[.glob] files contain a header, and then a list of entries, with one line per entry.
{3 [.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.
{3 [.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: + [ax] Axiom, Parameter or Variable(s), Hypothes{i,e}s, Context outside any section + [def] Definition + [coe] Coertion + [thm] Theorem + [subclass] Sub Class + [canonstruc] Canonical Declaration + [ex] Example + [scheme] Scheme + [class] Class declaration + [proj] Projection from a structure + [inst] Instance + [meth] Class Method + [defax] Definitional assumption + [prfax] Logical assumption + [prim] Primitive + [var] section Variable reference (Variable{,s}, Hypothes{i,e}s, Context) + [indrec] Inductive + [rec] Inductive (variant) + [corec] Coinductive + [ind] Record + [variant] Record (variant) + [coind] Coinductive Record + [constr] Constructor + [not] Notation + [binder] Binder + [lib] Require + [mod] Module Reference (Import, Module start / end) + [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 ...
+ 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.
+ 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 (* one glob file per .v file *)
| File ofstring(* Single file for all coqc arguments *)
(** [push_output o] temporarily overrides the output location to [o].
The original output can be restored using [pop_output] *) val push_output : glob_output -> unit
(** Restores the original output that was overridden by [push_output] *) val pop_output : unit -> unit
(** Alias for [push_output NoGlob] *) val pause : unit -> unit
(** Deprecated alias for [pop_output] *) val continue : unit -> unit
[@@ocaml.deprecated "(8.13) Use 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
(** Registration of constant information *) val add_constant_kind : Names.Constant.t -> Decls.logical_kind -> unit val constant_kind : Names.Constant.t -> Decls.logical_kind
[ Dauer der Verarbeitung: 0.17 Sekunden
(vorverarbeitet)
]
