'Running prover in why3 ,using coq - error
I run coq prover for why3 program and when I run it ,coq ide pops up.
Then I am trying to go forward one command, and immediately get this error Cannot find a physical path bound to logical path BuildIn on the first command Require Import BuiltIn..
Terminal from which I run why3 shows when I try to go forward Warning: Cannot open /usr/lib64/why3/coq [cannot-open-path,filesystem]
It is on Fedora Scientific, how to fix the problem, so I can conduct proofs.
Sources
This article follows the attribution requirements of Stack Overflow and is licensed under CC BY-SA 3.0.
Source: Stack Overflow
| Solution | Source |
|---|