diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -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:
diff --git a/agda2train.cabal b/agda2train.cabal
--- a/agda2train.cabal
+++ b/agda2train.cabal
@@ -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
diff --git a/src/Main.hs b/src/Main.hs
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -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