[Agda] Info on interacting with the Agda process

[Mateusz Kowalczyk]

On 10/24/2014 09:03 AM, Andreas Abel wrote:
> At Agda-hq, we are hardly aware of projects that use Agda as API.  We 
> have not tests ensuring that we maintain a certain interface of exported 
> functions that give you a handle to use Agda as API.

I suspect this may be in part because there Agda doesn't advertise its
library as API. I'm not blaming anyone however, was just asking for
status. It is understandable that man-power is limited.

> Maybe a way to proceed would be that you API users draft a module 
> Agda.API where you bind functions you care about to the respective 
> functions in this heap of 280 Agda.* modules.  We could then make an 
> effort to maintain this API.  (And of course, we would need tests, but 
> there is already a start in tests/api.)

This seems like a good idea. I think however I will initially talk to
the Agda process just like emacs) and attempt to move into the API
territory once I have that going and have a good idea of what kind of
output I can expect from Agda.

Thank you.

> Cheers,
> Andreas
> 
> On 23.10.2014 02:51, Andrés Sicard-Ramírez wrote:
>> Hi Mateusz,
>>
>> On 22 October 2014 19:02, Mateusz Kowalczyk <fuuzetsu at fuuzetsu.co.uk
>> <mailto:fuuzetsu at fuuzetsu.co.uk>> wrote:
>>
>>     I would also ask whether we could just talk to Agda directly, cutting
>>     out the process and parsing of the information: say we can talk to
>>     Haskell natively, would it be viable to just talk straight to the Agda
>>     library or would it be awkward to do so?
>>
>>
>> This is possible. I wrote Apia (https://github.com/asr/apia), a Haskell
>> program that (partially) uses Agda as a Haskell library (actually, Apia
>> uses a modified version of Agda).
>>
>>
>>     Notably, the package on Hackage says
>>     “Note that the Agda library does not follow the package versioning
>>     policy, because it is not intended to be used by third-party packages.”.
>>
>>
>> That is very true. Given the constant modifications to Agda (I'm not
>> complaing about it) keeping the Apia
>> program (and the modified version of Agda) updated is a time-consuming task.
>>
>> Best,
>>
>> --
>> Andrés
>>
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
> 
> 


-- 
Mateusz K.