[Agda] Absolute links in html rendering of Agda files

[Martin Escardo]

Thank you very much!

Martin

On 19/02/18 20:48, abela at chalmers.se wrote:
> 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
>>>>>
>>>>
>>>
>>>
>>
> 
> 

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe