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 |   PDataDir      : FC -> String -> DescField

  68 |   PBuildDir     : FC -> String -> DescField

  69 |   POutputDir    : FC -> String -> DescField

  70 |   PPrebuild     : FC -> String -> DescField

  71 |   PPostbuild    : FC -> String -> DescField

  72 |   PPreinstall   : FC -> String -> DescField

  73 |   PPostinstall  : FC -> String -> DescField

  74 |   PPreclean     : FC -> String -> DescField

  75 |   PPostclean    : FC -> String -> DescField

  77 | field : String -> Rule DescField

  78 | field fname

  79 |       = strField PAuthors "authors"

  80 |     <|> strField PMaintainers "maintainers"

  81 |     <|> strField PLicense "license"

  82 |     <|> strField PBrief "brief"

  83 |     <|> strField PReadMe "readme"

  84 |     <|> strField PHomePage "homepage"

  85 |     <|> strField PSourceLoc "sourceloc"

  86 |     <|> strField PBugTracker "bugtracker"

  87 |     <|> strField POpts "options"

  88 |     <|> strField POpts "opts"

  89 |     <|> strField PSourceDir "sourcedir"

  90 |     <|> strField PDataDir "datadir"

  91 |     <|> strField PBuildDir "builddir"

  92 |     <|> strField POutputDir "outputdir"

  93 |     <|> strField PPrebuild "prebuild"

  94 |     <|> strField PPostbuild "postbuild"

  95 |     <|> strField PPreinstall "preinstall"

  96 |     <|> strField PPostinstall "postinstall"

  97 |     <|> strField PPreclean "preclean"

  98 |     <|> strField PPostclean "postclean"

  99 |     <|> do start <- location

 100 |            ignore $ exactProperty "version"

 101 |            mustWork $ do

 102 |              equals

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

 104 |              end <- location

 105 |              the (EmptyRule _) $ case vs of

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

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

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

 109 |     <|> do start <- location

 110 |            ignore $ exactProperty "langversion"

 111 |            mustWork $ do

 112 |              lvs <- langversions

 113 |              end <- location

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

 115 |     <|> do start <- location

 116 |            ignore $ exactProperty "version"

 117 |            mustWork $ do

 118 |              equals

 119 |              v <- stringLit

 120 |              end <- location

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

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

 123 |            mustWork $ do

 124 |              equals

 125 |              ds <- sep depends

 126 |              pure (PDepends ds)

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

 128 |            mustWork $ do

 129 |              equals

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

 131 |                            m <- moduleIdent

 132 |                            end <- location

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

 134 |              pure (PModules ms)

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

 136 |            mustWork $ do

 137 |              equals

 138 |              start <- location

 139 |              m <- moduleIdent

 140 |              end <- location

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

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

 143 |            mustWork $ do

 144 |              equals

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

 146 |              pure (PExec e)

 147 |   where

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

 150 |     bound : Rule (List Bound)

 151 |     bound

 152 |         = do lte

 153 |              vs <- sepBy1 dot' integerLit

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

 155 |       <|> do gte

 156 |              vs <- sepBy1 dot' integerLit

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

 158 |       <|> do lt

 159 |              vs <- sepBy1 dot' integerLit

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

 161 |       <|> do gt

 162 |              vs <- sepBy1 dot' integerLit

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

 164 |       <|> do eqop

 165 |              vs <- sepBy1 dot' integerLit

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

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

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

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

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

 172 |                                upperInclusive := i } pkgbs))

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

 174 |                 pkgbs.upperBound

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

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

 177 |                                lowerInclusive := i } pkgbs))

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

 179 |                 pkgbs.lowerBound

 180 |     mkBound [] pkgbs = pure pkgbs

 182 |     langversions : EmptyRule PkgVersionBounds

 183 |     langversions

 184 |         = do bs <- sepBy andop bound

 185 |              mkBound (concat bs) anyBounds

 187 |     depends : Rule Depends

 188 |     depends

 189 |         = do name <- packageName

 190 |              bs <- sepBy andop bound

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

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

 194 |     strField fieldConstructor fieldName

 195 |         = do start <- location

 196 |              ignore $ exactProperty fieldName

 197 |              mustWork $ do

 198 |                equals

 199 |                str <- stringLit

 200 |                end <- location

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

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

 204 | parsePkgDesc fname

 205 |     = do ignore $ exactProperty "package"

 206 |          name <- packageName

 207 |          fields <- many (field fname)

 208 |          EndOfInput <- peek

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

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

 211 |          pure (name, fields)

 213 | data ParsedMods : Type where

 215 | data MainMod : Type where

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

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

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

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

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

 222 |            DescField -> PkgDesc -> Core PkgDesc

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

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

 225 | addField (PVersionDep fc n)   pkg

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

 227 |          pure pkg

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

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

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

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

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

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

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

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

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

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

 240 |                                       pure pkg

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

 242 |                                       pure pkg

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

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

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

 246 | addField (PDataDir fc a)     pkg = pure $ { datadir := Just a } pkg

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

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

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

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

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

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

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

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

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

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

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

 259 |             (setSrc : Bool) ->

 260 |             List DescField -> PkgDesc -> Core PkgDesc

 261 | addFields setSrc xs desc = do

 262 |   p <- newRef ParsedMods []

 263 |   m <- newRef MainMod Nothing

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

 265 |   when setSrc $ setSourceDir (sourcedir added)

 266 |   ms <- get ParsedMods

 267 |   mmod <- get MainMod

 268 |   pure $

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

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

 271 |     } added

 272 |   where

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

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

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

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

 277 |          List DescField -> PkgDesc -> Core PkgDesc

 278 |     go [] dsc = pure dsc

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

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

 282 | runScript Nothing = pure ()

 283 | runScript (Just (fc, s))

 284 |     = do res <- coreLift $ system s

 285 |          when (res /= 0) $

 286 |             throw (GenericMsg fc "Script failed")

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

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

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

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

 293 |                String -> Core PkgDesc

 294 | parsePkgFile setSrc file = do

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

 296 |         | Left err => do

 297 |               Right res <- coreLift (readFile file)

 298 |                 | _ => throw err

 299 |               setCurrentElabSource res

 300 |               doc <- perror err

 301 |               msg <- render doc

 302 |               throw (UserError msg)

 303 |     addFields setSrc fs (initPkgDesc pname)

 309 | record Candidate where

 310 |   constructor MkCandidate

 311 |   name      : String

 312 |   version   : Maybe PkgVersion

 313 |   directory : String

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

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

 318 | record ResolutionError where

 319 |   constructor MkRE

 320 |   decisions : List Candidate

 321 |   depends   : Depends

 322 |   version   : Maybe PkgVersion

 324 | prepend : Candidate -> ResolutionError -> ResolutionError

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

 327 | reason : Maybe PkgVersion -> String

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

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

 331 | printResolutionError : ResolutionError -> String

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

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

 334 |         go ss []        =

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

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

 337 |               candidates := case ss of

 338 |                                [<] => ""

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

 340 |            in failure ++ candidates

 341 |         go ss (c :: cs) =

 342 |           let v := fromMaybe defaultVersion c.version

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

 345 | data ResolutionRes : Type where

 346 |   Resolved : List String -> ResolutionRes

 347 |   Failed   : List ResolutionError -> ResolutionRes

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

 350 | printErrs pkgDirs x es =

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

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

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

 354 |                           :: map (indent 2) pkgDirs

 355 |   in """

 363 | tryAll :  List Candidate

 364 |        -> (Candidate -> Core ResolutionRes)

 365 |        -> Core ResolutionRes

 366 | tryAll ps f = go [<] ps

 367 |   where go :  SnocList ResolutionError

 368 |            -> List Candidate

 369 |            -> Core ResolutionRes

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

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

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

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

 375 | pkgDirs :

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

 377 |     Core (List String)

 378 | pkgDirs = do

 379 |   localdir <- pkgLocalDirectory

 380 |   d <- getDirs

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

 385 | addDeps :

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

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

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

 389 |     PkgDesc ->

 390 |     Core ()

 391 | addDeps pkg = do

 392 |   Resolved allPkgs <- getTransitiveDeps pkg.depends empty

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

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

 395 |   traverse_ addPackageDir allPkgs

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

 397 |   where

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

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

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

 401 |     --

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

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

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

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

 406 |     -- might lead to a resolvable situation.

 407 |     getTransitiveDeps :

 408 |         List Depends ->

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

 410 |         Core ResolutionRes

 411 |     getTransitiveDeps [] done = do

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

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

 414 |       pure . Resolved $ catMaybes ms

 416 |     getTransitiveDeps (dep :: deps) done =

 417 |       case lookup dep.pkgname done of

 418 |         Just mv =>

 419 |           if inBounds mv dep.pkgbounds

 420 |             -- already resolved dependency is in bounds

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

 422 |             then getTransitiveDeps deps done

 423 |             -- the resolved dependency does not satisfy the

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

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

 426 |         Nothing => do

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

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

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

 431 |           case candidates of

 432 |             [] => do

 433 |               defs <- get Ctxt

 434 |               if defs.options.session.ignoreMissingPkg

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

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

 437 |                 then getTransitiveDeps deps done

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

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

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

 442 |               True <- coreLift $ exists pkgFile

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

 444 |               pkg <- parsePkgFile False pkgFile

 445 |               getTransitiveDeps

 446 |                 (pkg.depends ++ deps)

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

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

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

 455 |                  {auto _ : Ref PostS PostSession} ->

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

 457 | processOptions Nothing = pure ()

 458 | processOptions (Just (fc, opts))

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

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

 461 |          ignore $ preOptions clopts

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

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

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

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

 467 | compileMain mainn mfilename exec

 468 |     = do modIdent <- ctxtPathToNS mfilename

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

 470 |          u <- newRef UST initUState

 471 |          ignore $ loadMainFile mfilename

 472 |          ignore $ compileExp (PRef replFC mainn) exec

 477 | withWarnings : Ref Ctxt Defs =>

 478 |                Ref Syn SyntaxInfo =>

 479 |                Ref ROpts REPLOpts =>

 480 |                Core a -> Core a

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

 482 |                            do emit

 483 |                               throw err

 484 |                      emit

 485 |                      pure o

 486 |   where

 487 |     emit : Core ()

 488 |     emit = do

 489 |       ignore emitWarnings

 490 |       update Ctxt { warnings := [] }

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

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

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

 495 |                      {auto _ : Ref PostS PostSession} ->

 496 |                      PkgDesc ->

 497 |                      List CLOpt ->

 498 |                      Core (List Error)

 499 | prepareCompilation pkg opts =

 500 |   do

 501 |     processOptions (options pkg)

 502 |     withWarnings $ addDeps pkg

 504 |     ignore $ preOptions opts

 506 |     runScript (prebuild pkg)

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

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

 510 |                         (mainmod pkg)

 511 |     buildAll toBuild

 513 | assertIdrisCompatibility : PkgDesc -> Core ()

 514 | assertIdrisCompatibility pkg

 515 |     = do let Just requiredBounds = pkg.langversion

 516 |            | Nothing => pure ()

 517 |          unless (inBounds version requiredBounds) $

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

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

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

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

 524 |         {auto _ : Ref PostS PostSession} ->

 525 |         PkgDesc ->

 526 |         List CLOpt ->

 527 |         Core (List Error)

 528 | build pkg opts

 529 |     = do assertIdrisCompatibility pkg

 530 |          [] <- prepareCompilation pkg opts

 531 |             | errs => pure errs

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

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

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

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

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

 538 |               compileMain mainName mainFile exec

 540 |          runScript (postbuild pkg)

 541 |          pure []

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

 545 | installBuildArtifactFrom file_extension builddir destdir ns

 546 |     = do let filename_trunk = ModuleIdent.toPath ns

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

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

 550 |          let destNest = joinPath modPath

 551 |          let destPath = destdir </> destNest

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

 554 |          Right _ <- coreLift $ mkdirAll $ destPath

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

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

 557 |                              , show err ]

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

 559 |          Right _ <- coreLift $ copyFile filename destFile

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

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

 562 |                              , show err ]

 564 |          pure ()

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

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

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

 569 | installFrom builddir destdir ns = do

 570 |   installBuildArtifactFrom "ttc" builddir destdir ns

 571 |   installBuildArtifactFrom "ttm" builddir destdir ns

 573 |   let filename_trunk = ModuleIdent.toPath ns

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

 575 |   let destNest = joinPath modPath

 576 |   let destPath = destdir </> destNest

 578 |   let installCodeGenFiles = \cg => do

 579 |     Just cgdata <- getCG cg

 580 |       | Nothing => pure Nothing

 581 |     let Just ext = incExt cgdata

 582 |       | Nothing => pure Nothing

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

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

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

 586 |       | Nothing => pure Nothing

 587 |     ensureDirectoryExists dir

 588 |     pure $ Just (srcFile, destFile)

 590 |   objPaths_in <- traverse

 591 |                     installCodeGenFiles

 592 |                     (incrementalCGs !getSession)

 593 |   let objPaths = mapMaybe id objPaths_in

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

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

 596 |   traverse_

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

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

 599 |       ignore $ coreLift $ copyFile obj dest)

 600 |     objPaths

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

 603 | installSrcFrom wdir destdir (ns, srcRelPath)

 604 |     = do let srcfile = ModuleIdent.toPath ns

 605 |          let srcPath = wdir </> srcRelPath

 606 |          let Just ext = extension srcPath

 607 |            | _ => throw (InternalError $

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

 609 |               ++ srcPath

 610 |               ++ "\n"

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

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

 614 |          let destNest = joinPath modPath

 615 |          let destPath = destdir </> destNest

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

 618 |          Right _ <- coreLift $ mkdirAll $ destPath

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

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

 621 |                              , show err ]

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

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

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

 625 |            Right _ <- coreLift $ chmod destFile

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

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

 628 |            pure ()

 629 |          Right _ <- coreLift $ copyFile srcPath destFile

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

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

 632 |                              , show err ]

 633 |          -- Make the source read-only

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

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

 636 |          pure ()

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

 639 | absoluteInstallDir relativeInstallDir = do

 640 |   mdestdir <- coreLift $ getEnv "DESTDIR"

 641 |   let destdir = fromMaybe "" mdestdir

 642 |   pure $ destdir ++ relativeInstallDir

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

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

 649 |           PkgDesc ->

 650 |           List CLOpt ->

 651 |           (installSrc : Bool) ->

 652 |           Core ()

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

 654 |     = do defs <- get Ctxt

 655 |          build <- ttcBuildDirectory

 656 |          let lib = installDir pkg

 657 |          libTargetDir <- absoluteInstallDir =<< libInstallDirectory lib

 658 |          ttcTargetDir <- absoluteInstallDir =<< ttcInstallDirectory lib

 659 |          srcTargetDir <- absoluteInstallDir =<< srcInstallDirectory lib

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

 662 |          runScript (preinstall pkg)

 663 |          let toInstall = maybe (modules pkg)

 664 |                                (:: modules pkg)

 665 |                                (mainmod pkg)

 666 |          wdir <- getWorkingDir

 667 |          -- Make the package installation directory

 668 |          Right _ <- coreLift $ mkdirAll libTargetDir

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

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

 671 |                              , show err ]

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

 675 |          when installSrc $ do

 676 |            traverse_ (installSrcFrom wdir srcTargetDir) toInstall

 678 |          -- install package file

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

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

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

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

 684 |          coreLift_ $ writeFile pkgFile pkgStr

 686 |          runScript (postinstall pkg)

 687 |   where

 688 |     savePkgMetadata : PkgDesc -> PkgDesc

 689 |     savePkgMetadata pkg =

 690 |       the (PkgDesc -> PkgDesc)

 691 |       { depends := pkg.depends

 692 |       , version := pkg.version

 693 |       } $ initPkgDesc pkg.name

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

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

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

 700 |         {auto _ : Ref PostS PostSession} ->

 701 |         PkgDesc ->

 702 |         List CLOpt ->

 703 |         Core (List Error)

 704 | check pkg opts =

 705 |   do assertIdrisCompatibility pkg

 706 |      [] <- prepareCompilation pkg opts

 707 |        | errs => pure errs

 709 |      runScript (postbuild pkg)

 710 |      pure []

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

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

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

 715 |           {auto _ : Ref PostS PostSession} ->

 716 |           PkgDesc ->

 717 |           List CLOpt ->

 718 |           Core (List Error)

 719 | makeDoc pkg opts =

 720 |     do [] <- prepareCompilation pkg opts

 721 |          | errs => pure errs

 723 |        defs <- get Ctxt

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

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

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

 727 |        Right () <- coreLift $ mkdirAll docDir

 728 |          | Left err => fileError docDir err

 729 |        u <- newRef UST initUState

 730 |        setPPrint docsPPrint

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

 733 |            -- load dependencies

 734 |            let ns = miAsNamespace mod

 735 |            addImport (MkImport emptyFC False mod ns)

 737 |            -- generate docs for all visible names

 738 |            defs <- get Ctxt

 739 |            let ctxt = gamma defs

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

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

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

 743 |                   | _ => pure Nothing

 744 |                 let Just nfc = isNonEmptyFC $ location gdef

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

 746 |                               [ show mod ++ ":"

 747 |                               , show (fullname gdef)

 748 |                               , "has an empty FC"

 749 |                               ]

 750 |                             pure Nothing

 751 |                 let PhysicalIdrSrc mod' = origin nfc

 752 |                   | _ => pure Nothing

 753 |                 let True = mod == mod'

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

 755 |                               [ show mod ++ ":"

 756 |                               , show (fullname gdef)

 757 |                               , "was defined in"

 758 |                               , show mod'

 759 |                               ]

 760 |                             pure Nothing

 761 |                 let True = visible gdef

 762 |                   | _ => pure Nothing

 763 |                 pure (Just gdef)

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

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

 767 |                         getDocsForName emptyFC (fullname def) shortNamesConfig

 768 |            let allDecls = annotate Declarations $ vcat allDocs

 770 |            -- grab module header doc

 771 |            syn  <- get Syn

 772 |            let modDoc = lookup mod (modDocstrings syn)

 773 |            log "doc.module" 10 $ unwords

 774 |              [ "Looked up doc for"

 775 |              , show mod

 776 |              , "and got:"

 777 |              , show modDoc

 778 |              ]

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

 781 |            -- grab publically re-exported modules

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

 783 |                                guard (not $ null docs)

 784 |                                pure docs

 785 |            whenJust mreexports $ \ reexports =>

 786 |              log "doc.module" 15 $ unwords

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

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

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

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

 793 |                           coreLift $ writeFile outputFilePath doc

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

 796 |            pure $ the (List Error) []

 797 |          )

 798 |          | errs => pure errs

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

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

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

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

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

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

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

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

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

 811 |        let [] = concat errs

 812 |            | err => pure err

 814 |        runScript (postbuild pkg)

 815 |        pure []

 816 |   where

 817 |     visible : GlobalDef -> Bool

 818 |     visible def = case definition def of

 819 |       DCon {} => False

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

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

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

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

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

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

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

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

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

 834 |   where

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

 836 |   go ks (MkStringTrie nd) =

 837 |     map bifold $ bitraverseC

 838 |                    (fv ks)

 839 |                    (\sm => foldlC

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

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

 842 |                                   y <- assert_total $ go ks' vs

 843 |                                   z <- fk ks'

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

 845 |                              neutral

 846 |                              (StringMap.toList sm))

 847 |                    nd

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

 850 |         PkgDesc ->

 851 |         List CLOpt ->

 852 |         Core ()

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

 854 |     = do defs <- get Ctxt

 855 |          runScript (preclean pkg)

 856 |          let pkgmods = maybe

 857 |                          (map fst (modules pkg))

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

 859 |                          (mainmod pkg)

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

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

 862 |                                        [] => Nothing

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

 864 |                           pkgmods

 865 |          srcdir <- getWorkingDir

 866 |          let d = dirs (options defs)

 867 |          bdir <- ttcBuildDirectory

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

 869 |          let outputdir = srcdir </> outputDirWithDefault d

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

 871 |          let pkgTrie : StringTrie (List String)

 872 |                      = foldl (\trie, ksv =>

 873 |                                 let ks = Builtin.fst ksv

 874 |                                     v = Builtin.snd ksv

 875 |                                   in

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

 877 |          foldWithKeysC (deleteFolder builddir)

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

 879 |                        pkgTrie

 880 |          deleteFolder builddir []

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

 882 |                (executable pkg)

 883 |          -- clean out the generated docs

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

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

 886 |          deleteDocsFolder $ build </> "docs"

 887 |          runScript (postclean pkg)

 888 |   where

 889 |     delete : String -> Core ()

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

 891 |                        | Left err => pure ()

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

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

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

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

 898 |     deleteBin builddir ns mod

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

 900 |              delete $ ttFile <.> "ttc"

 901 |              delete $ ttFile <.> "ttm"

 903 |     deleteDocsFolder : String -> Core ()

 904 |     deleteDocsFolder dir

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

 906 |                | Left err => pure ()

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

 908 |                        docbasefiles

 909 |              deleteFolder dir []

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

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

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

 916 |           Maybe String ->

 917 |           Core ()

 918 | runRepl fname = do

 919 |   u <- newRef UST initUState

 920 |   origin <- maybe

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

 922 |       modIdent <- ctxtPathToNS fname

 923 |       pure (PhysicalIdrSrc modIdent)

 924 |       ) fname

 925 |   m <- newRef MD (initMetadata origin)

 926 |   case fname of

 927 |       Nothing => pure ()

 928 |       Just fn => do

 929 |         errs <- loadMainFile fn

 930 |         displayStartupErrors errs

 931 |   repl {u} {s}

 935 | localPackageFile : Maybe String -> Core String

 936 | localPackageFile (Just fp) = pure fp

 937 | localPackageFile Nothing

 938 |   = do wdir <- getWorkingDir

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

 940 |        let candidates = map fileName tree.files

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

 942 |          [fp] => pure fp

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

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

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

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

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

 949 |                  {auto _ : Ref PostS PostSession} ->

 950 |                  List CLOpt ->

 951 |                  (PkgCommand, Maybe String) ->

 952 |                  Core ()

 953 | processPackage opts (cmd, mfile)

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

 955 |         Init =>

 956 |           do Just pkg <- coreLift interactive

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

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

 959 |              False <- coreLift (exists fp)

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

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

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

 963 |              pure ()

 964 |         _ =>

 965 |           do file <- localPackageFile mfile

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

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

 968 |              let True = isSuffixOf ".ipkg" filename

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

 970 |                            coreLift (exitWith (ExitFailure 1))

 971 |              setWorkingDir dir

 972 |              pkg <- parsePkgFile True filename

 973 |              whenJust (builddir pkg) setBuildDir

 974 |              whenJust (datadir pkg) addDataDir

 975 |              setOutputDir (outputdir pkg)

 976 |              case cmd of

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

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

 979 |                               pure ()

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

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

 982 |                               pure ()

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

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

 985 |                                 install pkg opts {installSrc = False}

 986 |                   InstallWithSrc =>

 987 |                              do [] <- build pkg opts

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

 989 |                                 install pkg opts {installSrc = True}

 990 |                   Typecheck => do

 991 |                     [] <- check pkg opts

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

 993 |                     pure ()

 994 |                   Clean => clean pkg opts

 995 |                   REPL => do

 996 |                     [] <- build pkg opts

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

 998 |                     runRepl (map snd $ mainmod pkg)

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

1000 |                   DumpJson => coreLift . putStrLn $ toJson pkg

1001 |                   DumpInstallDir => do

1002 |                     libInstallDir <- libInstallDirectory (installDir pkg)

1003 |                     dir <- absoluteInstallDir libInstallDir

1004 |                     coreLift (putStrLn dir)

1006 | record PackageOpts where

1007 |   constructor MkPFR

1008 |   pkgDetails : List (PkgCommand, Maybe String)

1009 |   oopts : List CLOpt

1010 |   hasError : Bool

1012 | partitionOpts : List CLOpt -> PackageOpts

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

1014 |   where

1015 |     data OptType : Type where

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

1017 |       POpt : OptType

1018 |       PIgnore : OptType

1019 |       PErr : OptType

1020 |     optType : CLOpt -> OptType

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

1022 |     optType Quiet                  = POpt

1023 |     optType Verbose                = POpt

1024 |     optType (Timing l)             = POpt

1025 |     optType (Logging l)            = POpt

1026 |     optType CaseTreeHeuristics     = POpt

1027 |     optType (DumpANF f)            = POpt

1028 |     optType (DumpCases f)          = POpt

1029 |     optType (DumpLifted f)         = POpt

1030 |     optType (DumpVMCode f)         = POpt

1031 |     optType DebugElabCheck         = POpt

1032 |     optType (SetCG f)              = POpt

1033 |     optType (IncrementalCG _)      = POpt

1034 |     optType (Directive d)          = POpt

1035 |     optType (BuildDir f)           = POpt

1036 |     optType (OutputDir f)          = POpt

1037 |     optType WarningsAsErrors       = POpt

1038 |     optType HashesInsteadOfModTime = POpt

1039 |     optType Profile                = POpt

1040 |     optType (ConsoleWidth n)       = PIgnore

1041 |     optType (Color b)              = PIgnore

1042 |     optType NoBanner               = PIgnore

1043 |     optType x                      = PErr

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

1046 |     pOptUpdate opt with (optType opt)

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

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

1049 |       pOptUpdate opt | PIgnore = id

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

1052 | errorMsg : String

1053 | errorMsg = unlines

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

1055 |   , "Overridable options are:"

1056 |   , "    --quiet"

1057 |   , "    --verbose"

1058 |   , "    --timing"

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

1060 |   , "    --dumpcases <file>"

1061 |   , "    --dumplifted <file>"

1062 |   , "    --dumpvmcode <file>"

1063 |   , "    --debug-elab-check"

1064 |   , "    --codegen <cg>"

1065 |   , "    --inc <cg>"

1066 |   , "    --directive <directive>"

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

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

1069 |   ]

1072 |   {auto c : Ref Ctxt Defs}

1073 |   {auto s : Ref Syn SyntaxInfo}

1074 |   {auto o : Ref ROpts REPLOpts}

1075 |   {auto p : Ref PostS PostSession}

1077 |   export

1078 |   processPackageOpts : List CLOpt -> Core ControlFlow

1079 |   processPackageOpts opts

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

1081 |                | (MkPFR Nil opts' _) => pure Continue

1082 |            if err

1083 |              then coreLift $ putStrLn errorMsg

1084 |              else traverse_ (processPackage opts') cmds

1085 |            pure Abort

1088 |   -- find an ipkg file in one of the parent directories

1089 |   -- If it exists, read it, set the current directory to the root of the source

1090 |   -- tree, and set the relevant command line options before proceeding

1091 |   export

1092 |   findIpkg : Maybe String -> Core (Maybe String)

1093 |   findIpkg fname

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