search

coq-community / math-classes

A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia]
https://math-classes.github.io
MIT License
162 stars 43 forks source link

master branch undocumented dependency on BigNums #57

Closed Zdancewic closed 6 years ago

Zdancewic commented 6 years ago

Even after repairing the Stream dependencies (see: this issue), make fails with:

COQC implementations/ZType_integers.v
File "./implementations/ZType_integers.v", line 4, characters 2-23:
Error:
Cannot find a physical path bound to logical path matching suffix
Bignums.SpecViaZ.

There is an undocumented dependency on the BigNums package. After building and installing it, math-classes does compile.

spitters commented 6 years ago

Thanks for spotting this. The dependency is in the opam file: https://github.com/math-classes/math-classes/blob/master/opam

I'll add it to the README.

Zimmi48 commented 6 years ago

The README was updated.