search

leanprover / LeanInk

LeanInk is a command line helper tool for Alectryon which aims to ease the integration of Lean 4.
Apache License 2.0
60 stars 16 forks source link

Fix test suite #19

Closed Kha closed 2 years ago

Kha commented 2 years ago

Logging could be improved, but at least we make sure not to discard any errors anymore. /cc @hargoniX

hargoniX commented 2 years ago

Rebasing and rerunning with your fixes locally also didn't surface any errors for me :(, maybe another rerun in the CI?

Kha commented 2 years ago

@hargoniX Oh no, that's expected since I fixed the test suite after all! The reason you couldn't reproduce it likely was that you already had an older lean_packages from a previous run that still worked.