[Agda] Info on interacting with the Agda process

[Andreas Abel]

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.

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

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
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/