[Agda] id number in html?

Jason Hu fdhzs2010 at hotmail.com
Wed Jun 8 15:29:58 CEST 2022


The HTML backend also creates (HTML) identifiers based on the names of
(Agda) identifiers:

   https://github.com/agda/agda/blob/6385f850a185523bb5241a71f5a7614a148f6b53/doc/release-notes/2.5.4.md#html-backend


That’s what I remembered in older versions. Is it still the case in 2.6+?


From: Nils Anders Danielsson<mailto:nad at cse.gu.se>
Sent: Wednesday, June 8, 2022 8:09 AM
To: Jason Hu<mailto:fdhzs2010 at hotmail.com>; agda<mailto:agda at lists.chalmers.se>
Subject: Re: [Agda] id number in html?

On 2022-06-07 21:28, Jason Hu wrote:
> When generating html files, Agda assigns an id to each definitions.
> Now when we need to refer to that id from elsewhere, e.g. another
> website, how stable can I assume this id to be?

The identifiers correspond to file positions.

> Is there a more recommended way to create links to an Agda html file?

The HTML backend also creates (HTML) identifiers based on the names of
(Agda) identifiers:

   https://github.com/agda/agda/blob/6385f850a185523bb5241a71f5a7614a148f6b53/doc/release-notes/2.5.4.md#html-backend

The current naming scheme is a little buggy
(https://github.com/agda/agda/issues/4653) and might change in the
future. If you use this kind of link, then I suggest that you test that
it points to the right thing.

--
/NAD

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20220608/2c70123c/attachment.html>


More information about the Agda mailing list