Skip to content

Commit

Permalink
Introduce package "notices" (#320)
Browse files Browse the repository at this point in the history
* Add notice config option

* expose any given notice as a warning when installing a package.
  • Loading branch information
mattpolzin authored Jan 19, 2025
1 parent dd32806 commit 12f5a13
Show file tree
Hide file tree
Showing 9 changed files with 41 additions and 30 deletions.
4 changes: 2 additions & 2 deletions src/Pack/Admin/Report/Types.idr
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
2 changes: 1 addition & 1 deletion src/Pack/Admin/Runner/Check.idr
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
8 changes: 4 additions & 4 deletions src/Pack/Config/Environment.idr
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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

Expand All @@ -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
Expand Down
1 change: 1 addition & 0 deletions src/Pack/Database/TOML.idr
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
23 changes: 13 additions & 10 deletions src/Pack/Database/Types.idr
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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

Expand Down Expand Up @@ -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)

Expand Down Expand Up @@ -452,29 +453,31 @@ 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}]"
, "type = \"local\""
, "path = \{quote dir}"
, "ipkg = \{quote ipkg}"
, "packagePath = \{tomlBool pp}"
] ++ testPath t
] ++ (catMaybes [testPath t])

printPair (x, Core c) =
[ "[db.\{x}]"
Expand Down
8 changes: 4 additions & 4 deletions src/Pack/Runner/Database.idr
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion src/Pack/Runner/Develop.idr
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
9 changes: 7 additions & 2 deletions src/Pack/Runner/Install.idr
Original file line number Diff line number Diff line change
Expand Up @@ -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}
Expand All @@ -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)
Expand All @@ -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 ()
Expand Down Expand Up @@ -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)
Expand Down
14 changes: 8 additions & 6 deletions src/Pack/Runner/Query.idr
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down

0 comments on commit 12f5a13

Please sign in to comment.