1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
|
(************************************************************************)
(* * 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 of string (* 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
|
