Ssreflect Users Discussion List

[Stéphane Glondu <>]

Le 18/10/2010 15:05, Nils Jähnig a écrit :
> make[1]: *** Keine Regel vorhanden, um das Target
> »doc/common/styles/html/simple/styles.hva«,
>    benötigt von »doc/refman/styles.hva«, zu erstellen.  Schluss.

You get that because documentation files are stripped from the source 
package (because they violate DFSG).

> install: Aufruf von stat für „doc/refman/html/*“ nicht möglich: No
> such file or directory

Same issue.

> I'm not sure what fakeroot debian/rules binary is about. i found that
> it works similar to make, but get this error:

This is (one of) the command(s) run by dpkg-buildpackage when building 
the Debian package. It should work with any Debian source package.

> nils@mann:~/coq-8.2.pl1+dfsg$ fakeroot debian/rules binary
> debian/rules:17: /usr/share/ocaml/ocamlvars.mk: No such file or directory
> make: *** Keine Regel, um »/usr/share/ocaml/ocamlvars.mk« zu
> erstellen.  Schluss.

You should install dh-ocaml.

Actually, the standard way to build a Debian package from source is to 
use dpkg-buildpackage. This way, it checks for build-dependencies and 
would have failed with a more sensible error message.

> And, by the way, my normal CoqIde works.

Note: if you use the Debian packages (that are in Ubuntu as well) for 
coq 8.2 / ssreflect 1.2 (the last stable release of ssreflect AFAIK), 
you shouldn't need a ssrcoqide (it is automatically loaded).

And starting from coq 8.3, the ide *.cmi files are installed by Coq, so 
they are installed with the libcoq-ocaml-dev Debian package, so no need 
to do this gymnastic (but there is no release of ssreflect that works 
with coq 8.3 so far).


Best regards,

--
Stéphane