Data

Tools

Indexes

Applications

Experiments

Open Source Science

https://github.com/agda/agda2lambox

Compiling Agda's internal syntax to λ-box terms.

https://github.com/agda/agda2lambox

Science Score: 57.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
    Found 1 DOI reference(s) in README
  • ✓
    Academic publication links
    Links to: arxiv.org, acm.org
  • ○
    Academic email domains
  • ✓
    Institutional organization owner
    Organization agda has institutional domain (wiki.portal.chalmers.se)
  • ○
    JOSS paper metadata
  • ○
    Scientific vocabulary similarity
    Low similarity (8.7%) to scientific vocabulary
Last synced: 6 months ago · JSON representation

Repository

Compiling Agda's internal syntax to λ-box terms.

Basic Info
  • Host: GitHub
  • Owner: agda
  • License: other
  • Language: Haskell
  • Default Branch: master
  • Size: 316 KB
Statistics
  • Stars: 6
  • Watchers: 3
  • Forks: 2
  • Open Issues: 14
  • Releases: 0
Created over 1 year ago · Last pushed about 1 year ago
Metadata Files
Readme License

README.md

agda2lambox

An Agda backend to generate MetaCoq λ□ (LambdaBox) programs for further (verified) extraction to WASM or Rust. The backend builds off Agda 2.7.0.1. Compatible with Coq 8.19.0, MetaCoq 1.3.1 and CertiCoq 0.9.

To install the backend, setup GHC (tested with 9.10.1) and cabal.

git clone git@github.com:omelkonian/agda2lambox.git cd agda2lambox cabal install

This will take a while, as it has to (recursively) clone the Agda repo and compile from source.

Then you're good to go.

agda2lambox [AGDAFLAGS] [--out-dir DIR] [--typed] FILE

Setup

The backend generates .v and .txt files that contain the extracted λ□ environment. To check what's generated, setup CertiCoq and compile the minimal Coq prelude.

opam pin add certicoq 0.9+8.19 coq_makefile -f _CoqProject -o CoqMakefile make -f CoqMakefile

TODO

  • [ ] Type aliases (See #3)
  • [ ] Improve type compilation
    • The (re)implementation of the type translation is currently incomplete. In particular, when compiling an application, we should retrieve the type of the head and compile the elims with it.
  • [ ] Check support for Agda-specific edge cases
    • [ ] Projection-like (See #6)
  • [ ] Support primitives (ints and floats)
  • [ ] Setup compilation to Wasm/Rust using Certicoq
  • [ ] Setup proper testing infrastructure

Icebox

Things that ought to be implemented, but not right now.

  • [ ] Caching of compiled modules.

References

Owner

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

GitHub Events

Total
  • Issues event: 2
  • Issue comment event: 1
  • Pull request event: 3
  • Fork event: 1
Last Year
  • Issues event: 2
  • Issue comment event: 1
  • Pull request event: 3
  • Fork event: 1

Issues and Pull Requests

Last synced: 6 months ago

All Time
  • Total issues: 2
  • Total pull requests: 3
  • Average time to close issues: N/A
  • Average time to close pull requests: N/A
  • Total issue authors: 1
  • Total pull request authors: 1
  • Average comments per issue: 0.0
  • Average comments per pull request: 0.0
  • Merged pull requests: 0
  • Bot issues: 0
  • Bot pull requests: 0
Past Year
  • Issues: 2
  • Pull requests: 3
  • Average time to close issues: N/A
  • Average time to close pull requests: N/A
  • Issue authors: 1
  • Pull request authors: 1
  • Average comments per issue: 0.0
  • Average comments per pull request: 0.0
  • Merged pull requests: 0
  • Bot issues: 0
  • Bot pull requests: 0
View more stats
Top Authors
Issue Authors
  • 4ever2 (2)
Pull Request Authors
  • 4ever2 (3)
Top Labels
Issue Labels
Pull Request Labels

Dependencies

.github/workflows/nix-ci.yml actions
  • DeterminateSystems/magic-nix-cache-action v4 composite
  • actions/checkout v4 composite
  • cachix/install-nix-action v22 composite
agda2lambox.cabal hackage
  • Agda >=2.7 && <=2.8
  • base >=4.10 && <4.22
  • deepseq >=1.4.4 && <1.6
  • mtl *
  • pretty-show *
.github/workflows/ci.yml actions
  • actions/cache/restore v4 composite
  • actions/cache/save v4 composite
  • actions/checkout v4 composite
  • haskell-actions/setup v2 composite