aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitlab-ci.yml2
-rw-r--r--Makefile.ci2
-rwxr-xr-xdev/ci/ci-basic-overlay.sh14
-rwxr-xr-xdev/ci/ci-iris.sh36
-rwxr-xr-xdev/ci/ci-lambda_rust.sh30
-rw-r--r--test-suite/output/bug_12887.out10
-rw-r--r--test-suite/output/bug_12887.v10
-rw-r--r--vernac/comInductive.ml12
-rw-r--r--vernac/comInductive.mli4
-rw-r--r--vernac/record.ml6
10 files changed, 82 insertions, 44 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index cc8a4d34c9..ca5584bcb5 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -803,7 +803,7 @@ library:ci-geocoq:
library:ci-hott:
extends: .ci-template
-library:ci-lambda_rust:
+library:ci-iris:
extends: .ci-template-flambda
library:ci-math_classes:
diff --git a/Makefile.ci b/Makefile.ci
index 85e4b965f9..af78f252df 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -37,7 +37,7 @@ CI_TARGETS= \
ci-geocoq \
ci-coqhammer \
ci-hott \
- ci-lambda_rust \
+ ci-iris \
ci-math_classes \
ci-mathcomp \
ci-metacoq \
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 2725e6b56c..75d9efaadc 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -62,9 +62,17 @@
: "${iris_CI_GITURL:=https://gitlab.mpi-sws.org/iris/iris}"
: "${iris_CI_ARCHIVEURL:=${iris_CI_GITURL}/-/archive}"
-: "${lambda_rust_CI_REF:=master}"
-: "${lambda_rust_CI_GITURL:=https://gitlab.mpi-sws.org/iris/lambda-rust}"
-: "${lambda_rust_CI_ARCHIVEURL:=${lambda_rust_CI_GITURL}/-/archive}"
+: "${autosubst_CI_REF:=coq86-devel}"
+: "${autosubst_CI_GITURL:=https://github.com/RalfJung/autosubst}"
+: "${autosubst_CI_ARCHIVEURL:=${autosubst_CI_GITURL}/archive}"
+
+: "${iris_string_ident_CI_REF:=master}"
+: "${iris_string_ident_CI_GITURL:=https://gitlab.mpi-sws.org/iris/string-ident}"
+: "${iris_string_ident_CI_ARCHIVEURL:=${iris_string_ident_CI_GITURL}/-/archive}"
+
+: "${iris_examples_CI_REF:=master}"
+: "${iris_examples_CI_GITURL:=https://gitlab.mpi-sws.org/iris/examples}"
+: "${iris_examples_CI_ARCHIVEURL:=${iris_examples_CI_GITURL}/-/archive}"
########################################################################
# HoTT
diff --git a/dev/ci/ci-iris.sh b/dev/ci/ci-iris.sh
new file mode 100755
index 0000000000..0256906112
--- /dev/null
+++ b/dev/ci/ci-iris.sh
@@ -0,0 +1,36 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+# Setup iris_examples and separate dependencies first
+git_download autosubst
+git_download iris_string_ident
+git_download iris_examples
+
+# Extract required version of Iris (avoiding "+" which does not work on MacOS :( *)
+iris_CI_REF=$(grep -F '"coq-iris"' < "${CI_BUILD_DIR}/iris_examples/opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/')
+
+# Setup Iris
+git_download iris
+
+# Extract required version of std++
+stdpp_CI_REF=$(grep -F '"coq-stdpp"' < "${CI_BUILD_DIR}/iris/opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/')
+
+# Setup std++
+git_download stdpp
+
+# Build std++
+( cd "${CI_BUILD_DIR}/stdpp" && make && make install )
+
+# Build and validate Iris
+( cd "${CI_BUILD_DIR}/iris" && make && make validate && make install )
+
+# Build autosubst
+( cd "${CI_BUILD_DIR}/autosubst" && make && make install )
+
+# Build iris-string-ident
+( cd "${CI_BUILD_DIR}/iris_string_ident" && make && make install )
+
+# Build Iris examples
+( cd "${CI_BUILD_DIR}/iris_examples" && make && make install )
diff --git a/dev/ci/ci-lambda_rust.sh b/dev/ci/ci-lambda_rust.sh
deleted file mode 100755
index 1ef0c2cb8f..0000000000
--- a/dev/ci/ci-lambda_rust.sh
+++ /dev/null
@@ -1,30 +0,0 @@
-#!/usr/bin/env bash
-
-ci_dir="$(dirname "$0")"
-. "${ci_dir}/ci-common.sh"
-
-install_ssreflect
-
-# Setup lambda_rust first
-git_download lambda_rust
-
-# Extract required version of Iris (avoiding "+" which does not work on MacOS :( *)
-iris_CI_REF=$(grep -F coq-iris < "${CI_BUILD_DIR}/lambda_rust/opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/')
-
-# Setup Iris
-git_download iris
-
-# Extract required version of std++
-stdpp_CI_REF=$(grep -F coq-stdpp < "${CI_BUILD_DIR}/iris/opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/')
-
-# Setup std++
-git_download stdpp
-
-# Build std++
-( cd "${CI_BUILD_DIR}/stdpp" && make && make install )
-
-# Build and validate Iris
-( cd "${CI_BUILD_DIR}/iris" && make && make validate && make install )
-
-# Build lambda_rust
-( cd "${CI_BUILD_DIR}/lambda_rust" && make && make install )
diff --git a/test-suite/output/bug_12887.out b/test-suite/output/bug_12887.out
new file mode 100644
index 0000000000..5ea7722bc6
--- /dev/null
+++ b/test-suite/output/bug_12887.out
@@ -0,0 +1,10 @@
+The command has indeed failed with message:
+Cannot infer this placeholder of type "Type" in
+environment:
+Functor : (Type -> Type) -> Type
+F : Type -> Type
+fmap : forall A B : Type, (A -> B) -> F A -> F B
+The command has indeed failed with message:
+Cannot infer an existential variable of type "nat" in
+environment:
+R : nat -> Type
diff --git a/test-suite/output/bug_12887.v b/test-suite/output/bug_12887.v
new file mode 100644
index 0000000000..4208c3e8e9
--- /dev/null
+++ b/test-suite/output/bug_12887.v
@@ -0,0 +1,10 @@
+Arguments id {_} _.
+
+Fail Record Functor (F : Type -> Type) := {
+ fmap : forall A B, (A -> B) -> F A -> F B;
+ fmap_identity : fmap _ _ id = id;
+}.
+
+Fail Inductive R (x:nat) := { y : R ltac:(clear x) }.
+
+Inductive R (x:nat) := { y : bool; z : R _ }.
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 673124296d..452de69b1d 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -451,7 +451,7 @@ let interp_params env udecl uparamsl paramsl =
do the unification.
[env_ar_par] is [uparams; inds; params]
*)
-let maybe_unify_params_in env_ar_par sigma ~ninds ~nparams c =
+let maybe_unify_params_in env_ar_par sigma ~ninds ~nparams ~binders:k c =
let is_ind sigma k c = match EConstr.kind sigma c with
| Constr.Rel n ->
(* env is [uparams; inds; params; k other things] *)
@@ -462,14 +462,18 @@ let maybe_unify_params_in env_ar_par sigma ~ninds ~nparams c =
| Constr.App (h,args) when is_ind sigma k h ->
Array.fold_left_i (fun i sigma arg ->
if i >= nparams || not (EConstr.isEvar sigma arg) then sigma
- else Evarconv.unify_delay env sigma arg (EConstr.mkRel (k+nparams-i)))
+ else begin try Evarconv.unify_delay env sigma arg (EConstr.mkRel (k+nparams-i))
+ with Evarconv.UnableToUnify _ ->
+ (* ignore errors, we will get a "Cannot infer ..." error instead *)
+ sigma
+ end)
sigma args
| _ -> Termops.fold_constr_with_full_binders
sigma
(fun d (env,k) -> EConstr.push_rel d env, k+1)
aux envk sigma c
in
- aux (env_ar_par,0) sigma c
+ aux (env_ar_par,k) sigma c
let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) notations ~cumulative ~poly ~private_ind finite =
check_all_names_different indl;
@@ -527,7 +531,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
let sigma =
List.fold_left (fun sigma (_,ctyps,_) ->
List.fold_left (fun sigma ctyp ->
- maybe_unify_params_in env_ar_params sigma ~ninds ~nparams ctyp)
+ maybe_unify_params_in env_ar_params sigma ~ninds ~nparams ~binders:0 ctyp)
sigma ctyps)
sigma constructors
in
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 9c876787a3..91e8f609d5 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -81,8 +81,8 @@ val template_polymorphism_candidate
monomorphic universe context that can be made parametric in its
conclusion sort, if one is given. *)
-val maybe_unify_params_in : Environ.env -> Evd.evar_map -> ninds:int -> nparams:int
+val maybe_unify_params_in : Environ.env -> Evd.evar_map -> ninds:int -> nparams:int -> binders:int
-> EConstr.t -> Evd.evar_map
(** [nparams] is the number of parameters which aren't treated as
uniform, ie the length of params (including letins) where the env
- is [uniform params, inductives, params]. *)
+ is [uniform params, inductives, params, binders]. *)
diff --git a/vernac/record.ml b/vernac/record.ml
index d0036e40f9..bd5b71cd6b 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -81,12 +81,12 @@ let interp_fields_evars env sigma ~ninds ~nparams impls_env nots l =
(EConstr.push_rel d env, sigma, impl :: uimpls, d::params, impls))
(env, sigma, [], [], impls_env) nots l
in
- let _, sigma = Context.Rel.fold_outside ~init:(env,sigma) (fun f (env,sigma) ->
+ let _, _, sigma = Context.Rel.fold_outside ~init:(env,0,sigma) (fun f (env,k,sigma) ->
let sigma = RelDecl.fold_constr (fun c sigma ->
- ComInductive.maybe_unify_params_in env sigma ~ninds ~nparams c)
+ ComInductive.maybe_unify_params_in env sigma ~ninds ~nparams ~binders:k c)
f sigma
in
- EConstr.push_rel f env, sigma)
+ EConstr.push_rel f env, k+1, sigma)
newfs
in
sigma, (impls, newfs)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 04:51:36 +0000