aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES.md2
-rw-r--r--dev/ci/ci-common.sh21
-rwxr-xr-xdev/lint-repository.sh13
-rw-r--r--dev/top_printers.dbg2
-rw-r--r--doc/sphinx/proof-engine/ltac.rst9
-rw-r--r--plugins/ltac/tacinterp.ml43
-rw-r--r--test-suite/output/Errors.v2
-rw-r--r--test-suite/output/FunExt.out7
-rw-r--r--test-suite/output/TypeclassDebug.out1
-rw-r--r--test-suite/output/bug5778.v1
-rw-r--r--test-suite/output/bug6404.v1
-rw-r--r--test-suite/output/ltac.v2
-rw-r--r--test-suite/output/ltac_missing_args.v2
-rw-r--r--test-suite/output/ssr_clear.out1
-rw-r--r--test-suite/output/ssr_explain_match.out1
15 files changed, 73 insertions, 35 deletions
diff --git a/CHANGES.md b/CHANGES.md
index 08519eb1fb..d0774276ad 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -95,6 +95,8 @@ Tactics
by posing the specifying equation for `Z.div` and `Z.modulo` before
replacing them with atoms.
+- Ltac backtraces can be turned on using the "Ltac Backtrace" option.
+
Vernacular commands
- `Combined Scheme` can now work when inductive schemes are generated in sort
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index a5aa54144c..b4d2a9ca4e 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -62,27 +62,30 @@ git_download()
{
local PROJECT=$1
local DEST="$CI_BUILD_DIR/$PROJECT"
+ local GITURL_VAR="${PROJECT}_CI_GITURL"
+ local GITURL="${!GITURL_VAR}"
+ local REF_VAR="${PROJECT}_CI_REF"
+ local REF="${!REF_VAR}"
if [ -d "$DEST" ]; then
echo "Warning: download and unpacking of $PROJECT skipped because $DEST already exists."
elif [ "$FORCE_GIT" = "1" ] || [ "$CI" = "" ]; then
- local GITURL_VAR="${PROJECT}_CI_GITURL"
- local GITURL="${!GITURL_VAR}"
- local REF_VAR="${PROJECT}_CI_REF"
- local REF="${!REF_VAR}"
git clone "$GITURL" "$DEST"
cd "$DEST"
git checkout "$REF"
else # When possible, we download tarballs to reduce bandwidth and latency
local ARCHIVEURL_VAR="${PROJECT}_CI_ARCHIVEURL"
local ARCHIVEURL="${!ARCHIVEURL_VAR}"
- local REF_VAR="${PROJECT}_CI_REF"
- local REF="${!REF_VAR}"
mkdir -p "$DEST"
cd "$DEST"
- wget "$ARCHIVEURL/$REF.tar.gz"
- tar xvfz "$REF.tar.gz" --strip-components=1
- rm -f "$REF.tar.gz"
+ local COMMIT=$(git ls-remote "$GITURL" "refs/heads/$REF" | cut -f 1)
+ if [[ "$COMMIT" == "" ]]; then
+ # $REF must have been a tag or hash, not a branch
+ COMMIT="$REF"
+ fi
+ wget "$ARCHIVEURL/$COMMIT.tar.gz"
+ tar xvfz "$COMMIT.tar.gz" --strip-components=1
+ rm -f "$COMMIT.tar.gz"
fi
}
diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh
index f588c20d02..2e8a7455de 100755
--- a/dev/lint-repository.sh
+++ b/dev/lint-repository.sh
@@ -9,10 +9,17 @@
CODE=0
-# We assume that all merge commits are from the main branch
+if [[ $(git log -n 1 --pretty='format:%s') == "Bot merge"* ]]; then
+ # The FIRST parent of bot merges is from the PR, the second is
+ # current master
+ head=$(git rev-parse HEAD~)
+else
+ head=$(git rev-parse HEAD)
+fi
+
+# We assume that all non-bot merge commits are from the main branch
# For Coq it is extremely rare for this assumption to be broken
-read -r base < <(git log -n 1 --merges --pretty='format:%H')
-head=$(git rev-parse HEAD)
+read -r base < <(git log -n 1 --merges --pretty='format:%H' "$head")
dev/lint-commits.sh "$base" "$head" || CODE=1
diff --git a/dev/top_printers.dbg b/dev/top_printers.dbg
index eab88c7290..a6ecec7e33 100644
--- a/dev/top_printers.dbg
+++ b/dev/top_printers.dbg
@@ -70,8 +70,6 @@ install_printer Top_printers.ppevar_universe_context
install_printer Top_printers.ppconstraints
install_printer Top_printers.ppuniverseconstraints
install_printer Top_printers.ppuniverse_context_future
-install_printer Top_printers.ppcumulativity_info
-install_printer Top_printers.ppabstract_cumulativity_info
install_printer Top_printers.ppuniverses
install_printer Top_printers.ppnamedcontextval
install_printer Top_printers.ppenv
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 4f486a777d..c134563efe 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -1162,6 +1162,15 @@ Printing |Ltac| tactics
Debugging |Ltac| tactics
------------------------
+Backtraces
+~~~~~~~~~~
+
+.. flag:: Ltac Backtrace
+
+ Setting this flag displays a backtrace on Ltac failures that can be useful
+ to find out what went wrong. It is disabled by default for performance
+ reasons.
+
Info trace
~~~~~~~~~~
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 62906303a4..30f716d764 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -117,9 +117,14 @@ let combine_appl appl1 appl2 =
let of_tacvalue v = in_gen (topwit wit_tacvalue) v
let to_tacvalue v = out_gen (topwit wit_tacvalue) v
+let log_trace = ref false
+
+let is_traced () =
+ !log_trace || !Flags.profile_ltac
+
(** More naming applications *)
let name_vfun appl vle =
- if has_type vle (topwit wit_tacvalue) then
+ if is_traced () && has_type vle (topwit wit_tacvalue) then
match to_tacvalue vle with
| VFun (appl0,trace,lfun,vars,t) -> of_tacvalue (VFun (combine_appl appl0 appl,trace,lfun,vars,t))
| _ -> vle
@@ -137,9 +142,11 @@ type interp_sign = Geninterp.interp_sign = {
lfun : value Id.Map.t;
extra : TacStore.t }
-let extract_trace ist = match TacStore.get ist.extra f_trace with
-| None -> []
-| Some l -> l
+let extract_trace ist =
+ if is_traced () then match TacStore.get ist.extra f_trace with
+ | None -> []
+ | Some l -> l
+ else []
let print_top_val env v = Pptactic.pr_value Pptactic.ltop v
@@ -161,8 +168,11 @@ let catch_error call_trace f x =
let e = CErrors.push e in
catching_error call_trace iraise e
+let wrap_error tac k =
+ if is_traced () then Proofview.tclORELSE tac k else tac
+
let catch_error_tac call_trace tac =
- Proofview.tclORELSE
+ wrap_error
tac
(catching_error call_trace (fun (e, info) -> Proofview.tclZERO ~info e))
@@ -203,9 +213,11 @@ let constr_of_id env id =
(** Generic arguments : table of interpretation functions *)
(* Some of the code further down depends on the fact that push_trace does not modify sigma (the evar map) *)
-let push_trace call ist = match TacStore.get ist.extra f_trace with
-| None -> Proofview.tclUNIT [call]
-| Some trace -> Proofview.tclUNIT (call :: trace)
+let push_trace call ist =
+ if is_traced () then match TacStore.get ist.extra f_trace with
+ | None -> Proofview.tclUNIT [call]
+ | Some trace -> Proofview.tclUNIT (call :: trace)
+ else Proofview.tclUNIT []
let propagate_trace ist loc id v =
if has_type v (topwit wit_tacvalue) then
@@ -1263,7 +1275,7 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
let fold accu (id, v) = Id.Map.add id v accu in
let newlfun = List.fold_left fold olfun extfun in
if List.is_empty lvar then
- begin Proofview.tclORELSE
+ begin wrap_error
begin
let ist = {
lfun = newlfun;
@@ -1423,7 +1435,7 @@ and interp_match_successes lz ist s =
(* Interprets the Match expressions *)
and interp_match ist lz constr lmr =
let (>>=) = Ftactic.bind in
- begin Proofview.tclORELSE
+ begin wrap_error
(interp_ltac_constr ist constr)
begin function
| (e, info) ->
@@ -1509,7 +1521,7 @@ and interp_genarg_var_list ist x =
(* Interprets tactic expressions : returns a "constr" *)
and interp_ltac_constr ist e : EConstr.t Ftactic.t =
let (>>=) = Ftactic.bind in
- begin Proofview.tclORELSE
+ begin wrap_error
(val_interp ist e)
begin function (err, info) -> match err with
| Not_found ->
@@ -2076,4 +2088,13 @@ let () =
optread = (fun () -> get_debug () != Tactic_debug.DebugOff);
optwrite = vernac_debug }
+let () =
+ let open Goptions in
+ declare_bool_option
+ { optdepr = false;
+ optname = "Ltac Backtrace";
+ optkey = ["Ltac"; "Backtrace"];
+ optread = (fun () -> !log_trace);
+ optwrite = (fun b -> log_trace := b) }
+
let () = Hook.set Vernacentries.interp_redexp_hook interp_redexp
diff --git a/test-suite/output/Errors.v b/test-suite/output/Errors.v
index edc35f17b4..b52537dec0 100644
--- a/test-suite/output/Errors.v
+++ b/test-suite/output/Errors.v
@@ -1,6 +1,8 @@
(* coq-prog-args: ("-top" "Errors") *)
(* Test error messages *)
+Set Ltac Backtrace.
+
(* Test non-regression of bug fixed in r13486 (bad printer for module names) *)
Module Type S.
diff --git a/test-suite/output/FunExt.out b/test-suite/output/FunExt.out
index 8d2a125c1d..2a823396d5 100644
--- a/test-suite/output/FunExt.out
+++ b/test-suite/output/FunExt.out
@@ -1,19 +1,12 @@
The command has indeed failed with message:
-Ltac call to "extensionality in (var)" failed.
Tactic failure: Not an extensional equality.
The command has indeed failed with message:
-Ltac call to "extensionality in (var)" failed.
Tactic failure: Not an extensional equality.
The command has indeed failed with message:
-Ltac call to "extensionality in (var)" failed.
Tactic failure: Not an extensional equality.
The command has indeed failed with message:
-Ltac call to "extensionality in (var)" failed.
Tactic failure: Not an extensional equality.
The command has indeed failed with message:
-Ltac call to "extensionality in (var)" failed.
Tactic failure: Already an intensional equality.
The command has indeed failed with message:
-In nested Ltac calls to "extensionality in (var)" and
-"clearbody (ne_var_list)", last call failed.
Hypothesis e depends on the body of H'
diff --git a/test-suite/output/TypeclassDebug.out b/test-suite/output/TypeclassDebug.out
index 8b38fe0ff4..7ea7a08cb3 100644
--- a/test-suite/output/TypeclassDebug.out
+++ b/test-suite/output/TypeclassDebug.out
@@ -14,5 +14,4 @@ Debug: 1.1-1.1-1.1-1.1-1: looking for foo without backtracking
Debug: 1.1-1.1-1.1-1.1-1.1: simple apply H on foo, 1 subgoal(s)
Debug: 1.1-1.1-1.1-1.1-1.1-1 : foo
The command has indeed failed with message:
-Ltac call to "typeclasses eauto (int_or_var_opt) with (ne_preident_list)" failed.
Tactic failure: Proof search reached its limit.
diff --git a/test-suite/output/bug5778.v b/test-suite/output/bug5778.v
index 0dcd76aeff..441e87af84 100644
--- a/test-suite/output/bug5778.v
+++ b/test-suite/output/bug5778.v
@@ -1,3 +1,4 @@
+Set Ltac Backtrace.
Ltac a _ := pose (I : I).
Ltac b _ := a ().
Ltac abs _ := abstract b ().
diff --git a/test-suite/output/bug6404.v b/test-suite/output/bug6404.v
index bbe6b1a00f..d9e5e20b66 100644
--- a/test-suite/output/bug6404.v
+++ b/test-suite/output/bug6404.v
@@ -1,3 +1,4 @@
+Set Ltac Backtrace.
Ltac a _ := pose (I : I).
Ltac b _ := a ().
Ltac abs _ := transparent_abstract b ().
diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v
index 40e743c3f0..fcd5dd05f0 100644
--- a/test-suite/output/ltac.v
+++ b/test-suite/output/ltac.v
@@ -1,3 +1,5 @@
+Set Ltac Backtrace.
+
(* This used to refer to b instead of z sometimes between 8.4 and 8.5beta3 *)
Goal True.
Fail let T := constr:((fun a b : nat => a+b) 1 1) in
diff --git a/test-suite/output/ltac_missing_args.v b/test-suite/output/ltac_missing_args.v
index 91331a1de5..e30c97aac6 100644
--- a/test-suite/output/ltac_missing_args.v
+++ b/test-suite/output/ltac_missing_args.v
@@ -1,3 +1,5 @@
+Set Ltac Backtrace.
+
Ltac foo x := idtac x.
Ltac bar x := fun y _ => idtac x y.
Ltac baz := foo.
diff --git a/test-suite/output/ssr_clear.out b/test-suite/output/ssr_clear.out
index 1515954060..1a0f90493e 100644
--- a/test-suite/output/ssr_clear.out
+++ b/test-suite/output/ssr_clear.out
@@ -1,3 +1,2 @@
The command has indeed failed with message:
-Ltac call to "move (ssrmovearg) (ssrclauses)" failed.
No assumption is named NO_SUCH_NAME
diff --git a/test-suite/output/ssr_explain_match.out b/test-suite/output/ssr_explain_match.out
index 32cfb354bf..0f68ab0b02 100644
--- a/test-suite/output/ssr_explain_match.out
+++ b/test-suite/output/ssr_explain_match.out
@@ -51,5 +51,4 @@ instance: (addnC y x) matches: (x + y)
instance: (addnC y x) matches: (x + y)
END INSTANCES
The command has indeed failed with message:
-Ltac call to "ssrinstancesoftpat (cpattern)" failed.
Not supported
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 01:43:58 +0000