Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[ new ] golden testing framework #1518

Merged
merged 84 commits into from Jun 21, 2021
Merged

[ new ] golden testing framework #1518

merged 84 commits into from Jun 21, 2021

Conversation

gallais
Copy link
Member

@gallais gallais commented Jun 8, 2021 •
edited

This is a port of the Idris2 golden testing library: https://github.com/idris-lang/Idris2/tree/master/libs/test

We can use it to compile and run some programs using the standard library's less
certified corners to check we get sensible results. This should help us:

Coverage: the tests are currently compiling 434 out of 943 modules

TODO

  • CHANGELOG
  • Turn off the interactive flag when running on CI
  • Reorder phases to typecheck the whole lib first
  • Test for the pretty-printer!
  • Add no-colour option to golden testing (& check TERM env variable is not DUMB)

gallais added 14 commits June 9, 2021 11:28
@gallais
[ cosmetic ] nicer printing of timing
b653654
@gallais
[ new ] System.FilePath.Posix
2051198
@gallais
[ new ] System.Directory
02c5e4f
@gallais
[ new ] System.Directory.Tree
a0e92be
@gallais
[ fix ] missing files & missing unsafe declarations
6e6f3c7
@gallais
[ fix ] checking filepaths exist before opening
01a1b13
@gallais
[ revert ] the addition of System.Directory.Tree
c240c44 
It's not clear it's usable without Sized IO so better not settle
on that one description quite yet.
@gallais
[ more ] flipped IO monad combinators
e9999b2
@gallais
[ new ] test suite for the stdlib
f2b83d1
@gallais
[ test ] new test for showing rose trees
d10c95b
@gallais
[ test ] new test showing nums
eeb7093
@gallais
[ cosmetic ] change package names
fa7b6aa
@gallais
[ fix ] exit codes can be negative
9df96f0 
In particular `git diff --exit-code` returns:
* 0 for success & no mismatch
* 1 for success & mismatch
* something else (< 0) otherwise
@gallais
[ caching ] use a shared --compile-dir for all tests
bee453c
@gallais gallais mentioned this pull request Jun 11, 2021
Open
gallais and others added 17 commits June 18, 2021 14:47
@gallais gallais marked this pull request as ready for review June 20, 2021 15:38
@gallais
Copy link
Member Author

gallais commented Jun 20, 2021

🚀

@MatthewDaggitt MatthewDaggitt merged commit 231d210 into agda:master Jun 21, 2021
@gallais gallais deleted the testing branch June 21, 2021 09:05
@MatthewDaggitt MatthewDaggitt modified the milestones: v1.8, v2.0 Jul 6, 2021
@MatthewDaggitt MatthewDaggitt linked an issue Jul 11, 2021 that may be closed by this pull request
Add a golden test framework #1456
Closed
@MatthewDaggitt MatthewDaggitt mentioned this pull request Jul 11, 2021
Closed
@barrettj12 barrettj12 mentioned this pull request Sep 8, 2021
Open
@gallais gallais mentioned this pull request Mar 5, 2022
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@andreasabel andreasabel andreasabel left review comments

@MatthewDaggitt MatthewDaggitt MatthewDaggitt left review comments

Assignees
No one assigned
Labels
continuous-integration test
Projects
None yet
Milestone
v2.0
Development

Successfully merging this pull request may close these issues.

Add a golden test framework
5 participants
@gallais @andreasabel @MatthewDaggitt @asr @Taneb