0 | module Pack.Config.Environment

  2 | import Data.Maybe

  3 | import Data.SortedMap as SM

  4 | import Data.String

  5 | import Idris.Package.Types

  6 | import Pack.CmdLn

  7 | import Pack.Config.TOML

  8 | import Pack.Config.Types

  9 | import public Pack.Config.Environment.Variable

 10 | import Pack.Core

 11 | import Pack.Database

 12 | import System

 13 | import System.Clock

 15 | %default total

 23 | packToml : Body

 24 | packToml = "pack.toml"

 27 | export %inline

 28 | dbDir : (pd : PackDirs) => Path Abs

 29 | dbDir = pd.state /> "db"

 32 | export %inline

 33 | cacheDir : (pd : PackDirs) => Path Abs

 34 | cacheDir = pd.cache

 38 | ipkgCachePath : PackDirs => PkgName -> Commit -> File Rel -> File Abs

 39 | ipkgCachePath p com = toAbsFile (cacheDir <//> p <//> com)

 43 | versionCachePath : PackDirs => (db : DB) => File Abs

 44 | versionCachePath = MkF (cacheDir <//> IdrisApi <//> db.idrisCommit) "version"

 48 | coreCachePath : PackDirs => (db : DB) => CorePkg -> File Abs

 49 | coreCachePath n =

 50 |   MkF (cacheDir <//> n <//> db.idrisCommit) (coreIpkgFile n)

 53 | export %inline

 54 | userDir : (pd : PackDirs) => Path Abs

 55 | userDir = pd.user

 58 | export %inline

 59 | globalPackToml : PackDirs => File Abs

 60 | globalPackToml = MkF userDir packToml

 63 | export %inline

 64 | collectionToml : (pd : PackDirs) => File Abs

 65 | collectionToml = MkF pd.state packToml

 69 | dbFile : PackDirs => (c : MetaConfig) => File Abs

 70 | dbFile = MkF dbDir $ c.collection.value <+> ".toml"

 75 | export %inline

 76 | packBinDir : (pd : PackDirs) => Path Abs

 77 | packBinDir = pd.bin

 80 | export %inline

 81 | installDir : (pd : PackDirs) => Path Abs

 82 | installDir = pd.state </> "install"

 85 | export %inline

 86 | packParentDir : PackDirs => Path Abs

 87 | packParentDir = installDir </> "pack"

 90 | export %inline

 91 | packInstallDir : PackDirs => Commit -> Path Abs

 92 | packInstallDir com = packParentDir </> cast com

 95 | export %inline

 96 | pathExec : PackDirs => Body -> File Abs

 97 | pathExec b = MkF packBinDir b

101 | packExec : PackDirs => File Abs

102 | packExec = pathExec "pack"

106 | patchesDir : PackDirs => Path Abs

107 | patchesDir = userDir /> "patches"

110 | commitsDir : PackDirs => Path Abs

111 | commitsDir = cacheDir </> "commits"

116 | commitFile : PackDirs => URL -> Branch -> File Abs

117 | commitFile url b =

118 |   let relPath := the (Path Rel) $ cast "\{url}/\{b}"

119 |    in MkF (commitsDir </> relPath) "commit"

123 | patchFile : PackDirs => (c : Config) => PkgName -> File Rel -> File Abs

124 | patchFile n (MkF p b) =

125 |   MkF

126 |     (patchesDir //> c.collection <//> n </> p)

127 |     (b <+> ".patch")

131 | export %inline

132 | commitDir : PackDirs => (db : DB) => Path Abs

133 | commitDir = installDir <//> db.idrisCommit

136 | export %inline

137 | idrisPrefixDir : PackDirs => DB => Path Abs

138 | idrisPrefixDir = commitDir /> "idris2"

141 | export %inline

142 | idrisBinDir : PackDirs => DB => Path Abs

143 | idrisBinDir = idrisPrefixDir /> "bin"

150 | idrisExec : PackDirs => DB => File Abs

151 | idrisExec = MkF idrisBinDir "idris2"

153 | export %inline

154 | idrisDir : (db : DB) => Body

155 | idrisDir = the Body "idris2" <-> db.idrisVersion

158 | export %inline

159 | idrisInstallDir : PackDirs => DB => Path Abs

160 | idrisInstallDir = idrisPrefixDir /> idrisDir

163 | export %inline

164 | idrisLibDir : PackDirs => DB => Path Abs

165 | idrisLibDir = idrisInstallDir /> "lib"

168 | export %inline

169 | idrisDataDir : PackDirs => DB => Path Abs

170 | idrisDataDir = idrisInstallDir /> "support"

173 | export %inline

174 | pkgPrefixDir : PackDirs => DB => PkgName -> Hash -> Package -> Path Abs

175 | pkgPrefixDir n h (Git {})   = commitDir <//> n <//> h

176 | pkgPrefixDir n h (Local {}) = commitDir <//> n <//> h

177 | pkgPrefixDir n h (Core _)   = idrisPrefixDir

182 | export %inline

183 | pkgPathDir : PackDirs => DB => PkgName -> Hash -> Package -> Path Abs

184 | pkgPathDir n h p = pkgPrefixDir n h p /> idrisDir

187 | export %inline

188 | pkgBinDir : PackDirs => DB => PkgName -> Hash -> Package -> Path Abs

189 | pkgBinDir n h p = pkgPrefixDir n h p /> "bin"

194 | export %inline

195 | pkgLibDir : PackDirs => DB => PkgName -> Hash -> Package -> Path Abs

196 | pkgLibDir n h p = pkgPathDir n h p /> "lib"

201 | export %inline

202 | pkgDataDir : PackDirs => DB => PkgName -> Hash -> Package -> Path Abs

203 | pkgDataDir n h p = pkgPathDir n h p /> "support"

207 | export %inline

208 | libTimestamp :  PackDirs => DB => PkgName -> File Abs

209 | libTimestamp n = MkF (cacheDir </> "local" <//> n) ".timestamp"

213 | export %inline

214 | localSrcDir : Desc t -> Path Abs

215 | localSrcDir d = sourcePath d

217 | pkgRelDir : Desc t -> Path Rel

218 | pkgRelDir d = case Body.parse d.desc.name of

219 |   Just b  => neutral /> (b <-> d.desc.version)

220 |   Nothing => cast d.desc.name //> d.desc.version

225 | pkgInstallDir : PackDirs => (db : DB) => PkgName -> Hash -> Package -> Desc t -> Path Abs

226 | pkgInstallDir n h p d =

227 |   let vers := db.idrisVersion

228 |       dir  := pkgPrefixDir n h p /> idrisDir

229 |    in case p of

230 |         Core c          => dir /> (c <-> vers)

231 |         Git _ _ _ _ _ _ => dir </> pkgRelDir d

232 |         Local _ _ _ _   => dir </> pkgRelDir d

235 | export %inline

236 | pkgDocs : PackDirs => DB => PkgName -> Hash -> Package -> Desc t -> Path Abs

237 | pkgDocs n h p d = pkgInstallDir n h p d /> "docs"

241 | pkgExec : PackDirs => DB => PkgName -> Hash -> Package -> (exe : Body) -> File Abs

242 | pkgExec n h p exe = MkF (pkgBinDir n h p) exe

246 | resolvedExec : PackDirs => DB => ResolvedApp t -> File Abs

247 | resolvedExec (RA p h n d _ exe _) = pkgExec n h p exe

250 | export %inline

251 | packRepo : (c : Config) => URL

252 | packRepo = fromMaybe defaultPackRepo c.packURL

255 | export %inline

256 | packCommit : (c : Config) => Maybe Commit

257 | packCommit = c.packCommit

262 | useRacket : (c : Config) => Bool

263 | useRacket = map snd (split c.scheme) == Just "racket"

267 | bootstrapCmd : (c : Config) => String

268 | bootstrapCmd = if useRacket then "bootstrap-racket" else "bootstrap"

276 | prefixVar : PackDirs => DB => EnvVar

277 | prefixVar = PrefixVar idrisPrefixDir

281 | idrisBootVar : PackDirs => DB => EnvVar

282 | idrisBootVar = IdrisBootVar idrisExec

286 | schemeVar : (c : Config) => EnvVar

287 | schemeVar = if useRacket then IdrisCodegenVar Racket else SchemeVar c.scheme

292 | libInstallPrefix : PackDirs => DB => ResolvedLib t -> List EnvVar

293 | libInstallPrefix rl = [IdrisPrefixVar $ pkgPrefixDir rl.name rl.hash rl.pkg]

297 | idrisCmd : (e : Env) => CmdArgList

298 | idrisCmd = idrisExec :: e.config.extraArgs

303 | idrisWithCG : (e : Env) => CmdArgList

304 | idrisWithCG = case e.config.codegen of

305 |   Default => idrisCmd

306 |   cg      => idrisCmd ++ ["--cg", cg]

312 | getEnvPath : HasIO io => String -> io (Maybe (Path Abs))

313 | getEnvPath s = (>>= parse) <$> getEnv s

315 | getUserDir  : HasIO io => (home : Path Abs) -> io (Path Abs)

316 | getUserDir home = do

317 |   Nothing <- getEnvPath "PACK_USER_DIR"   | Just p => pure p

318 |   Nothing <- getEnvPath "XDG_CONFIG_HOME" | Just p => pure (p </> "pack")

319 |   pure (home </> ".config/pack")

321 | getStateDir : HasIO io => (home : Path Abs) -> io (Path Abs)

322 | getStateDir home = do

323 |   Nothing <- getEnvPath "PACK_STATE_DIR" | Just p => pure p

324 |   Nothing <- getEnvPath "XDG_STATE_HOME" | Just p => pure (p </> "pack")

325 |   pure (home </> ".local/state/pack")

327 | getCacheDir : HasIO io => (home : Path Abs) -> io (Path Abs)

328 | getCacheDir home = do

329 |   Nothing <- getEnvPath "PACK_CACHE_DIR" | Just p => pure p

330 |   Nothing <- getEnvPath "XDG_CACHE_HOME" | Just p => pure (p </> "pack")

331 |   pure (home </> ".cache/pack")

333 | getBinDir   : HasIO io => (home : Path Abs) -> io (Path Abs)

334 | getBinDir home = do

335 |   Nothing <- getEnvPath "PACK_BIN_DIR"   | Just p => pure p

336 |   pure (home </> ".local/bin")

342 | getPackDirs : HasIO io => EitherT PackErr io PackDirs

343 | getPackDirs = do

344 |   Just h <- getEnvPath "HOME" | Nothing => throwE NoPackDir

345 |   u      <- getUserDir h

346 |   s      <- getStateDir h

347 |   c      <- getCacheDir h

348 |   b      <- getBinDir h

349 |   pure (PD u s c b)

353 | updateDB : HasIO io => TmpDir => PackDirs => EitherT PackErr io ()

354 | updateDB = do

355 |   rmDir dbDir

356 |   commit <- gitLatest dbRepo "main"

357 |   withGit packDB dbRepo commit True $ \d =>

358 |     copyDir (d /> "collections") dbDir

362 | latestCollection : HasIO io => (dir : Path Abs) -> EitherT PackErr io DBName

363 | latestCollection dir = do

364 |   (x :: xs) <- filter ("HEAD.toml" /=) <$> tomlFiles dir

365 |     | [] => pure Head

366 |   pure

367 |     . maybe Head MkDBName

368 |     . fileStem

369 |     $ foldl max x xs

373 | copyLatest : HasIO io => TmpDir => PackDirs => EitherT PackErr io DBName

374 | copyLatest = do

375 |   commit <- gitLatest dbRepo "main"

376 |   withGit packDB dbRepo commit True $ \d => do

377 |     db <- latestCollection (d /> "collections")

378 |     let body := cast {to = Body} db <+> ".toml"

379 |     copyFile (d /> "collections" /> body) (dbDir /> body)

380 |     pure db

385 | defaultColl : HasIO io => TmpDir => PackDirs => EitherT PackErr io DBName

386 | defaultColl = do

387 |   when !(missing dbDir) updateDB

388 |   latestCollection dbDir

395 | resolveMeta :

396 |      {auto _ : HasIO io}

397 |   -> {auto _ : PackDirs}

398 |   -> (fetch : Bool)

399 |   -> URL

400 |   -> MetaCommit

401 |   -> EitherT PackErr io Commit

402 | resolveMeta _ u (MC x)     = pure x

403 | resolveMeta _ u (Fetch x)  = gitLatest u x

404 | resolveMeta b u (Latest x) = do

405 |   let cfile := commitFile u x

406 |   commitMissing <- fileMissing cfile

407 |   case commitMissing || b of

408 |     True  => do

409 |       c <- gitLatest u x

410 |       write cfile c.value

411 |       pure c

412 |     False => (\s => MkCommit $ trim s) <$> read cfile

417 | collectionTomlContent : DBName -> String

418 | collectionTomlContent db =

419 |   """

428 | export covering

429 | getConfig :

430 |      (0 c : Type)

431 |   -> {auto _   : Command c}

432 |   -> (args : ParsedArgs c)

433 |   -> {auto _   : HasIO io}

434 |   -> {auto pd  : PackDirs}

435 |   -> {auto td  : TmpDir}

436 |   -> EitherT PackErr io MetaConfig

437 | getConfig c args = do

438 |   -- relevant directories

439 |   coll       <- defaultColl

440 |   let cur = args.curDir

442 |   -- Initialize `pack.toml` if none exists

443 |   when !(fileMissing globalPackToml) $

444 |     write globalPackToml (initToml "scheme")

446 |   -- Initialize collection `pack.toml` if none exists

447 |   when !(fileMissing collectionToml) $

448 |     write collectionToml (collectionTomlContent coll)

450 |   localTomls  <- findInAllParentDirs (packToml ==) curDir

451 |   localConfs  <- for localTomls $ readFromTOML UserConfig

452 |   collToml    <- readOptionalFromTOML UserConfig collectionToml

453 |   global      <- readOptionalFromTOML UserConfig globalPackToml

455 |   let ini = foldl update (init coll) (global::collToml::localConfs)

457 |   conf' <- liftEither $ applyArgs c ini args

458 |   conf  <- adjConfig args.cmd conf'

460 |   let logRef := MkLogRef conf.logLevel

462 |   debug "Pack user dir is \{pd.user}"

463 |   debug "Pack state dir is \{pd.state}"

464 |   debug "Pack cache dir is \{pd.cache}"

465 |   debug "Pack bin dir is \{pd.bin}"

466 |   debug "Current directory is \{cur}"

467 |   case localTomls of

468 |     _::_ =>

469 |       logMany

470 |         Info

471 |         {inlineSingle=True}

472 |         "Found local config at"

473 |         (interpolate <$> localTomls)

474 |     []   => debug "No local config found"

475 |   info "Using package collection \{conf.collection}"

476 |   debug "Config loaded"

477 |   mkDir pd.user

478 |   mkDir pd.state

479 |   mkDir pd.cache

480 |   mkDir pd.bin

481 |   pure conf

484 | getLineBufferingCmd : HasIO io => io LineBufferingCmd

485 | getLineBufferingCmd = findCmd variants

487 |   where

488 |     findCmd : List (String, CmdArgList) -> io LineBufferingCmd

489 |     findCmd [] = pure $ MkLineBufferingCmd []

490 |     findCmd ((cmd, args)::rest) = do

491 |       0 <- system $ escapeCmd

492 |              ["type", cmd, NoEscape ">", "/dev/null", NoEscape "2>", "/dev/null"]

493 |         | _ => findCmd rest

494 |       0 <- system $ escapeCmd

495 |              [ cmd, "-oL", "ls", NoEscape ">", "/dev/null", NoEscape "2>", "/dev/null"]

496 |         | _ => findCmd rest

497 |       pure $ MkLineBufferingCmd $ [cmd] ++ args

499 |     variants : List (String, CmdArgList)

500 |     variants =

501 |       [ ("stdbuf",  ["-oL"])

502 |       , ("gstdbuf", ["-oL"])

503 |       ]

509 | pkgs : SortedMap PkgName Package

510 | pkgs = fromList $ (\c => (corePkgName c, Core c)) <$> corePkgs

513 | export covering

514 | loadDB :

515 |      {auto _ : HasIO io}

516 |   -> {auto _ : TmpDir}

517 |   -> {auto _ : PackDirs}

518 |   -> MetaConfig

519 |   -> EitherT PackErr io MetaDB

520 | loadDB mc = do

521 |   when !(missing dbDir) updateDB

522 |   debug "reading package collection"

523 |   raw <- readFromTOML MetaDB dbFile

524 |   case fileStem dbFile of

525 |     Just "HEAD" => pure $ map toLatest raw

526 |     _           => pure raw

530 | withCoreGit :

531 |      {auto _ : HasIO io}

532 |   -> {auto e : Env}

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

534 |   -> EitherT PackErr io a

535 | withCoreGit = withGit compiler e.db.idrisURL e.db.idrisCommit False

540 | cacheCoreIpkgFiles : HasIO io => Env => Path Abs -> EitherT PackErr io ()

541 | cacheCoreIpkgFiles dir = do

542 |   for_ corePkgs $ \c =>

543 |     copyFile (toAbsFile dir (coreIpkgPath c)) (coreCachePath c)

544 |   let api := coreCachePath IdrisApi

545 |   desc <- parseIpkgFile api api

546 |   write versionCachePath (maybe "0.0.0" show desc.desc.version)

550 | notCached : HasIO io => (e : Env) => PkgName -> Package -> io Bool

551 | notCached n (Git u c i _ _ _) = fileMissing $ ipkgCachePath n c i

552 | notCached n (Local d i _ _) = pure False

553 | notCached n (Core c)        = fileMissing $ coreCachePath c

556 | cachePkg :

557 |      {auto _ : HasIO io}

558 |   -> {auto e : Env}

559 |   -> PkgName

560 |   -> Package

561 |   -> EitherT PackErr io ()

562 | cachePkg n (Git u c i _ _ _) =

563 |   let cache  := ipkgCachePath n c i

564 |       tmpLoc := gitTmpDir n </> i

565 |    in withGit n u c False $ \dir => do

566 |         let pf := patchFile n i

567 |         when !(fileExists pf) (patch tmpLoc pf)

568 |         copyFile tmpLoc cache

569 | cachePkg n (Local d i _ _)    = pure ()

570 | cachePkg n (Core c)           =

571 |   let cache  := coreCachePath c

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

573 |    in withCoreGit cacheCoreIpkgFiles

576 | cachePkgs : HasIO io => (e : Env) => EitherT PackErr io PkgVersion

577 | cachePkgs =

578 |   let pkgs := toList e.all

579 |    in do

580 |      (S n,ml,ps) <- needCaching Lin 0 60 pkgs | (0,_,_) => readIdrisVersion

581 |      traverse_ (doCache (S n) ml) ps

582 |      readIdrisVersion

584 |   where

585 |     needCaching :

586 |          SnocList (Nat,PkgName,Package)

587 |       -> (count : Nat)

588 |       -> (maxLen : Nat)

589 |       -> List (PkgName,Package)

590 |       -> EitherT PackErr io (Nat,Nat,List (Nat,PkgName,Package))

591 |     needCaching sp n ml []               = pure (n, ml, sp <>> [])

592 |     needCaching sp n ml ((pn,pkg) :: ps) = do

593 |       True <- notCached pn pkg | False => needCaching sp n ml ps

594 |       let n'  := S n

595 |           ml' := max ml (length (interpolate pn) + 26)

596 |       needCaching (sp :< (n', pn, pkg)) n' ml' ps

598 |     cacheInfo : (tot, maxLength, ix : Nat) -> PkgName -> String

599 |     cacheInfo tot ml ix pn =

600 |       let line := padRight ml '.' "Caching package info for \{pn} "

601 |           stot := show tot

602 |           six  := padLeft (length stot) ' ' (show ix)

603 |        in "\{line} (\{six}/\{stot})"

605 |     doCache :

606 |           (tot : Nat)

607 |        -> (maxLenght : Nat)

608 |        -> (Nat,PkgName,Package)

609 |        -> EitherT PackErr io ()

610 |     doCache tot ml (n,pn,pkg) = do

611 |       cache (cacheInfo tot ml n pn)

612 |       cachePkg pn pkg

614 |     readIdrisVersion : EitherT PackErr io PkgVersion

615 |     readIdrisVersion = do

616 |       when !(fileMissing versionCachePath)

617 |         (cachePkg (corePkgName IdrisApi) $ Core IdrisApi)

618 |       s <- trim <$> read versionCachePath

619 |       let vers := MkPkgVersion $ map cast $ split ('.' ==) s

620 |       debug "compiler version is \{show vers}"

621 |       pure vers

625 | export covering

626 | env :

627 |      {auto _   : HasIO io}

628 |   -> {auto pd  : PackDirs}

629 |   -> {auto td  : TmpDir}

630 |   -> {auto ch  : LibCache}

631 |   -> {auto lbf : LineBufferingCmd}

632 |   -> (mc       : MetaConfig)

633 |   -> (fetch    : FetchMethod)

634 |   -> EitherT PackErr io Env

635 | env mc fetch = do

636 |   mdb <- loadDB mc

637 |   clk <- liftIO $ clockTime UTC

638 |   debug "clock time is \{show $ toNano clk}"

639 |   when (fetch == ClearCommits) (rmDir commitsDir)

640 |   db  <- traverseDB (resolveMeta $ fetch > MissingOnly) mdb

641 |   c   <- traverse (resolveMeta $ fetch > MissingOnly) db.idrisURL mc

643 |   let url    := fromMaybe db.idrisURL c.idrisURL

644 |       commit := fromMaybe db.idrisCommit c.idrisCommit

645 |       -- take the DB's idris commit into account

646 |       c'     := {allIdrisCommits $= (db.idrisCommit ::)} c

647 |       -- adjust the idrisCommit and URL to use according to user overrides

648 |       db'    := {idrisURL := url, idrisCommit := commit} db

649 |       pkgs   := SortedMap.fromList $ (\c => (corePkgName c, Core c)) <$> corePkgs

650 |       all    := fromMaybe empty $ lookup All c'.custom

651 |       loc    := fromMaybe empty $ lookup c'.collection c.custom

652 |       allps  := db.packages `mergeRight` all `mergeRight` loc `mergeRight` pkgs

653 |       env    := MkEnv pd td c' ch db' allps lbf clk

655 |   vers <- cachePkgs

656 |   pure $ {db $= setVersion vers} env

660 | export covering

661 | writeCollection :

662 |      {auto _ : HasIO io}

663 |   -> {auto _ : PackDirs}

664 |   -> {auto c : Config}

665 |   -> EitherT PackErr io ()

666 | writeCollection = do

667 |   str <- read globalPackToml

668 |   write collectionToml (collectionTomlContent c.collection)