Hierarchy of tests

[amelieled]

This PR is about the hierarchy of tests (Issue #487 ). More details should be discussed.

[gabrielhdt]

Could you provide the hierarchy you are planning to implement in the pull request description? So that we can discuss it beforehand.

[amelieled]

Yes, of course @gabrielhdt ! :) So until now, I've done:

• parsing_tests/ (empty file and escaped identifier)
• queries_tests/ (assert / assertnot / type / compute)
• require_open_tests/ (require / require as / open / and paths)
• rule_tests/ (on rules : arity / free variable in LHS / patterns / non linearity / order instanciation performance )
• set_option_tests/ (test suite on set option)
• inductive_tests/ (on inductive types)
• symbol_tests/ (on symbols)
• tactics_tests/ (on tactics)
• term_tests/ (implicit argument / lambda construction / let construction / wildcard )

Maybe, I can add the name of testing files (for each category) in the file description_*.

Now, we need to discuss on files are listed on the file named "theory".

[amelieled]

Problems:

• Files which their name begins by a number (related to an issue so).
• Maybe we can create the folder "theory_tests" or "examples_tests" (or remove redundancies)
• I don't understand the goal of these testing files: bug0.dk bug2.dk bug.dk raphael.dk sujective.dk symbol.lp

[gabrielhdt]

Thanks @amelieled. I'm quite happy with your categories. I'll be picky, but I'd remove the suffix _test, because we know these are all tests, we're already in the tests folder... I'd rename require_open into require, rule into rewriting, perhaps symbol into declaration? Perhaps term into scoping?

Files which their name begins by a number (related to an issue so).

I'd put that into parsing I think. Or another system category. Or even create a miscellaneous category, don't bother, it will still be better than what we have.

Yes, examples would be fine I think.

For the remaining files, I'll have a look later, don't worry.

[amelieled]

I'll be picky, but I'd remove the suffix _test, because we know these are all tests, we're already in the tests folder...

Yes, sure! Same thing for "description_blabla".

I'd rename require_open into require,

import ? I think require could be ambiguous.

rule into rewriting,

Done.

perhaps symbol into declaration?

inductive and rule are declaration too?

Perhaps term into scoping?

Done.

Files which their name begins by a number (related to an issue so). I'd put that into parsing I think. Or another system category. Or even create a miscellaneous category, don't bother, it will still be better than what we have.

The problem is that it breaks the links on the "issue" discussions. Moreover, some of them are about parsing, or tactic, etc. One category for them doesn't seem satisfying.

Yes, examples would be fine I think.

Done.

[gabrielhdt]

import ? I think require could be ambiguous.

Indeed.

The problem is that it breaks the links on the "issue" discussions.

What do you mean?

One category for them doesn't seem satisfying.

Rome wasn't built in a day, as we say. It's not a big deal if we have some files not categorised yet.

[fblanqui]

I'm closing this PR because it is too old now.