0 | module Pack.Runner.Install

  2 | import Core.FC

  3 | import Data.IORef

  4 | import Data.Maybe

  5 | import Data.SortedMap

  6 | import Idris.Package.Types

  7 | import Pack.Config

  8 | import Pack.Core

  9 | import Pack.Database

 10 | import Pack.Runner.Database

 11 | import System.Escape

 13 | %default total

 19 | pathDirs :

 20 |      {auto _ : HasIO io}

 21 |   -> {auto _ : PackDirs}

 22 |   -> {auto e : Env}

 23 |   -> (pre : Path Abs)

 24 |   -> (pth : PkgName -> Hash -> Package -> Path Abs)

 25 |   -> EitherT PackErr io DirList

 26 | pathDirs pre pth = do

 27 |   rs <- traverse resolveLib (keys e.all)

 28 |   ps <- filterM (\r => exists $ pth r.name r.hash r.pkg) rs

 29 |   let ps' := filter (not . isCorePkg . value . name) ps

 30 |   pure $ (pre ::) $ map (\r => pth r.name r.hash r.pkg) ps'

 35 | packagePathDirs : HasIO io => Env -> EitherT PackErr io DirList

 36 | packagePathDirs _ = pathDirs idrisInstallDir pkgPathDir

 41 | packageLibDirs : HasIO io => Env -> EitherT PackErr io DirList

 42 | packageLibDirs _ = pathDirs idrisLibDir pkgLibDir

 47 | packageDataDirs : HasIO io => Env -> EitherT PackErr io DirList

 48 | packageDataDirs _ = pathDirs idrisDataDir pkgDataDir

 53 | packagePath : HasIO io => Env => EitherT PackErr io EnvVar

 54 | packagePath = IdrisPackagePathVar <$> packagePathDirs %search

 59 | libPath : HasIO io => Env => EitherT PackErr io EnvVar

 60 | libPath = IdrisLibsVar <$> packageLibDirs %search

 65 | dataPath : HasIO io => Env => EitherT PackErr io EnvVar

 66 | dataPath = IdrisDataVar <$> packageDataDirs %search

 72 | buildEnv : HasIO io => Env => EitherT PackErr io (List EnvVar)

 73 | buildEnv =

 74 |   let pre := if useRacket then [IdrisCodegenVar Racket] else []

 75 |    in (pre ++ ) <$> sequence [packagePath, libPath, dataPath]

 80 | idrisWithPkg :

 81 |      {auto _ : HasIO io}

 82 |   -> {auto _ : IdrisEnv}

 83 |   -> ResolvedLib t

 84 |   -> EitherT PackErr io (CmdArgList, List EnvVar)

 85 | idrisWithPkg rl =

 86 |   (idrisWithCG ++ ["-p", name rl],) <$> buildEnv

 91 | idrisWithPkgs :

 92 |      {auto _ : HasIO io}

 93 |   -> {auto _ : IdrisEnv}

 94 |   -> List (ResolvedLib t)

 95 |   -> EitherT PackErr io (CmdArgList, List EnvVar)

 96 | idrisWithPkgs [] = pure (idrisWithCG, [])

 97 | idrisWithPkgs pkgs =

 98 |   let ps = concatMap (\p => ["-p", name p]) pkgs

 99 |    in (idrisWithCG ++ ps,) <$> buildEnv

106 | ipkgCodeGen : (e : Env) => PkgDesc -> Codegen

107 | ipkgCodeGen desc = case e.config.codegen of

108 |   Default => getCG (maybe [] (filter (not . null) . words . snd) desc.options)

109 |   cg      => cg

111 |   where

112 |     getCG : List String -> Codegen

113 |     getCG ("--cg"      :: cg :: _) = fromString cg

114 |     getCG ("--codegen" :: cg :: _) = fromString cg

115 |     getCG [_]                      = Default

116 |     getCG []                       = Default

117 |     getCG (h :: t)                 = getCG t

119 | coreGitDir : (e : Env) => Path Abs

120 | coreGitDir = gitTmpDir compiler

122 | copyApp : HasIO io => IdrisEnv => SafeApp -> EitherT PackErr io ()

123 | copyApp ra =

124 |   let dir := pkgBinDir ra.name ra.hash ra.pkg

125 |    in do

126 |      debug "Copying application to \{dir}"

127 |      mkDir dir

128 |      sys ["cp", "-r", Escapable "\{buildPath ra.desc}/exec/" ++ NoEscape "*", dir]

130 | noAppError : (app : PkgName) -> List String

131 | noAppError app = lines $ """

138 | pthStr : (c : Config) => PackDirs => Bool -> (packBinaryLoc : String) -> String

139 | pthStr False _ = ""

140 | pthStr True packBinaryLoc =

141 |   let racket := if useRacket then "export \{schemeVar}" else ""

142 |    in """

156 | appLink :

157 |      {auto _ : HasIO io}

158 |   -> {auto e : Env}

159 |   -> {auto _ : PackDirs}

160 |   -> (exec        : Body)

161 |   -> (app         : PkgName)

162 |   -> (withPkgPath : Bool)

163 |   -> (codeGen     : Codegen)

164 |   -> EitherT PackErr io ()

165 | appLink exec app withPkgPath cg =

166 |   let

167 |       interp  := case cg of

168 |         Node => "node "

169 |         _ => ""

170 |       target  := MkF packBinDir exec

171 |       content := """

187 |    in write target content >> sys ["chmod", "+x", target]

189 | installCmd : (withSrc : Bool) -> CmdArgList

190 | installCmd True  = ["--install-with-src"]

191 | installCmd False = ["--install"]

197 | export covering

198 | checkBuildDir :  HasIO io => (e : IdrisEnv) => Desc Safe -> EitherT PackErr io ()

199 | checkBuildDir d =

200 |   let buildDir := buildPath d

201 |       version  := the (File Abs) (buildDir /> ".idrisCommit")

202 |       commit   := e.env.db.idrisCommit.value

203 |    in do

204 |      str <- readIfExists version ""

205 |      when (str /= commit) $ do

206 |        rmDir buildDir

207 |        write version commit

209 | dependsMsg : Path Abs -> String

210 | dependsMsg p = """

219 | export covering

220 | libPkg :

221 |      {auto _     : HasIO io}

222 |   -> {auto e     : IdrisEnv}

223 |   -> (env        : List EnvVar)

224 |   -> (logLevel   : LogLevel)

225 |   -> (cleanBuild : Bool)

226 |   -> (cmd        : CmdArgList)

227 |   -> (desc       : Desc Safe)

228 |   -> EitherT PackErr io ()

229 | libPkg env lvl cleanBuild cmd desc =

230 |   let exe := idrisWithCG

231 |       s   := exe ++ cmd ++ [desc.path.file]

232 |    in do

233 |      pre <- (env ++) <$> buildEnv

234 |      debug "About to run: \{escapeCmd s}"

235 |      when cleanBuild (checkBuildDir desc)

237 |      -- warn if we find a `depends` directory in a local package

238 |      let dependsDir := desc.path.parent /> "depends"

239 |      when !(exists dependsDir) $

240 |        when e.env.config.warnDepends $ warn (dependsMsg dependsDir)

242 |      inDir (desc.path.parent) (\_ => sysWithEnvAndLog lvl s pre)

248 | hasTTC : String -> Bool

249 | hasTTC = any (("--ttc-version" `isPrefixOf`) . trim) . lines

252 | getTTCVersion : HasIO io => Env => EitherT PackErr io TTCVersion

253 | getTTCVersion = do

254 |   hlp <- sysRun [idrisExec, "--help"]

255 |   case hasTTC hlp of

256 |     True  => do

257 |       str <- sysRun [idrisExec, "--ttc-version"]

258 |       case Body.parse (trim str) of

259 |         Just v  => debug "Using TTC version \{v}" $> TTCV (Just v)

260 |         Nothing => warn "Failed to parse TTC version \{str}" $> TTCV Nothing

261 |     False => debug "No TTC version given by Idris" $> TTCV Nothing

264 | tryDirectBuild : HasIO io => Env => io (Either PackErr ())

265 | tryDirectBuild =

266 |   runEitherT $ do

267 |     sysAndLog Build ["make", "support"]

268 |     sysAndLog Build ["make", "idris2-exec", prefixVar, schemeVar]

270 | idrisCleanup : HasIO io => Env => io ()

271 | idrisCleanup =

272 |   ignoreError $ do

273 |     sysAndLog Build ["make", "clean-libs"]

274 |     sysAndLog Build ["rm", "-r", "build/ttc", "build/exec"]

276 | idrisBootstrapWithStage3 : HasIO io => (e : Env) => Path Abs -> EitherT PackErr io ()

277 | idrisBootstrapWithStage3 dir = do

278 |   let bootstrappedPrefixVar = PrefixVar dir

279 |   sysAndLog Build ["make", bootstrapCmd, bootstrappedPrefixVar, schemeVar]

280 |   debug "Install bootstrapped Idris..."

281 |   sysAndLog Build ["make", "bootstrap-install", bootstrappedPrefixVar, schemeVar]

282 |   idrisCleanup

284 |   debug "Stage 3: Rebuilding Idris..."

285 |   let idrisBootVar = IdrisBootVar $ dir /> "bin" /> "idris2"

286 |   let idrisDataVar = IdrisDataVar [dir /> idrisDir /> "support"]

287 |   sysAndLog Build ["make", "idris2-exec", prefixVar, idrisBootVar, idrisDataVar, schemeVar]

289 |   ignoreError $ sysAndLog Build ["rm", "-rf", dir]

291 | idrisBootstrap : HasIO io => (e : Env) => Path Abs -> EitherT PackErr io ()

292 | idrisBootstrap dir = do

293 |   debug "Bootstrapping Idris..."

294 |   if e.config.bootstrapStage3

295 |      then idrisBootstrapWithStage3 $ dir </> "bootstrapped"

296 |      else sysAndLog Build ["make", bootstrapCmd, prefixVar, schemeVar]

297 |   ignoreError $ sysAndLog Build ["make", "bootstrap-clean"]

300 | export covering

301 | mkIdris : HasIO io => (e : Env) => EitherT PackErr io IdrisEnv

302 | mkIdris = do

303 |   debug "Checking Idris installation"

304 |   when !(missing idrisInstallDir) $ do

305 |     debug "No Idris compiler found. Installing..."

306 |     withCoreGit $ \dir => do

307 |       case e.config.bootstrap of

308 |         True  => idrisBootstrap dir

309 |         False =>

310 |           -- if building with an existing installation fails for whatever reason

311 |           -- we revert to bootstrapping

312 |           tryDirectBuild >>= \case

313 |             Left x => do

314 |               warn "Building Idris failed. Trying to bootstrap now."

315 |               idrisBootstrap dir

316 |             Right () => pure ()

318 |       sysAndLog Build ["make", "install-support", prefixVar]

319 |       sysAndLog Build ["make", "install-idris2", prefixVar]

320 |       idrisCleanup

321 |       cacheCoreIpkgFiles dir

323 |   appLink "idris2" "idris2" True Default

324 |   ttc <- getTTCVersion

325 |   pure $ MkIdrisEnv %search ttc ItHasIdris

331 | withSrcStr : (c : Config) => String

332 | withSrcStr = case c.withSrc of

333 |   True  => " (with sources)"

334 |   False => ""

336 | maybeGiveNotice : HasIO io => Config => SafeLib -> io ()

337 | maybeGiveNotice (RL (Git _ _ _ _ _ (Just notice)) _ _ _ _ _) = warn notice

338 | maybeGiveNotice _ = pure ()

340 | installImpl :

341 |      {auto _ : HasIO io}

342 |   -> {auto e : IdrisEnv}

343 |   -> (dir : Path Abs)

344 |   -> SafeLib

345 |   -> EitherT PackErr io ()

346 | installImpl dir rl =

347 |   let pre      := libInstallPrefix rl

348 |       instCmd  := installCmd e.env.config.withSrc

349 |       libDir   := rl.desc.path.parent </> "lib"

350 |    in do

351 |      info "Installing library\{withSrcStr}: \{name rl}"

352 |      maybeGiveNotice rl

353 |      when (isInstalled rl) $ do

354 |        info "Removing currently installed version of \{name rl}"

355 |        rmDir (pkgInstallDir rl.name rl.hash rl.pkg rl.desc)

356 |        rmDir (pkgLibDir rl.name rl.hash rl.pkg)

357 |      libPkg pre Build True ["--build"] rl.desc

358 |      libPkg pre Debug False instCmd rl.desc

359 |      debug "checking if libdir at \{libDir} exists"

360 |      when !(exists libDir) $ do

361 |        debug "copying lib dir"

362 |        copyDir libDir (pkgLibDir rl.name rl.hash rl.pkg)

364 | preInstall :

365 |      {auto _ : HasIO io}

366 |   -> {auto e : IdrisEnv}

367 |   -> SafeLib

368 |   -> EitherT PackErr io ()

369 | preInstall rl = withPkgEnv rl.name rl.pkg $ \dir =>

370 |   let ipkgAbs := ipkg dir rl.pkg

371 |    in case rl.pkg of

372 |         Git u c ipkg _ _ _ => do

373 |           let cache := ipkgCachePath rl.name c ipkg

374 |           copyFile cache ipkgAbs

375 |         Local _ _ _ _ => pure ()

377 |         Core c => do

378 |           let cache   := coreCachePath c

379 |           copyFile cache ipkgAbs

380 |           case c of

381 |             IdrisApi =>

382 |               sysAndLog Build ["make", "src/IdrisPaths.idr", prefixVar]

383 |             _        => pure ()

386 | installLib :

387 |      {auto _ : HasIO io}

388 |   -> {auto e : IdrisEnv}

389 |   -> SafeLib

390 |   -> EitherT PackErr io ()

391 | installLib rl = case rl.status of

392 |   Installed _ _ => pure ()

393 |   _             => do

394 |     preInstall rl

395 |     withPkgEnv rl.name rl.pkg $ \dir => do

396 |       installImpl dir rl

397 |       case rl.pkg of

398 |         Local _ _ _ _ =>

399 |           when (not $ isInstalled rl) $ do

400 |             debug "writing \{nanoString} to \{libTimestamp rl.name}"

401 |             write (libTimestamp rl.name) nanoString

402 |         _             => pure ()

404 |     uncacheLib (name rl)

413 | installApp :

414 |      {auto _ : HasIO io}

415 |   -> {auto e : IdrisEnv}

416 |   -> (withWrapperScript : Bool)

417 |   -> SafeApp

418 |   -> EitherT PackErr io ()

419 | installApp b ra =

420 |   let cg := ipkgCodeGen ra.desc.desc

421 |   in case ra.status of

422 |     BinInstalled _ => pure ()

423 |     Installed    _ => case b of

424 |       False => pure ()

425 |       True  => appLink ra.exec ra.name (usePackagePath ra) cg

426 |     _            => withPkgEnv ra.name ra.pkg $ \dir =>

427 |       let ipkgAbs := ipkg dir ra.pkg

428 |        in case ra.pkg of

429 |             Core _            => pure ()

430 |             Git u c ipkg pp _ _ => do

431 |               let cache   := ipkgCachePath ra.name c ipkg

432 |               copyFile cache ipkgAbs

433 |               libPkg [] Build True ["--build"] (notPackIsSafe ra.desc)

434 |               copyApp ra

435 |               when b $ appLink ra.exec ra.name pp cg

436 |             Local _ _ pp _    => do

437 |               libPkg [] Build True ["--build"] (notPackIsSafe ra.desc)

438 |               copyApp ra

439 |               when b $ appLink ra.exec ra.name pp cg

440 |               write (libTimestamp ra.name) nanoString

449 | installDocs :

450 |      {auto _ : HasIO io}

451 |   -> {auto e : IdrisEnv}

452 |   -> SafeLib

453 |   -> EitherT PackErr io ()

454 | installDocs rl = case rl.status of

455 |   Installed _ True => pure ()

456 |   _                => withPkgEnv rl.name rl.pkg $ \dir => do

457 |     let docsDir : Path Abs

458 |         docsDir = buildPath rl.desc /> "docs"

460 |         pre : List EnvVar

461 |         pre = libInstallPrefix rl

463 |         htmlDir : Path Abs

464 |         htmlDir = docsDir /> "docs"

466 |     info "Building source docs for: \{name rl}"

467 |     preInstall rl

468 |     libPkg pre Build False ["--mkdoc"] rl.desc

470 |     when e.env.config.useKatla $ do

471 |       info "Building highlighted sources for: \{name rl}"

472 |       mkDir htmlDir

473 |       rp <- resolveApp "katla"

474 |       let katla := pkgExec rp.name rp.hash rp.pkg rp.exec

475 |       fs <- map (MkF htmlDir) <$> htmlFiles htmlDir

476 |       for_ fs $ \htmlFile =>

477 |         let Just ds@(MkDS _ src ttm srcHtml) := sourceForDoc rl.desc htmlFile

478 |               | Nothing => pure ()

479 |          in when !(srcExists ds) $ do

480 |               sysAndLog Build [katla, "html", src, ttm, NoEscape ">", srcHtml]

481 |               insertSources ds

483 |     let docs := pkgDocs rl.name rl.hash rl.pkg rl.desc

484 |     when !(exists docs) (rmDir docs)

485 |     copyDir docsDir docs

486 |     uncacheLib (name rl)

488 | katla : (c : Config) => List (InstallType, PkgName)

489 | katla = if c.withDocs && c.useKatla then [(App False, "katla")] else []

491 | autoPairs : (c : Config) => List (InstallType, PkgName)

492 | autoPairs =

493 |      map ((Library,) . corePkgName) [ Prelude, Base, Network ]

494 |   ++ map (Library,) c.autoLibs

495 |   ++ map (App True,) c.autoApps

497 | libInfo : List SafePkg -> List String

498 | libInfo = mapMaybe $ \case Lib rl  => Just "\{rl.name}"

499 |                            App _ _ => Nothing

501 | appInfo : List SafePkg -> List String

502 | appInfo = mapMaybe $ \case App _ ra => Just "\{ra.name}"

503 |                            Lib _    => Nothing

508 | export covering

509 | install :

510 |      {auto _ : HasIO io}

511 |   -> {auto e : IdrisEnv}

512 |   -> List (InstallType, PkgName)

513 |   -> EitherT PackErr io ()

514 | install ps = do

515 |   all <- plan $ katla <+> autoPairs <+> ps

516 |   logMany Info "Installing libraries:" (libInfo all)

517 |   logMany Info "Installing apps:" (appInfo all)

518 |   for_ all $ \case Lib rl   => installLib rl

519 |                    App b rl => installApp b rl

521 |   when e.env.config.withDocs $

522 |     for_ all $ \case Lib rl  => installDocs rl

523 |                      App _ _ => pure ()

528 | export covering %inline

529 | installLibs : HasIO io => IdrisEnv => List PkgName -> EitherT PackErr io ()

530 | installLibs = install . map (Library,)

535 | export covering %inline

536 | installApps : HasIO io => IdrisEnv => List PkgName -> EitherT PackErr io ()

537 | installApps = install . map (App True,)

541 | export covering

542 | installDeps :

543 |      {auto _ : HasIO io}

544 |   -> {auto _ : IdrisEnv}

545 |   -> Desc Safe

546 |   -> EitherT PackErr io ()

547 | installDeps = install . map (Library,) . dependencies

550 | export covering

551 | idrisEnv :

552 |      {auto _ : HasIO io}

553 |   -> {auto _ : PackDirs}

554 |   -> {auto _ : TmpDir}

555 |   -> {auto _ : LibCache}

556 |   -> {auto _ : LineBufferingCmd}

557 |   -> MetaConfig

558 |   -> (fetch : FetchMethod)

559 |   -> EitherT PackErr io IdrisEnv

560 | idrisEnv mc fetch = env mc fetch >>= (\e => mkIdris)

563 | export covering

564 | update : HasIO io => IdrisEnv -> EitherT PackErr io ()

565 | update e =

566 |   let bin  := packBinDir

567 |    in do

568 |      info "Updating pack. If this fails, try switching to the latest package collection."

569 |      commit <- maybe (gitLatest packRepo "main") pure packCommit

570 |      info "Using commit \{commit}"

572 |      withGit "pack" packRepo commit True $ \dir => do

573 |        let ipkg := MkF dir "pack.ipkg"

574 |        d <- parseLibIpkg ipkg ipkg

575 |        installDeps d

576 |        let installDir    := packInstallDir commit

577 |            installedExec := installDir /> "pack"

578 |        ex <- exists installedExec

579 |        case ex of

580 |          True  => link installedExec packExec

581 |          False => do

582 |            libPkg [] Build True ["--build"] d

583 |            mkDir installDir

584 |            sys ["cp", "-r", NoEscape "build/exec/*", installDir]

585 |            link installedExec packExec

592 | removeApp : HasIO io => Env => PkgName -> EitherT PackErr io ()

593 | removeApp n = do

594 |   info "Removing application \{n}"

595 |   ra <- resolveApp n

596 |   rmFile (pathExec ra.exec)

597 |   rmDir (pkgBinDir ra.name ra.hash ra.pkg)

600 | removeLib : HasIO io => Env => PkgName -> EitherT PackErr io ()

601 | removeLib n = do

602 |   rl <- resolveLib n

603 |   case isInstalled rl of

604 |     True  => do

605 |       info "Removing library \{n}"

606 |       rmDir (pkgInstallDir rl.name rl.hash rl.pkg rl.desc)

607 |       rmDir (pkgLibDir rl.name rl.hash rl.pkg)

608 |     False => warn "Package \{n} is not installed. Ignoring."

611 | export covering

612 | remove : HasIO io => Env => List (PkgType,PkgName) -> EitherT PackErr io ()

613 | remove ps = do

614 |   ref <- emptyCache

615 |   for_ ps  $ \case (PLib,n) => removeLib n

616 |                    (PApp,n) => removeApp n

619 | export covering

620 | removeLibs : HasIO io => Env => List PkgName -> EitherT PackErr io ()

621 | removeLibs ns = do

622 |   checkDeletable ns

623 |   remove $ map (PLib,) ns

626 | export covering

627 | removeApps : HasIO io => Env => List PkgName -> EitherT PackErr io ()

628 | removeApps = remove . map (PApp,)