aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitlab-ci.yml7
-rw-r--r--dev/ci/ci-common.sh8
-rwxr-xr-xdev/ci/ci-compcert.sh4
-rwxr-xr-xdev/ci/ci-vst.sh2
-rwxr-xr-xdev/tools/make-changelog.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--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
17 files changed, 113 insertions, 26 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 819ad8a214..3b95800f0d 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -751,6 +751,7 @@ library:ci-fiat_crypto:
dependencies:
- build:edge+flambda
- library:ci-coqprime
+ - plugin:ci-bignums
- plugin:ci-rewriter
library:ci-fiat_crypto_legacy:
@@ -765,9 +766,15 @@ library:ci-fiat_crypto_ocaml:
stage: stage-5
needs:
- build:edge+flambda
+ - library:ci-coqprime
+ - plugin:ci-bignums
+ - plugin:ci-rewriter
- library:ci-fiat_crypto
dependencies:
- build:edge+flambda
+ - library:ci-coqprime
+ - plugin:ci-bignums
+ - plugin:ci-rewriter
- library:ci-fiat_crypto
library:ci-flocq:
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index f0dbe485f7..c01bc57f72 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -37,17 +37,19 @@ export PATH="$COQBIN:$PATH"
# Coq's tools need an ending slash :S, we should fix them.
export COQBIN="$COQBIN/"
-ls "$COQBIN"
+ls -l "$COQBIN"
# Where we download and build external developments
CI_BUILD_DIR="$PWD/_build_ci"
+ls -l "$CI_BUILD_DIR" || true
+
+set +x
for overlay in "${ci_dir}"/user-overlays/*.sh; do
# shellcheck source=/dev/null
. "${overlay}"
done
-set +x
# shellcheck source=ci-basic-overlay.sh
. "${ci_dir}/ci-basic-overlay.sh"
set -x
@@ -84,7 +86,7 @@ git_download()
COMMIT="$REF"
fi
wget "$ARCHIVEURL/$COMMIT.tar.gz"
- tar xvfz "$COMMIT.tar.gz" --strip-components=1
+ tar xfz "$COMMIT.tar.gz" --strip-components=1
rm -f "$COMMIT.tar.gz"
fi
}
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/dev/tools/make-changelog.sh b/dev/tools/make-changelog.sh
index de58527cca..413433ef41 100755
--- a/dev/tools/make-changelog.sh
+++ b/dev/tools/make-changelog.sh
@@ -28,7 +28,7 @@ esac
printf "Fixes? (space separated list of bug numbers)\n"
read -r fixes_list
-fixes_string="$(echo $fixes_list | sed 's/ /~ and /g; s,\([0-9]\+\),`#\1 <https://github.com/coq/coq/issues/\1>`_,g' | tr '~' '\n')"
+fixes_string="$(echo $fixes_list | sed 's/ /~ and /g; s,\([0-9][0-9]*\),`#\1 <https://github.com/coq/coq/issues/\1>`_,g' | tr '~' '\n')"
if [ ! -z "$fixes_string" ]; then fixes_string="$(printf '\n fixes %s,' "$fixes_string")"; fi
# shellcheck disable=SC2016
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/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-01 16:14:50 +0000