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.

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

Setup testing over all of tptp/smtlib libraries #22

Open
Gbury opened this issue Feb 18, 2020 · 3 comments
Open

Setup testing over all of tptp/smtlib libraries #22

Gbury opened this issue Feb 18, 2020 · 3 comments

Comments

@Gbury
Copy link
Owner

Gbury commented Feb 18, 2020

Still not clear on how an automated setup could work, the libs are definitely too big for the free CI on github.

@bobot
Copy link
Contributor

bobot commented Apr 10, 2020

In which sense are they too big? Are they too long to download or to typecheck with dolmen binary?

@c-cube
Copy link
Collaborator

c-cube commented Apr 10, 2020

I imagine they're too big to download and store on a normal CI machine, and if caching is done wrong it'd be a strain on smtlib/tptp infrastructure?

@Gbury
Copy link
Owner Author

Gbury commented Apr 10, 2020

Both: I doubt the free travis CI machines wouldn't fare very well trying to:

  • download a few Go (the whole smtlib/tptp libraries) for each run, typically free CI infrastructures specify a reasonable maximum cache size of a few hundreds MB.
  • run the generated dolmen binary on all these problems; considering each run is limited to about 30min / 1h of real time (iirc), setting up testing would probably require to split the runs into separate jobs.

All in all, even if it might be possible I think it would be an abuse of free CI in this situation. Instead I'll leave in the repo and check with CI the following:

  • tests that try and test most syntax constructions in a few files
  • tests for each error message
  • tests for each reported bug

For testing on the whole smtlib, I'll first do it manually on my personal machines, and in the long term I might try and see if the new alt-ergo benchmarking machine can be used (either to test dolmen directly, or indirectly since it should be integrated into alt-ergo soon-ish).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants