aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.circleci/config.yml4
-rw-r--r--.gitlab-ci.yml3
-rw-r--r--.travis.yml3
-rw-r--r--Makefile.ci2
-rw-r--r--configure.ml44
-rwxr-xr-xdev/ci/ci-basic-overlay.sh6
-rwxr-xr-xdev/ci/ci-mtac2.sh (renamed from dev/ci/ci-metacoq.sh)6
-rw-r--r--dev/doc/debugging.md2
-rw-r--r--doc/sphinx/language/gallina-extensions.rst6
-rw-r--r--engine/evarutil.ml10
-rw-r--r--engine/evarutil.mli2
-rw-r--r--tactics/tactics.ml52
12 files changed, 93 insertions, 47 deletions
diff --git a/.circleci/config.yml b/.circleci/config.yml
index 8b6b43a552..d6a8e059c1 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -207,6 +207,9 @@ jobs:
math-comp:
<<: *ci-template
+ mtac2:
+ <<: *ci-template
+
sf:
<<: *ci-template
environment:
@@ -251,6 +254,7 @@ workflows:
requires:
- build
- bignums
+ - mtac2: *req-main
- corn:
requires:
- build
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 7d6b539644..e1c5b5255a 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -360,6 +360,9 @@ ci-math-classes:
ci-math-comp:
<<: *ci-template
+ci-mtac2:
+ <<: *ci-template
+
ci-sf:
<<: *ci-template
variables:
diff --git a/.travis.yml b/.travis.yml
index fe376431e3..052979bcb3 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -117,6 +117,9 @@ matrix:
- TEST_TARGET="ci-math-comp"
- if: NOT (type = pull_request)
env:
+ - TEST_TARGET="ci-mtac2"
+ - if: NOT (type = pull_request)
+ env:
- TEST_TARGET="ci-sf"
- if: NOT (type = pull_request)
env:
diff --git a/Makefile.ci b/Makefile.ci
index 6b30f87232..37b14ed918 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -28,7 +28,7 @@ CI_TARGETS=ci-bignums \
ci-ltac2 \
ci-math-classes \
ci-math-comp \
- ci-metacoq \
+ ci-mtac2 \
ci-sf \
ci-tlc \
ci-unimath \
diff --git a/configure.ml b/configure.ml
index 2ac705ad27..e77310eb72 100644
--- a/configure.ml
+++ b/configure.ml
@@ -21,11 +21,18 @@ let distributed_exec = ["coqtop";"coqc";"coqchk";"coqdoc";"coqworkmgr";
let verbose = ref false (* for debugging this script *)
+let red, yellow, reset =
+ if Unix.isatty Unix.stdout && Unix.isatty Unix.stderr && Sys.os_type = "Unix"
+ then "\027[31m", "\027[33m", "\027[0m"
+ else "", "", ""
+
(** * Utility functions *)
let cfprintf oc = kfprintf (fun oc -> fprintf oc "\n%!") oc
let cprintf s = cfprintf stdout s
let ceprintf s = cfprintf stderr s
-let die msg = ceprintf "%s\nConfiguration script failed!" msg; exit 1
+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 s2i = int_of_string
let i2s = string_of_int
@@ -109,7 +116,7 @@ let run ?(fatal=true) ?(err=StdErr) prog args =
let cmd = String.concat " " (prog::args) in
let exn = match e with Failure s -> s | _ -> Printexc.to_string e in
let msg = sprintf "Error while running '%s' (%s)" cmd exn in
- if fatal then die msg else (cprintf "W: %s" msg; "", [])
+ if fatal then die msg else (warn "%s" msg; "", [])
let tryrun prog args = run ~fatal:false ~err:DevNull prog args
@@ -205,7 +212,7 @@ let win_aware_quote_executable str =
sprintf "%S" str
else
let _ = if contains_suspicious_characters str then
- cprintf "*Warning* The string %S contains suspicious characters; ocamlfind might fail" str in
+ warn "The string %S contains suspicious characters; ocamlfind might fail" str in
Str.global_replace (Str.regexp "\\\\") "/" str
(** * Date *)
@@ -414,8 +421,8 @@ let args_options = Arg.align [
" Do not add debugging information in the Coq executables";
"-profiling", arg_set (fun p profile -> { p with profile }),
" Add profiling information in the Coq executables";
- "-annotate", Arg.Unit (fun () -> cprintf "*Warning* -annotate is deprecated. Please use -annot or -bin-annot instead."),
- " Deprecated. Please use -annot or -bin-annot instead";
+ "-annotate", Arg.Unit (fun () -> die "-annotate has been removed. Please use -annot or -bin-annot instead."),
+ " Removed option. Please use -annot or -bin-annot instead";
"-annot", arg_set (fun p annot -> { p with annot }),
" Dumps ml text annotation files while compiling Coq (e.g. for Tuareg)";
"-bin-annot", arg_set (fun p bin_annot -> { p with bin_annot }),
@@ -598,7 +605,7 @@ let check_caml_version () =
else
let () = cprintf "Your version of OCaml is %s." caml_version in
if !prefs.force_caml_version then
- cprintf "*Warning* Your version of OCaml is outdated."
+ warn "Your version of OCaml is outdated."
else
die "You need OCaml 4.02.1 or later."
@@ -620,7 +627,7 @@ let check_findlib_version () =
else
let () = cprintf "Your version of OCamlfind is %s." findlib_version in
if !prefs.force_findlib_version then
- cprintf "*Warning* Your version of OCamlfind is outdated."
+ warn "Your version of OCamlfind is outdated."
else
die "You need OCamlfind 1.4.1 or later."
@@ -731,17 +738,17 @@ let camlp5libdir = shorten_camllib fullcamlp5libdir
(** * Native compiler *)
-let msg_byteonly () =
- cprintf "Only the bytecode version of Coq will be available."
+let msg_byteonly =
+ "Only the bytecode version of Coq will be available."
let msg_no_ocamlopt () =
- cprintf "Cannot find the OCaml native-code compiler."; msg_byteonly ()
+ warn "Cannot find the OCaml native-code compiler.\n%s" msg_byteonly
let msg_no_camlp5_cmxa () =
- cprintf "Cannot find the native-code library of camlp5."; msg_byteonly ()
+ warn "Cannot find the native-code library of camlp5.\n%s" msg_byteonly
let msg_no_dynlink_cmxa () =
- cprintf "Cannot find native-code dynlink library."; msg_byteonly ();
+ warn "Cannot find native-code dynlink library.\n%s" msg_byteonly;
cprintf "For building a native-code Coq, you may try to first";
cprintf "compile and install a dummy dynlink.cmxa (see dev/dynlink.ml)";
cprintf "and then run ./configure -natdynlink no"
@@ -757,8 +764,7 @@ let check_native () =
else
let () =
if version <> caml_version then
- cprintf
- "Warning: Native and bytecode compilers do not have the same version!"
+ warn "Native and bytecode compilers do not have the same version!"
in cprintf "You have native-code compilation. Good!"
let best_compiler =
@@ -813,7 +819,7 @@ let get_source = function
(** Is some location a suitable LablGtk2 installation ? *)
let check_lablgtkdir ?(fatal=false) src dir =
- let yell msg = if fatal then die msg else (cprintf "%s" msg; false) in
+ let yell msg = if fatal then die msg else (warn "%s" msg; false) in
let msg = get_source src in
if not (dir_exists dir) then
yell (sprintf "No such directory '%s' (%s)." dir msg)
@@ -849,7 +855,7 @@ let get_lablgtkdir () =
let check_lablgtk_version src dir = match src with
| Manual | Stdlib ->
- cprintf "Warning: could not check the version of lablgtk2.\nMake sure your version is at least 2.18.3.";
+ warn "Could not check the version of lablgtk2.\nMake sure your version is at least 2.18.3.";
(true, "an unknown version")
| OCamlFind ->
let v, _ = tryrun camlexec.find ["query"; "-format"; "%v"; "lablgtk2"] in
@@ -860,7 +866,11 @@ let check_lablgtk_version src dir = match src with
else if vi < [2; 18; 3] then
begin
(* Version 2.18.3 is known to report incorrectly as 2.18.0, and Launchpad packages report as version 2.16.0 due to a misconfigured META file; see https://bugs.launchpad.net/ubuntu/+source/lablgtk2/+bug/1577236 *)
- cprintf "Warning: Your installed lablgtk reports as %s.\n It is possible that the installed version is actually more recent\n but reports an incorrect version. If the installed version is\n actually more recent than 2.18.3, that's fine; if it is not,\n CoqIDE will compile but may be very unstable." v;
+ warn "Your installed lablgtk reports as %s.\n\
+It is possible that the installed version is actually more recent\n\
+but reports an incorrect version. If the installed version is\n\
+actually more recent than 2.18.3, that's fine; if it is not,\n
+CoqIDE will compile but may be very unstable." v;
(true, "an unknown version")
end
else
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 5566a51175..5cee72cc73 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -19,13 +19,13 @@
: "${UniMath_CI_GITURL:=https://github.com/UniMath/UniMath.git}"
########################################################################
-# Unicoq + Metacoq
+# Unicoq + Mtac2
########################################################################
: "${unicoq_CI_BRANCH:=master}"
: "${unicoq_CI_GITURL:=https://github.com/unicoq/unicoq.git}"
-: "${metacoq_CI_BRANCH:=master}"
-: "${metacoq_CI_GITURL:=https://github.com/MetaCoq/MetaCoq.git}"
+: "${mtac2_CI_BRANCH:=master-sync}"
+: "${mtac2_CI_GITURL:=https://github.com/Mtac2/Mtac2.git}"
########################################################################
# Mathclasses + Corn
diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-mtac2.sh
index a66dc1e762..1372acb8e5 100755
--- a/dev/ci/ci-metacoq.sh
+++ b/dev/ci/ci-mtac2.sh
@@ -4,7 +4,7 @@ ci_dir="$(dirname "$0")"
. "${ci_dir}/ci-common.sh"
unicoq_CI_DIR=${CI_BUILD_DIR}/unicoq
-metacoq_CI_DIR=${CI_BUILD_DIR}/MetaCoq
+mtac2_CI_DIR=${CI_BUILD_DIR}/Mtac2
# Setup UniCoq
@@ -14,6 +14,6 @@ git_checkout "${unicoq_CI_BRANCH}" "${unicoq_CI_GITURL}" "${unicoq_CI_DIR}"
# Setup MetaCoq
-git_checkout "${metacoq_CI_BRANCH}" "${metacoq_CI_GITURL}" "${metacoq_CI_DIR}"
+git_checkout "${mtac2_CI_BRANCH}" "${mtac2_CI_GITURL}" "${mtac2_CI_DIR}"
-( cd "${metacoq_CI_DIR}" && coq_makefile -f _CoqProject -o Makefile && make )
+( cd "${mtac2_CI_DIR}" && coq_makefile -f _CoqProject -o Makefile && make )
diff --git a/dev/doc/debugging.md b/dev/doc/debugging.md
index fd3cbd1bc3..14a1cc693c 100644
--- a/dev/doc/debugging.md
+++ b/dev/doc/debugging.md
@@ -47,7 +47,7 @@ Debugging with ocamldebug from Emacs
7. some hints:
- To debug a failure/error/anomaly, add a breakpoint in
- Vernac.vernac_com at the with clause of the "try ... interp com
+ `Vernac.interp_vernac` (in `toplevel/vernac.ml`) at the with clause of the "try ... interp com
with ..." block, then go "back" a few steps to find where the
failure/error/anomaly has been raised
- Alternatively, for an error or an anomaly, add breakpoints in the middle
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 1a7628d893..a93e9b156d 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -874,7 +874,7 @@ In the syntax of module application, the ! prefix indicates that any
Starts an interactive module satisfying each `module_type`.
- .. cmdv:: Module @ident {* @module_binding} <: {+<; @module_type }.
+ .. cmdv:: Module @ident {* @module_binding} <: {+<: @module_type }.
Starts an interactive functor with parameters given by the list of `module_binding`. The output module type
is verified against each `module_type`.
@@ -1436,7 +1436,9 @@ For instance, the first argument of
in module ``List.v`` is strict because :g:`list` is an inductive type and :g:`A`
will always be inferable from the type :g:`list A` of the third argument of
-:g:`cons`. On the contrary, the second argument of a term of type
+:g:`cons`. Also, the first argument of :g:`cons` is strict with respect to the second one,
+since the first argument is exactly the type of the second argument.
+On the contrary, the second argument of a term of type
::
forall P:nat->Prop, forall n:nat, P n -> ex nat P
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 6a8f8fb1db..710491f848 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -534,7 +534,7 @@ type clear_dependency_error =
| OccurHypInSimpleClause of Id.t option
| EvarTypingBreak of existential
-exception ClearDependencyError of Id.t * clear_dependency_error
+exception ClearDependencyError of Id.t * clear_dependency_error * Globnames.global_reference option
exception Depends of Id.t
@@ -545,13 +545,13 @@ let rec check_and_clear_in_constr env evdref err ids global c =
is a section variable *)
match kind c with
| Var id' ->
- if Id.Set.mem id' ids then raise (ClearDependencyError (id', err)) else c
+ if Id.Set.mem id' ids then raise (ClearDependencyError (id', err, None)) else c
| ( Const _ | Ind _ | Construct _ ) ->
let () = if global then
let check id' =
if Id.Set.mem id' ids then
- raise (ClearDependencyError (id',err))
+ raise (ClearDependencyError (id',err,Some (Globnames.global_of_constr c)))
in
Id.Set.iter check (Environ.vars_of_global env c)
in
@@ -599,8 +599,8 @@ let rec check_and_clear_in_constr env evdref err ids global c =
let global = Id.Set.exists is_section_variable nids in
let concl = EConstr.Unsafe.to_constr (evar_concl evi) in
check_and_clear_in_constr env evdref (EvarTypingBreak ev) nids global concl
- with ClearDependencyError (rid,err) ->
- raise (ClearDependencyError (Id.Map.find rid rids,err)) in
+ with ClearDependencyError (rid,err,where) ->
+ raise (ClearDependencyError (Id.Map.find rid rids,err,where)) in
if Id.Map.is_empty rids then c
else
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index c3de488c6a..d3937f28e4 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -232,7 +232,7 @@ type clear_dependency_error =
| OccurHypInSimpleClause of Id.t option
| EvarTypingBreak of Constr.existential
-exception ClearDependencyError of Id.t * clear_dependency_error
+exception ClearDependencyError of Id.t * clear_dependency_error * Globnames.global_reference option
val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> types ->
Id.Set.t -> named_context_val * types
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index aae4bc0885..c6d262fef3 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -198,32 +198,40 @@ end
let convert x y = convert_gen Reduction.CONV x y
let convert_leq x y = convert_gen Reduction.CUMUL x y
-let clear_dependency_msg env sigma id = function
+let clear_in_global_msg = function
+ | None -> mt ()
+ | Some ref -> str " implicitly in " ++ Printer.pr_global ref
+
+let clear_dependency_msg env sigma id err inglobal =
+ let pp = clear_in_global_msg inglobal in
+ match err with
| Evarutil.OccurHypInSimpleClause None ->
- Id.print id ++ str " is used in conclusion."
+ Id.print id ++ str " is used" ++ pp ++ str " in conclusion."
| Evarutil.OccurHypInSimpleClause (Some id') ->
- Id.print id ++ strbrk " is used in hypothesis " ++ Id.print id' ++ str"."
+ Id.print id ++ strbrk " is used" ++ pp ++ str " in hypothesis " ++ Id.print id' ++ str"."
| Evarutil.EvarTypingBreak ev ->
str "Cannot remove " ++ Id.print id ++
strbrk " without breaking the typing of " ++
Printer.pr_existential env sigma ev ++ str"."
-let error_clear_dependency env sigma id err =
- user_err (clear_dependency_msg env sigma id err)
+let error_clear_dependency env sigma id err inglobal =
+ user_err (clear_dependency_msg env sigma id err inglobal)
-let replacing_dependency_msg env sigma id = function
+let replacing_dependency_msg env sigma id err inglobal =
+ let pp = clear_in_global_msg inglobal in
+ match err with
| Evarutil.OccurHypInSimpleClause None ->
- str "Cannot change " ++ Id.print id ++ str ", it is used in conclusion."
+ str "Cannot change " ++ Id.print id ++ str ", it is used" ++ pp ++ str " in conclusion."
| Evarutil.OccurHypInSimpleClause (Some id') ->
str "Cannot change " ++ Id.print id ++
- strbrk ", it is used in hypothesis " ++ Id.print id' ++ str"."
+ strbrk ", it is used" ++ pp ++ str " in hypothesis " ++ Id.print id' ++ str"."
| Evarutil.EvarTypingBreak ev ->
str "Cannot change " ++ Id.print id ++
strbrk " without breaking the typing of " ++
Printer.pr_existential env sigma ev ++ str"."
-let error_replacing_dependency env sigma id err =
- user_err (replacing_dependency_msg env sigma id err)
+let error_replacing_dependency env sigma id err inglobal =
+ user_err (replacing_dependency_msg env sigma id err inglobal)
(* This tactic enables the user to remove hypotheses from the signature.
* Some care is taken to prevent him from removing variables that are
@@ -242,7 +250,7 @@ let clear_gen fail = function
let evdref = ref sigma in
let (hyps, concl) =
try clear_hyps_in_evi env evdref (named_context_val env) concl ids
- with Evarutil.ClearDependencyError (id,err) -> fail env sigma id err
+ with Evarutil.ClearDependencyError (id,err,inglobal) -> fail env sigma id err inglobal
in
let env = reset_with_named_context hyps env in
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref)
@@ -426,8 +434,8 @@ let clear_hyps2 env sigma ids sign t cl =
let evdref = ref (Evd.clear_metas sigma) in
let (hyps,t,cl) = Evarutil.clear_hyps2_in_evi env evdref sign t cl ids in
(hyps, t, cl, !evdref)
- with Evarutil.ClearDependencyError (id,err) ->
- error_replacing_dependency env sigma id err
+ with Evarutil.ClearDependencyError (id,err,inglobal) ->
+ error_replacing_dependency env sigma id err inglobal
let internal_cut_gen ?(check=true) dir replace id t =
Proofview.Goal.enter begin fun gl ->
@@ -3007,8 +3015,24 @@ let unfold_body x =
end
end
+let warn_cannot_remove_as_expected =
+ CWarnings.create ~name:"cannot-remove-as-expected" ~category:"tactics"
+ (fun (id,inglobal) ->
+ let pp = match inglobal with
+ | None -> mt ()
+ | Some ref -> str ", it is used implicitly in " ++ Printer.pr_global ref in
+ str "Cannot remove " ++ Id.print id ++ pp ++ str ".")
+
+let clear_for_destruct ids =
+ Proofview.tclORELSE
+ (clear_gen (fun env sigma id err inglobal -> raise (ClearDependencyError (id,err,inglobal))) ids)
+ (function
+ | ClearDependencyError (id,err,inglobal),_ -> warn_cannot_remove_as_expected (id,inglobal); Proofview.tclUNIT ()
+ | e -> iraise e)
+
(* Either unfold and clear if defined or simply clear if not a definition *)
-let expand_hyp id = Tacticals.New.tclTRY (unfold_body id) <*> clear [id]
+let expand_hyp id =
+ Tacticals.New.tclTRY (unfold_body id) <*> clear_for_destruct [id]
(*****************************)
(* High-level induction *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 00:54:22 +0000