From 12f5a13977c6682f269e5f03758cea1c8e61ac77 Mon Sep 17 00:00:00 2001
From: Mathew Polzin <matt.polzin@gmail.com>
Date: Sat, 18 Jan 2025 22:43:05 -0600
Subject: [PATCH] Introduce package "notices" (#320)

* Add notice config option

* expose any given notice as a warning when installing a package.
---
 src/Pack/Admin/Report/Types.idr |  4 ++--
 src/Pack/Admin/Runner/Check.idr |  2 +-
 src/Pack/Config/Environment.idr |  8 ++++----
 src/Pack/Database/TOML.idr      |  1 +
 src/Pack/Database/Types.idr     | 23 +++++++++++++----------
 src/Pack/Runner/Database.idr    |  8 ++++----
 src/Pack/Runner/Develop.idr     |  2 +-
 src/Pack/Runner/Install.idr     |  9 +++++++--
 src/Pack/Runner/Query.idr       | 14 ++++++++------
 9 files changed, 41 insertions(+), 30 deletions(-)

diff --git a/src/Pack/Admin/Report/Types.idr b/src/Pack/Admin/Report/Types.idr
index 53c6f6e..6d8c949 100644
--- a/src/Pack/Admin/Report/Types.idr
+++ b/src/Pack/Admin/Report/Types.idr
@@ -59,12 +59,12 @@ apiLink p =
   "https://stefan-hoeck.github.io/idris2-pack-db/docs/\{p}/docs/index.html"
 
 url : (e : Env) => Package -> URL
-url (Git u _ _ _ _)            = u
+url (Git u _ _ _ _ _)            = u
 url (Local dir ipkg pkgPath _) = MkURL "\{dir}"
 url (Core _)                   = e.db.idrisURL
 
 commit : (e : Env) => Package -> Commit
-commit (Git _ c _ _ _)            = c
+commit (Git _ c _ _ _ _)            = c
 commit (Local dir ipkg pkgPath _) = ""
 commit (Core _)                   = e.db.idrisCommit
 
diff --git a/src/Pack/Admin/Runner/Check.idr b/src/Pack/Admin/Runner/Check.idr
index f7a756f..c940655 100644
--- a/src/Pack/Admin/Runner/Check.idr
+++ b/src/Pack/Admin/Runner/Check.idr
@@ -43,7 +43,7 @@ test (RL pkg n d _ _) =
   case e.env.config.skipTests of
     True  => pure Skipped
     False => case  pkg of
-      Git u c _ _ (Just t) => do
+      Git u c _ _ (Just t) _ => do
         d <- withGit n u c pure
         runIpkg (d </> t) [] e
         pure TestSuccess
diff --git a/src/Pack/Config/Environment.idr b/src/Pack/Config/Environment.idr
index 9dca202..051d4cf 100644
--- a/src/Pack/Config/Environment.idr
+++ b/src/Pack/Config/Environment.idr
@@ -157,7 +157,7 @@ idrisDataDir = idrisInstallDir /> "support"
 ||| Directory where an installed library or app goes
 export %inline
 pkgPrefixDir : PackDir => DB => PkgName -> Package -> Path Abs
-pkgPrefixDir n (Git _ c _ _ _) = commitDir <//> n <//> c
+pkgPrefixDir n (Git _ c _ _ _ _) = commitDir <//> n <//> c
 pkgPrefixDir n (Local _ _ _ _) = commitDir </> "local" <//> n
 pkgPrefixDir n (Core _)        = idrisPrefixDir
 
@@ -219,7 +219,7 @@ pkgInstallDir n p d =
       dir  := pkgPrefixDir n p /> idrisDir
    in case p of
         Core c        => dir /> (c <-> vers)
-        Git _ _ _ _ _ => dir </> pkgRelDir d
+        Git _ _ _ _ _ _ => dir </> pkgRelDir d
         Local _ _ _ _ => dir </> pkgRelDir d
 
 ||| Directory where the API docs of the package will be installed.
@@ -577,7 +577,7 @@ cacheCoreIpkgFiles dir = for_ corePkgs $ \c =>
 
 export
 notCached : HasIO io => (e : Env) => PkgName -> Package -> io Bool
-notCached n (Git u c i _ _) = fileMissing $ ipkgCachePath n c i
+notCached n (Git u c i _ _ _) = fileMissing $ ipkgCachePath n c i
 notCached n (Local d i _ _) = pure False
 notCached n (Core c)        = fileMissing $ coreCachePath c
 
@@ -588,7 +588,7 @@ cachePkg :
   -> PkgName
   -> Package
   -> EitherT PackErr io ()
-cachePkg n (Git u c i _ _) =
+cachePkg n (Git u c i _ _ _) =
   let cache  := ipkgCachePath n c i
       tmpLoc := gitTmpDir n </> i
    in withGit n u c $ \dir => do
diff --git a/src/Pack/Database/TOML.idr b/src/Pack/Database/TOML.idr
index 9c75b7b..d74a05d 100644
--- a/src/Pack/Database/TOML.idr
+++ b/src/Pack/Database/TOML.idr
@@ -21,6 +21,7 @@ git f v =
        (valAt "ipkg" f v)
        (optValAt "packagePath" f False v)
        (maybeValAt "test" f v)
+       (maybeValAt "notice" f v)
   |]
 
 local : File Abs -> TomlValue -> Either TOMLErr (Package_ c)
diff --git a/src/Pack/Database/Types.idr b/src/Pack/Database/Types.idr
index a695000..661327c 100644
--- a/src/Pack/Database/Types.idr
+++ b/src/Pack/Database/Types.idr
@@ -143,6 +143,7 @@ data Package_ : (c : Type) -> Type where
       -> (ipkg     : File Rel)
       -> (pkgPath  : Bool)
       -> (testIpkg : Maybe (File Rel))
+      -> (notice   : Maybe String)
       -> Package_ c
 
   ||| A local Idris project given as an absolute path to a local
@@ -161,13 +162,13 @@ data Package_ : (c : Type) -> Type where
 
 export
 Functor Package_ where
-  map f (Git u c i p t) = Git u (f c) i p t
+  map f (Git u c i p t n) = Git u (f c) i p t n
   map f (Local d i p t) = Local d i p t
   map f (Core c)        = Core c
 
 export
 traverse : Applicative f => (URL -> a -> f b) -> Package_ a -> f (Package_ b)
-traverse g (Git u c i p t) = (\c' => Git u c' i p t) <$> g u c
+traverse g (Git u c i p t n) = (\c' => Git u c' i p t n) <$> g u c
 traverse _ (Local d i p t)    = pure $ Local d i p t
 traverse _ (Core c)           = pure $ Core c
 
@@ -250,14 +251,14 @@ isGit (Local {}) = No absurd
 ||| folders where Idris package are installed.
 export
 usePackagePath : Package_ c -> Bool
-usePackagePath (Git _ _ _ pp _) = pp
+usePackagePath (Git _ _ _ pp _ _) = pp
 usePackagePath (Local _ _ pp _) = pp
 usePackagePath (Core _)         = False
 
 ||| Absolute path to the `.ipkg` file of a package.
 export
 ipkg : (dir : Path Abs) -> Package -> File Abs
-ipkg dir (Git _ _ i _ _) = toAbsFile dir i
+ipkg dir (Git _ _ i _ _ _) = toAbsFile dir i
 ipkg dir (Local _ i _ _) = toAbsFile dir i
 ipkg dir (Core c)        = toAbsFile dir (coreIpkgPath c)
 
@@ -452,21 +453,23 @@ tomlBool : Bool -> String
 tomlBool True  = "true"
 tomlBool False = "false"
 
-testPath : Maybe (File Rel) -> List String
-testPath Nothing  = []
-testPath (Just x) = [ "test        = \{quote x}" ]
+testPath : Maybe (File Rel) -> Maybe String
+testPath = map (\x => "test        = \{quote x}")
+
+notice : Maybe String -> Maybe String
+notice = map (\x =>   "notice      = \{quote x}")
 
 -- we need to print `Git` packages as `"github"` at
 -- least for the time being for reasons of compatibility
 printPair : (PkgName,Package) -> List String
-printPair (x, Git url commit ipkg pp t) =
+printPair (x, Git url commit ipkg pp t n) =
   [ "[db.\{x}]"
   , "type        = \"github\""
   , "url         = \{quote url}"
   , "commit      = \{quote commit}"
   , "ipkg        = \{quote ipkg}"
   , "packagePath = \{tomlBool pp}"
-  ] ++ testPath t
+  ] ++ (catMaybes [testPath t, notice n])
 
 printPair (x, Local dir ipkg pp t) =
   [ "[db.\{x}]"
@@ -474,7 +477,7 @@ printPair (x, Local dir ipkg pp t) =
   , "path        = \{quote dir}"
   , "ipkg        = \{quote ipkg}"
   , "packagePath = \{tomlBool pp}"
-  ] ++ testPath t
+  ] ++ (catMaybes [testPath t])
 
 printPair (x, Core c) =
   [ "[db.\{x}]"
diff --git a/src/Pack/Runner/Database.idr b/src/Pack/Runner/Database.idr
index 975ed05..b4ae6b0 100644
--- a/src/Pack/Runner/Database.idr
+++ b/src/Pack/Runner/Database.idr
@@ -181,9 +181,9 @@ withPkgEnv :
   -> Package
   -> (Path Abs -> EitherT PackErr io a)
   -> EitherT PackErr io a
-withPkgEnv n (Git u c i _ _) f = withGit n u c f
-withPkgEnv n (Local d i _ _) f = inDir d f
-withPkgEnv n (Core _)        f = withCoreGit f
+withPkgEnv n (Git u c i _ _ _) f = withGit n u c f
+withPkgEnv n (Local d i _ _)   f = inDir d f
+withPkgEnv n (Core _)          f = withCoreGit f
 
 isOutdated : DPair Package PkgStatus -> Bool
 isOutdated (fst ** Outdated) = True
@@ -265,7 +265,7 @@ loadIpkg :
   -> PkgName
   -> Package
   -> EitherT PackErr io (Desc U)
-loadIpkg n (Git u c i _ _) =
+loadIpkg n (Git u c i _ _ _) =
   let cache  := ipkgCachePath n c i
       tmpLoc := gitTmpDir n </> i
    in parseIpkgFile cache tmpLoc
diff --git a/src/Pack/Runner/Develop.idr b/src/Pack/Runner/Develop.idr
index 2a6683e..348242f 100644
--- a/src/Pack/Runner/Develop.idr
+++ b/src/Pack/Runner/Develop.idr
@@ -184,7 +184,7 @@ runTest :
   -> EitherT PackErr io ()
 runTest n args e = case lookup n allPackages of
   Nothing                     => throwE (UnknownPkg n)
-  Just (Git u c _ _ $ Just t) => do
+  Just (Git u c _ _ (Just t) _) => do
     d <- withGit n u c pure
     runIpkg (d </> t) args e
   Just (Local d _ _ $ Just t) => runIpkg (d </> t) args e
diff --git a/src/Pack/Runner/Install.idr b/src/Pack/Runner/Install.idr
index 7111d47..2341706 100644
--- a/src/Pack/Runner/Install.idr
+++ b/src/Pack/Runner/Install.idr
@@ -222,6 +222,10 @@ withSrcStr = case c.withSrc of
   True  => " (with sources)"
   False => ""
 
+maybeGiveNotice : HasIO io => Config => SafeLib -> io ()
+maybeGiveNotice (RL (Git _ _ _ _ _ (Just notice)) _ _ _ _) = warn notice
+maybeGiveNotice _ = pure ()
+
 installImpl :
      {auto _ : HasIO io}
   -> {auto e : IdrisEnv}
@@ -234,6 +238,7 @@ installImpl dir rl =
       libDir   := rl.desc.path.parent </> "lib"
    in do
      info "Installing library\{withSrcStr}: \{name rl}"
+     maybeGiveNotice rl
      when (isInstalled rl) $ do
        info "Removing currently installed version of \{name rl}"
        rmDir (pkgInstallDir rl.name rl.pkg rl.desc)
@@ -253,7 +258,7 @@ preInstall :
 preInstall rl = withPkgEnv rl.name rl.pkg $ \dir =>
   let ipkgAbs := ipkg dir rl.pkg
    in case rl.pkg of
-        Git u c ipkg _ _ => do
+        Git u c ipkg _ _ _ => do
           let cache := ipkgCachePath rl.name c ipkg
           copyFile cache ipkgAbs
         Local _ _ _ _ => pure ()
@@ -308,7 +313,7 @@ installApp b ra =
       let ipkgAbs := ipkg dir ra.pkg
        in case ra.pkg of
             Core _            => pure ()
-            Git u c ipkg pp _ => do
+            Git u c ipkg pp _ _ => do
               let cache   := ipkgCachePath ra.name c ipkg
               copyFile cache ipkgAbs
               libPkg [] Build True ["--build"] (notPackIsSafe ra.desc)
diff --git a/src/Pack/Runner/Query.idr b/src/Pack/Runner/Query.idr
index 597fbb5..8c06732 100644
--- a/src/Pack/Runner/Query.idr
+++ b/src/Pack/Runner/Query.idr
@@ -147,25 +147,27 @@ appStatus qp = case qp.app of
     , "App          : \{status' st}"
     ]
 
-testFile : Maybe (File Rel) -> List String
-testFile Nothing  = []
-testFile (Just f) = ["Test File    : \{f}"]
+testFile : Maybe (File Rel) -> Maybe String
+testFile = map (\f => "Test File    : \{f}")
+
+notice : Maybe String -> Maybe String
+notice = map (\f =>   "Notice       : \{f}")
 
 details : QPkg -> List String
 details qp = case qp.lib.pkg of
-  Git url commit ipkg _ t => [
+  Git url commit ipkg _ t n => [
     "Type         : Git project"
   , "URL          : \{url}"
   , "Commit       : \{commit}"
   , "ipkg File    : \{ipkg}"
-  ] ++ testFile t
+  ] ++ (catMaybes [testFile t, notice n])
 
   Local d i _ t =>
     let ipkg := toAbsFile d i
      in [ "Type         : Local Idris project"
         , "Location     : \{ipkg.parent}"
         , "ipkg File    : \{ipkg.file}"
-        ] ++ testFile t
+        ] ++ (catMaybes [testFile t])
 
   Core _            => [
     "Type         : Idris core package"