[Agda] Agda Tutorial darcs repo & pandoc backend

Peter Divianszky divipp at gmail.com
Mon Feb 25 11:20:02 CET 2013


On 28/01/2013 15:47, Nils Anders Danielsson wrote:
> On 2013-01-23 15:14, Peter Divianszky wrote:
>> On the other hand, pandoc dependencies are too much for the Agda
>> compiler.
>> Maybe conditional compilation could solve this.
>> What do you think?
>
> Can you use Agda as a library instead of putting the new functionality
> in the main code base? (Ignoring the lack of a welldefined library
> API...)

I have done it, and uploaded it to HackageDB as PandocAgda.

The goal was to split Pandoc support for literate Agda files from the 
modified Agda compiler to a separate package and reuse as much
as possible from the Agda compiler libraries.

The following Haskell source files were modified:
    Agda.Main
    Agda.Interaction.Highlighting
        -- only Agda.Main depends on it
    Agda.Interaction.Options
        -- lots of modules depends on it

So the only obstacle was the modified Agda.Interaction.Options to
reuse all other modules from the Agda compiler libraries.
I solved this with the hack that I parse the options with the
modified options parser and then convert the modified CommandLineOptions
data to the original CommandLineOptions data.

I had to copy and slightly modify these files too:
    Agda.cabal
    LICENSE
    src/main/Agda/Main.hs
    src/full/Agda/undefined.h
    src/data/Agda.css

I took just two hours to complete this task.
I have tested it with the darcs version of the Agda compiler.

Cheers,

Peter





More information about the Agda mailing list