Data

Tools

Indexes

Applications

Experiments

Open Source Science

https://github.com/agda/agda2hs

Compiling Agda code to readable Haskell

https://github.com/agda/agda2hs

Science Score: 36.0%

This score indicates how likely this project is to be science-related based on various indicators:

  • ○
    CITATION.cff file
  • ✓
    codemeta.json file
    Found codemeta.json file
  • ✓
    .zenodo.json file
    Found .zenodo.json file
  • ○
    DOI references
  • ○
    Academic publication links
  • ✓
    Committers with academic emails
    2 of 26 committers (7.7%) from academic institutions
  • ○
    Institutional organization owner
  • ○
    JOSS paper metadata
  • ○
    Scientific vocabulary similarity
    Low similarity (9.8%) to scientific vocabulary

Keywords from Contributors

agda type-theory dependent-types programming-language proof-assistant proof cubical-type-theory cabal ghc haskell
Last synced: 9 months ago · JSON representation

Repository

Compiling Agda code to readable Haskell

Basic Info
Statistics
  • Stars: 190
  • Watchers: 22
  • Forks: 43
  • Open Issues: 72
  • Releases: 0
Created over 5 years ago · Last pushed 11 months ago
Metadata Files
Readme Changelog License

README.md

GitHub CI

agda2hs

Agda2hs is a tool for producing verified and readable Haskell code by extracting it from a (lightly annotated) Agda program. The goal of this project is not to translate arbitrary Agda code to Haskell. Rather it is to carve out a common sublanguage between Agda and Haskell, with a straightforward translation from the Agda side to the Haskell side. This lets you write your program in the Agda fragment, using full Agda to prove properties about it, and then translate it to nice looking readable Haskell code that you can show your Haskell colleagues without shame.

Documentation

Documentation can be viewed at https://agda.github.io/agda2hs. You can also find examples in the test directory of this repository, in particular the file Test.agda. The documentation is a work in progress, so if you have been using agda2hs and want to contribute in some way, adding documentation or examples would be very welcome.

agda2hs was introduced in the Haskell Symposium '22 paper Reasonable Agda is Correct Haskell: Writing Verified Haskell using agda2hs.

Future work

Currently agda2hs is under active development, please take a look at the issue tracker. If you have a suggestion for a new feature that is not yet on the issue tracker, you are welcome to create a new issue or a PR. Feature requests should be of the form "Add support for Haskell feature X", not "Add support for Agda feature Y" (see "Objective" above). If you want to compile arbitrary Agda code to Haskell, you are advised to use Agda's built-in GHC backend instead.

Owner

  • Name: Agda Github Community
  • Login: agda
  • Kind: organization

GitHub Events

Total
  • Issues event: 36
  • Watch event: 14
  • Delete event: 3
  • Issue comment event: 104
  • Push event: 69
  • Pull request review comment event: 50
  • Pull request review event: 52
  • Pull request event: 52
  • Fork event: 4
  • Create event: 5
Last Year
  • Issues event: 36
  • Watch event: 14
  • Delete event: 3
  • Issue comment event: 104
  • Push event: 69
  • Pull request review comment event: 50
  • Pull request review event: 52
  • Pull request event: 52
  • Fork event: 4
  • Create event: 5

Committers

Last synced: about 1 year ago

All Time
  • Total Commits: 633
  • Total Committers: 26
  • Avg Commits per committer: 24.346
  • Development Distribution Score (DDS): 0.61
Past Year
  • Commits: 135
  • Committers: 13
  • Avg Commits per committer: 10.385
  • Development Distribution Score (DDS): 0.6
Top Committers
Name Email Commits
Jesper Cockx j****r@s****e 247
Ulf Norell u****l@g****m 84
flupe l****s@e****e 75
Orestis Melkonian m****r@g****m 36
Sára Juhošová s****a@s****l 36
Bohdan b****t@g****m 21
viktorcsimma c****3@g****m 21
pmbittner p****r@u****e 18
Aleksandra Wolska w****a@g****m 18
Heinrich Apfelmus a****s@q****e 17
Andreas Källberg a****3@g****m 16
James Chapman j****n@i****o 13
Jakob Naucke j****e@p****e 7
avery t****k@h****k 5
Luka Janjić l****c@g****m 5
Amélia Liao me@a****w 3
Henry Blanchette 7****1 2
Peter Dragos p****r@m****y 1
dxts d****5@g****m 1
anuyts a****s 1
amesgen a****n@a****e 1
Victor Cacciari Miraldo v****o@c****m 1
Guillaume Allais g****s@e****g 1
Andreas Abel a****l@i****e 1
Robin S C****d@p****m 1
José Carlos Padilla Cancio j****o@g****m 1
Committer Domains (Top 20 + Academic)
ifi.lmu.de: 1 ens-lyon.org: 1 channable.com: 1 amesgen.de: 1 mlabs.city: 1 amelia.how: 1 hotmail.co.uk: 1 posteo.de: 1 iohk.io: 1 quantentunnel.de: 1 uni-ulm.de: 1 student.tudelft.nl: 1 escot.me: 1 sikanda.be: 1

Issues and Pull Requests

Last synced: 10 months ago

All Time
  • Total issues: 86
  • Total pull requests: 146
  • Average time to close issues: 4 months
  • Average time to close pull requests: about 1 month
  • Total issue authors: 22
  • Total pull request authors: 17
  • Average comments per issue: 1.0
  • Average comments per pull request: 1.25
  • Merged pull requests: 113
  • Bot issues: 0
  • Bot pull requests: 0
Past Year
  • Issues: 26
  • Pull requests: 72
  • Average time to close issues: 27 days
  • Average time to close pull requests: 5 days
  • Issue authors: 10
  • Pull request authors: 8
  • Average comments per issue: 0.77
  • Average comments per pull request: 1.15
  • Merged pull requests: 55
  • Bot issues: 0
  • Bot pull requests: 0
View more stats
Top Authors
Issue Authors
  • jespercockx (29)
  • omelkonian (9)
  • flupe (8)
  • HeinrichApfelmus (7)
  • bwbush (7)
  • anka-213 (3)
  • jmchapman (3)
  • liesnikov (3)
  • ju-sh (2)
  • jakobn-ai (2)
  • steve-anunknown (2)
  • viktorcsimma (1)
  • pmbittner (1)
  • stites (1)
  • cho-m (1)
Pull Request Authors
  • jespercockx (47)
  • HeinrichApfelmus (18)
  • omelkonian (17)
  • liesnikov (14)
  • flupe (10)
  • viktorcsimma (9)
  • anka-213 (6)
  • dragospe (4)
  • odderwiser (4)
  • PPKFS (4)
  • jakobn-ai (3)
  • pmbittner (2)
  • ndcroos (2)
  • J0s3c4rl0s (2)
  • VictorCMiraldo (2)
Top Labels
Issue Labels
enhancement (26) bug (23) error-reporting (9) question (5) good first issue (3) documentation (2) CI (2) prelude (2) help wanted (2) levels (2) wontfix (1)
Pull Request Labels
CI (3) documentation (2) enhancement (2)

Packages

  • Total packages: 1
  • Total downloads: unknown
  • Total dependent packages: 0
  • Total dependent repositories: 0
  • Total versions: 4
proxy.golang.org: github.com/agda/agda2hs
  • Versions: 4
  • Dependent Packages: 0
  • Dependent Repositories: 0
Rankings
Dependent packages count: 5.4%
Average: 5.6%
Dependent repos count: 5.8%
Last synced: 10 months ago

Dependencies

agda2hs.cabal hackage
  • Agda ==2.6.3.*
  • base >=4.10 && <4.16
  • containers ==0.6.*
  • deepseq >=1.4.1.1
  • directory >=1.2.6.2 && <1.4
  • filepath >=1.4.1.0 && <1.5
  • haskell-src-exts >=1.23 && <1.25
  • mtl >=2.2
  • syb >=0.7
  • text >=1.2.3.0
  • unordered-containers >=0.2
.github/workflows/ci.yml actions
  • actions/cache v2 composite
  • actions/checkout v2 composite
  • actions/setup-haskell v1 composite
.github/workflows/docs.yml actions
  • actions/checkout v3 composite
  • actions/configure-pages v2 composite
  • actions/deploy-pages v1 composite
  • actions/setup-python v4 composite
  • actions/upload-pages-artifact v1 composite
docs/requirements.txt pypi
  • myst_parser ==0.18.1
  • readthedocs-sphinx-search ==0.1.2
  • sphinx ==5.3.0
  • sphinx_rtd_theme ==1.1.1