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?
can't launch CoqIde
110 views Asked by Huan Sun At
1
There are 1 answers
Related Questions in COQ
- CoqIDE loadpath error for ssreflect
- How to assign a natural number to variable in Coq?
- Handling let in hypothesis
- Sum of exponents with same base
- How to run Athena | Coq | Isabelle codes remotely?
- Is equality decidable on any coinductive type?
- Coq "convoy pattern"
- In coq, how to do "induction n eqn: Hn" in a way that doesn't mess up the inductive hypothesis?
- Pattern matching multiple constructors in a single clause in Coq
- How to use Coq GenericMinMax to prove facts about the reals
- what does the colon greater than sign mean in coq
- Subtyping in Coq
- How to write coq definitions with "subtypes"
- Stronger completeness axiom for real numbers in Coq
- When is the first input to `list_rec` not a constant function?
Related Questions in FORMAL-VERIFICATION
- Primitive operations in proofs
- Agda: proving that, when values are equal, their constructor arguments are equal
- Promela system with unranged values
- how to apply separation logic "lookup" rule
- C# static array bound check
- Code Contracts failing example Graph.Remove(Edge e)
- Should I use computer-aided verification tools?
- is there any tactic in Coq that can transform a bool expression to a Prop one?
- Coq error: Unable to unify "true" with "is_true (0 < a - b - 3)"
- In Yosys I am getting a Warning saying Literal has a width of 8 bit, can anyone elaborate on it
- If two constructor expressions of an inductive type are equal in Coq, can I do rewriting based on their corresponding arguments?
- Can I use destruct here given the constraint I have for index range of a list?
- How can I build a list of bytes from its specification in Coq
- How to pass Induction in SymbiYosys?
- Why this dafny post-condition is not inferred?
Related Questions in FORMAL-METHODS
- Automated tools for applying formal methods to verify security policy in existing software
- Why are the set of variables in lambda calculus typically defined as countable infinite?
- Is this TLA+ specification correct?
- Where to get hardware model data?
- Problem with predicate in Alloy
- How to write bigvee and big wedge in Isabelle
- Why this dafny post-condition is not inferred?
- Formal Methods (Z-notation) - adding a new multiple relation
- how to solve the undetermined issue in a let-such-that expression in Dafny?
- How to capture a change in an element of an array in TLA+
- Dafny verification fails "post condition might not hold"
- UPPAAL chooses to loop on instead of a transition of a higher priority
- Formal Methods, Logic and VDM past exam paper questions
- Proving correctness in formal logic
- Potential aliasing violation in swap array indexes SPARK-Ada
Related Questions in COQIDE
- How to prove this in Coq
- Importing a Module in Coq
- Is there a way to redirect Coqide messages and errors to the same output?
- How to avoid "Cannot guess decreasing argument of fix." in Coq
- Warning : “Set this option from the IDE menu instead” in coq
- Concatenation of 2 lists in lambda-calculus
- how to create a polymorphe couple such as "( a : type A, b : type B ) " in lambda-calculus
- How to activate the Coq messages in vscode/vscoq like in the CoqIde/jscoq?
- How to write intermediate proof statements inside Coq - similar to how in Isar one has `have Statement using Lemma1, Lemma2 by auto` but in Coq?
- How to Import Coq library HoTT in CoqIde
- can't launch CoqIde
- Coqide does not see global clipboard in wsl
- How to prove this DeMorgan law without using automation tactics in Coq?
- Error: Cannot interpret this number as a value of type nat
- VSCoq ProofView not printing
Popular Questions
- How do I undo the most recent local commits in Git?
- How can I remove a specific item from an array in JavaScript?
- How do I delete a Git branch locally and remotely?
- Find all files containing a specific text (string) on Linux?
- How do I revert a Git repository to a previous commit?
- How do I create an HTML button that acts like a link?
- How do I check out a remote Git branch?
- How do I force "git pull" to overwrite local files?
- How do I list all files of a directory?
- How to check whether a string contains a substring in JavaScript?
- How do I redirect to another webpage?
- How can I iterate over rows in a Pandas DataFrame?
- How do I convert a String to an int in Java?
- Does Python have a string 'contains' substring method?
- How do I check if a string contains a specific word?
Trending Questions
- UIImageView Frame Doesn't Reflect Constraints
- Is it possible to use adb commands to click on a view by finding its ID?
- How to create a new web character symbol recognizable by html/javascript?
- Why isn't my CSS3 animation smooth in Google Chrome (but very smooth on other browsers)?
- Heap Gives Page Fault
- Connect ffmpeg to Visual Studio 2008
- Both Object- and ValueAnimator jumps when Duration is set above API LvL 24
- How to avoid default initialization of objects in std::vector?
- second argument of the command line arguments in a format other than char** argv or char* argv[]
- How to improve efficiency of algorithm which generates next lexicographic permutation?
- Navigating to the another actvity app getting crash in android
- How to read the particular message format in android and store in sqlite database?
- Resetting inventory status after order is cancelled
- Efficiently compute powers of X in SSE/AVX
- Insert into an external database using ajax and php : POST 500 (Internal Server Error)
On Windows the user configuration files of CoqIDE are in:
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
coqidercin this folder (or fix it with a text editor).