aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rwxr-xr-xdev/ci/ci-basic-overlay.sh3
-rwxr-xr-xdev/ci/ci-coquelicot.sh1
-rw-r--r--dev/ci/nix/coquelicot.nix9
-rw-r--r--dev/ci/nix/default.nix1
-rw-r--r--dev/ci/nix/flocq.nix1
-rw-r--r--dev/ci/user-overlays/10052-ppedrot-cleanup-logic-convert-hyp.sh6
-rw-r--r--dev/ci/user-overlays/10076-vbgl-canonical-disable-hint.sh6
-rw-r--r--dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh6
-rw-r--r--dev/doc/changes.md7
-rw-r--r--dev/doc/release-process.md22
-rw-r--r--dev/include_printers1
-rw-r--r--dev/top_printers.dbg1
-rw-r--r--dev/top_printers.ml10
-rw-r--r--dev/top_printers.mli1
14 files changed, 69 insertions, 6 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index f97e781832..95fceb773a 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -98,7 +98,8 @@
# Coquelicot
########################################################################
: "${coquelicot_CI_REF:=master}"
-: "${coquelicot_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot}"
+: "${coquelicot_CI_GITURL:=https://gitlab.inria.fr/coquelicot/coquelicot}"
+: "${coquelicot_CI_ARCHIVEURL:=${coquelicot_CI_GITURL}/-/archive}"
########################################################################
# CompCert
diff --git a/dev/ci/ci-coquelicot.sh b/dev/ci/ci-coquelicot.sh
index 33627fd8ef..6cb8dad604 100755
--- a/dev/ci/ci-coquelicot.sh
+++ b/dev/ci/ci-coquelicot.sh
@@ -5,7 +5,6 @@ ci_dir="$(dirname "$0")"
install_ssreflect
-FORCE_GIT=1
git_download coquelicot
( cd "${CI_BUILD_DIR}/coquelicot" && ./autogen.sh && ./configure && ./remake "-j${NJOBS}" )
diff --git a/dev/ci/nix/coquelicot.nix b/dev/ci/nix/coquelicot.nix
new file mode 100644
index 0000000000..d379bfa73d
--- /dev/null
+++ b/dev/ci/nix/coquelicot.nix
@@ -0,0 +1,9 @@
+{ autoconf, automake, ssreflect }:
+
+{
+ buildInputs = [ autoconf automake ];
+ coqBuildInputs = [ ssreflect ];
+ configure = "./autogen.sh && ./configure";
+ make = "./remake";
+ clean = "./remake clean";
+}
diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix
index 17070e66ee..a9cc91170f 100644
--- a/dev/ci/nix/default.nix
+++ b/dev/ci/nix/default.nix
@@ -72,6 +72,7 @@ let projects = {
CoLoR = callPackage ./CoLoR.nix {};
CompCert = callPackage ./CompCert.nix {};
coq_dpdgraph = callPackage ./coq_dpdgraph.nix {};
+ coquelicot = callPackage ./coquelicot.nix {};
Corn = callPackage ./Corn.nix {};
cross_crypto = callPackage ./cross_crypto.nix {};
Elpi = callPackage ./Elpi.nix {};
diff --git a/dev/ci/nix/flocq.nix b/dev/ci/nix/flocq.nix
index e153043557..71028ec2dc 100644
--- a/dev/ci/nix/flocq.nix
+++ b/dev/ci/nix/flocq.nix
@@ -4,4 +4,5 @@
buildInputs = [ autoconf automake ];
configure = "./autogen.sh && ./configure";
make = "./remake";
+ clean = "./remake clean";
}
diff --git a/dev/ci/user-overlays/10052-ppedrot-cleanup-logic-convert-hyp.sh b/dev/ci/user-overlays/10052-ppedrot-cleanup-logic-convert-hyp.sh
new file mode 100644
index 0000000000..9f9cc19e83
--- /dev/null
+++ b/dev/ci/user-overlays/10052-ppedrot-cleanup-logic-convert-hyp.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10052" ] || [ "$CI_BRANCH" = "cleanup-logic-convert-hyp" ]; then
+
+ relation_algebra_CI_REF=cleanup-logic-convert-hyp
+ relation_algebra_CI_GITURL=https://github.com/ppedrot/relation-algebra
+
+fi
diff --git a/dev/ci/user-overlays/10076-vbgl-canonical-disable-hint.sh b/dev/ci/user-overlays/10076-vbgl-canonical-disable-hint.sh
new file mode 100644
index 0000000000..2015935dd9
--- /dev/null
+++ b/dev/ci/user-overlays/10076-vbgl-canonical-disable-hint.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10076" ] || [ "$CI_BRANCH" = "canonical-disable-hint" ]; then
+
+ elpi_CI_REF=canonical-disable-hint
+ elpi_CI_GITURL=https://github.com/vbgl/coq-elpi
+
+fi
diff --git a/dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh b/dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh
new file mode 100644
index 0000000000..bc8aa33565
--- /dev/null
+++ b/dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10135" ] || [ "$CI_BRANCH" = "detype-anonymous" ]; then
+
+ unicoq_CI_REF=detype-anonymous
+ unicoq_CI_GITURL=https://github.com/maximedenes/unicoq
+
+fi
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 9e0d47651e..7221c3de56 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -1,3 +1,10 @@
+## Changes between Coq 8.10 and Coq 8.11
+
+### ML API
+
+- Functions and types deprecated in 8.10 have been removed in Coq
+ 8.11.
+
## Changes between Coq 8.9 and Coq 8.10
### ML4 Pre Processing
diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md
index 60c0886896..189d6f9fa5 100644
--- a/dev/doc/release-process.md
+++ b/dev/doc/release-process.md
@@ -84,10 +84,18 @@
Coq has been tagged.
- [ ] Have some people test the recently auto-generated Windows and MacOS
packages.
-- [ ] Change the version name from alpha to beta1 (see
+- [ ] In a PR:
+ - Change the version name from alpha to beta1 (see
[#7009](https://github.com/coq/coq/pull/7009/files)).
- We generally do not update the magic numbers at this point.
+ - We generally do not update the magic numbers at this point.
+ - Set `is_a_released_version` to `true` in `configure.ml`.
- [ ] Put the `VX.X+beta1` tag using `git tag -s`.
+- [ ] Check using `git push --tags --dry-run` that you are not
+ pushing anything else than the new tag. If needed, remove spurious
+ tags with `git tag -d`. When this is OK, proceed with `git push --tags`.
+- [ ] Set `is_a_released_version` to `false` in `configure.ml`
+ (if you forget about it, you'll be reminded whenever you try to
+ backport a PR with a changelog entry).
### These steps are the same for all releases (beta, final, patch-level) ###
@@ -112,9 +120,17 @@
## At the final release time ##
-- [ ] Change the version name to X.X.0 and the magic numbers (see
+- [ ] In a PR:
+ - Change the version name from X.X.0 and the magic numbers (see
[#7271](https://github.com/coq/coq/pull/7271/files)).
+ - Set `is_a_released_version` to `true` in `configure.ml`.
- [ ] Put the `VX.X.0` tag.
+- [ ] Check using `git push --tags --dry-run` that you are not
+ pushing anything else than the new tag. If needed, remove spurious
+ tags with `git tag -d`. When this is OK, proceed with `git push --tags`.
+- [ ] Set `is_a_released_version` to `false` in `configure.ml`
+ (if you forget about it, you'll be reminded whenever you try to
+ backport a PR with a changelog entry).
Repeat the generic process documented above for all releases.
diff --git a/dev/include_printers b/dev/include_printers
index 90088e40bf..d077075eeb 100644
--- a/dev/include_printers
+++ b/dev/include_printers
@@ -11,6 +11,7 @@
#install_printer (* universes *) ppuniverses;;
#install_printer (* univ level *) ppuni_level;;
#install_printer (* univ context *) ppuniverse_context;;
+#install_printer (* univ context *) ppaucontext;;
#install_printer (* univ context future *) ppuniverse_context_future;;
#install_printer (* univ context set *) ppuniverse_context_set;;
#install_printer (* univ set *) ppuniverse_set;;
diff --git a/dev/top_printers.dbg b/dev/top_printers.dbg
index a6ecec7e33..82f2e79549 100644
--- a/dev/top_printers.dbg
+++ b/dev/top_printers.dbg
@@ -62,6 +62,7 @@ install_printer Top_printers.ppuni_level
install_printer Top_printers.ppuniverse_set
install_printer Top_printers.ppuniverse_instance
install_printer Top_printers.ppuniverse_context
+install_printer Top_printers.ppaucontext
install_printer Top_printers.ppuniverse_context_set
install_printer Top_printers.ppuniverse_subst
install_printer Top_printers.ppuniverse_opt_subst
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 816316487c..2859b56cbe 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -27,7 +27,6 @@ open Clenv
let _ = Detyping.print_evar_arguments := true
let _ = Detyping.print_universes := true
let _ = Goptions.set_bool_option_value ["Printing";"Matching"] false
-let _ = Detyping.set_detype_anonymous (fun ?loc _ -> raise Not_found)
(* std_ppcmds *)
let pp x = Pp.pp_with !Topfmt.std_ft x
@@ -236,6 +235,15 @@ let ppnamedcontextval e =
let sigma = Evd.from_env env in
pp (pr_named_context env sigma (named_context_of_val e))
+let ppaucontext auctx =
+ let nas = AUContext.names auctx in
+ let prlev l = match Level.var_index l with
+ | Some n -> Name.print nas.(n)
+ | None -> prlev l
+ in
+ pp (pr_universe_context prlev (AUContext.repr auctx))
+
+
let ppenv e = pp
(str "[" ++ pr_named_context_of e Evd.empty ++ str "]" ++ spc() ++
str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]")
diff --git a/dev/top_printers.mli b/dev/top_printers.mli
index cb32d2294c..2aa1808322 100644
--- a/dev/top_printers.mli
+++ b/dev/top_printers.mli
@@ -137,6 +137,7 @@ val prlev : Univ.Level.t -> Pp.t (* with global names (does this work?) *)
val ppuniverse_set : Univ.LSet.t -> unit
val ppuniverse_instance : Univ.Instance.t -> unit
val ppuniverse_context : Univ.UContext.t -> unit
+val ppaucontext : Univ.AUContext.t -> unit
val ppuniverse_context_set : Univ.ContextSet.t -> unit
val ppuniverse_subst : Univ.universe_subst -> unit
val ppuniverse_opt_subst : UnivSubst.universe_opt_subst -> unit
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 06:17:17 +0000