如何将Coqide消息与错误重定向至同一输出并批量记录？

你遇到的问题核心是coqc会在错误处终止，而Coqide的默认输出无法完整保留目标和错误信息，以下是几个可行的解决办法：

方案一：用coqtop+脚本自动化处理 #

利用coqtop的交互特性，结合脚本批量发送命令，即使tactic失败也能继续执行后续目标，同时捕获所有输出。

示例shell脚本：

#!/bin/bash

# 定义要测试的目标集合
targets=(
  "Theorem test1: 1 = 2. Proof."
  "Theorem test2: forall n:nat, n = S n. Proof."
)

# 启动coqtop并批量执行命令
coqtop -batch -quiet << EOF
Require Import Arith.
$(for t in "${targets[@]}"; do
  echo "$t"
  echo "Show."          # 打印当前目标
  echo "Fail my_tactic."# 用Fail捕获错误，避免进程终止
  echo "Admitted."
done)
EOF

运行脚本时将结果重定向到日志文件：

./run_tactics.sh > tactic_errors.log

Fail命令会执行指定tactic并输出错误信息，但不会终止Coq进程，所有目标和错误都会被写入日志。

方案二：自定义tactic记录目标与错误 #

通过Coq的Ltac2编写辅助tactic，自动打印当前目标、捕获错误并写入文件。

在你的Coq文件中添加以下代码：

Require Import Ltac2.Ltac2.

Ltac2 record_error (t : unit -> unit) :=
  let current_goal := Message.of_goal (Goal.goal ()) in
  Message.print current_goal;  (* 打印目标到Messages面板 *)
  try
    t ()
  with
  | Tac2Error err =>
    let err_msg := Message.of_string (Tac2Error.to_string err) in
    Message.print err_msg;
    (* 将信息追加到日志文件 *)
    let _ := Sys.command ("echo 'Goal: " ^ Message.to_string current_goal ^ "' >> tactic_log.txt") in
    let _ := Sys.command ("echo 'Error: " ^ Tac2Error.to_string err ^ "' >> tactic_log.txt") in
    let _ := Sys.command ("echo '-------------------------' >> tactic_log.txt") in
    ()
.

(* 使用示例 *)
Theorem test1: 1 = 2.
Proof.
record_error (fun _ => my_tactic).
Admitted.

Theorem test2: forall n:nat, n = S n.
Proof.
record_error (fun _ => my_tactic).
Admitted.

用coqc -q your_file.v执行，或在Coqide中全选运行，所有目标和错误会同时显示在Messages面板，并写入tactic_log.txt文件。

方案三：优化Coqide的使用方式 #

如果你偏好Coqide，可通过以下方式解决现有问题：

• 保留目标输出：替换Show命令为自定义打印逻辑（如方案二中的Message.of_goal），确保目标信息留在Messages标签页。
• 复制错误内容：右键点击Errors标签页的空白区域，选择「Copy All」即可复制所有错误信息；若该选项不可用，可启动Coqide时添加--debug参数，Coq会生成包含所有输出的调试日志文件。

内容的提问来源于stack exchange，提问作者Arjun Viswanathan