[Agda] Announcement: agda2hs release v1.0

[Orestis Melkonian]

Briefly, the main difference is that MAlonzo covers the entirety of 
Agda, while agda2hs does not really care about that, we instead want to 
cover as many Haskell features as possible, i.e. writing Haskell within 
Agda if you will.

Also see the 'Related Work: Program Extraction' section of the paper for 
more details and comparisons.

Cheers,
--OM


On 07/04/2023 16:31, Jason Hu wrote:
>
> That’s great Jesper. But I don’t quite understand the difference 
> between the built-in extraction and agda2hs. I understand that code 
> from agda2hs is more readable, but why can’t we make the built-in 
> extracted code more readable?
>
> Thanks,
>
> Jason Hu
>
> *From: *Jesper Cockx <mailto:jesper at sikanda.be>
> *Sent: *Friday, April 7, 2023 6:17 AM
> *To: *Agda list <mailto:agda at lists.chalmers.se>
> *Subject: *[Agda] Announcement: agda2hs release v1.0
>
> Dear all,
>
> I am very pleased to announce the first official release of agda2hs, a 
> tool for producing verified and readable Haskell code by extracting it 
> from a (lightly annotated) Agda program. You can find it at 
> https://hackage.haskell.org/package/agda2hs-1.0 or on a cabal package 
> manager near you. The official documentation can be found at 
> https://agda.github.io/agda2hs/, and more details about the motivation 
> and design are available in our paper at the Haskell Symposium: 
> https://dl.acm.org/doi/10.1145/3546189.3549920.
>
> This release is just a first step for agda2hs into the wider world and 
> we have many exciting features that will be added in the future. If 
> you want to report a bug or a feature request, you can do so at 
> https://github.com/agda/agda2hs/issues. We are also open to 
> contributions by new developers, feel free to contact me via email or 
> on Zulip if you have any questions about this.
>
> Best regards,
>
> Jesper Cockx
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20230407/7e4abf98/attachment-0001.html>