search

leanprover-community / lean-client-python

Python talking to the Lean theorem prover
Apache License 2.0
39 stars 6 forks source link

Run tests in CI #20

Closed Julian closed 1 year ago

Julian commented 3 years ago

Some GitHub actioning, a tox setup, some minor packaging things, a LICENSE, and pre-commit, which is highly useful (though yeah let me know if you don't want/like any of the above and obviously can drop it, this is just essentially a "standard" setup I have generated for anything I've got).

This will undoubtedly conflict with #19 but should be somewhat easy to rebase (happy to do that too of course).

Julian commented 3 years ago

(And this will undoubtedly fail, even when I get the kinks out, given #18, but yeah will see...)

Julian commented 3 years ago

OK these are failing for real reasons I think now. (Though yeah some likely affected by #19) -- the first one being subclassing something in trio (which generally doesn't like things subclassing it), which fails during import, so tests haven't started running yet even.

Julian commented 3 years ago

Uh, whoops, I didn't notice #12 either, which this would close, but hopefully @jasonrute you'll forgive me for preempting your attempt to understand how said stuff works better :D

jasonrute commented 3 years ago

Julian, I for one would be more than happy for you to take over CI (#12). I did some initial research on it, and then got caught up on other things.

jasonrute commented 3 years ago

@Julian If this is going to auto format, I'd prefer to put it in after my massive refactor.

jasonrute commented 3 years ago

But other than that, my only question is if it also runs mypy. I've found mypy very helpful for this project with all the type stuff and it would be good for it to be run in CI.

Julian commented 3 years ago

But other than that, my only question is if it also runs mypy. I've found mypy very helpful for this project with all the type stuff and it would be good for it to be run in CI.

I didn't add it, but I'm happy to.

@Julian If this is going to auto format, I'd prefer to put it in after my massive refactor.

Want me to split that piece off and just do the CI first for a first PR? Or just wait on all of it? Either way seems fine with me.

jasonrute commented 3 years ago

Want me to split that piece off and just do the CI first for a first PR? Or just wait on all of it? Either way seems fine with me.

If we can get the other one in soon, let's wait. If not, then let's break it up and push the CI in without all the formatting changes.