[Agda] Absolute links in html rendering of Agda files

[Andreas Abel]

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

On 16.02.2018 20:57, Martín Hötzel Escardó wrote:
> 
> 
> On 16/02/18 15:03, abela at chalmers.se wrote:
>> 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
> 
>>
>> On 16.02.2018 14:42, Martin Escardo wrote:
>>> 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
>>>
>>> On 16/02/18 12:40, guillaume.allais at ens-lyon.org wrote:
>>>> 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
>>>>
>>>> On 16/02/18 11:32, Martin Escardo wrote:
>>>>> 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
>>>> Agda at lists.chalmers.se
>>>> 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

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/