0 | module Pack.Runner.Database

  2 | import Core.FC

  3 | import Core.Name.Namespace

  4 | import Data.SortedMap

  5 | import Data.IORef

  6 | import Idris.Package.Types

  7 | import Pack.Config

  8 | import Pack.Core

  9 | import Pack.Core.Hash

 10 | import Pack.Database

 11 | import Pack.Version as V

 13 | %default total

 23 | data Safe : PkgDesc -> Type where

 24 |   IsSafe : Safe d

 27 | public export

 28 | 0 SafeLib : Type

 29 | SafeLib = ResolvedLib Safe

 35 | data NotPack : PkgDesc -> Type where

 36 |   IsNotPack : Safe d -> NotPack d

 40 | 0 toSafe : NotPack d -> Safe d

 41 | toSafe (IsNotPack s) = s

 44 | public export

 45 | 0 SafeApp : Type

 46 | SafeApp = ResolvedApp NotPack

 49 | public export

 50 | 0 SafePkg : Type

 51 | SafePkg = LibOrApp Safe NotPack

 56 | notPackIsSafe : Desc NotPack -> Desc Safe

 57 | notPackIsSafe (MkDesc x y z s) = MkDesc x y z $ toSafe s

 65 | safe : HasIO io => (e : Env) => Desc t -> EitherT PackErr io (Desc Safe)

 66 | safe (MkDesc d s f _) =

 67 |   let unsafe :=

 68 |         isJust $

 69 |               d.prebuild

 70 |           <|> d.postbuild

 71 |           <|> d.preinstall

 72 |           <|> d.postinstall

 73 |    in case e.config.safetyPrompt &&

 74 |            unsafe &&

 75 |            not (MkPkgName d.name `elem` e.config.whitelist) of

 76 |         False => pure $ MkDesc d s f IsSafe

 77 |         True  => do

 78 |           let msg := "Package \{name d} uses custom build hooks."

 79 |           confirmOrAbort Warning msg

 80 |           pure $ MkDesc d s f IsSafe

 85 | notPack : HasIO io => Env => Desc t -> EitherT PackErr io (Desc NotPack)

 86 | notPack d = do

 87 |   MkDesc d s f p <- safe d

 88 |   case d.executable of

 89 |     Just "pack" => throwE ManualInstallPackApp

 90 |     _           => pure $ MkDesc d s f (IsNotPack p)

 94 | parseLibIpkg :

 95 |      {auto _ : HasIO io}

 96 |   -> {auto e : Env}

 97 |   -> (file : File Abs)

 98 |   -> (loc : File Abs)

 99 |   -> EitherT PackErr io (Desc Safe)

100 | parseLibIpkg p loc = parseIpkgFile p loc >>= safe

105 | findAndParseLocalIpkg :

106 |      {auto _ : HasIO io}

107 |   -> {auto e: Env}

108 |   -> (file : PkgOrIpkg)

109 |   -> EitherT PackErr io (Desc Safe)

110 | findAndParseLocalIpkg (Ipkg p) = parseLibIpkg p p

111 | findAndParseLocalIpkg (Pkg n)  =

112 |   case lookup n e.all of

113 |     Nothing                   => throwE (UnknownPkg n)

114 |     Just (Local dir ipkg _ _) => let p = dir </> ipkg in parseLibIpkg p p

115 |     Just _                    => throwE (NotLocalPkg n)

119 | findTheOnlyIpkg :

120 |      {auto _ : HasIO io}

121 |   -> {auto _ : CurDir}

122 |   -> EitherT PackErr io PkgOrIpkg

123 | findTheOnlyIpkg = do

124 |   [ipkg] <- filter isIpkgBody <$> entries curDir

125 |     | lfs => throwE (BuildMany lfs)

126 |   pure $ Ipkg $ curDir /> ipkg

130 | refinePkg :

131 |      {auto _ : HasIO io}

132 |   -> {auto _ : CurDir}

133 |   -> Maybe PkgOrIpkg

134 |   -> EitherT PackErr io PkgOrIpkg

135 | refinePkg (Just p) = pure p

136 | refinePkg Nothing  = findTheOnlyIpkg

142 | parseAppIpkg :

143 |      {auto _ : HasIO io}

144 |   -> {auto _ : Env}

145 |   -> (file : File Abs)

146 |   -> (loc : File Abs)

147 |   -> EitherT PackErr io (Desc NotPack)

148 | parseAppIpkg p loc = parseIpkgFile p loc >>= notPack

153 | safeLib : HasIO io => Env => ResolvedLib t -> EitherT PackErr io SafeLib

154 | safeLib l  = reTag l <$> safe l.desc

162 | safeApp : HasIO io => Env => ResolvedApp t -> EitherT PackErr io SafeApp

163 | safeApp a = reTag a <$> notPack a.desc

167 | checkLOA : HasIO io => Env => LibOrApp U U -> EitherT PackErr io SafePkg

168 | checkLOA (Lib x)   = Lib <$> safeLib x

169 | checkLOA (App b x) = App b <$> safeApp x

177 | withPkgEnv :

178 |      {auto _ : HasIO io}

179 |   -> {auto _ : Env}

180 |   -> PkgName

181 |   -> Package

182 |   -> (Path Abs -> EitherT PackErr io a)

183 |   -> EitherT PackErr io a

184 | withPkgEnv n (Git u c i _ _ _) f = withGit n u c False f

185 | withPkgEnv n (Local d i _ _)   f = inDir d f

186 | withPkgEnv n (Core _)          f = withCoreGit f

188 | newerSrc : HasIO io => File Abs -> Path Abs -> EitherT PackErr io String

189 | newerSrc ts src = trim <$> sysRun ["find", src, "-newer", ts]

191 | newerIpkg : HasIO io => File Abs -> File Abs -> EitherT PackErr io String

192 | newerIpkg ts ipkg =

193 |   trim <$> sysRun ["find", ipkg.parent, "-name", "\{ipkg.file}", "-newer", ts]

196 | libStatus :

197 |      {auto _ : HasIO io}

198 |   -> {auto e : Env}

199 |   -> PkgName

200 |   -> (p    : Package)

201 |   -> (d    : Desc t)

202 |   -> (deps : List (DPair Package PkgStatus))

203 |   -> EitherT PackErr io (PkgStatus p)

204 | libStatus n p d deps = do

205 |   h    <- pkgHash

206 |   True <- exists (pkgInstallDir n h p d) | False => do pure (Missing missingHash)

207 |   b    <- exists $ pkgDocs n h p d

208 |   pure (Installed h b)

209 |   where

210 |     mkHash : String -> Hash

211 |     mkHash s =

212 |       MkHash $ hashStrings $ s :: map (\(_ ** s) => value $ hash s) deps

214 |     localHash : Hash

215 |     localHash = mkHash nanoString

217 |     missingHash : Hash

218 |     missingHash =

219 |       case p of

220 |         Git _ c _ _ _ _          => mkHash c.value

221 |         Core                   _ => MkHash e.db.idrisCommit.value

222 |         Local {}                 => localHash

224 |     pkgHash : EitherT PackErr io Hash

225 |     pkgHash =

226 |       case p of

227 |         Local dir ipkg pkgPath _ => do

228 |           let ts  := libTimestamp n

229 |               dir := localSrcDir d

230 |           True <- fileExists ts       | False => pure localHash

231 |           ""   <- newerSrc ts dir     | s     => pure localHash

232 |           ""   <- newerIpkg ts d.path | s     => pure localHash

233 |           s    <- read ts

234 |           debug "timestamp for \{n}: \{s}"

235 |           debug "hash for \{n}: \{mkHash $ trim s}"

236 |           pure (mkHash $ trim s)

237 |         _ => pure missingHash

241 | appStatus :

242 |      {auto _ : HasIO io}

243 |   -> {auto _ : Env}

244 |   -> PkgName

245 |   -> (h    : Hash)

246 |   -> (p    : Package)

247 |   -> (exe  : Body)

248 |   -> EitherT PackErr io (AppStatus p)

249 | appStatus n h p exe = do

250 |   True <- fileExists (pkgExec n h p exe) | False => pure (Missing h)

251 |   True <- fileExists (pathExec exe)      | False => pure (Installed h)

252 |   pure (BinInstalled h)

254 | loadIpkg :

255 |      {auto _ : HasIO io}

256 |   -> {auto e : Env}

257 |   -> PkgName

258 |   -> Package

259 |   -> EitherT PackErr io (Desc U)

260 | loadIpkg n (Git u c i _ _ _) =

261 |   let cache  := ipkgCachePath n c i

262 |       tmpLoc := gitTmpDir n </> i

263 |    in parseIpkgFile cache tmpLoc

264 | loadIpkg n (Local d i _ _)    = parseIpkgFile (d </> i) (d </> i)

265 | loadIpkg n (Core c)           =

266 |   let cache  := coreCachePath c

267 |       tmpLoc := gitTmpDir compiler </> coreIpkgPath c

268 |    in parseIpkgFile cache tmpLoc

274 | resolveLib :

275 |      {auto _ : HasIO io}

276 |   -> {auto e : Env}

277 |   -> {default [<] vis : SnocList PkgName}

278 |   -> PkgName

279 |   -> EitherT PackErr io (ResolvedLib U)

280 | resolveLib n = assert_total $ do

281 |   checkCycle vis [n]

282 |   Nothing <- lookupLib n | Just pkg => pure pkg

283 |   case lookup n e.all of

284 |     Nothing => throwE (UnknownPkg n)

285 |     Just p  => do

286 |       d    <- loadIpkg n p

287 |       deps <- traverse resolveDep $ dependencies d

288 |       lib  <- libStatus n p d deps

289 |       cacheLib n $ RL p (hash lib) n d lib deps

291 |   where

292 |     checkCycle : SnocList PkgName -> List PkgName -> EitherT PackErr io ()

293 |     checkCycle [<]       xs = pure ()

294 |     checkCycle (sx :< x) xs =

295 |       if x == n then throwE (CyclicDeps $ x::xs) else checkCycle sx (x::xs)

297 |     resolveDep : PkgName -> EitherT PackErr io (DPair Package PkgStatus)

298 |     resolveDep m =

299 |       (\l => (_ ** l.status)) <$> resolveLib {vis = vis :< n} m

304 | export covering

305 | resolveApp : HasIO io => Env => PkgName -> EitherT PackErr io (ResolvedApp U)

306 | resolveApp n = do

307 |   RL p h n d _ ds <- resolveLib n

308 |   case exec d of

309 |     Nothing  => throwE (NoApp n)

310 |     Just exe => (\s => RA p h n d s exe ds) <$> appStatus n h p exe

315 | export covering

316 | resolveAny :

317 |      {auto _ : HasIO io}

318 |   -> {auto _ : Env}

319 |   -> InstallType

320 |   -> PkgName

321 |   -> EitherT PackErr io (LibOrApp U U)

322 | resolveAny Library n = Lib   <$> resolveLib n

323 | resolveAny (App b) n = App b <$> resolveApp n

329 | export covering

330 | appPath : HasIO io => PkgName -> Env -> EitherT PackErr io ()

331 | appPath "idris2" e = putStrLn "\{idrisExec}"

332 | appPath n e = do

333 |   ref <- emptyCache

334 |   ra <- resolveApp n

335 |   putStrLn . interpolate $ pkgExec ra.name ra.hash ra.pkg ra.exec

341 | depString : (depsOfX : List PkgName) -> (x,y : PkgName) -> Maybe String

342 | depString depsOfX x y =

343 |   toMaybe (y `elem` depsOfX) "\{quote x} depends on \{quote y}"

345 | consider : List PkgName -> ResolvedLib s -> Bool

346 | consider ns x = isInstalled x && not (x.name `elem` ns)

348 | printDeps :

349 |      {auto _ : HasIO io}

350 |   -> {auto _ : Env}

351 |   -> List (ResolvedLib s)

352 |   -> PkgName

353 |   -> EitherT PackErr io Bool

354 | printDeps rls n =

355 |   case map nameStr (filter (elem n . dependencies) rls) of

356 |     Nil  => pure False

357 |     [n1] => warn "Package \{quote n1} depends on \{quote n}." $> True

358 |     ns   => logMany Warning

359 |               "The following packages depend on \{quote n}:" ns $> True

361 | delPrompt : String

362 | delPrompt = """

369 | export covering

370 | checkDeletable : HasIO io => (e : Env) => List PkgName -> EitherT PackErr io ()

371 | checkDeletable ns = do

372 |   ss <- filter (consider ns) <$> traverse resolveLib (keys e.all)

373 |   bs <- traverse (printDeps ss) ns

374 |   when (any id bs) $ confirmOrAbort Warning delPrompt

380 | idrisDelDir : (e : Env) => Body -> Maybe (Path Abs)

381 | idrisDelDir b =

382 |   let s := interpolate b

383 |    in toMaybe (s /= "pack" && all (\ic => s /= ic.value) e.config.allIdrisCommits) (installDir /> b)

385 | packDelDir : (e : Env) => Body -> Maybe (Path Abs)

386 | packDelDir b =

387 |   let s := interpolate b

388 |    in toMaybe (s /= V.version.value) (packParentDir /> b)

390 | tmpDelDir : (e : Env) => Body -> Maybe (Path Abs)

391 | tmpDelDir b =

392 |   let s := interpolate b

393 |       p := cacheDir /> b

394 |    in toMaybe ((".tmp" `isPrefixOf` s) && p /= Types.tmpDir) p

396 | purgeDirs : HasIO io => (e : Env) => EitherT PackErr io (List $ Path Abs)

397 | purgeDirs = join <$> (entries commitDir >>= traverse purgePaths)

398 |   where

399 |     purgePaths : Body -> EitherT PackErr io (List $ Path Abs)

400 |     purgePaths "idris2" = pure []

401 |     purgePaths x        =

402 |      let pkg := MkPkgName (interpolate x)

403 |          dir := commitDir /> x

404 |       in case lookup pkg e.all of

405 |            Nothing => pure [dir]

406 |            Just _  => do

407 |              rl <- resolveLib pkg

408 |              es <- entries (commitDir /> x)

409 |              pure $ (dir />) <$> filter (\b => "\{b}" /= rl.hash.value) es

411 | gcDirs : HasIO io => (e : Env) => EitherT PackErr io (List $ Path Abs)

412 | gcDirs = do

413 |   ds <- mapMaybe idrisDelDir <$> entries installDir

414 |   ps <- mapMaybe packDelDir <$> entries packParentDir

415 |   ts <- mapMaybe tmpDelDir <$> entries cacheDir

416 |   pd <- if e.config.gcPurge then purgeDirs else pure []

417 |   pure (ds ++ ps ++ ts ++ pd)

421 | garbageCollector : HasIO io => Env -> EitherT PackErr io ()

422 | garbageCollector e = do

423 |   all <- gcDirs

424 |   when (e.config.gcPrompt && not (null all)) $ do

425 |     let msg := "The following directories will be deleted."

426 |     confirmManyOrAbort Warning msg (interpolate <$> all)

427 |   when (null all) $ info "Nothing to clean up."

428 |   for_ all rmDir

434 | pkgNeedsInstalling : {auto c : Config} -> PkgStatus p -> Bool

435 | pkgNeedsInstalling (Missing h)         = True

436 | pkgNeedsInstalling (Installed h True)  = False

437 | pkgNeedsInstalling (Installed h False) = c.withDocs

439 | appNeedsInstalling : (withWrapperScript : Bool) -> AppStatus p -> Bool

440 | appNeedsInstalling _ (Missing h)      = True

441 | appNeedsInstalling b (Installed h)    = b

442 | appNeedsInstalling _ (BinInstalled h) = False

444 | needsInstalling : {auto c : Config} -> LibOrApp t s -> Bool

445 | needsInstalling (Lib x)   = pkgNeedsInstalling x.status

446 | needsInstalling (App b x) = appNeedsInstalling b x.status

448 | showPlan : List (InstallType, PkgName) -> String

449 | showPlan = unlines . map (\(t,n) => "\{t} \{n}")

452 | export covering

453 | transitiveDeps :

454 |      {auto _ : HasIO io}

455 |   -> {auto _ : Env}

456 |   -> List (InstallType, PkgName)

457 |   -> EitherT PackErr io (List $ LibOrApp U U)

458 | transitiveDeps ps = go empty Lin (map Right ps)

459 |   where

460 |     covering

461 |     go :

462 |          (planned  : SortedMap (InstallType, PkgName) ())

463 |       -> (resolved : SnocList $ LibOrApp U U)

464 |       -> List (Either (LibOrApp U U) (InstallType,PkgName))

465 |       -> EitherT PackErr io (List $ LibOrApp U U)

466 |     go ps sx []             = pure (sx <>> [])

468 |     -- the lib or app has already been resolved and

469 |     -- its dependencies are already part of the build plan `sx`

470 |     -- We make sure its not added as a dep again and add

471 |     -- it to the list of handled packages.

472 |     go ps sx (Left (Lib lib) :: xs) =

473 |       go (insert (Library, name lib) () ps) (sx :< Lib lib) xs

475 |     go ps sx (Left (App b app) :: xs) =

476 |       go (insert (App b, name app) () ps) (sx :< App b app) xs

478 |     -- the package `p` might have been resolved already

479 |     -- if it was a dependency of another package

480 |     -- if that's the case, we ignore it. Otherwise, we

481 |     go ps sx (Right p :: xs) = case lookup p ps of

482 |       Just ()  => go ps sx xs

483 |       Nothing  => do

484 |         loa <- resolveAny (fst p) (snd p)

485 |         let deps := (\d => Right (Library, d)) <$> dependencies loa

486 |         go ps sx $ deps ++ Left loa :: xs

488 | compilerApp : (InstallType, PkgName) -> Bool

489 | compilerApp (App _, MkPkgName "idris2") = True

490 | compilerApp _ = False

497 | export covering

498 | plan :

499 |      {auto _ : HasIO io}

500 |   -> {auto _ : Env}

501 |   -> List (InstallType, PkgName)

502 |   -> EitherT PackErr io (List SafePkg)

503 | plan ps =

504 |   let neededPs := filter (not . compilerApp) ps

505 |   -- ^ we never need the compiler app because it is installed as part of the

506 |   -- requisite environment to run any Install command.

507 |       ps' := (Library, "prelude") :: (Library, "base") :: neededPs

508 |    in do

509 |      debug "Building plan for the following libraries: \n\{showPlan ps}"

510 |      loas <- filter needsInstalling <$> transitiveDeps ps'

511 |      traverse checkLOA loas