aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--INSTALL.doc5
-rw-r--r--configure.ml2
-rw-r--r--engine/uState.ml125
-rw-r--r--kernel/names.ml18
-rw-r--r--kernel/names.mli5
-rw-r--r--kernel/uGraph.mli1
-rw-r--r--proofs/proof_global.ml4
-rw-r--r--test-suite/output/goal_output.out8
-rw-r--r--test-suite/output/goal_output.v13
9 files changed, 102 insertions, 79 deletions
diff --git a/INSTALL.doc b/INSTALL.doc
index 2472d2b2a..21b21163c 100644
--- a/INSTALL.doc
+++ b/INSTALL.doc
@@ -41,6 +41,7 @@ Compilation
To produce all documentation about Coq, just run:
+ ./configure (if you hadn't already)
make doc
@@ -71,6 +72,10 @@ Alternatively, you can use some specific targets:
to produce all formats of the Coq standard library
+Also note the "-with-doc yes" option of ./configure to enable the
+build of the documentation as part of the default make target.
+
+
Installation
------------
diff --git a/configure.ml b/configure.ml
index 5330da7d3..679f52417 100644
--- a/configure.ml
+++ b/configure.ml
@@ -328,7 +328,7 @@ let args_options = Arg.align [
"-browser", arg_string_option Prefs.browser,
"<command> Use <command> to open URL %s";
"-nodoc", Arg.Clear Prefs.withdoc,
- " Do not compile the documentation";
+ " Deprecated: use -with-doc no instead";
"-with-doc", arg_bool Prefs.withdoc,
"(yes|no) Compile the documentation or not";
"-with-geoproof", arg_bool Prefs.geoproof,
diff --git a/engine/uState.ml b/engine/uState.ml
index c66af02bb..e27d0536d 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -131,84 +131,87 @@ let instantiate_variable l b v =
exception UniversesDiffer
let process_universe_constraints ctx cstrs =
+ let open Univ in
let univs = ctx.uctx_universes in
let vars = ref ctx.uctx_univ_variables in
let normalize = Universes.normalize_universe_opt_subst vars in
- let rec unify_universes fo l d r local =
+ let is_local l = Univ.LMap.mem l !vars in
+ let varinfo x =
+ match Univ.Universe.level x with
+ | None -> Inl x
+ | Some l -> Inr l
+ in
+ let equalize_variables fo l l' r r' local =
+ (** Assumes l = [l',0] and r = [r',0] *)
+ let () =
+ if is_local l' then
+ instantiate_variable l' r vars
+ else if is_local r' then
+ instantiate_variable r' l vars
+ else if not (UGraph.check_eq_level univs l' r') then
+ (* Two rigid/global levels, none of them being local,
+ one of them being Prop/Set, disallow *)
+ if Univ.Level.is_small l' || Univ.Level.is_small r' then
+ raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None))
+ else if fo then
+ raise UniversesDiffer
+ in
+ Univ.enforce_eq_level l' r' local
+ in
+ let equalize_universes l r local = match varinfo l, varinfo r with
+ | Inr l', Inr r' -> equalize_variables false l l' r r' local
+ | Inr l, Inl r | Inl r, Inr l ->
+ let alg = Univ.LSet.mem l ctx.uctx_univ_algebraic in
+ let inst = Univ.univ_level_rem l r r in
+ if alg then (instantiate_variable l inst vars; local)
+ else
+ let lu = Univ.Universe.make l in
+ if Univ.univ_level_mem l r then
+ Univ.enforce_leq inst lu local
+ else raise (Univ.UniverseInconsistency (Univ.Eq, lu, r, None))
+ | Inl _, Inl _ (* both are algebraic *) ->
+ if UGraph.check_eq univs l r then local
+ else raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None))
+ in
+ let unify_universes (l, d, r) local =
let l = normalize l and r = normalize r in
if Univ.Universe.equal l r then local
else
- let varinfo x =
- match Univ.Universe.level x with
- | None -> Inl x
- | Some l -> Inr (l, Univ.LMap.mem l !vars, Univ.LSet.mem l ctx.uctx_univ_algebraic)
- in
- if d == Universes.ULe then
+ match d with
+ | Universes.ULe ->
if UGraph.check_leq univs l r then
(** Keep Prop/Set <= var around if var might be instantiated by prop or set
later. *)
- if Univ.Universe.is_level l then
- match Univ.Universe.level r with
- | Some r ->
- Univ.Constraint.add (Option.get (Univ.Universe.level l),Univ.Le,r) local
- | _ -> local
- else local
+ match Univ.Universe.level l, Univ.Universe.level r with
+ | Some l, Some r ->
+ Univ.Constraint.add (l, Univ.Le, r) local
+ | _ -> local
else
- match Univ.Universe.level r with
+ begin match Univ.Universe.level r with
| None -> error ("Algebraic universe on the right")
- | Some rl ->
- if Univ.Level.is_small rl then
+ | Some r' ->
+ if Univ.Level.is_small r' then
let levels = Univ.Universe.levels l in
- Univ.LSet.fold (fun l local ->
- if Univ.Level.is_small l || Univ.LMap.mem l !vars then
- unify_universes fo (Univ.Universe.make l) Universes.UEq r local
- else raise (Univ.UniverseInconsistency (Univ.Le, Univ.Universe.make l, r, None)))
- levels local
+ let fold l' local =
+ let l = Univ.Universe.make l' in
+ if Univ.Level.is_small l' || is_local l' then
+ equalize_variables false l l' r r' local
+ else raise (Univ.UniverseInconsistency (Univ.Le, l, r, None))
+ in
+ Univ.LSet.fold fold levels local
else
Univ.enforce_leq l r local
- else if d == Universes.ULub then
- match varinfo l, varinfo r with
- | (Inr (l, true, _), Inr (r, _, _))
- | (Inr (r, _, _), Inr (l, true, _)) ->
- instantiate_variable l (Univ.Universe.make r) vars;
- Univ.enforce_eq_level l r local
- | Inr (_, _, _), Inr (_, _, _) ->
- unify_universes true l Universes.UEq r local
+ end
+ | Universes.ULub ->
+ begin match Universe.level l, Universe.level r with
+ | Some l', Some r' ->
+ equalize_variables true l l' r r' local
| _, _ -> assert false
- else (* d = Universes.UEq *)
- match varinfo l, varinfo r with
- | Inr (l', lloc, _), Inr (r', rloc, _) ->
- let () =
- if lloc then
- instantiate_variable l' r vars
- else if rloc then
- instantiate_variable r' l vars
- else if not (UGraph.check_eq univs l r) then
- (* Two rigid/global levels, none of them being local,
- one of them being Prop/Set, disallow *)
- if Univ.Level.is_small l' || Univ.Level.is_small r' then
- raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None))
- else
- if fo then
- raise UniversesDiffer
- in
- Univ.enforce_eq_level l' r' local
- | Inr (l, loc, alg), Inl r
- | Inl r, Inr (l, loc, alg) ->
- let inst = Univ.univ_level_rem l r r in
- if alg then (instantiate_variable l inst vars; local)
- else
- let lu = Univ.Universe.make l in
- if Univ.univ_level_mem l r then
- Univ.enforce_leq inst lu local
- else raise (Univ.UniverseInconsistency (Univ.Eq, lu, r, None))
- | _, _ (* One of the two is algebraic or global *) ->
- if UGraph.check_eq univs l r then local
- else raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None))
+ end
+ | Universes.UEq -> equalize_universes l r local
in
let local =
- Universes.Constraints.fold (fun (l,d,r) local -> unify_universes false l d r local)
- cstrs Univ.Constraint.empty
+ Universes.Constraints.fold unify_universes cstrs Univ.Constraint.empty
in
!vars, local
diff --git a/kernel/names.ml b/kernel/names.ml
index 811b4a62a..f5b3f4e00 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -34,16 +34,8 @@ struct
let hash = String.hash
- let warn_invalid_identifier =
- CWarnings.create ~name:"invalid-identifier" ~category:"parsing"
- ~default:CWarnings.Disabled
- (fun s -> str s)
-
- let check_soft ?(warn = true) x =
- let iter (fatal, x) =
- if fatal then CErrors.error x else
- if warn then warn_invalid_identifier x
- in
+ let check_valid ?(strict=true) x =
+ let iter (fatal, x) = if fatal || strict then CErrors.error x in
Option.iter iter (Unicode.ident_refutation x)
let is_valid s = match Unicode.ident_refutation s with
@@ -52,15 +44,15 @@ struct
let of_bytes s =
let s = Bytes.to_string s in
- check_soft s;
+ check_valid s;
String.hcons s
let of_string s =
- let () = check_soft s in
+ let () = check_valid s in
String.hcons s
let of_string_soft s =
- let () = check_soft ~warn:false s in
+ let () = check_valid ~strict:false s in
String.hcons s
let to_string id = id
diff --git a/kernel/names.mli b/kernel/names.mli
index be9b9422b..5b0163aa5 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -46,11 +46,12 @@ sig
val of_bytes : bytes -> t
val of_string : string -> t
(** Converts a string into an identifier.
- @raise UserError if the string is not valid, or echo a warning if it contains invalid identifier characters.
+ @raise UserError if the string is invalid as an identifier.
@raise Unicode.Unsupported if the provided string contains unsupported UTF-8 characters. *)
val of_string_soft : string -> t
- (** Same as {!of_string} except that no warning is ever issued.
+ (** Same as {!of_string} except that any string made of supported UTF-8 characters is accepted.
+ @raise UserError if the string is invalid as an UTF-8 string.
@raise Unicode.Unsupported if the provided string contains unsupported UTF-8 characters. *)
val to_string : t -> string
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index c8ac7df5c..935a3cab4 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -17,6 +17,7 @@ type universes = t
type 'a check_function = universes -> 'a -> 'a -> bool
val check_leq : universe check_function
val check_eq : universe check_function
+val check_eq_level : universe_level check_function
(** The empty graph of universes *)
val empty_universes : universes
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 5f4a7766f..99fab0848 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -516,7 +516,7 @@ module Bullet = struct
| NeedClosingBrace -> str"Try unfocusing with \"}\"."
| NoBulletInUse -> assert false (* This should never raise an error. *)
| ProofFinished -> str"No more subgoals."
- | Suggest b -> str"Bullet " ++ pr_bullet b ++ str" is mandatory here."
+ | Suggest b -> str"Expecting " ++ pr_bullet b ++ str"."
| Unfinished b -> str"Current bullet " ++ pr_bullet b ++ str" is not finished."
exception FailedBullet of t * suggestion
@@ -525,7 +525,7 @@ module Bullet = struct
CErrors.register_handler
(function
| FailedBullet (b,sugg) ->
- let prefix = str"Wrong bullet " ++ pr_bullet b ++ str" : " in
+ let prefix = str"Wrong bullet " ++ pr_bullet b ++ str": " in
CErrors.user_err ~hdr:"Focus" (prefix ++ suggest_on_error sugg)
| _ -> raise CErrors.Unhandled)
diff --git a/test-suite/output/goal_output.out b/test-suite/output/goal_output.out
new file mode 100644
index 000000000..773533a8d
--- /dev/null
+++ b/test-suite/output/goal_output.out
@@ -0,0 +1,8 @@
+Nat.t = nat
+ : Set
+Nat.t = nat
+ : Set
+1 subgoal
+
+ ============================
+ False
diff --git a/test-suite/output/goal_output.v b/test-suite/output/goal_output.v
new file mode 100644
index 000000000..327b80b0a
--- /dev/null
+++ b/test-suite/output/goal_output.v
@@ -0,0 +1,13 @@
+(* From
+ - https://coq.inria.fr/bugs/show_bug.cgi?id=5529
+ - https://coq.inria.fr/bugs/show_bug.cgi?id=5537
+ *)
+
+Print Nat.t.
+Timeout 1 Print Nat.t.
+
+Lemma toto: False.
+Set Printing All.
+Show.
+Abort.
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-14 17:32:40 +0000