command-line arguments for Alectryon Sphinx extension

Stream: lean4

[Heather Macbeth]

To use LeanInk for a Lean file with dependencies, one must use a command-line argument to specify the lakefile:

leanInk a MyFile.lean --lake lakefile.lean

(See the LeanInk readme). To use Alectryon directly on a Lean file with dependencies it seems I can just give the same command line argument:

alectryon MyFile.lean --lake lakefile.lean

gives the correct MyFile.html output.

I am now trying to set up Alectryon as a Sphinx extension. How can I specify command-line arguments for LeanInk here? I would have guessed this would be one of the things covered in "Setting options", but nothing there seems relevant.

[Heather Macbeth]

(deleted)

[Sebastian Ullrich]

I'm not quite sure to be honest, but also it looks like the Sphinx module might be Coq-specific at the moment? https://github.com/cpitclaudel/alectryon/blob/master/alectryon/sphinx.py#L56

[Heather Macbeth]

Thanks for looking into it. I was hoping that the Lean 4 fork of Alectryon would feature Lean 4 support for Sphinx, but the line you point to is the same in the fork.