[Agda] id number in html?

[Jason Hu]

NAD,

If I read your answer correctly, even comments will shift the id number? Wouldn’t that be a bit fragile? At this point, is there a way to use a different id scheme?


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


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/31e4a0a5/attachment-0001.html>