From ab3bd6acaf4527329af1f3c524fd757ce7f07bdc Mon Sep 17 00:00:00 2001
From: flupe <lucas@escot.me>
Date: Tue, 1 Oct 2024 11:15:57 +0200
Subject: [PATCH 1/3] [ fix #370 ] add locate command, data-files in cabal
 config

---
 agda2hs.cabal |  5 ++++-
 src/Main.hs   | 19 +++++++++++++------
 2 files changed, 17 insertions(+), 7 deletions(-)

diff --git a/agda2hs.cabal b/agda2hs.cabal
index 93ac52bd..7e177075 100644
--- a/agda2hs.cabal
+++ b/agda2hs.cabal
@@ -1,4 +1,4 @@
-cabal-version:       2.2
+cabal-version:       2.4
 name:                agda2hs
 version:             1.3
 license:             BSD-3-Clause
@@ -18,6 +18,9 @@ description:
 extra-doc-files:    CHANGELOG.md
                     README.md
 
+data-files: agda2hs.agda-lib
+            lib/**/*.agda
+
 source-repository head
   type:     git
   location: https://github.com/agda/agda2hs.git
diff --git a/src/Main.hs b/src/Main.hs
index c8642aec..3d4827e4 100644
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -21,7 +21,7 @@ import Agda2Hs.Config ( checkConfig )
 import Agda2Hs.Compile.Types
 import Agda2Hs.Render
 
-import Paths_agda2hs ( version )
+import Paths_agda2hs ( version, getDataFileName )
 
 
 -- | Agda2Hs default config
@@ -87,8 +87,15 @@ isInteractive = do
   return $ not $ null i
 
 main = do
-  -- Issue #201: disable backend when run in interactive mode
-  isInt <- isInteractive
-  if isInt
-    then runAgda [Backend backend{isEnabled = const False}]
-    else runAgda [Backend backend]
+  args <- getArgs
+
+  -- Issue #370: `agda2hs locate` will print out the path to the prelude agda-lib file
+  if args == ["locate"] then
+    putStrLn =<< getDataFileName "agda2hs.agda-lib"
+  else do
+    -- Issue #201: disable backend when run in interactive mode
+    isInt <- isInteractive
+
+    if isInt
+      then runAgda [Backend backend{isEnabled = const False}]
+      else runAgda [Backend backend]

From e2aa107607193df063ba926054e5739767222ed4 Mon Sep 17 00:00:00 2001
From: flupe <lucas@escot.me>
Date: Tue, 1 Oct 2024 11:32:26 +0200
Subject: [PATCH 2/3] update installation instructions

---
 docs/source/introduction.md | 24 +++++++++++++++++++++++-
 1 file changed, 23 insertions(+), 1 deletion(-)

diff --git a/docs/source/introduction.md b/docs/source/introduction.md
index a81015ef..e5db0db5 100644
--- a/docs/source/introduction.md
+++ b/docs/source/introduction.md
@@ -15,7 +15,29 @@
   - you can navigate the library in [HTML format](https://agda.github.io/agda2hs/lib/),
     along with a comprehensive [test suite](https://agda.github.io/agda2hs/test/)
 
-### Installation
+### Installation with Cabal
+
+agda2hs is released [on Hackage](https://hackage.haskell.org/package/agda2hs),
+and can be installed with Cabal:
+
+```sh
+cabal install agda2hs
+```
+
+Once installed, the agda2hs prelude bundled with agda2hs
+can be registered in the Agda config using the `agda2hs locate` command:
+
+```sh
+agda2hs locate >> ~/.agda/libaries
+```
+
+Optionally, the agda2hs prelude can also be added as a default global import:
+
+```sh
+echo agda2hs >> ~/.agda/defaults
+```
+
+### Manual installation
 
 Let `DIR` be the directory in which you start running these shell commands.
 ```sh

From 4c7396e61e121ad51e0c0e167b22f9b8515eb6de Mon Sep 17 00:00:00 2001
From: flupe <lucas@escot.me>
Date: Tue, 1 Oct 2024 11:41:24 +0200
Subject: [PATCH 3/3] update changelog

---
 CHANGELOG.md | 1 +
 1 file changed, 1 insertion(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 79083de0..92508833 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -13,6 +13,7 @@ Changes to agda2hs:
 - Non-erased implicit arguments and instance arguments are now compiled to regular arguments in Haskell
 - Non-erased module parameters are now compiled to regular arguments in Haskell
 - Rank-N Haskell types are now supported
+- Added `agda2hs locate` command printing the path to the agda2hs prelude `.agda-lib` file
 
 Additions to the agda2hs Prelude:
 - New module `Haskell.Extra.Dec` for working with decidability proofs (compiled to `Bool`)