Question: Can I use it with Lean 4?

[vyorkin]

Hi! Works great with Coq! I wonder if it is possible to use it with Lean 4. The readme and this commit says it is supported but I couldn't figure out how to run it.

Running smth like this:

alectryon Proofs/Basic.lean --frontend lean4

Gives me error:

alectryon: error: argument --frontend: invalid choice: 'lean4' (choose from 'coq', 'coq+rst', 'coq.io.json', 'coq.json', 'coqdoc', 'json', 'md', 'rst')

❯ alectryon --version
Alectryon v1.4.0

---

Or it is better to use https://github.com/leanprover/verso instead?

[vyorkin]

Ah, I see, the latest release doesn't support lean4 frontend. I had to install alectryon from a local clone and then it asks for leanInk