aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rwxr-xr-xdev/ci/ci-compcert.sh4
-rwxr-xr-xdev/ci/ci-vst.sh2
-rw-r--r--doc/changelog/03-notations/12683-master+fix12682-notation-printing-nary-application-ref.rst5
-rw-r--r--doc/changelog/07-commands-and-options/12677-require-v811-error-compat.rst5
-rw-r--r--doc/sphinx/changes.rst25
-rw-r--r--interp/constrextern.ml16
-rw-r--r--interp/constrintern.ml6
-rw-r--r--interp/notation.ml18
-rw-r--r--interp/notation.mli7
-rw-r--r--lib/objFile.ml2
-rw-r--r--lib/system.ml7
-rw-r--r--pretyping/evarconv.ml10
-rw-r--r--test-suite/bugs/closed/bug_12534.v9
-rw-r--r--test-suite/output/Notations.out6
-rw-r--r--test-suite/output/Notations.v25
15 files changed, 121 insertions, 26 deletions
diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh
index 59a85e4726..9cb7a65ab5 100755
--- a/dev/ci/ci-compcert.sh
+++ b/dev/ci/ci-compcert.sh
@@ -6,4 +6,6 @@ ci_dir="$(dirname "$0")"
git_download compcert
( cd "${CI_BUILD_DIR}/compcert" && \
- ./configure -ignore-coq-version x86_32-linux && make && make check-proof )
+ ./configure -ignore-coq-version x86_32-linux && \
+ make && \
+ make check-proof COQCHK='"$(COQBIN)coqchk" -silent -o $(COQINCLUDES)')
diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh
index 169d1a41db..4a332406a2 100755
--- a/dev/ci/ci-vst.sh
+++ b/dev/ci/ci-vst.sh
@@ -5,4 +5,6 @@ ci_dir="$(dirname "$0")"
git_download vst
+export COMPCERT=bundled
+
( cd "${CI_BUILD_DIR}/vst" && make IGNORECOQVERSION=true )
diff --git a/doc/changelog/03-notations/12683-master+fix12682-notation-printing-nary-application-ref.rst b/doc/changelog/03-notations/12683-master+fix12682-notation-printing-nary-application-ref.rst
new file mode 100644
index 0000000000..ab8768a079
--- /dev/null
+++ b/doc/changelog/03-notations/12683-master+fix12682-notation-printing-nary-application-ref.rst
@@ -0,0 +1,5 @@
+- **Fixed:**
+ Printing bug with notations for n-ary applications used with applied references.
+ (`#12683 <https://github.com/coq/coq/pull/12683>`_,
+ fixes `#12682 <https://github.com/coq/coq/pull/12682>`_,
+ by Hugo Herbelin).
diff --git a/doc/changelog/07-commands-and-options/12677-require-v811-error-compat.rst b/doc/changelog/07-commands-and-options/12677-require-v811-error-compat.rst
new file mode 100644
index 0000000000..c654ddd69d
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/12677-require-v811-error-compat.rst
@@ -0,0 +1,5 @@
+- **Fixed:**
+ Properly report the mismatched magic number of vo files
+ (`#12677 <https://github.com/coq/coq/pull/12677>`_,
+ fixes `#12513 <https://github.com/coq/coq/issues/12513>`_,
+ by Pierre-Marie Pédrot).
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index e5c2056c40..d4707a04d8 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -14,9 +14,9 @@ Version 8.12
Summary of changes
~~~~~~~~~~~~~~~~~~
-|Coq| version 8.12 integrates many quality-of-life improvements,
+|Coq| version 8.12 integrates many usability improvements,
in particular with respect to notations, scopes and implicit arguments,
-along with many bug-fixes and major improvements to the reference manual.
+along with many bug fixes and major improvements to the reference manual.
The main changes include:
- New :ref:`binder notation<812Implicit>` for non-maximal implicit arguments using :g:`[ ]`
@@ -64,6 +64,23 @@ Guillaume Claret, Karl Palmskog, Matthieu Sozeau and Enrico Tassi with
contributions from many users. A list of packages is available at
https://coq.inria.fr/opam/www/.
+Previously, most components of Coq had a single principal maintainer.
+This was changed in 8.12 (`#11295
+<https://github.com/coq/coq/pull/11295>`_) so that every component now has
+a team of maintainers, who are in charge of reviewing and
+merging incoming pull requests. This gave us a chance to
+significantly expand the pool of maintainters and provide faster
+feedback to contributors. Special thanks to all our maintainers!
+
+Our current 31 maintainers are Yves Bertot, Frédéric Besson, Tej
+Chajed, Cyril Cohen, Pierre Corbineau, Pierre Courtieu, Maxime Dénès,
+Jim Fehrle, Julien Forest, Emilio Jesús Gallego Arias, Gaëtan Gilbert,
+Georges Gonthier, Benjamin Grégoire, Jason Gross, Hugo Herbelin,
+Vincent Laporte, Assia Mahboubi, Kenji Maillard, Guillaume Melquiond,
+Pierre-Marie Pédrot, Clément Pit-Claudel, Kazuhiko Sakaguchi, Vincent
+Semeria, Michael Soegtrop, Arnaud Spiwack, Matthieu Sozeau, Enrico
+Tassi, Laurent Théry, Anton Trunov, Li-yao Xia, Théo Zimmermann
+
The 59 contributors to this version are Abhishek Anand, Yves Bertot, Frédéric
Besson, Lasse Blaauwbroek, Simon Boulier, Quentin Carbonneaux, Tej Chajed,
Arthur Charguéraud, Cyril Cohen, Pierre Courtieu, Matthew Dempsky, Maxime Dénès,
@@ -72,8 +89,8 @@ Jesús Gallego Arias, Paolo G. Giarrusso, Gaëtan Gilbert, Jason Gross, Samuel
Gruetter, Attila Gáspár, Hugo Herbelin, Jan-Oliver Kaiser, Robbert Krebbers,
Vincent Laporte, Olivier Laurent, Xavier Leroy, Thomas Letan, Yishuai Li,
Kenji Maillard, Erik Martin-Dorel, Guillaume Melquiond, Ike Mulder,
-Guillaume Munch-Maccagnoni, Antonio Nikishaev, Karl Palmskog, Clément
-Pit-Claudel, Pierre-Marie Pédrot, Ramkumar Ramachandra, Lars Rasmusson, Daniel
+Guillaume Munch-Maccagnoni, Antonio Nikishaev, Karl Palmskog, Pierre-Marie
+Pédrot, Clément Pit-Claudel, Ramkumar Ramachandra, Lars Rasmusson, Daniel
de Rauglaudre, Talia Ringer, Pierre Roux, Kazuhiko Sakaguchi, Vincent Semeria,
@scinart, Kartik Singhal, Michael Soegtrop, Matthieu Sozeau, Enrico Tassi,
Laurent Théry, Ralf Treinen, Anton Trunov, Bernhard M. Wiedemann, Li-yao Xia,
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 95df626d4c..3667757a2f 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -858,10 +858,17 @@ let extern_possible_prim_token (custom,scopes) r =
insert_entry_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key)
let filter_enough_applied nargs l =
+ (* This is to ensure that notations for coercions are used only when
+ the coercion is fully applied; not explicitly done yet, but we
+ could also expect that the notation is exactly talking about the
+ coercion *)
match nargs with
| None -> l
| Some nargs ->
- List.filter (fun (keyrule,pat,n as _rule) -> match n with Some n -> n > nargs | None -> false) l
+ List.filter (fun (keyrule,pat,n as _rule) ->
+ match n with
+ | AppBoundedNotation n -> n > nargs
+ | AppUnboundedNotation | NotAppNotation -> false) l
(* Helper function for safe and optimal printing of primitive tokens *)
(* such as those for Int63 *)
@@ -1247,7 +1254,7 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
[], [] in
(* Adjust to the number of arguments expected by the notation *)
let (t,args,argsscopes,argsimpls) = match n with
- | Some n when nallargs >= n ->
+ | AppBoundedNotation n when nallargs >= n ->
let args1, args2 = List.chop n args in
let args2scopes = try List.skipn n argsscopes with Failure _ -> [] in
let args2impls =
@@ -1257,12 +1264,13 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
[]
else try List.skipn n argsimpls with Failure _ -> [] in
DAst.make @@ GApp (f,args1), args2, args2scopes, args2impls
- | None ->
+ | AppUnboundedNotation -> t, [], [], []
+ | NotAppNotation ->
begin match DAst.get f with
| GRef (ref,us) -> f, args, argsscopes, argsimpls
| _ -> t, [], [], []
end
- | _ -> raise No_match in
+ | AppBoundedNotation _ -> raise No_match in
(* Try matching ... *)
let terms,termlists,binders,binderlists =
match_notation_constr !print_universes t pat in
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 987aa63392..6d4ab8b4d6 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1659,12 +1659,12 @@ let drop_notations_pattern looked_for genv =
| None -> DAst.make ?loc @@ RCPatAtom None
| Some (n, head, pl) ->
let pl =
- if get_asymmetric_patterns () then pl else
let pars = List.make n (CAst.make ?loc @@ CPatAtom None) in
- List.rev_append pars pl in
+ List.rev_append pars pl
+ in
let (_,argscs) = find_remaining_scopes [] pl head in
let pats = List.map2 (in_pat_sc scopes) argscs pl in
- DAst.make ?loc @@ RCPatCstr(head, [], pats)
+ DAst.make ?loc @@ RCPatCstr(head, pats, [])
end
| CPatCstr (head, None, pl) ->
begin
diff --git a/interp/notation.ml b/interp/notation.ml
index e282d62396..c4e9496b95 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -293,7 +293,12 @@ let key_compare k1 k2 = match k1, k2 with
module KeyOrd = struct type t = key let compare = key_compare end
module KeyMap = Map.Make(KeyOrd)
-type notation_rule = interp_rule * interpretation * int option
+type notation_applicative_status =
+ | AppBoundedNotation of int
+ | AppUnboundedNotation
+ | NotAppNotation
+
+type notation_rule = interp_rule * interpretation * notation_applicative_status
let keymap_add key interp map =
let old = try KeyMap.find key map with Not_found -> [] in
@@ -329,13 +334,14 @@ let cases_pattern_key c = match DAst.get c with
| _ -> Oth
let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
- | NApp (NRef ref,args) -> RefKey(canonical_gr ref), Some (List.length args)
+ | NApp (NRef ref,args) -> RefKey(canonical_gr ref), AppBoundedNotation (List.length args)
| NList (_,_,NApp (NRef ref,args),_,_)
| NBinderList (_,_,NApp (NRef ref,args),_,_) ->
- RefKey (canonical_gr ref), Some (List.length args)
- | NRef ref -> RefKey(canonical_gr ref), None
- | NApp (_,args) -> Oth, Some (List.length args)
- | _ -> Oth, None
+ RefKey (canonical_gr ref), AppBoundedNotation (List.length args)
+ | NRef ref -> RefKey(canonical_gr ref), NotAppNotation
+ | NApp (_,args) -> Oth, AppBoundedNotation (List.length args)
+ | NList (_,_,NApp (NVar x,_),_,_) when x = Notation_ops.ldots_var -> Oth, AppUnboundedNotation
+ | _ -> Oth, NotAppNotation
(** Dealing with precedences *)
diff --git a/interp/notation.mli b/interp/notation.mli
index c39bfa6e28..05ddd25a62 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -239,7 +239,12 @@ val declare_uninterpretation : interp_rule -> interpretation -> unit
val interp_notation : ?loc:Loc.t -> notation -> subscopes ->
interpretation * (notation_location * scope_name option)
-type notation_rule = interp_rule * interpretation * int option
+type notation_applicative_status =
+ | AppBoundedNotation of int
+ | AppUnboundedNotation
+ | NotAppNotation
+
+type notation_rule = interp_rule * interpretation * notation_applicative_status
(** Return the possible notations for a given term *)
val uninterp_notations : 'a glob_constr_g -> notation_rule list
diff --git a/lib/objFile.ml b/lib/objFile.ml
index 96db51a010..26367aaffa 100644
--- a/lib/objFile.ml
+++ b/lib/objFile.ml
@@ -182,7 +182,7 @@ let open_in ~file =
let version = input_int32 ch in
let () =
if not (Int32.equal magic magic_number) then
- let e = { filename = file; actual = version; expected = magic_number } in
+ let e = { filename = file; actual = magic; expected = magic_number } in
raise (Bad_magic_number e)
in
let () =
diff --git a/lib/system.ml b/lib/system.ml
index e25f758865..1aadaf6d3a 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -239,9 +239,12 @@ let intern_state magic filename =
let with_magic_number_check f a =
try f a
with
- | Bad_magic_number {filename=fname; _} ->
+ | Bad_magic_number {filename=fname; actual; expected} ->
CErrors.user_err ~hdr:"with_magic_number_check"
- (str"File " ++ str fname ++ strbrk" is corrupted.")
+ (str"File " ++ str fname ++ strbrk" has bad magic number " ++
+ (str @@ Int32.to_string actual) ++ str" (expected " ++ (str @@ Int32.to_string expected) ++ str")." ++
+ spc () ++
+ strbrk "It is corrupted or was compiled with another version of Coq.")
| Bad_version_number {filename=fname;actual=actual;expected=expected} ->
CErrors.user_err ~hdr:"with_magic_number_check"
(str"File " ++ str fname ++ strbrk" has bad version number " ++
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 400acc25b6..2feae8cc25 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1334,6 +1334,12 @@ let thin_evars env sigma sign c =
let c' = applyrec (env,0) c in
(!sigma, c')
+exception NotFoundInstance of exn
+let () = CErrors.register_handler (function
+ | NotFoundInstance e ->
+ Some Pp.(str "Failed to instantiate evar: " ++ CErrors.print e)
+ | _ -> None)
+
let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
try
let evi = Evd.find_undefined evd evk in
@@ -1478,7 +1484,9 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
List.exists (fun c -> isVarId evd id (EConstr.of_constr c)) l ->
instantiate_evar evar_unify flags env_rhs evd ev vid
| _ -> evd)
- with e -> user_err (Pp.str "Cannot find an instance")
+ with e when CErrors.noncritical e ->
+ let e, info = Exninfo.capture e in
+ Exninfo.iraise (NotFoundInstance e, info)
else
((if debug_ho_unification () then
let evi = Evd.find evd evk in
diff --git a/test-suite/bugs/closed/bug_12534.v b/test-suite/bugs/closed/bug_12534.v
new file mode 100644
index 0000000000..a55515feb6
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12534.v
@@ -0,0 +1,9 @@
+Record C {PROP: Prop} (P : PROP) : Type := { c : unit}.
+Check fun '{|c:=x|} => tt. (* Fine *)
+Arguments Build_C {_ _} _.
+Check fun '(Build_C _) => tt. (* Works. Note: just 1 argument! *)
+Check fun '{|c:=x|} => tt.
+(* Error: The constructor @Build_C (in type @C) expects 1 argument. *)
+
+Set Asymmetric Patterns.
+Check fun '{|c:=x|} => tt.
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 53ad8a9612..90a6a2ad96 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -80,6 +80,12 @@ NIL : list nat
: Z * Z * (Z * Z) * (Z * Z) * (Z * bool * (Z * bool) * (Z * bool))
fun f : Z -> Z -> Z -> Z => {|f; 0; 1; 2|} : Z
: (Z -> Z -> Z -> Z) -> Z
+{|fun x : Z => x + x; 0|}
+ : Z
+{|op; 0; 1|}
+ : Z
+false = 0
+ : Prop
Init.Nat.add
: nat -> nat -> nat
S
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index 7d2f1e9ba8..d0b2f40f9c 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -216,13 +216,32 @@ Check [|0*(1,2,3);(4,5,6)*false|].
(**********************************************************************)
(* Test recursive notations involving applications *)
-(* Caveat: does not work for applied constant because constants are *)
-(* classified as notations for the particular constant while this *)
-(* generic application notation is classified as generic *)
+
+Module Application.
Notation "{| f ; x ; .. ; y |}" := ( .. (f x) .. y).
+
+(* Application to a variable *)
+
Check fun f => {| f; 0; 1; 2 |} : Z.
+(* Application to a fun *)
+
+Check {| (fun x => x+x); 0 |}.
+
+(* Application to a reference *)
+
+Axiom op : Z -> Z -> Z.
+Check {| op; 0; 1 |}.
+
+(* Interaction with coercion *)
+
+Axiom c : Z -> bool.
+Coercion c : Z >-> bool.
+Check false = {| c; 0 |}.
+
+End Application.
+
(**********************************************************************)
(* Check printing of notations from other modules *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 23:54:32 +0000