ITP 2023 LaTeX question

Stream: general

[Martin Dvořák]

I mean [I should have specified my question better.] how should I typeset the links on the LaTeX side, so that the editors won't eventually kick them out?

[Johan Commelin]

@Martin Dvořák I moved your question to a new thread.

[Eric Wieser]

I already sent this to Martin Dvořák privately when the thread was in #announce, but now that it's not:

I have a script that exports line number information from my lean project here, with some usage explanation here. If you use something like this then you don't need to carefully manage the links yourself.

[Eric Wieser]

It lets you write \leanlink{some_lemma_name} in the paper and it creates a link to the right repo, commit, file, and line number on GitHub.