can't launch CoqIde
Everything is fine until I changed the preferences -> Externals -> coqtop in CoqIde and then I found myself in trouble launching CoqIde as the picture shows. It seems that I wrote the wrong path in the coqtop. I have tried to reinstall the coqplatform and It seems useless. So how can I restart my CoqIde?
Solution
On Windows the user configuration files of CoqIDE are in:
C:\Users\<Yourname>\AppData\Local\coq
Please note that AppData is typically a hidden folder, so you can't see it. Either enable display of hidden folders in file explorer or use the console.
You need to delete the file coqiderc in this folder (or fix it with a text editor).
- Pigeonhole proof without decidable equality or excluded middle
- Why does Coq solve_in_Union tactic fail directly but works through assertion of identical goal?
- How to prove existence in COQ?
- How can I prove excluded middle with the given hypothesis (forall P Q : Prop, (P -> Q) -> (~P \/ Q))?
- Lemma cannot be used as a hint
- Unfolding an opaque fixpoint in Coq
- Ltac for deterministic rewriting/sorting of operands
- Can I use a tactics under `coqtop -nois`?
- What is to be used in place of exfalso omega?
- Casting a value from one fintype to another?
- How can we use the familiar notation of integer arithmetics in ssreflect?
- Stuck at a simple inequality of natural number proof in Coq
- Coq - VSCode highlight Compute command in blue
- Turn `P(?x)` into `exists x,P(x)` to give different instantiations for different subgoals in Coq
- Why doesn't Coq notation defined by other notation working well?
- "Cannot guess decreasing argument of fix" error when defining a Fixpoint for extracting the first half of a list
- Wrong Typeclass Instance used in Coq Proof
- Coq's Search command and modules
- How to make OCaml (or Coq) code from the llvmir code using vellvm framework
- Coq repeating "destruct" for disjunctive hypothesis causing unwanted destruction in the end
- Is there a lightweight way to define a mutable dictionary that can return all of its keys in Coq?
- Constructing proof terms inside a recursive function
- Coq notation defined inside a module expecting type without module prefix
- How does one implement Coq?
- Can a dependently typed language be Turing complete?
- Beta-reduction after delta-reduction in unfold tactic
- Equality for elements of sig type in Coq
- Defining mutually recursive types in Coq?
- How to mix sections with hints in Coq?
- Non-trivial Fixpoint on nested recursive types