aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitlab-ci.yml3
-rw-r--r--Makefile.ci4
-rw-r--r--clib/cMap.ml8
-rw-r--r--clib/cMap.mli4
-rw-r--r--configure.ml2
-rwxr-xr-xdev/ci/ci-basic-overlay.sh12
-rw-r--r--dev/ci/ci-common.sh2
-rwxr-xr-xdev/ci/ci-ext-lib.sh16
-rwxr-xr-xdev/ci/ci-pidetop.sh4
-rwxr-xr-xdev/ci/ci-quickchick.sh18
-rw-r--r--interp/constrintern.ml2
-rw-r--r--interp/syntax_def.ml8
-rw-r--r--interp/syntax_def.mli2
-rw-r--r--tactics/term_dnet.mli2
14 files changed, 70 insertions, 17 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 05d2c635a..a6eed661e 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -342,6 +342,9 @@ ci-mtac2:
ci-pidetop:
<<: *ci-template
+ci-quickchick:
+ <<: *ci-template-flambda
+
ci-sf:
<<: *ci-template
diff --git a/Makefile.ci b/Makefile.ci
index ce725d19d..7f63157fa 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -17,6 +17,7 @@ CI_TARGETS=ci-bignums \
ci-cpdt \
ci-cross-crypto \
ci-elpi \
+ ci-ext-lib \
ci-equations \
ci-fcsl-pcm \
ci-fiat-crypto \
@@ -31,6 +32,7 @@ CI_TARGETS=ci-bignums \
ci-math-comp \
ci-mtac2 \
ci-pidetop \
+ ci-quickchick \
ci-sf \
ci-tlc \
ci-unimath \
@@ -50,6 +52,8 @@ ci-math-classes: ci-bignums
ci-corn: ci-math-classes
+ci-quickchick: ci-ext-lib
+
ci-formal-topology: ci-corn
# Generic rule, we use make to ease travis integration with mixed rules
diff --git a/clib/cMap.ml b/clib/cMap.ml
index f6e52594b..54a8b2585 100644
--- a/clib/cMap.ml
+++ b/clib/cMap.ml
@@ -35,9 +35,9 @@ sig
val fold_left : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val fold_right : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val smartmap : ('a -> 'a) -> 'a t -> 'a t
- (** [@@ocaml.deprecated "Same as [Smart.map]"] *)
+ [@@ocaml.deprecated "Same as [Smart.map]"]
val smartmapi : (key -> 'a -> 'a) -> 'a t -> 'a t
- (** [@@ocaml.deprecated "Same as [Smart.mapi]"] *)
+ [@@ocaml.deprecated "Same as [Smart.mapi]"]
val height : 'a t -> int
module Smart :
sig
@@ -66,9 +66,9 @@ sig
val fold_left : (M.t -> 'a -> 'b -> 'b) -> 'a map -> 'b -> 'b
val fold_right : (M.t -> 'a -> 'b -> 'b) -> 'a map -> 'b -> 'b
val smartmap : ('a -> 'a) -> 'a map -> 'a map
- (** [@@ocaml.deprecated "Same as [Smart.map]"] *)
+ [@@ocaml.deprecated "Same as [Smart.map]"]
val smartmapi : (M.t -> 'a -> 'a) -> 'a map -> 'a map
- (** [@@ocaml.deprecated "Same as [Smart.mapi]"] *)
+ [@@ocaml.deprecated "Same as [Smart.mapi]"]
val height : 'a map -> int
module Smart :
sig
diff --git a/clib/cMap.mli b/clib/cMap.mli
index b45effb95..127bf23ab 100644
--- a/clib/cMap.mli
+++ b/clib/cMap.mli
@@ -58,10 +58,10 @@ sig
(** Folding keys in decreasing order. *)
val smartmap : ('a -> 'a) -> 'a t -> 'a t
- (** [@@ocaml.deprecated "Same as [Smart.map]"] *)
+ [@@ocaml.deprecated "Same as [Smart.map]"]
val smartmapi : (key -> 'a -> 'a) -> 'a t -> 'a t
- (** [@@ocaml.deprecated "Same as [Smart.mapi]"] *)
+ [@@ocaml.deprecated "Same as [Smart.mapi]"]
val height : 'a t -> int
(** An indication of the logarithmic size of a map *)
diff --git a/configure.ml b/configure.ml
index 45c3bb67a..933143e68 100644
--- a/configure.ml
+++ b/configure.ml
@@ -33,7 +33,7 @@ let cprintf s = cfprintf stdout s
let ceprintf s = cfprintf stderr s
let die msg = ceprintf "%s%s%s\nConfiguration script failed!" red msg reset; exit 1
-let warn s = cprintf ("%sWarning: " ^^ s ^^ "%s") yellow reset
+let warn s = kfprintf (fun oc -> cfprintf oc "%s" reset) stdout ("%sWarning: " ^^ s) yellow
let s2i = int_of_string
let i2s = string_of_int
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 5c882ee85..87d837b38 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -170,3 +170,15 @@
########################################################################
: "${pidetop_CI_BRANCH:=v8.9}"
: "${pidetop_CI_GITURL:=https://bitbucket.org/coqpide/pidetop.git}"
+
+########################################################################
+# ext-lib
+########################################################################
+: "${ext_lib_CI_BRANCH:=master}"
+: "${ext_lib_CI_GITURL:=https://github.com/coq-ext-lib/coq-ext-lib.git}"
+
+########################################################################
+# quickchick
+########################################################################
+: "${quickchick_CI_BRANCH:=master}"
+: "${quickchick_CI_GITURL:=https://github.com/QuickChick/QuickChick.git}"
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index f867fd189..5b5cbd11a 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -8,6 +8,7 @@ export NJOBS
if [ -n "${GITLAB_CI}" ];
then
+ export OCAMLPATH="$PWD/_install_ci/lib:$OCAMLPATH"
export COQBIN="$PWD/_install_ci/bin"
export CI_BRANCH="$CI_COMMIT_REF_NAME"
if [[ ${CI_BRANCH#pr-} =~ ^[0-9]*$ ]]
@@ -27,6 +28,7 @@ else
CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)"
export CI_BRANCH
fi
+ export OCAMLPATH="$PWD:$OCAMLPATH"
export COQBIN="$PWD/bin"
fi
export PATH="$COQBIN:$PATH"
diff --git a/dev/ci/ci-ext-lib.sh b/dev/ci/ci-ext-lib.sh
new file mode 100755
index 000000000..cf212c2fb
--- /dev/null
+++ b/dev/ci/ci-ext-lib.sh
@@ -0,0 +1,16 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+
+# This script could be included inside other ones
+# Let's avoid to source ci-common twice in this case
+if [ -z "${CI_BUILD_DIR}" ];
+then
+ . "${ci_dir}/ci-common.sh"
+fi
+
+ext_lib_CI_DIR="${CI_BUILD_DIR}/ExtLib"
+
+git_checkout "${ext_lib_CI_BRANCH}" "${ext_lib_CI_GITURL}" "${ext_lib_CI_DIR}"
+
+( cd "${ext_lib_CI_DIR}" && make && make install)
diff --git a/dev/ci/ci-pidetop.sh b/dev/ci/ci-pidetop.sh
index 2ac4d2167..32cba0808 100755
--- a/dev/ci/ci-pidetop.sh
+++ b/dev/ci/ci-pidetop.sh
@@ -12,13 +12,11 @@ git_checkout "${pidetop_CI_BRANCH}" "${pidetop_CI_GITURL}" "${pidetop_CI_DIR}"
# `-local`. We need to improve this divergence but if we use Dune this
# "local" oddity goes away automatically so not bothering...
if [ -d "$COQBIN/../lib/coq" ]; then
- COQOCAMLLIB="$COQBIN/../lib/"
COQLIB="$COQBIN/../lib/coq/"
else
- COQOCAMLLIB="$COQBIN/../"
COQLIB="$COQBIN/../"
fi
-( cd "${pidetop_CI_DIR}" && OCAMLPATH="$COQOCAMLLIB" jbuilder build @install )
+( cd "${pidetop_CI_DIR}" && jbuilder build @install )
echo -en '4\nexit' | "$pidetop_CI_DIR/_build/install/default/bin/pidetop" -coqlib "$COQLIB" -main-channel stdfds
diff --git a/dev/ci/ci-quickchick.sh b/dev/ci/ci-quickchick.sh
new file mode 100755
index 000000000..fc39e2685
--- /dev/null
+++ b/dev/ci/ci-quickchick.sh
@@ -0,0 +1,18 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+
+# This script could be included inside other ones
+# Let's avoid to source ci-common twice in this case
+if [ -z "${CI_BUILD_DIR}" ];
+then
+ . "${ci_dir}/ci-common.sh"
+fi
+
+quickchick_CI_DIR="${CI_BUILD_DIR}/Quickchick"
+
+install_ssreflect
+
+git_checkout "${quickchick_CI_BRANCH}" "${quickchick_CI_GITURL}" "${quickchick_CI_DIR}"
+
+( cd "${quickchick_CI_DIR}" && make && make install)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index f77c4d327..848180743 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -999,7 +999,7 @@ let intern_qualid qid intern env ntnvars us args =
match intern_extended_global_of_qualid qid with
| TrueGlobal ref -> (DAst.make ?loc @@ GRef (ref, us)), true, args
| SynDef sp ->
- let (ids,c) = Syntax_def.search_syntactic_definition sp in
+ let (ids,c) = Syntax_def.search_syntactic_definition ?loc sp in
let nids = List.length ids in
if List.length args < nids then error_not_enough_arguments ?loc;
let args1,args2 = List.chop nids args in
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 47faa5885..a4f20fd73 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -96,13 +96,13 @@ let warn_compatibility_notation =
CWarnings.(create ~name:"compatibility-notation"
~category:"deprecated" ~default:Enabled pr_compat_warning)
-let verbose_compat kn def = function
+let verbose_compat ?loc kn def = function
| Some v when Flags.version_strictly_greater v ->
- warn_compatibility_notation (kn, def, v)
+ warn_compatibility_notation ?loc (kn, def, v)
| _ -> ()
-let search_syntactic_definition kn =
+let search_syntactic_definition ?loc kn =
let pat,v = KNmap.find kn !syntax_table in
let def = out_pat pat in
- verbose_compat kn def v;
+ verbose_compat ?loc kn def v;
def
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index 1933b8a9a..c5b6655ff 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -18,4 +18,4 @@ type syndef_interpretation = (Id.t * subscopes) list * notation_constr
val declare_syntactic_definition : bool -> Id.t ->
Flags.compat_version option -> syndef_interpretation -> unit
-val search_syntactic_definition : KerName.t -> syndef_interpretation
+val search_syntactic_definition : ?loc:Loc.t -> KerName.t -> syndef_interpretation
diff --git a/tactics/term_dnet.mli b/tactics/term_dnet.mli
index 2c748f9c9..7bce57789 100644
--- a/tactics/term_dnet.mli
+++ b/tactics/term_dnet.mli
@@ -26,7 +26,7 @@ open Mod_subst
The results returned here are perfect, since post-filtering is done
inside here.
- See lib/dnet.mli for more details.
+ See tactics/dnet.mli for more details.
*)
(** Identifiers to store (right hand side of the association) *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 22:21:27 +0000