search

idris-lang / Idris-dev

A Dependently Typed Functional Programming Language
http://idris-lang.org
Other
3.43k stars 643 forks source link

What should be allowed in the tests ipkg field? #4325

Open mpickering opened 6 years ago

mpickering commented 6 years ago

I am reading the documentation to understand what should be allowed to be in the tests field.

It seems that it is expected that the user provides list of functions defined in the current package in this list. However, it seems you can also specify functions, not in the package or any dependency of the package.

For example, the specdris package specifies test.SpecDris.SpecTest which is not a module of the main package but from a separate test package which the user has to install manually.

https://github.com/pheymann/specdris/blob/master/specdris.ipkg

Should this be allowed or is this use case dependent on the current implementation?

ahmadsalim commented 6 years ago

@jfdm Do you have an idea?

jfdm commented 6 years ago

The test field option was added by @david-christiansen. It's purpose, IIRC, was to provide a simple test harness (with tests written in IO) for Idris packages. Package authors were/are welcome to include and use their ow,n more advanced, test suites to enhance the set of tests run.

For me the described behaviour by @mpickering is expected.