Hi Martin,
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:
https://github.com/agda/agda/blob/master/CHANGELOG.md#html-backend
A living example is our POPL 2018 paper, see:
http://www.cse.chalmers.se/~abela/publications.html#popl18
The blue formulas in the PDF are clickable and take you to the
HTML-rendered Agda code.
Enjoy!
Andreas
Post by MartÃn Hötzel EscardóPost by Andreas AbelThat 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.
Best,
Martin
Post by Andreas AbelPost by Martin EscardoThanks, 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 AllaisHi Martin,
https://github.com/agda/agda/issues/2604
This feature was shipped as part of 2.5.3
Cheers,
--
gallais
Post by Martin EscardoSay 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?
Thanks,
Martin
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
--
Andreas Abel <>< Du bist der geliebte Mensch.
Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden
***@gu.se
http://www.cse.chalmers.se/~abela/