I just reenabled the feature, fixing a problem we had with it.
This means it should be present in Agda 2.5.4 and 2.6.0 as well.
The documentation is here:
A living example is our POPL 2018 paper, see:
The blue formulas in the PDF are clickable and take you to the
HTML-rendered Agda code.
Post by Martín Hötzel Escardó Post by Andreas Abel
That feature was useful but wasn't working flawlessly, so it is not in
the current development versions. (See gallais pointer.)
I think that if Agda wants to succeed in the long term, this is an
important feature. People want to write papers, blog posts, grant
applications, promotion applications, and more generally do and
disseminate research. It is very difficult to disseminate research if
you can't point reliable and somewhat permanently to it on the web.
Post by Andreas Abel Post by Martin Escardo
Thanks, this seems to be exactly what I want, although I haven't
managed to make it work (with Agda version 2.6.0-5135fd5). I will ask
questions in that issue page, rather than here. Martin
Post by Guillaume Allais
This feature was shipped as part of 2.5.3
Post by Martin Escardo
Say I have a function `blah` in some Agda file. The html link of
`blah` changes every time I change my agda file and regenerate the
html file. Is there a way to get an absolute link that won't change,
so that I can use it from another html document?
Agda mailing list
Andreas Abel <>< Du bist der geliebte Mensch.
Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden