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

415 | adjPkgMap :

416 |      {auto _ : HasIO io}

417 |   -> {auto _ : PackDirs}

418 |   -> (fetch : Bool)

419 |   -> List (PkgName, UserPackage)

420 |   -> PackageMap

421 |   -> EitherT PackErr io PackageMap

422 | adjPkgMap fetch []            m = pure m

423 | adjPkgMap fetch ((nm,up)::ps) m = adj >>= adjPkgMap fetch ps

424 |   where

425 |     adj : EitherT PackErr io PackageMap

426 |     adj =

427 |       case up of

428 |         Local d i p t => pure $ insert nm (Local d i p t) m

429 |         Core c        => pure $ insert nm (Core c) m

430 |         Git (Just u) (Just c) (Just i) p t n =>

431 |           (\x => insert nm (Git u x i (fromMaybe False p) t n) m) <$> resolveMeta fetch u c

432 |         Git mu mc mi mp mt mn => case lookup nm m of

433 |           Just (Git u c i p t n) =>

434 |            let u2 := fromMaybe u mu

435 |                i2 := fromMaybe i mi

436 |                p2 := fromMaybe p mp

437 |                t2 := mt <|> t

438 |                n2 := mn <|> n

439 |             in case mc of

440 |                  Nothing => pure $ insert nm (Git u2 c i2 p2 t2 n2) m

441 |                  Just y  =>

442 |                    (\x => insert nm (Git u2 x i2 p2 t2 n2) m) <$> resolveMeta fetch u y

443 |           _ => throwE (IncompletePkg nm)

448 | collectionTomlContent : DBName -> String

449 | collectionTomlContent db =

450 |   """

459 | export covering

460 | getConfig :

461 |      (0 c : Type)

462 |   -> {auto _   : Command c}

463 |   -> (args : ParsedArgs c)

464 |   -> {auto _   : HasIO io}

465 |   -> {auto pd  : PackDirs}

466 |   -> {auto td  : TmpDir}

467 |   -> EitherT PackErr io MetaConfig

468 | getConfig c args = do

469 |   -- relevant directories

470 |   coll       <- defaultColl

471 |   let cur = args.curDir

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

474 |   when !(fileMissing globalPackToml) $

475 |     write globalPackToml (initToml "scheme")

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

478 |   when !(fileMissing collectionToml) $

479 |     write collectionToml (collectionTomlContent coll)

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

482 |   localConfs  <- for localTomls $ readFromTOML UserConfig

483 |   collToml    <- readOptionalFromTOML UserConfig collectionToml

484 |   global      <- readOptionalFromTOML UserConfig globalPackToml

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

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

489 |   conf  <- adjConfig args.cmd conf'

491 |   let logRef := MkLogRef conf.logLevel

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

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

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

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

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

498 |   case localTomls of

499 |     _::_ =>

500 |       logMany

501 |         Info

502 |         {inlineSingle=True}

503 |         "Found local config at"

504 |         (interpolate <$> localTomls)

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

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

507 |   debug "Config loaded"

508 |   mkDir pd.user

509 |   mkDir pd.state

510 |   mkDir pd.cache

511 |   mkDir pd.bin

512 |   pure conf

515 | getLineBufferingCmd : HasIO io => io LineBufferingCmd

516 | getLineBufferingCmd = findCmd variants

518 |   where

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

520 |     findCmd [] = pure $ MkLineBufferingCmd []

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

522 |       0 <- system $ escapeCmd

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

524 |         | _ => findCmd rest

525 |       0 <- system $ escapeCmd

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

527 |         | _ => findCmd rest

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

530 |     variants : List (String, CmdArgList)

531 |     variants =

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

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

534 |       ]

540 | addCore : PackageMap -> PackageMap

541 | addCore m = foldl (\m,c => insert (corePkgName c) (Core c) m) m corePkgs

544 | export covering

545 | loadDB :

546 |      {auto _ : HasIO io}

547 |   -> {auto _ : TmpDir}

548 |   -> {auto _ : PackDirs}

549 |   -> MetaConfig

550 |   -> EitherT PackErr io MetaDB

551 | loadDB mc = do

552 |   when !(missing dbDir) updateDB

553 |   debug "reading package collection"

554 |   raw <- readFromTOML MetaDB dbFile

555 |   case fileStem dbFile of

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

557 |     _           => pure raw

561 | withCoreGit :

562 |      {auto _ : HasIO io}

563 |   -> {auto e : Env}

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

565 |   -> EitherT PackErr io a

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

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

572 | cacheCoreIpkgFiles dir = do

573 |   for_ corePkgs $ \c =>

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

575 |   let api := coreCachePath IdrisApi

576 |   desc <- parseIpkgFile api api

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

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

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

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

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

587 | cachePkg :

588 |      {auto _ : HasIO io}

589 |   -> {auto e : Env}

590 |   -> PkgName

591 |   -> Package

592 |   -> EitherT PackErr io ()

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

594 |   let cache  := ipkgCachePath n c i

595 |       tmpLoc := gitTmpDir n </> i

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

597 |         let pf := patchFile n i

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

599 |         copyFile tmpLoc cache

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

601 | cachePkg n (Core c)           =

602 |   let cache  := coreCachePath c

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

604 |    in withCoreGit cacheCoreIpkgFiles

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

608 | cachePkgs =

609 |   let pkgs := toList e.all

610 |    in do

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

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

613 |      readIdrisVersion

615 |   where

616 |     needCaching :

617 |          SnocList (Nat,PkgName,Package)

618 |       -> (count : Nat)

619 |       -> (maxLen : Nat)

620 |       -> List (PkgName,Package)

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

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

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

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

625 |       let n'  := S n

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

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

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

630 |     cacheInfo tot ml ix pn =

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

632 |           stot := show tot

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

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

636 |     doCache :

637 |           (tot : Nat)

638 |        -> (maxLenght : Nat)

639 |        -> (Nat,PkgName,Package)

640 |        -> EitherT PackErr io ()

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

642 |       cache (cacheInfo tot ml n pn)

643 |       cachePkg pn pkg

645 |     readIdrisVersion : EitherT PackErr io PkgVersion

646 |     readIdrisVersion = do

647 |       when !(fileMissing versionCachePath)

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

649 |       s <- trim <$> read versionCachePath

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

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

652 |       pure vers

656 | export covering

657 | env :

658 |      {auto _   : HasIO io}

659 |   -> {auto pd  : PackDirs}

660 |   -> {auto td  : TmpDir}

661 |   -> {auto ch  : LibCache}

662 |   -> {auto lbf : LineBufferingCmd}

663 |   -> (mc       : MetaConfig)

664 |   -> (fetch    : FetchMethod)

665 |   -> EitherT PackErr io Env

666 | env mc fetch = do

667 |   mdb <- loadDB mc

668 |   clk <- liftIO $ clockTime UTC

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

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

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

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

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

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

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

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

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

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

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

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

683 |   -- adjusting list of packages to customizations

684 |   p1   <- adjPkgMap (fetch > MissingOnly) (kvList all) (addCore db.packages)

685 |   p2   <- adjPkgMap (fetch > MissingOnly) (kvList loc) p1

686 |   let env    := MkEnv pd td c' ch db' p2 lbf clk

688 |   vers <- cachePkgs

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

693 | export covering

694 | writeCollection :

695 |      {auto _ : HasIO io}

696 |   -> {auto _ : PackDirs}

697 |   -> {auto c : Config}

698 |   -> EitherT PackErr io ()

699 | writeCollection = do

700 |   str <- read globalPackToml

701 |   write collectionToml (collectionTomlContent c.collection)