aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitlab-ci.yml3
-rw-r--r--Makefile.ci1
-rw-r--r--dev/ci/README-developers.md4
-rwxr-xr-xdev/ci/ci-basic-overlay.sh7
-rwxr-xr-xdev/ci/ci-coq-tools.sh9
-rw-r--r--doc/dune6
-rw-r--r--doc/sphinx/README.rst7
-rw-r--r--doc/sphinx/_static/notations.css8
-rw-r--r--doc/sphinx/appendix/indexes/index.rst1
-rw-r--r--doc/sphinx/std-glossindex.rst7
-rw-r--r--doc/tools/coqrst/coqdomain.py58
-rw-r--r--engine/uState.ml8
-rw-r--r--engine/uState.mli5
13 files changed, 113 insertions, 11 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 1a1d31bdd7..468161ff73 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -676,6 +676,9 @@ library:ci-color:
library:ci-compcert:
extends: .ci-template-flambda
+library:ci-coq-tools:
+ extends: .ci-template
+
library:ci-coqprime:
stage: stage-3
extends: .ci-template-flambda
diff --git a/Makefile.ci b/Makefile.ci
index 1a5e8166a2..b545c9de45 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -20,6 +20,7 @@ CI_TARGETS= \
ci-coquelicot \
ci-corn \
ci-cross-crypto \
+ ci-coq-tools \
ci-coqprime \
ci-elpi \
ci-ext-lib \
diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md
index 6a740b9033..88d08a1724 100644
--- a/dev/ci/README-developers.md
+++ b/dev/ci/README-developers.md
@@ -72,10 +72,10 @@ Moreover your PR must absolutely update the [`CHANGES.md`](../../CHANGES.md) fil
### Experimental automatic overlay creation and building
If you break external projects that are hosted on GitHub, you can use
-the `create-overlays.sh` script to automatically perform most of the
+the `create_overlays.sh` script to automatically perform most of the
above steps. In order to do so, call the script as:
```
-./dev/tools/create-overlays.sh ejgallego 9873 aac_tactics elpi ltac
+./dev/tools/create_overlays.sh ejgallego 9873 aac_tactics elpi ltac
```
replacing `ejgallego` by your GitHub nickname and `9873` by the actual PR
number. The script will:
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index c18e556da8..88f410ef04 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -95,6 +95,13 @@
: "${Flocq_CI_ARCHIVEURL:=${Flocq_CI_GITURL}/-/archive}"
########################################################################
+# coq-tools
+########################################################################
+: "${coq_tools_CI_REF:=master}"
+: "${coq_tools_CI_GITURL:=https://github.com/JasonGross/coq-tools}"
+: "${coq_tools_CI_ARCHIVEURL:=${coq_tools_CI_GITURL}/archive}"
+
+########################################################################
# Coquelicot
########################################################################
: "${coquelicot_CI_REF:=master}"
diff --git a/dev/ci/ci-coq-tools.sh b/dev/ci/ci-coq-tools.sh
new file mode 100755
index 0000000000..9c95c49c9f
--- /dev/null
+++ b/dev/ci/ci-coq-tools.sh
@@ -0,0 +1,9 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download coq_tools
+
+( cd "${CI_BUILD_DIR}/coq_tools" && make check || \
+ { RV=$?; echo "The build broke, if an overlay is needed, mention @JasonGross in describing the expected change in Coq that needs to be taken into account, and he'll prepare a fix for coq-tools"; exit $RV; } )
diff --git a/doc/dune b/doc/dune
index 8b005f5b2f..c82e5a3df4 100644
--- a/doc/dune
+++ b/doc/dune
@@ -32,7 +32,7 @@
unreleased.rst
(env_var SPHINXWARNOPT))
(action
- (run env COQLIB=%{project_root} sphinx-build %{env:SPHINXWARNOPT=-W} -b html sphinx %{targets})))
+ (run env COQLIB=%{project_root} sphinx-build -q %{env:SPHINXWARNOPT=-W} -b html sphinx %{targets})))
(rule
(targets refman-pdf)
@@ -48,8 +48,8 @@
(env_var SPHINXWARNOPT))
(action
(progn
- (run env COQLIB=%{project_root} sphinx-build %{env:SPHINXWARNOPT=-W} -b latex sphinx %{targets})
- (chdir %{targets} (run make)))))
+ (run env COQLIB=%{project_root} sphinx-build -q %{env:SPHINXWARNOPT=-W} -b latex sphinx %{targets})
+ (chdir %{targets} (run make LATEXMKOPTS=-silent)))))
; Installable directories are not yet fully supported by Dune. See
; ocaml/dune#1868. Yet, this makes coq-doc.install a valid target to
diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index 0802b5d0b4..e20469bb8b 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -358,6 +358,13 @@ In addition to the objects and directives above, the ``coqrst`` Sphinx plugin de
<http://www.sphinx-doc.org/en/stable/markup/para.html#directive-productionlist>`_
and reference its tokens using ``:token:`…```.
+``:gdef:`` Marks the definition of a glossary term inline in the text. Matching :term:`XXX`
+ constructs will link to it. The term will also appear in the Glossary Index.
+
+ Example::
+
+ A :gdef:`prime` number is divisible only by itself and 1.
+
Common mistakes
===============
diff --git a/doc/sphinx/_static/notations.css b/doc/sphinx/_static/notations.css
index 733a73bd21..9546f7107e 100644
--- a/doc/sphinx/_static/notations.css
+++ b/doc/sphinx/_static/notations.css
@@ -215,6 +215,14 @@
margin-bottom: 0.28em;
}
+.term-defn {
+ font-style: italic;
+}
+
+.std-term {
+ color: #2980B9; /* override if :visited */
+}
+
/* We can't display nested blocks otherwise */
code, .rst-content tt, .rst-content code {
background: transparent !important;
diff --git a/doc/sphinx/appendix/indexes/index.rst b/doc/sphinx/appendix/indexes/index.rst
index 2ece726df7..c8b2cf46dc 100644
--- a/doc/sphinx/appendix/indexes/index.rst
+++ b/doc/sphinx/appendix/indexes/index.rst
@@ -17,6 +17,7 @@ find what you are looking for.
../../coq-optindex
../../coq-exnindex
../../coq-attrindex
+ ../../std-glossindex
For reference, here are direct links to the documentation of:
diff --git a/doc/sphinx/std-glossindex.rst b/doc/sphinx/std-glossindex.rst
new file mode 100644
index 0000000000..3f085ca737
--- /dev/null
+++ b/doc/sphinx/std-glossindex.rst
@@ -0,0 +1,7 @@
+:orphan:
+
+.. hack to get index in TOC
+
+--------------
+Glossary index
+--------------
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index 57243207f0..9d51d2198a 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -472,8 +472,7 @@ class ProductionObject(CoqObject):
op = "|"
rhs = parts[1].strip()
else:
- nsplits = 2
- parts = signature.split(maxsplit=nsplits)
+ parts = signature.split(maxsplit=2)
if len(parts) != 3:
loc = os.path.basename(get_node_location(signode))
raise ExtensionError(ProductionObject.SIG_ERROR.format(loc, signature))
@@ -1116,6 +1115,19 @@ class IndexXRefRole(XRefRole):
title = index.localname
return title, target
+class StdGlossaryIndex(Index):
+ name, localname, shortname = "glossindex", "Glossary", "terms"
+
+ def generate(self, docnames=None):
+ content = defaultdict(list)
+
+ for ((type, itemname), (docname, anchor)) in self.domain.data['objects'].items():
+ if type == 'term':
+ entries = content[itemname[0].lower()]
+ entries.append([itemname, 0, docname, anchor, '', '', ''])
+ content = sorted(content.items())
+ return content, False
+
def GrammarProductionRole(typ, rawtext, text, lineno, inliner, options={}, content=[]):
"""A grammar production not included in a ``productionlist`` directive.
@@ -1132,7 +1144,7 @@ def GrammarProductionRole(typ, rawtext, text, lineno, inliner, options={}, conte
"""
#pylint: disable=dangerous-default-value, unused-argument
env = inliner.document.settings.env
- targetid = 'grammar-token-{}'.format(text)
+ targetid = nodes.make_id('grammar-token-{}'.format(text))
target = nodes.target('', '', ids=[targetid])
inliner.document.note_explicit_target(target)
code = nodes.literal(rawtext, text, role=typ.lower())
@@ -1143,6 +1155,35 @@ def GrammarProductionRole(typ, rawtext, text, lineno, inliner, options={}, conte
GrammarProductionRole.role_name = "production"
+
+def GlossaryDefRole(typ, rawtext, text, lineno, inliner, options={}, content=[]):
+ """Marks the definition of a glossary term inline in the text. Matching :term:`XXX`
+ constructs will link to it. The term will also appear in the Glossary Index.
+
+ Example::
+
+ A :gdef:`prime` number is divisible only by itself and 1.
+ """
+ #pylint: disable=dangerous-default-value, unused-argument
+ env = inliner.document.settings.env
+ std = env.domaindata['std']['objects']
+ key = ('term', text)
+
+ if key in std:
+ MSG = 'Duplicate object: {}; other is at {}'
+ msg = MSG.format(text, env.doc2path(std[key][0]))
+ inliner.document.reporter.warning(msg, line=lineno)
+
+ targetid = nodes.make_id('term-{}'.format(text))
+ std[key] = (env.docname, targetid)
+ target = nodes.target('', '', ids=[targetid], names=[text])
+ inliner.document.note_explicit_target(target)
+ node = nodes.inline(rawtext, '', target, nodes.Text(text), classes=['term-defn'])
+ set_role_source_info(inliner, lineno, node)
+ return [node], []
+
+GlossaryDefRole.role_name = "gdef"
+
class CoqDomain(Domain):
"""A domain to document Coq code.
@@ -1305,18 +1346,23 @@ COQ_ADDITIONAL_DIRECTIVES = [CoqtopDirective,
InferenceDirective,
PreambleDirective]
-COQ_ADDITIONAL_ROLES = [GrammarProductionRole]
+COQ_ADDITIONAL_ROLES = [GrammarProductionRole,
+ GlossaryDefRole]
def setup(app):
"""Register the Coq domain"""
# A few sanity checks:
subdomains = set(obj.subdomain for obj in CoqDomain.directives.values())
- assert subdomains.issuperset(chain(*(idx.subdomains for idx in CoqDomain.indices)))
- assert subdomains.issubset(CoqDomain.roles.keys())
+ found = set (obj for obj in chain(*(idx.subdomains for idx in CoqDomain.indices)))
+ assert subdomains.issuperset(found), "Missing subdomains: {}".format(found.difference(subdomains))
+
+ assert subdomains.issubset(CoqDomain.roles.keys()), \
+ "Missing from CoqDomain.roles: {}".format(subdomains.difference(CoqDomain.roles.keys()))
# Add domain, directives, and roles
app.add_domain(CoqDomain)
+ app.add_index_to_domain('std', StdGlossaryIndex)
for role in COQ_ADDITIONAL_ROLES:
app.add_role(role.role_name, role)
diff --git a/engine/uState.ml b/engine/uState.ml
index abd5f2828f..00649ce042 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -527,6 +527,14 @@ let demote_seff_univs univs uctx =
let seff = LSet.union uctx.uctx_seff_univs univs in
{ uctx with uctx_seff_univs = seff }
+let demote_global_univs env uctx =
+ let env_ugraph = Environ.universes env in
+ let global_univs = UGraph.domain env_ugraph in
+ let global_constraints, _ = UGraph.constraints_of_universes env_ugraph in
+ let promoted_uctx =
+ ContextSet.(of_set global_univs |> add_constraints global_constraints) in
+ { uctx with uctx_local = ContextSet.diff uctx.uctx_local promoted_uctx }
+
let merge_seff uctx ctx' =
let levels = ContextSet.levels ctx' in
let declare g =
diff --git a/engine/uState.mli b/engine/uState.mli
index cd1c9a174e..6707826aae 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -110,6 +110,11 @@ val merge : ?loc:Loc.t -> sideff:bool -> rigid -> t -> Univ.ContextSet.t -> t
val merge_subst : t -> UnivSubst.universe_opt_subst -> t
val emit_side_effects : Safe_typing.private_constants -> t -> t
+val demote_global_univs : Environ.env -> t -> t
+(** Removes from the uctx_local part of the UState the universes and constraints
+ that are present in the universe graph in the input env (supposedly the
+ global ones *)
+
val demote_seff_univs : Univ.LSet.t -> t -> t
(** Mark the universes as not local any more, because they have been
globally declared by some side effect. You should be using
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 09:00:36 +0000