Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Introduce package "notices" #320

Merged
merged 2 commits into from
Jan 19, 2025
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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
Loading