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

Move Main to top level #16

Closed xubaiw closed 2 years ago

xubaiw commented 2 years ago

So that there is no duplicate main problem when we use it as dependency.

Kha commented 2 years ago

Thanks, looks good to me! Unfortunately, it seems I broke the tests, and I can't repair them right now because clang seems to segfault building LeanInk :grimacing: . Could you fix them as described in the readme?

xubaiw commented 2 years ago

I'll take a look tomorrow 👀

xubaiw commented 2 years ago

Looking at the test diff, it seems that the changes are from newly parsed .variable semantic types and new doc strings. So I just capture a new test output and push it.

Kha commented 2 years ago

Thanks!