我想在Coq中编写和调试代码，就像在Python、R等中编写代码一样。具体来说。
我有一个终端窗口 code.v 文件被显示出来，例如
Definition double (x:nat) : nat := 2 * x.
Definition tripple (x:nat) : nat := 3 * x.
现在在另一个终端上，我想有一个交互式的shell，它可以接受命令，从一个... code.v、检查等。比如说
Load code.v // What's the command for this?
Print double. // Expect to see output "double : nat -> nat"
问题一： 什么样的命令提供给我这样的交互式shell，我应该在交互式shell中执行什么命令来加载文件？
另外，如果在我的 code.v 文件中我有一个未完成的证明，如
Lemma ex4: forall (X : Set) (P : X -> Prop),
~(forall x, ~ (P x)) -> (exists x, (P x)).
Proof.
intros X P A.
apply not_all_ex_not in A.
destruct A.
问题2: 有没有一个交互式的shell命令，比如 check code.v 这将打印出我的证明状态，就像Coqide一样，当你按下 ctrl+down
1 subgoal
X : Set
P : X -> Prop
x : X
H : ~ ~ P x
______________________________________(1/1)
exists x0 : X, P x0
请注意，我更喜欢通过linux终端来完成一切，而不是使用IDE。
通常如果你安装了 coq 和 coqide 通过通常的方式，你应该有一个叫做 coqtop (它是 coq toplevel 的简写)。 它读取所有来自 stdin 并打印所有结果（通常会进入目标或响应窗口的 coqide)在 stdout.
以你的例子 code.v 你可以运行以下命令。
coqtop -require-import Classical < code.v
这将显示文件中所有命令产生的所有输出并终止。 最后的输出将是最后一条命令的结果，从而可以看到最后一个打开的目标。 注意 -require-import Classical 是需要的，因为外稃 not_all_ex_not 是在该模块中定义的。
在实际操作中，这样做不是很方便，因为每次添加新的命令都要重新运行整个文件。 你也可以保持系统运行，效果是执行文件的 code.v 已经被记录下来，通过键入以下命令行。
coqtop -require-import Classical -load-vernac-source code.v
这不会显示最后一条命令后的目标，但你可以通过键入命令来要求它。Show. 然后你可以在终端中输入更多的命令来查看它们对状态的影响。coqtop 程序。 然后，你有责任记录下你发送给以下程序的命令 coqtop 以便日后复制证明。 用户界面如 coqide, proof-general 或 vscoq 主要是为了帮助你完成这个记录任务。
要了解更多信息，你应该输入
coqtop --help
您还应该考虑使用 coqtop 结合 rlwrap.