Discussion:
Absolute links in html rendering of Agda files
(too old to reply)
Martin Escardo
2018-02-16 10:32:59 UTC
Permalink
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?
Thanks,
Martin
--
Martin Escardo
http://www.cs.bham.ac.uk/~mhe
Guillaume Allais
2018-02-16 12:40:24 UTC
Permalink
Hi Martin,

This discussion seems relevant: https://github.com/agda/agda/issues/2604
This feature was shipped as part of 2.5.3

Cheers,
--
gallais
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?
Thanks,
Martin
Martin Escardo
2018-02-16 14:42:03 UTC
Permalink
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
Hi Martin,
This discussion seems relevant: https://github.com/agda/agda/issues/2604
This feature was shipped as part of 2.5.3
Cheers,
--
gallais
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?
Thanks,
Martin
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
--
Martin Escardo
http://www.cs.bham.ac.uk/~mhe
Andreas Abel
2018-02-16 15:03:08 UTC
Permalink
That feature was useful but wasn't working flawlessly, so it is not in
the current development versions. (See gallais pointer.)
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
Hi Martin,
This discussion seems relevant: https://github.com/agda/agda/issues/2604
This feature was shipped as part of 2.5.3
Cheers,
--
gallais
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?
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/
Martín Hötzel Escardó
2018-02-16 19:57:33 UTC
Permalink
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.

Best,
Martin
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
Hi Martin,
This discussion seems relevant: https://github.com/agda/agda/issues/2604
This feature was shipped as part of 2.5.3
Cheers,
--
gallais
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?
Thanks,
Martin
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
--
http://www.cs.bham.ac.uk/~mhe
Andreas Abel
2018-02-19 20:48:52 UTC
Permalink
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 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.
Best,
Martin
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
Hi Martin,
https://github.com/agda/agda/issues/2604
This feature was shipped as part of 2.5.3
Cheers,
--
gallais
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?
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/
Martin Escardo
2018-02-20 14:36:53 UTC
Permalink
Thank you very much!

Martin
Post by Guillaume Allais
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.
  https://github.com/agda/agda/blob/master/CHANGELOG.md#html-backend
  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 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.
Best,
Martin
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
Hi Martin,
https://github.com/agda/agda/issues/2604
This feature was shipped as part of 2.5.3
Cheers,
--
gallais
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?
Thanks,
Martin
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda
--
Martin Escardo
http://www.cs.bham.ac.uk/~mhe
Loading...