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).
- 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
- Is there an intuitionistic proof of `(A -> B \/ C) -> (A -> B) \/ (A -> C)`?
- InteractionTrees library - simple program on ASM
- What is the difference between Lemma and Theorem in Coq
- How to instruct `auto` to simplify the goal during proof search?
- Is is possible to rename a coq term?
- What are the practical limitations of a non-turing complete language like Coq?
- Coq : mutually recursive definitions with [mrec] in InteractionTrees Library
- Is there a function that returns a list of values with specific type in OCaml?
- Formualting a logic in farmer astronaught
- What's the correct setup for Kami (Coq framework for Bluespec) to be able to run on WSL Ubuntu?
- Coq: keeping information in a match statement
- Showing polynomial equality in coq/ssreflect
- Syntax of the case tactic in coq
- Understanding nat_ind2 in Logical Foundations