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/top_printers.ml4
-rw-r--r--doc/sphinx/language/gallina-extensions.rst6
-rw-r--r--kernel/uGraph.ml5
-rw-r--r--kernel/univ.ml15
-rw-r--r--kernel/univ.mli2
-rw-r--r--lib/flags.ml1
-rw-r--r--lib/flags.mli3
-rw-r--r--pretyping/detyping.ml2
15 files changed, 63 insertions, 43 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/top_printers.ml b/dev/top_printers.ml
index f9b4025866..8d5b5bef4a 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -162,8 +162,8 @@ let pp_state_t n = pp (Reductionops.pr_state n)
(* proof printers *)
let pr_evar ev = Pp.int (Evar.repr ev)
let ppmetas metas = pp(Termops.pr_metaset metas)
-let ppevm evd = pp(Termops.pr_evar_map ~with_univs:!Flags.univ_print (Some 2) evd)
-let ppevmall evd = pp(Termops.pr_evar_map ~with_univs:!Flags.univ_print None evd)
+let ppevm evd = pp(Termops.pr_evar_map ~with_univs:!Detyping.print_universes (Some 2) evd)
+let ppevmall evd = pp(Termops.pr_evar_map ~with_univs:!Detyping.print_universes None evd)
let pr_existentialset evars =
prlist_with_sep spc pr_evar (Evar.Set.elements evars)
let ppexistentialset evars =
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/kernel/uGraph.ml b/kernel/uGraph.ml
index 5d1644614d..b4ea04a56b 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -21,7 +21,7 @@ open Univ
(* Revisions by Bruno Barras, Hugo Herbelin, Pierre Letouzey, Matthieu
Sozeau, Pierre-Marie Pédrot, Jacques-Henri Jourdan *)
-let error_inconsistency o u v (p:explanation option) =
+let error_inconsistency o u v p =
raise (UniverseInconsistency (o,Universe.make u,Universe.make v,p))
(* Universes are stratified by a partial ordering $\le$.
@@ -557,8 +557,7 @@ let get_explanation strict u v g =
else match traverse strict u with Some exp -> exp | None -> assert false
let get_explanation strict u v g =
- if !Flags.univ_print then Some (get_explanation strict u v g)
- else None
+ Some (lazy (get_explanation strict u v g))
(* To compare two nodes, we simply do a forward search.
We implement two improvements:
diff --git a/kernel/univ.ml b/kernel/univ.ml
index ea3a522953..8e19fa4e52 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -541,11 +541,11 @@ let constraint_type_ord c1 c2 = match c1, c2 with
(* Universe inconsistency: error raised when trying to enforce a relation
that would create a cycle in the graph of universes. *)
-type univ_inconsistency = constraint_type * universe * universe * explanation option
+type univ_inconsistency = constraint_type * universe * universe * explanation Lazy.t option
exception UniverseInconsistency of univ_inconsistency
-let error_inconsistency o u v (p:explanation option) =
+let error_inconsistency o u v p =
raise (UniverseInconsistency (o,make u,make v,p))
(* Constraints and sets of constraints. *)
@@ -1235,13 +1235,16 @@ let explain_universe_inconsistency prl (o,u,v,p) =
| Eq -> str"=" | Lt -> str"<" | Le -> str"<="
in
let reason = match p with
- | None | Some [] -> mt()
+ | None -> mt()
| Some p ->
- str " because" ++ spc() ++ pr_uni v ++
+ let p = Lazy.force p in
+ if p = [] then mt ()
+ else
+ str " because" ++ spc() ++ pr_uni v ++
prlist (fun (r,v) -> spc() ++ pr_rel r ++ str" " ++ pr_uni v)
- p ++
+ p ++
(if Universe.equal (snd (List.last p)) u then mt() else
- (spc() ++ str "= " ++ pr_uni u))
+ (spc() ++ str "= " ++ pr_uni u))
in
str "Cannot enforce" ++ spc() ++ pr_uni u ++ spc() ++
pr_rel o ++ spc() ++ pr_uni v ++ reason
diff --git a/kernel/univ.mli b/kernel/univ.mli
index aaed899bf4..b68bbdf359 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -205,7 +205,7 @@ val enforce_leq_level : Level.t constraint_function
Constraint.t...
*)
type explanation = (constraint_type * Universe.t) list
-type univ_inconsistency = constraint_type * Universe.t * Universe.t * explanation option
+type univ_inconsistency = constraint_type * Universe.t * Universe.t * explanation Lazy.t option
exception UniverseInconsistency of univ_inconsistency
diff --git a/lib/flags.ml b/lib/flags.ml
index 8491873e07..2a1c50f52b 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -60,7 +60,6 @@ let profile = false
let ide_slave = ref false
let raw_print = ref false
-let univ_print = ref false
let we_are_parsing = ref false
diff --git a/lib/flags.mli b/lib/flags.mli
index 85aaf879f3..53a69f3566 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -42,9 +42,6 @@ val we_are_parsing : bool ref
(* Set Printing All flag. For some reason it is a global flag *)
val raw_print : bool ref
-(* Univ print flag, never set anywere. Maybe should belong to Univ? *)
-val univ_print : bool ref
-
type compat_version = V8_6 | V8_7 | Current
val compat_version : compat_version ref
val version_compare : compat_version -> compat_version -> int
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index bb563220b6..56e5828918 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -36,7 +36,7 @@ type _ delay =
| Later : [ `thunk ] delay
(** Should we keep details of universes during detyping ? *)
-let print_universes = Flags.univ_print
+let print_universes = ref false
(** If true, prints local context of evars, whatever print_arguments *)
let print_evar_arguments = ref false
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 13:28:36 +0000