Gbury / dolmen

Dolmen provides a library and a binary to parse, typecheck, and evaluate languages used in automated deduction
BSD 2-Clause "Simplified" License
80 stars 17 forks source link

Setup testing over all of tptp/smtlib libraries #22

Open Gbury opened 4 years ago

Gbury commented 4 years ago

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

bobot commented 4 years ago

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

c-cube commented 4 years ago

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 commented 4 years ago

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

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:

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).