0 | module Idris.Package

   2 | import Compiler.Common

   4 | import Core.Directory

   5 | import Core.Metadata

   6 | import Core.Unify

   8 | import Data.Maybe

   9 | import Data.SortedMap

  10 | import Data.String

  11 | import Data.These

  13 | import Parser.Package

  14 | import System

  15 | import System.Directory

  16 | import Libraries.System.Directory.Tree

  17 | import System.File

  19 | import Libraries.Data.StringMap

  20 | import Libraries.Data.StringTrie

  21 | import Libraries.Data.WithDefault

  22 | import Libraries.Text.Parser

  23 | import Libraries.Utils.Path

  24 | import Libraries.Text.PrettyPrint.Prettyprinter.Render.String

  26 | import Idris.CommandLine

  27 | import Idris.Doc.HTML

  28 | import Idris.Doc.String

  29 | import Idris.Error

  30 | import Idris.ModTree

  31 | import Idris.Pretty

  32 | import Idris.ProcessIdr

  33 | import Idris.REPL

  34 | import Idris.SetOptions

  35 | import Idris.Syntax

  36 | import Idris.Version

  38 | import public Idris.Package.Types

  39 | import Idris.Package.Init

  40 | import Idris.Package.ToJson

  42 | %default covering

  44 | installDir : PkgDesc -> String

  45 | installDir p = name p

  46 |             ++ "-"

  47 |             ++ show (fromMaybe (MkPkgVersion (0 ::: [])) (version p))

  49 | data DescField  : Type where

  50 |   PVersion      : FC -> PkgVersion -> DescField

  51 |   PLangVersions : FC -> PkgVersionBounds -> DescField

  52 |   PVersionDep   : FC -> String -> DescField

  53 |   PAuthors      : FC -> String -> DescField

  54 |   PMaintainers  : FC -> String -> DescField

  55 |   PLicense      : FC -> String -> DescField

  56 |   PBrief        : FC -> String -> DescField

  57 |   PReadMe       : FC -> String -> DescField

  58 |   PHomePage     : FC -> String -> DescField

  59 |   PSourceLoc    : FC -> String -> DescField

  60 |   PBugTracker   : FC -> String -> DescField

  61 |   PDepends      : List Depends -> DescField

  62 |   PModules      : List (FC, ModuleIdent) -> DescField

  63 |   PMainMod      : FC -> ModuleIdent -> DescField

  64 |   PExec         : String -> DescField

  65 |   POpts         : FC -> String -> DescField

  66 |   PSourceDir    : FC -> String -> DescField

  67 |   PBuildDir     : FC -> String -> DescField

  68 |   POutputDir    : FC -> String -> DescField

  69 |   PPrebuild     : FC -> String -> DescField

  70 |   PPostbuild    : FC -> String -> DescField

  71 |   PPreinstall   : FC -> String -> DescField

  72 |   PPostinstall  : FC -> String -> DescField

  73 |   PPreclean     : FC -> String -> DescField

  74 |   PPostclean    : FC -> String -> DescField

  76 | field : String -> Rule DescField

  77 | field fname

  78 |       = strField PAuthors "authors"

  79 |     <|> strField PMaintainers "maintainers"

  80 |     <|> strField PLicense "license"

  81 |     <|> strField PBrief "brief"

  82 |     <|> strField PReadMe "readme"

  83 |     <|> strField PHomePage "homepage"

  84 |     <|> strField PSourceLoc "sourceloc"

  85 |     <|> strField PBugTracker "bugtracker"

  86 |     <|> strField POpts "options"

  87 |     <|> strField POpts "opts"

  88 |     <|> strField PSourceDir "sourcedir"

  89 |     <|> strField PBuildDir "builddir"

  90 |     <|> strField POutputDir "outputdir"

  91 |     <|> strField PPrebuild "prebuild"

  92 |     <|> strField PPostbuild "postbuild"

  93 |     <|> strField PPreinstall "preinstall"

  94 |     <|> strField PPostinstall "postinstall"

  95 |     <|> strField PPreclean "preclean"

  96 |     <|> strField PPostclean "postclean"

  97 |     <|> do start <- location

  98 |            ignore $ exactProperty "version"

  99 |            mustWork $ do

 100 |              equals

 101 |              vs <- choose stringLit (sepBy1 dot' integerLit)

 102 |              end <- location

 103 |              the (EmptyRule _) $ case vs of

 104 |                 Left v   => pure (PVersionDep (MkFC (PhysicalPkgSrc fname) start end) v)

 105 |                 Right vs => pure (PVersion (MkFC (PhysicalPkgSrc fname) start end)

 106 |                                     (MkPkgVersion (fromInteger <$> vs)))

 107 |     <|> do start <- location

 108 |            ignore $ exactProperty "langversion"

 109 |            mustWork $ do

 110 |              lvs <- langversions

 111 |              end <- location

 112 |              pure (PLangVersions (MkFC (PhysicalPkgSrc fname) start end) lvs)

 113 |     <|> do start <- location

 114 |            ignore $ exactProperty "version"

 115 |            mustWork $ do

 116 |              equals

 117 |              v <- stringLit

 118 |              end <- location

 119 |              pure (PVersionDep (MkFC (PhysicalPkgSrc fname) start end) v)

 120 |     <|> do ignore $ exactProperty "depends"

 121 |            mustWork $ do

 122 |              equals

 123 |              ds <- sep depends

 124 |              pure (PDepends ds)

 125 |     <|> do ignore $ exactProperty "modules"

 126 |            mustWork $ do

 127 |              equals

 128 |              ms <- sep (do start <- location

 129 |                            m <- moduleIdent

 130 |                            end <- location

 131 |                            pure (MkFC (PhysicalPkgSrc fname) start end, m))

 132 |              pure (PModules ms)

 133 |     <|> do ignore $ exactProperty "main"

 134 |            mustWork $ do

 135 |              equals

 136 |              start <- location

 137 |              m <- moduleIdent

 138 |              end <- location

 139 |              pure (PMainMod (MkFC (PhysicalPkgSrc fname) start end) m)

 140 |     <|> do ignore $ exactProperty "executable"

 141 |            mustWork $ do

 142 |              equals

 143 |              e <- (stringLit <|> packageName)

 144 |              pure (PExec e)

 145 |   where

 146 |     data Bound = LT PkgVersion Bool | GT PkgVersion Bool

 148 |     bound : Rule (List Bound)

 149 |     bound

 150 |         = do lte

 151 |              vs <- sepBy1 dot' integerLit

 152 |              pure [LT (MkPkgVersion (fromInteger <$> vs)) True]

 153 |       <|> do gte

 154 |              vs <- sepBy1 dot' integerLit

 155 |              pure [GT (MkPkgVersion (fromInteger <$> vs)) True]

 156 |       <|> do lt

 157 |              vs <- sepBy1 dot' integerLit

 158 |              pure [LT (MkPkgVersion (fromInteger <$> vs)) False]

 159 |       <|> do gt

 160 |              vs <- sepBy1 dot' integerLit

 161 |              pure [GT (MkPkgVersion (fromInteger <$> vs)) False]

 162 |       <|> do eqop

 163 |              vs <- sepBy1 dot' integerLit

 164 |              pure [LT (MkPkgVersion (fromInteger <$> vs)) True,

 165 |                    GT (MkPkgVersion (fromInteger <$> vs)) True]

 167 |     mkBound : List Bound -> PkgVersionBounds -> EmptyRule PkgVersionBounds

 168 |     mkBound (LT b i :: bs) pkgbs

 169 |         = maybe (mkBound bs ({ upperBound := Just b,

 170 |                                upperInclusive := i } pkgbs))

 171 |                 (\_ => fail "Dependency already has an upper bound")

 172 |                 pkgbs.upperBound

 173 |     mkBound (GT b i :: bs) pkgbs

 174 |         = maybe (mkBound bs ({ lowerBound := Just b,

 175 |                                lowerInclusive := i } pkgbs))

 176 |                 (\_ => fail "Dependency already has a lower bound")

 177 |                 pkgbs.lowerBound

 178 |     mkBound [] pkgbs = pure pkgbs

 180 |     langversions : EmptyRule PkgVersionBounds

 181 |     langversions

 182 |         = do bs <- sepBy andop bound

 183 |              mkBound (concat bs) anyBounds

 185 |     depends : Rule Depends

 186 |     depends

 187 |         = do name <- packageName

 188 |              bs <- sepBy andop bound

 189 |              pure (MkDepends name !(mkBound (concat bs) anyBounds))

 191 |     strField : (FC -> String -> DescField) -> String -> Rule DescField

 192 |     strField fieldConstructor fieldName

 193 |         = do start <- location

 194 |              ignore $ exactProperty fieldName

 195 |              mustWork $ do

 196 |                equals

 197 |                str <- stringLit

 198 |                end <- location

 199 |                pure $ fieldConstructor (MkFC (PhysicalPkgSrc fname) start end) str

 201 | parsePkgDesc : String -> Rule (String, List DescField)

 202 | parsePkgDesc fname

 203 |     = do ignore $ exactProperty "package"

 204 |          name <- packageName

 205 |          fields <- many (field fname)

 206 |          EndOfInput <- peek

 207 |             | DotSepIdent _ name => fail "Unrecognised property \{show name}"

 208 |             | tok => fail "Expected end of file"

 209 |          pure (name, fields)

 211 | data ParsedMods : Type where

 213 | data MainMod : Type where

 215 | addField : {auto c : Ref Ctxt Defs} ->

 216 |            {auto s : Ref Syn SyntaxInfo} ->

 217 |            {auto o : Ref ROpts REPLOpts} ->

 218 |            {auto p : Ref ParsedMods (List (FC, ModuleIdent))} ->

 219 |            {auto m : Ref MainMod (Maybe (FC, ModuleIdent))} ->

 220 |            DescField -> PkgDesc -> Core PkgDesc

 221 | addField (PVersion fc n)       pkg = pure $ { version := Just n } pkg

 222 | addField (PLangVersions fc bs) pkg = pure $ { langversion := Just bs } pkg

 223 | addField (PVersionDep fc n)   pkg

 224 |     = do emitWarning (Deprecated fc "version numbers must now be of the form x.y.z" Nothing)

 225 |          pure pkg

 226 | addField (PAuthors fc a)     pkg = pure $ { authors := Just a } pkg

 227 | addField (PMaintainers fc a) pkg = pure $ { maintainers := Just a } pkg

 228 | addField (PLicense fc a)     pkg = pure $ { license := Just a } pkg

 229 | addField (PBrief fc a)       pkg = pure $ { brief := Just a } pkg

 230 | addField (PReadMe fc a)      pkg = pure $ { readme := Just a } pkg

 231 | addField (PHomePage fc a)    pkg = pure $ { homepage := Just a } pkg

 232 | addField (PSourceLoc fc a)   pkg = pure $ { sourceloc := Just a } pkg

 233 | addField (PBugTracker fc a)  pkg = pure $ { bugtracker := Just a } pkg

 234 | addField (PDepends ds)       pkg = pure $ { depends := ds } pkg

 237 | addField (PModules ms)       pkg = do put ParsedMods ms

 238 |                                       pure pkg

 239 | addField (PMainMod loc n)    pkg = do put MainMod (Just (loc, n))

 240 |                                       pure pkg

 241 | addField (PExec e)           pkg = pure $ { executable := Just e } pkg

 242 | addField (POpts fc e)        pkg = pure $ { options := Just (fc, e) } pkg

 243 | addField (PSourceDir fc a)   pkg = pure $ { sourcedir := Just a } pkg

 244 | addField (PBuildDir fc a)    pkg = pure $ { builddir := Just a } pkg

 245 | addField (POutputDir fc a)   pkg = pure $ { outputdir := Just a } pkg

 246 | addField (PPrebuild fc e)    pkg = pure $ { prebuild := Just (fc, e) } pkg

 247 | addField (PPostbuild fc e)   pkg = pure $ { postbuild := Just (fc, e) } pkg

 248 | addField (PPreinstall fc e)  pkg = pure $ { preinstall := Just (fc, e) } pkg

 249 | addField (PPostinstall fc e) pkg = pure $ { postinstall := Just (fc, e) } pkg

 250 | addField (PPreclean fc e)    pkg = pure $ { preclean := Just (fc, e) } pkg

 251 | addField (PPostclean fc e)   pkg = pure $ { postclean := Just (fc, e) } pkg

 253 | addFields : {auto c : Ref Ctxt Defs} ->

 254 |             {auto s : Ref Syn SyntaxInfo} ->

 255 |             {auto o : Ref ROpts REPLOpts} ->

 256 |             (setSrc : Bool) ->

 257 |             List DescField -> PkgDesc -> Core PkgDesc

 258 | addFields setSrc xs desc = do

 259 |   p <- newRef ParsedMods []

 260 |   m <- newRef MainMod Nothing

 261 |   added <- go {p} {m} xs desc

 262 |   when setSrc $ setSourceDir (sourcedir added)

 263 |   ms <- get ParsedMods

 264 |   mmod <- get MainMod

 265 |   pure $

 266 |     { modules := !(traverse toSource ms)

 267 |     , mainmod := !(traverseOpt toSource mmod)

 268 |     } added

 269 |   where

 270 |     toSource : (FC, ModuleIdent) -> Core (ModuleIdent, String)

 271 |     toSource (loc, ns) = pure (ns, !(nsToSource loc ns))

 272 |     go : {auto p : Ref ParsedMods (List (FC, ModuleIdent))} ->

 273 |          {auto m : Ref MainMod (Maybe (FC, ModuleIdent))} ->

 274 |          List DescField -> PkgDesc -> Core PkgDesc

 275 |     go [] dsc = pure dsc

 276 |     go (x :: xs) dsc = go xs !(addField x dsc)

 278 | runScript : Maybe (FC, String) -> Core ()

 279 | runScript Nothing = pure ()

 280 | runScript (Just (fc, s))

 281 |     = do res <- coreLift $ system s

 282 |          when (res /= 0) $

 283 |             throw (GenericMsg fc "Script failed")

 286 | parsePkgFile : {auto c : Ref Ctxt Defs} ->

 287 |                {auto s : Ref Syn SyntaxInfo} ->

 288 |                {auto o : Ref ROpts REPLOpts} ->

 289 |                (setSrc : Bool) -> -- parse package file as a dependency

 290 |                String -> Core PkgDesc

 291 | parsePkgFile setSrc file = do

 292 |     Right (pname, fs) <- coreLift $ parseFile file $ parsePkgDesc file

 293 |         | Left err => do

 294 |               Right res <- coreLift (readFile file)

 295 |                 | _ => throw err

 296 |               setCurrentElabSource res

 297 |               doc <- perror err

 298 |               msg <- render doc

 299 |               throw (UserError msg)

 300 |     addFields setSrc fs (initPkgDesc pname)

 306 | record Candidate where

 307 |   constructor MkCandidate

 308 |   name      : String

 309 |   version   : Maybe PkgVersion

 310 |   directory : String

 312 | toCandidate : (name : String) -> (String,Maybe PkgVersion) -> Candidate

 313 | toCandidate name (dir,v) = MkCandidate name v dir

 315 | record ResolutionError where

 316 |   constructor MkRE

 317 |   decisions : List Candidate

 318 |   depends   : Depends

 319 |   version   : Maybe PkgVersion

 321 | prepend : Candidate -> ResolutionError -> ResolutionError

 322 | prepend p = { decisions $= (p ::)}

 324 | reason : Maybe PkgVersion -> String

 325 | reason Nothing  = "no matching version is installed."

 326 | reason (Just x) = "only found version \{show x} which is out of bounds."

 328 | printResolutionError : ResolutionError -> String

 329 | printResolutionError (MkRE ds d v) = go [<] ds

 330 |   where go : SnocList String -> List Candidate -> String

 331 |         go ss []        =

 332 |           let pre        := "Required \{d.pkgname} \{show d.pkgbounds} but"

 333 |               failure    := "\{pre} \{reason v}"

 334 |               candidates := case ss of

 335 |                                [<] => ""

 336 |                                ss  => " Resolved transitive dependencies: " ++ (fastConcat $ intersperse "; " $ cast ss) ++ "."

 337 |            in failure ++ candidates

 338 |         go ss (c :: cs) =

 339 |           let v := fromMaybe defaultVersion c.version

 340 |            in go (ss :< "\{c.name}-\{show v}") cs

 342 | data ResolutionRes : Type where

 343 |   Resolved : List String -> ResolutionRes

 344 |   Failed   : List ResolutionError -> ResolutionRes

 346 | printErrs : (pkgDirs : List String) -> PkgDesc -> List ResolutionError -> String

 347 | printErrs pkgDirs x es =

 348 |   let errors := unlines $ "Failed to resolve the dependencies for \{x.name}:"

 349 |                           :: map (indent 2 . printResolutionError) es

 350 |       dirs   := unlines $ "Searched for packages in:"

 351 |                           :: map (indent 2) pkgDirs

 352 |   in """

 360 | tryAll :  List Candidate

 361 |        -> (Candidate -> Core ResolutionRes)

 362 |        -> Core ResolutionRes

 363 | tryAll ps f = go [<] ps

 364 |   where go :  SnocList ResolutionError

 365 |            -> List Candidate

 366 |            -> Core ResolutionRes

 367 |         go se []        = pure (Failed $ se <>> [])

 368 |         go se (x :: xs) = do

 369 |           Failed errs <- f x | Resolved res => pure (Resolved res)

 370 |           go (se <>< map (prepend x) errs) xs

 372 | pkgDirs :

 373 |     {auto c : Ref Ctxt Defs} ->

 374 |     Core (List String)

 375 | pkgDirs = do

 376 |   localdir <- pkgLocalDirectory

 377 |   d <- getDirs

 378 |   pure (localdir ::  (show <$> d.package_search_paths))

 382 | addDeps :

 383 |     {auto c : Ref Ctxt Defs} ->

 384 |     {auto s : Ref Syn SyntaxInfo} ->

 385 |     {auto o : Ref ROpts REPLOpts} ->

 386 |     PkgDesc ->

 387 |     Core ()

 388 | addDeps pkg = do

 389 |   Resolved allPkgs <- getTransitiveDeps pkg.depends empty

 390 |     | Failed errs => throw $ GenericMsg EmptyFC (printErrs !pkgDirs pkg errs)

 391 |   log "package.depends" 10 $ "all depends: \{show allPkgs}"

 392 |   traverse_ addPackageDir allPkgs

 393 |   traverse_ addDataDir ((</> "data") <$> allPkgs)

 394 |   where

 395 |     -- Note: findPkgDir throws an error if a package is not found

 396 |     -- *unless* --ignore-missing-ipkg is enabled

 397 |     -- therefore, if findPkgDir returns Nothing, skip the package

 398 |     --

 399 |     -- We use a backtracking algorithm here: If several versions of

 400 |     -- a package are installed, we must try all, which are are

 401 |     -- potentially in bounds, because their set of dependencies

 402 |     -- might be different across versions and not all of them

 403 |     -- might lead to a resolvable situation.

 404 |     getTransitiveDeps :

 405 |         List Depends ->

 406 |         (done : StringMap (Maybe PkgVersion)) ->

 407 |         Core ResolutionRes

 408 |     getTransitiveDeps [] done = do

 409 |       ms <- for (StringMap.toList done) $

 410 |         \(pkg, mv) => findPkgDir pkg (exactBounds mv)

 411 |       pure . Resolved $ catMaybes ms

 413 |     getTransitiveDeps (dep :: deps) done =

 414 |       case lookup dep.pkgname done of

 415 |         Just mv =>

 416 |           if inBounds mv dep.pkgbounds

 417 |             -- already resolved dependency is in bounds

 418 |             -- so we keep it and resolve remaining deps

 419 |             then getTransitiveDeps deps done

 420 |             -- the resolved dependency does not satisfy the

 421 |             -- current bounds. we return an error and backtrack

 422 |             else pure (Failed [MkRE [] dep $ mv <|> Just defaultVersion])

 423 |         Nothing => do

 424 |           log "package.depends" 50 "adding new dependency: \{dep.pkgname} (\{show dep.pkgbounds})"

 425 |           pkgDirs <- findPkgDirs dep.pkgname dep.pkgbounds

 426 |           let candidates := toCandidate dep.pkgname <$> pkgDirs

 428 |           case candidates of

 429 |             [] => do

 430 |               defs <- get Ctxt

 431 |               if defs.options.session.ignoreMissingPkg

 432 |                 -- this corresponds to what `findPkgDir` does in

 433 |                 -- case of `ignoreMissingPkg` being set to `True`

 434 |                 then getTransitiveDeps deps done

 435 |                 else pure (Failed [MkRE [] dep Nothing])

 437 |             _  => tryAll candidates $ \(MkCandidate name mv pkgDir) => do

 438 |               let pkgFile = pkgDir </> name <.> "ipkg"

 439 |               True <- coreLift $ exists pkgFile

 440 |                 | False => getTransitiveDeps deps (insert name mv done)

 441 |               pkg <- parsePkgFile False pkgFile

 442 |               getTransitiveDeps

 443 |                 (pkg.depends ++ deps)

 444 |                 (insert pkg.name pkg.version done)

 450 | processOptions : {auto c : Ref Ctxt Defs} ->

 451 |                  {auto o : Ref ROpts REPLOpts} ->

 452 |                  Maybe (FC, String) -> Core ()

 453 | processOptions Nothing = pure ()

 454 | processOptions (Just (fc, opts))

 455 |     = do let Right clopts = getOpts (words opts)

 456 |                 | Left err => throw (GenericMsg fc err)

 457 |          ignore $ preOptions clopts

 459 | compileMain : {auto c : Ref Ctxt Defs} ->

 460 |               {auto s : Ref Syn SyntaxInfo} ->

 461 |               {auto o : Ref ROpts REPLOpts} ->

 462 |               Name -> String -> String -> Core ()

 463 | compileMain mainn mfilename exec

 464 |     = do modIdent <- ctxtPathToNS mfilename

 465 |          m <- newRef MD (initMetadata (PhysicalIdrSrc modIdent))

 466 |          u <- newRef UST initUState

 467 |          ignore $ loadMainFile mfilename

 468 |          ignore $ compileExp (PRef replFC mainn) exec

 473 | withWarnings : Ref Ctxt Defs =>

 474 |                Ref Syn SyntaxInfo =>

 475 |                Ref ROpts REPLOpts =>

 476 |                Core a -> Core a

 477 | withWarnings op = do o <- catch op $ \err =>

 478 |                            do emit

 479 |                               throw err

 480 |                      emit

 481 |                      pure o

 482 |   where

 483 |     emit : Core ()

 484 |     emit = do

 485 |       ignore emitWarnings

 486 |       update Ctxt { warnings := [] }

 488 | prepareCompilation : {auto c : Ref Ctxt Defs} ->

 489 |                      {auto s : Ref Syn SyntaxInfo} ->

 490 |                      {auto o : Ref ROpts REPLOpts} ->

 491 |                      PkgDesc ->

 492 |                      List CLOpt ->

 493 |                      Core (List Error)

 494 | prepareCompilation pkg opts =

 495 |   do

 496 |     processOptions (options pkg)

 497 |     withWarnings $ addDeps pkg

 499 |     ignore $ preOptions opts

 501 |     runScript (prebuild pkg)

 503 |     let toBuild = maybe (map snd (modules pkg))

 504 |                         (\m => snd m :: map snd (modules pkg))

 505 |                         (mainmod pkg)

 506 |     buildAll toBuild

 508 | assertIdrisCompatibility : PkgDesc -> Core ()

 509 | assertIdrisCompatibility pkg

 510 |     = do let Just requiredBounds = pkg.langversion

 511 |            | Nothing => pure ()

 512 |          unless (inBounds version requiredBounds) $

 513 |            throw (GenericMsg emptyFC "\{pkg.name} requires Idris2 \{show requiredBounds} but the installed version of Idris2 is \{show Version.version}.")

 516 | build : {auto c : Ref Ctxt Defs} ->

 517 |         {auto s : Ref Syn SyntaxInfo} ->

 518 |         {auto o : Ref ROpts REPLOpts} ->

 519 |         PkgDesc ->

 520 |         List CLOpt ->

 521 |         Core (List Error)

 522 | build pkg opts

 523 |     = do assertIdrisCompatibility pkg

 524 |          [] <- prepareCompilation pkg opts

 525 |             | errs => pure errs

 527 |          whenJust (executable pkg) $ \ exec =>

 528 |            do let Just (mainNS, mainFile) = mainmod pkg

 529 |                  | Nothing => throw (GenericMsg emptyFC "No main module given")

 530 |               let mainName = NS (miAsNamespace mainNS) (UN $ Basic "main")

 531 |               coreLift $ putStrLn "Now compiling the executable: \{exec}"

 532 |               compileMain mainName mainFile exec

 534 |          runScript (postbuild pkg)

 535 |          pure []

 537 | installBuildArtifactFrom : String -> String -> String -> ModuleIdent -> Core ()

 539 | installBuildArtifactFrom file_extension builddir destdir ns

 540 |     = do let filename_trunk = ModuleIdent.toPath ns

 541 |          let filename = builddir </> filename_trunk <.> file_extension

 543 |          let modPath  = reverse $ fromMaybe [] $ tail' $ unsafeUnfoldModuleIdent ns

 544 |          let destNest = joinPath modPath

 545 |          let destPath = destdir </> destNest

 546 |          let destFile = destdir </> filename_trunk <.> file_extension

 548 |          Right _ <- coreLift $ mkdirAll $ destPath

 549 |              | Left err => throw $ InternalError $ unlines

 550 |                              [ "Can't make directories " ++ show modPath

 551 |                              , show err ]

 552 |          coreLift $ putStrLn $ "Installing " ++ filename ++ " to " ++ destPath

 553 |          Right _ <- coreLift $ copyFile filename destFile

 554 |              | Left err => throw $ InternalError $ unlines

 555 |                              [ "Can't copy file " ++ filename ++ " to " ++ destPath

 556 |                              , show err ]

 558 |          pure ()

 560 | installFrom : {auto o : Ref ROpts REPLOpts} ->

 561 |               {auto c : Ref Ctxt Defs} ->

 562 |               String -> String -> ModuleIdent -> Core ()

 563 | installFrom builddir destdir ns = do

 564 |   installBuildArtifactFrom "ttc" builddir destdir ns

 565 |   installBuildArtifactFrom "ttm" builddir destdir ns

 567 |   let filename_trunk = ModuleIdent.toPath ns

 568 |   let modPath  = reverse $ fromMaybe [] $ tail' $ unsafeUnfoldModuleIdent ns

 569 |   let destNest = joinPath modPath

 570 |   let destPath = destdir </> destNest

 572 |   let installCodeGenFiles = \cg => do

 573 |     Just cgdata <- getCG cg

 574 |       | Nothing => pure Nothing

 575 |     let Just ext = incExt cgdata

 576 |       | Nothing => pure Nothing

 577 |     let srcFile = builddir </> filename_trunk <.> ext

 578 |     let destFile = destdir </> filename_trunk <.> ext

 579 |     let Just (dir, _) = splitParent destFile

 580 |       | Nothing => pure Nothing

 581 |     ensureDirectoryExists dir

 582 |     pure $ Just (srcFile, destFile)

 584 |   objPaths_in <- traverse

 585 |                     installCodeGenFiles

 586 |                     (incrementalCGs !getSession)

 587 |   let objPaths = mapMaybe id objPaths_in

 588 |   -- Copy object files, if any. They don't necessarily get created,

 589 |   -- since some modules don't generate any code themselves.

 590 |   traverse_

 591 |     (\ (obj, dest) => do

 592 |       coreLift $ putStrLn $ "Installing " ++ obj ++ " to " ++ destPath

 593 |       ignore $ coreLift $ copyFile obj dest)

 594 |     objPaths

 596 | installSrcFrom : String -> String -> (ModuleIdent, FileName) -> Core ()

 597 | installSrcFrom wdir destdir (ns, srcRelPath)

 598 |     = do let srcfile = ModuleIdent.toPath ns

 599 |          let srcPath = wdir </> srcRelPath

 600 |          let Just ext = extension srcPath

 601 |            | _ => throw (InternalError $

 602 |                 "Unexpected failure when installing source file:\n"

 603 |               ++ srcPath

 604 |               ++ "\n"

 605 |               ++ "Can't extract file extension.")

 607 |          let modPath  = reverse $ fromMaybe [] $ tail' $ unsafeUnfoldModuleIdent ns

 608 |          let destNest = joinPath modPath

 609 |          let destPath = destdir </> destNest

 610 |          let destFile = destdir </> srcfile <.> ext

 612 |          Right _ <- coreLift $ mkdirAll $ destPath

 613 |              | Left err => throw $ InternalError $ unlines

 614 |                              [ "Can't make directories " ++ show modPath

 615 |                              , show err ]

 616 |          coreLift $ putStrLn $ "Installing " ++ srcPath ++ " to " ++ destPath

 617 |          when !(coreLift $ exists destFile) $ do

 618 |            -- Grant read/write access to the file we are about to overwrite.

 619 |            Right _ <- coreLift $ chmod destFile

 620 |              (MkPermissions [Read, Write] [Read, Write] [Read, Write])

 621 |              | Left err => throw $ UserError (show err)

 622 |            pure ()

 623 |          Right _ <- coreLift $ copyFile srcPath destFile

 624 |              | Left err => throw $ InternalError $ unlines

 625 |                              [ "Can't copy file " ++ srcPath ++ " to " ++ destPath

 626 |                              , show err ]

 627 |          -- Make the source read-only

 628 |          Right _ <- coreLift $ chmod destFile (MkPermissions [Read] [Read] [Read])

 629 |            | Left err => throw $ UserError (show err)

 630 |          pure ()

 632 | absoluteInstallDir : (relativeInstallDir : String) -> Core String

 633 | absoluteInstallDir relativeInstallDir = do

 634 |   mdestdir <- coreLift $ getEnv "DESTDIR"

 635 |   let destdir = fromMaybe "" mdestdir

 636 |   pure $ destdir ++ relativeInstallDir

 641 | install : {auto c : Ref Ctxt Defs} ->

 642 |           {auto o : Ref ROpts REPLOpts} ->

 643 |           PkgDesc ->

 644 |           List CLOpt ->

 645 |           (installSrc : Bool) ->

 646 |           Core ()

 647 | install pkg opts installSrc -- not used but might be in the future

 648 |     = do defs <- get Ctxt

 649 |          build <- ttcBuildDirectory

 650 |          let lib = installDir pkg

 651 |          libTargetDir <- absoluteInstallDir =<< libInstallDirectory lib

 652 |          ttcTargetDir <- absoluteInstallDir =<< ttcInstallDirectory lib

 653 |          srcTargetDir <- absoluteInstallDir =<< srcInstallDirectory lib

 655 |          let src = source_dir (dirs (options defs))

 656 |          runScript (preinstall pkg)

 657 |          let toInstall = maybe (modules pkg)

 658 |                                (:: modules pkg)

 659 |                                (mainmod pkg)

 660 |          wdir <- getWorkingDir

 661 |          -- Make the package installation directory

 662 |          Right _ <- coreLift $ mkdirAll libTargetDir

 663 |              | Left err => throw $ InternalError $ unlines

 664 |                              [ "Can't make directory " ++ libTargetDir

 665 |                              , show err ]

 667 |          traverse_ (installFrom (wdir </> build) ttcTargetDir . fst) toInstall

 669 |          when installSrc $ do

 670 |            traverse_ (installSrcFrom wdir srcTargetDir) toInstall

 672 |          -- install package file

 673 |          let pkgFile = libTargetDir </> pkg.name <.> "ipkg"

 674 |          coreLift $ putStrLn $ "Installing package file for \{pkg.name} to \{libTargetDir}"

 676 |          let pkgStr = String.renderString $ layoutUnbounded $ pretty $ savePkgMetadata pkg

 677 |          log "package.depends" 25 $ "  package file:\n\{pkgStr}"

 678 |          coreLift_ $ writeFile pkgFile pkgStr

 680 |          runScript (postinstall pkg)

 681 |   where

 682 |     savePkgMetadata : PkgDesc -> PkgDesc

 683 |     savePkgMetadata pkg =

 684 |       the (PkgDesc -> PkgDesc)

 685 |       { depends := pkg.depends

 686 |       , version := pkg.version

 687 |       } $ initPkgDesc pkg.name

 691 | check : {auto c : Ref Ctxt Defs} ->

 692 |         {auto s : Ref Syn SyntaxInfo} ->

 693 |         {auto o : Ref ROpts REPLOpts} ->

 694 |         PkgDesc ->

 695 |         List CLOpt ->

 696 |         Core (List Error)

 697 | check pkg opts =

 698 |   do assertIdrisCompatibility pkg

 699 |      [] <- prepareCompilation pkg opts

 700 |        | errs => pure errs

 702 |      runScript (postbuild pkg)

 703 |      pure []

 705 | makeDoc : {auto c : Ref Ctxt Defs} ->

 706 |           {auto s : Ref Syn SyntaxInfo} ->

 707 |           {auto o : Ref ROpts REPLOpts} ->

 708 |           PkgDesc ->

 709 |           List CLOpt ->

 710 |           Core (List Error)

 711 | makeDoc pkg opts =

 712 |     do [] <- prepareCompilation pkg opts

 713 |          | errs => pure errs

 715 |        defs <- get Ctxt

 716 |        let build = build_dir (dirs (options defs))

 717 |        let docBase = build </> "docs"

 718 |        let docDir = docBase </> "docs"

 719 |        Right () <- coreLift $ mkdirAll docDir

 720 |          | Left err => fileError docDir err

 721 |        u <- newRef UST initUState

 722 |        setPPrint docsPPrint

 724 |        [] <- concat <$> for (modules pkg) (\(mod, filename) => do

 725 |            -- load dependencies

 726 |            let ns = miAsNamespace mod

 727 |            addImport (MkImport emptyFC False mod ns)

 729 |            -- generate docs for all visible names

 730 |            defs <- get Ctxt

 731 |            let ctxt = gamma defs

 732 |            visibleDefs <- map catMaybes $ for [1..nextEntry ctxt - 1] $ \ i =>

 733 |              do -- Select the entries that are from `mod` and visible

 734 |                 Just gdef <- lookupCtxtExact (Resolved i) ctxt

 735 |                   | _ => pure Nothing

 736 |                 let Just nfc = isNonEmptyFC $ location gdef

 737 |                   | _ => do log "doc.module.definitions" 70 $ unwords

 738 |                               [ show mod ++ ":"

 739 |                               , show (fullname gdef)

 740 |                               , "has an empty FC"

 741 |                               ]

 742 |                             pure Nothing

 743 |                 let PhysicalIdrSrc mod' = origin nfc

 744 |                   | _ => pure Nothing

 745 |                 let True = mod == mod'

 746 |                   | _ => do log "doc.module.definitions" 60 $ unwords

 747 |                               [ show mod ++ ":"

 748 |                               , show (fullname gdef)

 749 |                               , "was defined in"

 750 |                               , show mod'

 751 |                               ]

 752 |                             pure Nothing

 753 |                 let True = visible gdef

 754 |                   | _ => pure Nothing

 755 |                 pure (Just gdef)

 757 |            let outputFilePath = docDir </> (show mod ++ ".html")

 758 |            allDocs <- for (sortBy (compare `on` startPos . toNonEmptyFC . location) visibleDefs) $ \ def =>

 759 |                         getDocsForName emptyFC (fullname def) shortNamesConfig

 760 |            let allDecls = annotate Declarations $ vcat allDocs

 762 |            -- grab module header doc

 763 |            syn  <- get Syn

 764 |            let modDoc = lookup mod (modDocstrings syn)

 765 |            log "doc.module" 10 $ unwords

 766 |              [ "Looked up doc for"

 767 |              , show mod

 768 |              , "and got:"

 769 |              , show modDoc

 770 |              ]

 771 |            log "doc.module" 100 $ "from: " ++ show (modDocstrings syn)

 773 |            -- grab publically re-exported modules

 774 |            let mreexports = do docs <- lookup mod $ modDocexports syn

 775 |                                guard (not $ null docs)

 776 |                                pure docs

 777 |            whenJust mreexports $ \ reexports =>

 778 |              log "doc.module" 15 $ unwords

 779 |                [ "All imported:", show reexports]

 781 |            let modExports = map (map (reAnnotate Syntax . prettyImport)) mreexports

 783 |            Right () <- do doc <- renderModuleDoc mod modDoc modExports

 784 |                                    (allDecls <$ guard (not $ null allDocs))

 785 |                           coreLift $ writeFile outputFilePath doc

 786 |              | Left err => fileError (docBase </> "index.html") err

 788 |            pure $ the (List Error) []

 789 |          )

 790 |          | errs => pure errs

 792 |        Right () <- do syn <- get Syn

 793 |                       coreLift $ writeFile (docBase </> "index.html") $ renderDocIndex pkg (modDocstrings syn)

 794 |          | Left err => fileError (docBase </> "index.html") err

 796 |        errs <- for cssFiles $ \ cssFile => do

 797 |           let fn = cssFile.filename ++ ".css"

 798 |           css <- readDataFile ("docs/" ++ fn)

 799 |           Right () <- coreLift $ writeFile (docBase </> fn) css

 800 |             | Left err => fileError (docBase </> fn) err

 801 |           pure (the (List Error) [])

 803 |        let [] = concat errs

 804 |            | err => pure err

 806 |        runScript (postbuild pkg)

 807 |        pure []

 808 |   where

 809 |     visible : GlobalDef -> Bool

 810 |     visible def = case definition def of

 811 |       DCon {} => False

 812 |       _ => (collapseDefault (visibility def) /= Private)

 814 |     fileError : String -> FileError -> Core (List Error)

 815 |     fileError filename err = pure [FileErr filename err]

 818 | bitraverseC : (a -> Core c) -> (b -> Core d) -> These a b -> Core (These c d)

 819 | bitraverseC f g (This a)   = [| This (f a) |]

 820 | bitraverseC f g (That b)   = [| That (g b) |]

 821 | bitraverseC f g (Both a b) = [| Both (f a) (g b) |]

 824 | foldWithKeysC : Monoid b => (List String -> Core b) -> (List String -> a -> Core b) -> StringTrie a -> Core b

 825 | foldWithKeysC {a} {b} fk fv = go []

 826 |   where

 827 |   go : List String -> StringTrie a -> Core b

 828 |   go ks (MkStringTrie nd) =

 829 |     map bifold $ bitraverseC

 830 |                    (fv ks)

 831 |                    (\sm => foldlC

 832 |                              (\x, (k, vs) =>

 833 |                                do let ks' = ks++[k]

 834 |                                   y <- assert_total $ go ks' vs

 835 |                                   z <- fk ks'

 836 |                                   pure $ x <+> y <+> z)

 837 |                              neutral

 838 |                              (StringMap.toList sm))

 839 |                    nd

 841 | clean : {auto c : Ref Ctxt Defs} ->

 842 |         PkgDesc ->

 843 |         List CLOpt ->

 844 |         Core ()

 845 | clean pkg opts -- `opts` is not used but might be in the future

 846 |     = do defs <- get Ctxt

 847 |          runScript (preclean pkg)

 848 |          let pkgmods = maybe

 849 |                          (map fst (modules pkg))

 850 |                          (\m => fst m :: map fst (modules pkg))

 851 |                          (mainmod pkg)

 852 |          let toClean : List (List String, String)

 853 |                = mapMaybe (\ mod => case unsafeUnfoldModuleIdent mod of

 854 |                                        [] => Nothing

 855 |                                        (x :: xs) => Just(xs, x))

 856 |                           pkgmods

 857 |          srcdir <- getWorkingDir

 858 |          let d = dirs (options defs)

 859 |          bdir <- ttcBuildDirectory

 860 |          let builddir = srcdir </> bdir </> "ttc"

 861 |          let outputdir = srcdir </> outputDirWithDefault d

 862 |          -- the usual pair syntax breaks with `No such variable a` here for some reason

 863 |          let pkgTrie : StringTrie (List String)

 864 |                      = foldl (\trie, ksv =>

 865 |                                 let ks = Builtin.fst ksv

 866 |                                     v = Builtin.snd ksv

 867 |                                   in

 868 |                                 insertWith (reverse ks) (maybe [v] (v::)) trie) empty toClean

 869 |          foldWithKeysC (deleteFolder builddir)

 870 |                        (\ks => map concat . traverse (deleteBin builddir ks))

 871 |                        pkgTrie

 872 |          deleteFolder builddir []

 873 |          maybe (pure ()) (\e => delete (outputdir </> e))

 874 |                (executable pkg)

 875 |          -- clean out the generated docs

 876 |          let build = build_dir (dirs (options defs))

 877 |          deleteDocsFolder $ build </> "docs" </> "docs"

 878 |          deleteDocsFolder $ build </> "docs"

 879 |          runScript (postclean pkg)

 880 |   where

 881 |     delete : String -> Core ()

 882 |     delete path = do Right () <- coreLift $ removeFile path

 883 |                        | Left err => pure ()

 884 |                      coreLift $ putStrLn $ "Removed: " ++ path

 886 |     deleteFolder : String -> List String -> Core ()

 887 |     deleteFolder builddir ns = delete $ builddir </> joinPath ns

 889 |     deleteBin : String -> List String -> String -> Core ()

 890 |     deleteBin builddir ns mod

 891 |         = do let ttFile = builddir </> joinPath ns </> mod

 892 |              delete $ ttFile <.> "ttc"

 893 |              delete $ ttFile <.> "ttm"

 895 |     deleteDocsFolder : String -> Core ()

 896 |     deleteDocsFolder dir

 897 |         = do Right docbasefiles <- coreLift $ listDir dir

 898 |                | Left err => pure ()

 899 |              traverse_ (\x => delete $ dir </> x)

 900 |                        docbasefiles

 901 |              deleteFolder dir []

 905 | runRepl : {auto c : Ref Ctxt Defs} ->

 906 |           {auto s : Ref Syn SyntaxInfo} ->

 907 |           {auto o : Ref ROpts REPLOpts} ->

 908 |           Maybe String ->

 909 |           Core ()

 910 | runRepl fname = do

 911 |   u <- newRef UST initUState

 912 |   origin <- maybe

 913 |     (pure $ Virtual Interactive) (\fname => do

 914 |       modIdent <- ctxtPathToNS fname

 915 |       pure (PhysicalIdrSrc modIdent)

 916 |       ) fname

 917 |   m <- newRef MD (initMetadata origin)

 918 |   case fname of

 919 |       Nothing => pure ()

 920 |       Just fn => do

 921 |         errs <- loadMainFile fn

 922 |         displayStartupErrors errs

 923 |   repl {u} {s}

 927 | localPackageFile : Maybe String -> Core String

 928 | localPackageFile (Just fp) = pure fp

 929 | localPackageFile Nothing

 930 |   = do wdir <- getWorkingDir

 931 |        tree <- coreLift (explore $ parse wdir)

 932 |        let candidates = map fileName tree.files

 933 |        case filter (".ipkg" `isSuffixOf`) candidates of

 934 |          [fp] => pure fp

 935 |          [] => throw $ UserError "No .ipkg file supplied and none could be found in the working directory."

 936 |          _ => throw $ UserError "No .ipkg file supplied and the working directory contains more than one."

 938 | processPackage : {auto c : Ref Ctxt Defs} ->

 939 |                  {auto s : Ref Syn SyntaxInfo} ->

 940 |                  {auto o : Ref ROpts REPLOpts} ->

 941 |                  List CLOpt ->

 942 |                  (PkgCommand, Maybe String) ->

 943 |                  Core ()

 944 | processPackage opts (cmd, mfile)

 945 |     = withCtxt . withSyn . withROpts $ case cmd of

 946 |         Init =>

 947 |           do Just pkg <- coreLift interactive

 948 |                | Nothing => coreLift (exitWith (ExitFailure 1))

 949 |              let fp = fromMaybe (pkg.name ++ ".ipkg") mfile

 950 |              False <- coreLift (exists fp)

 951 |                | _ => throw (GenericMsg emptyFC ("File " ++ fp ++ " already exists"))

 952 |              Right () <- coreLift $ writeFile fp (show $ pretty pkg)

 953 |                | Left err => throw (FileErr fp err)

 954 |              pure ()

 955 |         _ =>

 956 |           do file <- localPackageFile mfile

 957 |              let Just (dir, filename) = splitParent file

 958 |                  | _ => throw $ InternalError "Tried to split empty string"

 959 |              let True = isSuffixOf ".ipkg" filename

 960 |                  | _ => do coreLift $ putStrLn ("Packages must have an '.ipkg' extension: " ++ show file ++ ".")

 961 |                            coreLift (exitWith (ExitFailure 1))

 962 |              setWorkingDir dir

 963 |              pkg <- parsePkgFile True filename

 964 |              whenJust (builddir pkg) setBuildDir

 965 |              setOutputDir (outputdir pkg)

 966 |              case cmd of

 967 |                   Build => do [] <- build pkg opts

 968 |                                  | errs => coreLift (exitWith (ExitFailure 1))

 969 |                               pure ()

 970 |                   MkDoc => do [] <- makeDoc pkg opts

 971 |                                  | errs => coreLift (exitWith (ExitFailure 1))

 972 |                               pure ()

 973 |                   Install => do [] <- build pkg opts

 974 |                                    | errs => coreLift (exitWith (ExitFailure 1))

 975 |                                 install pkg opts {installSrc = False}

 976 |                   InstallWithSrc =>

 977 |                              do [] <- build pkg opts

 978 |                                    | errs => coreLift (exitWith (ExitFailure 1))

 979 |                                 install pkg opts {installSrc = True}

 980 |                   Typecheck => do

 981 |                     [] <- check pkg opts

 982 |                       | errs => coreLift (exitWith (ExitFailure 1))

 983 |                     pure ()

 984 |                   Clean => clean pkg opts

 985 |                   REPL => do

 986 |                     [] <- build pkg opts

 987 |                        | errs => coreLift (exitWith (ExitFailure 1))

 988 |                     runRepl (map snd $ mainmod pkg)

 989 |                   Init => pure () -- already handled earlier

 990 |                   DumpJson => coreLift . putStrLn $ toJson pkg

 991 |                   DumpInstallDir => do

 992 |                     libInstallDir <- libInstallDirectory (installDir pkg)

 993 |                     dir <- absoluteInstallDir libInstallDir

 994 |                     coreLift (putStrLn dir)

 996 | record PackageOpts where

 997 |   constructor MkPFR

 998 |   pkgDetails : List (PkgCommand, Maybe String)

 999 |   oopts : List CLOpt

1000 |   hasError : Bool

1002 | partitionOpts : List CLOpt -> PackageOpts

1003 | partitionOpts opts = foldr pOptUpdate (MkPFR [] [] False) opts

1004 |   where

1005 |     data OptType : Type where

1006 |       PPackage : PkgCommand -> Maybe String -> OptType

1007 |       POpt : OptType

1008 |       PIgnore : OptType

1009 |       PErr : OptType

1010 |     optType : CLOpt -> OptType

1011 |     optType (Package cmd f)        = PPackage cmd f

1012 |     optType Quiet                  = POpt

1013 |     optType Verbose                = POpt

1014 |     optType (Timing l)             = POpt

1015 |     optType (Logging l)            = POpt

1016 |     optType CaseTreeHeuristics     = POpt

1017 |     optType (DumpANF f)            = POpt

1018 |     optType (DumpCases f)          = POpt

1019 |     optType (DumpLifted f)         = POpt

1020 |     optType (DumpVMCode f)         = POpt

1021 |     optType DebugElabCheck         = POpt

1022 |     optType (SetCG f)              = POpt

1023 |     optType (IncrementalCG _)      = POpt

1024 |     optType (Directive d)          = POpt

1025 |     optType (BuildDir f)           = POpt

1026 |     optType (OutputDir f)          = POpt

1027 |     optType WarningsAsErrors       = POpt

1028 |     optType HashesInsteadOfModTime = POpt

1029 |     optType Profile                = POpt

1030 |     optType (ConsoleWidth n)       = PIgnore

1031 |     optType (Color b)              = PIgnore

1032 |     optType NoBanner               = PIgnore

1033 |     optType x                      = PErr

1035 |     pOptUpdate : CLOpt -> (PackageOpts -> PackageOpts)

1036 |     pOptUpdate opt with (optType opt)

1037 |       pOptUpdate opt | (PPackage cmd f) = {pkgDetails $= ((cmd, f)::)}

1038 |       pOptUpdate opt | POpt    = {oopts $= (opt::)}

1039 |       pOptUpdate opt | PIgnore = id

1040 |       pOptUpdate opt | PErr    = {hasError := True}

1042 | errorMsg : String

1043 | errorMsg = unlines

1044 |   [ "Not all command line options can be used to override package options.\n"

1045 |   , "Overridable options are:"

1046 |   , "    --quiet"

1047 |   , "    --verbose"

1048 |   , "    --timing"

1049 |   , "    --log <log level>"

1050 |   , "    --dumpcases <file>"

1051 |   , "    --dumplifted <file>"

1052 |   , "    --dumpvmcode <file>"

1053 |   , "    --debug-elab-check"

1054 |   , "    --codegen <cg>"

1055 |   , "    --inc <cg>"

1056 |   , "    --directive <directive>"

1057 |   , "    --build-dir <dir>"

1058 |   , "    --output-dir <dir>"

1059 |   ]

1062 | processPackageOpts : {auto c : Ref Ctxt Defs} ->

1063 |                      {auto s : Ref Syn SyntaxInfo} ->

1064 |                      {auto o : Ref ROpts REPLOpts} ->

1065 |                      List CLOpt -> Core Bool

1066 | processPackageOpts opts

1067 |     = do (MkPFR cmds@(_::_) opts' err) <- pure $ partitionOpts opts

1068 |              | (MkPFR Nil opts' _) => pure False

1069 |          if err

1070 |            then coreLift $ putStrLn errorMsg

1071 |            else traverse_ (processPackage opts') cmds

1072 |          pure True

1079 | findIpkg : {auto c : Ref Ctxt Defs} ->

1080 |            {auto r : Ref ROpts REPLOpts} ->

1081 |            {auto s : Ref Syn SyntaxInfo} ->

1082 |            Maybe String -> Core (Maybe String)

1083 | findIpkg fname

1084 |    = do Just (dir, ipkgn, up) <- coreLift findIpkgFile

1085 |              | Nothing => pure fname

1086 |         coreLift_ $ changeDir dir

1087 |         setWorkingDir dir

1088 |         pkg <- parsePkgFile True ipkgn

1089 |         maybe (pure ()) setBuildDir (builddir pkg)

1090 |         setOutputDir (outputdir pkg)

1091 |         processOptions (options pkg)

1092 |         addDeps pkg

1093 |         case fname of

1094 |              Nothing => pure Nothing

1095 |              Just srcpath  =>

1096 |                 do let src' = up </> srcpath