No tests for tagged releases

[wenkokke]

No tests for tagged releases

[andreasabel]

Yeah, stripping all tests is something that I have had my doubts in. We should at least ship some basic test suites that do elementary validation of the core functionality (e.g. can process a sample agda file that contains a tour through the features).

I have done some work in 2021 towards running the testsuite also under Windows:

• #5549

However, I didn't really think we should ship our whole testsuite that takes 2 hours to run...

Isolating a small shippable testsuite would be the path I'd take here.

[wenkokke]

Two hours?!

realizes she's never run the test suite

[wenkokke]

My current approach to test executables is to simply check the standard library, which I suppose achieves the goal of making sure the executable works... but I was hoping for something that covers a few more odd edge cases.

[andreasabel]

(@UlfNorell says: installing Agda is a minimal test of its functionality, because it invokes itself on the primitive modules.)

I am anyway for a small cabal test with a tour through the features...

[wenkokke]

(@UlfNorell says: installing Agda is a minimal test of its functionality, because it invokes itself on the primitive modules.)

I am anyway for a small cabal test with a tour through the features...

That's really only true if I'm building Agda from source, not if I'm running pip install agda.