agda2train 0.0.2.0 → 0.0.3.0
raw patch · 3 files changed
+66/−52 lines, 3 filesdep +agda2trainPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
Dependencies added: agda2train
API changes (from Hackage documentation)
- Main: Options :: Bool -> Maybe FilePath -> Options
- Main: [outDir] :: Options -> Maybe FilePath
- Main: [recurse, noJson, ignoreJson, printJson, includeDefs, includePrivs] :: Options -> Bool
- Main: data Options
- Main: defaultOptions :: Options
- Main: encode :: ToJSON a => a -> ByteString
- Main: encodeFile :: ToJSON a => FilePath -> a -> IO ()
- Main: getOutDir :: Options -> FilePath
- Main: getOutFn :: Options -> String -> FilePath
- Main: ignoreJsonOpt :: Monad m => Options -> m Options
- Main: includeDefsOpt :: Monad m => Options -> m Options
- Main: includePrivsOpt :: Monad m => Options -> m Options
- Main: instance Control.DeepSeq.NFData Main.Options
- Main: instance GHC.Generics.Generic Main.Options
- Main: main :: IO ()
- Main: mkBackend :: TrainF -> Backend' Options Options ([ScopeEntry], [ScopeEntry]) () (String, [Sample])
- Main: noJsonOpt :: Monad m => Options -> m Options
- Main: outDirOpt :: Monad m => FilePath -> Options -> m Options
- Main: printJsonOpt :: Monad m => Options -> m Options
- Main: recOpt :: Monad m => Options -> m Options
Files
- README.md +14/−0
- agda2train.cabal +51/−51
- src/Main.hs +1/−1
README.md view
@@ -13,6 +13,20 @@ $ 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:+```bash+$ 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:
agda2train.cabal view
@@ -1,66 +1,66 @@-cabal-version: 2.4-name: agda2train-version: 0.0.2.0-synopsis: Agda backend to generate training data for machine learning purposes.+cabal-version: 2.4+name: agda2train+version: 0.0.3.0+synopsis: Agda backend to generate training data for machine learning purposes. description: 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). -category: Agda, machine learning-author: Orestis Melkonian-maintainer: melkon.or@gmail.com-stability: experimental-homepage: https://github.com/omelkonian/agda2train/-bug-reports: https://github.com/omelkonian/agda2train/issues-license: BSD-3-Clause-license-file: LICENSE-copyright: (c) 2023 Orestis Melkonian+category: Agda, machine learning+author: Orestis Melkonian+maintainer: melkon.or@gmail.com+stability: experimental+homepage: https://github.com/omelkonian/agda2train/+bug-reports: https://github.com/omelkonian/agda2train/issues+license: BSD-3-Clause+license-file: LICENSE+copyright: (c) 2023 Orestis Melkonian extra-source-files:- data/defsToSkip.txt- README.md- LICENSE+ data/defsToSkip.txt+ README.md+ LICENSE source-repository head type: git location: git://github.com/omelkonian/agda2train.git +common globalOptions+ hs-source-dirs: src+ default-language: Haskell2010+ default-extensions:+ LambdaCase NamedFieldPuns OverloadedStrings RecordWildCards TupleSections+ DeriveGeneric DeriveAnyClass DeriveFunctor DeriveFoldable DeriveTraversable+ StandaloneDeriving PatternSynonyms TypeFamilies TypeOperators FunctionalDependencies+ build-depends:+ base >=4.12.0.0 && <4.20+ , Agda >=2.6.3 && <2.6.4+ , pretty >=1.1.3.3 && <1.2+ , containers >=0.5.11.0 && <0.8+ , aeson >=2.0 && <2.3+ , mtl >=2.2.1 && <2.4+ , async >=2.2 && <2.3+ , file-embed == 0.0.15.0 +library agda2train-lib+ import: globalOptions+ exposed-modules:+ ToTrain+ Output+ AgdaInternals executable agda2train- main-is: Main.hs- other-modules: ToTrain, Output, AgdaInternals- build-depends: base >=4.12.0.0 && <4.20- , Agda >=2.6.3 && <2.6.4- , pretty >=1.1.3.3 && <1.2- , containers >=0.5.11.0 && <0.8- , unordered-containers >=0.2.9.0 && <0.3- , aeson >=2.0 && <2.3- , aeson-pretty == 0.8.10- , bytestring >=0.10.8.1 && <0.13- , mtl >=2.2.1 && <2.4- , directory >=1.2.6.2 && <1.4- , filepath >=1.4.1.0 && <1.5- , deepseq >=1.4.2.0 && <1.6- , async >=2.2 && <2.3- , file-embed == 0.0.15.0- hs-source-dirs: src- default-language: Haskell2010- default-extensions: LambdaCase- , NamedFieldPuns- , OverloadedStrings- , RecordWildCards- , TupleSections- , DeriveGeneric- , DeriveAnyClass- , DeriveFunctor- , DeriveFoldable- , DeriveTraversable- , DerivingVia- , StandaloneDeriving- , PatternSynonyms- , TypeFamilies- , TypeOperators- , FunctionalDependencies- ghc-options: -threaded -rtsopts -with-rtsopts=-N+ import: globalOptions+ main-is: Main.hs+ ghc-options:+ -threaded -rtsopts -with-rtsopts=-N+ -Wno-missing-home-modules+ build-depends:+ agda2train-lib+ , deepseq >=1.4.2.0 && <1.6+ , bytestring >=0.10.8.1 && <0.13+ , directory >=1.2.6.2 && <1.4+ , filepath >=1.4.1.0 && <1.5+ , unordered-containers >=0.2.9.0 && <0.3+ , aeson-pretty == 0.8.10
src/Main.hs view
@@ -169,7 +169,7 @@ -- -- ['includePrivs'] whether to include private definitions as well ----- (run @agda2train -h/--help@ for a human-readable description of all options)+-- (run @agda2train --help@ for a human-readable description of all options) data Options = Options { recurse, noJson, ignoreJson, printJson, includeDefs, includePrivs :: Bool , outDir :: Maybe FilePath