After installing ssreflect, its libraries for Coq are installed in /usr/local/lib/coq/user-contrib/theories. When ever I want to import libraries of ssreflect in CoqIDE (ssrcoqide), I get the following error messages:
There are two ways to solve this problem. I don't know which one is better.
Error: The file /usr/local/lib/coq/user-contrib/theories/ssreflect.vo
contains library ssreflect and not library theories.ssreflect
Error: The file /usr/local/lib/coq/user-contrib/theories/eqtype.vo
contains library eqtype and not library theories.eqtype
......
There are two ways to solve this problem. I don't know which one is better.
Method 1
Move all the ssreflect libraries for Coq from /usr/local/lib/coq/user-contrib/theories to /usr/local/lib/coq/user-contrib.
Method 2
Add "-I /usr/local/lib/coq/user-contrib/theories" to launch ssrcoq and ssrcoqide. Actually, I rename ssrcoq and ssrcoqide to ssrcoq.opt and ssrcoqide.opt respectively, and use the following two scripts to launch them.
The script /usr/local/bin/ssrcoq:
#!/bin/bash
/usr/local/bin/ssrcoq.opt -I /usr/local/lib/coq/user-contrib/theories $*
The script /usr/local/bin/ssrcoqide:
#!/bin/bash
/usr/local/bin/ssrcoqide.opt -I /usr/local/lib/coq/user-contrib/theories $*
0 意見:
張貼留言