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

Please suggest example file for Coq Platform "smoke test kit" #106

Open MSoegtropIMC opened 3 years ago

MSoegtropIMC commented 3 years ago

I just added math-classes to Coq Platform (sorry for the long delay). In Coq Platform we have a so called "smoke test kit", which runs one or two example files from each package in order to test if the package has been properly installed. The example should test as much as possible, but shouldn't run longer than a few seconds (<10). Can you please suggest one or two files for this purpose?

Preferably the files should run with math-classes installed via opam without patching require statements and without -Q or -R options.

spitters commented 3 years ago

Perhaps take the files at the bottom of these hierarchies: https://math-classes.github.io/

E.g. https://github.com/coq-community/math-classes/blob/master/theory/dec_fields.v https://github.com/coq-community/math-classes/blob/master/interfaces/orders.v