[Agda] Absolute links in html rendering of Agda files

[Martín Hötzel Escardó]

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
>>>
>>
> 
> 

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