Hackage :: [Package]

agda2train: Agda backend to generate training data for machine learning purposes.

[ agda, bsd3, library, machine-learning, program ] [ Propose Tags ] [ Report a vulnerability ]

Compiles Agda modules to JSON files, containing information about the imported scope of each module, its definitions and information about each sub-term appearing in the code (i.e. context, goal type, term).

[Skip to Readme]

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

  • No Candidates
Versions [RSS] 0.0.1.0, 0.0.2.0, 0.0.3.0
Dependencies aeson (>=2.0 && <2.3), aeson-pretty (==0.8.10), Agda (>=2.6.3 && <2.6.4), agda2train, async (>=2.2 && <2.3), base (>=4.12.0.0 && <4.20), bytestring (>=0.10.8.1 && <0.13), containers (>=0.5.11.0 && <0.8), deepseq (>=1.4.2.0 && <1.6), directory (>=1.2.6.2 && <1.4), file-embed (==0.0.15.0), filepath (>=1.4.1.0 && <1.5), mtl (>=2.2.1 && <2.4), pretty (>=1.1.3.3 && <1.2), unordered-containers (>=0.2.9.0 && <0.3) [details]
License BSD-3-Clause
Copyright (c) 2023 Orestis Melkonian
Author Orestis Melkonian
Maintainer melkon.or@gmail.com
Uploaded by omelkonian at 2023-10-17T20:29:40Z
Category Agda, machine learning
Home page https://github.com/omelkonian/agda2train/
Bug tracker https://github.com/omelkonian/agda2train/issues
Source repo head: git clone git://github.com/omelkonian/agda2train.git
Distributions
Executables agda2train
Downloads 186 total (12 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs uploaded by user [build log]
All reported builds failed as of 2023-10-19 [all 1 reports]

Readme for agda2train-0.0.3.0

[back to package description]

agda2train: An Agda backend to generate training data for machine learning

CI Hackage

This is work in progress and a neural network trained on these data to provide premise selection is under way.

How to run

The agda2train package is published on Hackage, so one can simply:

$ cabal install agda2train
$ agda2train SomeFile.agda

Run agda2train --help to see the available flags; apart from the standard flags inherited by the agda executable we get the following backend-specific options:

$ agda2train --help
...
agda2train backend options
  -r      --recurse               Recurse into imports/dependencies.
  -x      --no-json               Skip generation of JSON files. (just debug print)
          --ignore-existing-json  Ignore existing JSON files. (i.e. always overwrite)
          --print-json            Print JSON output. (for debugging)
          --no-terms              Do not include definitions of things in scope
  -o DIR  --out-dir=DIR           Generate data at DIR. (default: project root)

Alternatively, assuming a working Haskell installation (cabal available), one can clone this repo and use the provided Makefile to build the package locally, as well as run our test suite:

$ git clone git@github.com:omelkonian/agda2train.git
$ cd agda2train
$ make build # build package
$ make install # install `agda2train` executable
$ make test # run the test-suite (based on golden files in `test/golden/*`)
$ make repl # REPL for developers
$ make allTests # extract JSON data from all example files in `test/*`
$ make stdlib # extract JSON data from Agda's standard library

Relevant Agda issues