0 | module Idris.SetOptions

  2 | import Compiler.Common

  4 | import Core.Binary

  5 | import Core.Directory

  6 | import Core.Metadata

  7 | import Core.Unify

  8 | import Libraries.Utils.Path

  9 | import Libraries.Data.List.Extra

 11 | import Idris.CommandLine

 12 | import Idris.Package.Types

 13 | import Idris.Parser

 14 | import Idris.Pretty

 15 | import Idris.ProcessIdr

 16 | import Idris.REPL

 17 | import Idris.Syntax

 18 | import Idris.Version

 20 | import Data.List1

 21 | import Data.String

 23 | import System

 24 | import System.Directory

 26 | %default covering

 29 | record PkgDir where

 30 |   constructor MkPkgDir

 31 |   ||| Directory name. Example "contrib-0.3.0"

 32 |   dirName : String

 33 |   ||| Package name. Example "contrib"

 34 |   pkgName : String

 35 |   ||| Package version. Example `Just $ MkPkgVersion (0 ::: [3,0])`

 36 |   version : Maybe PkgVersion

 37 |   ||| Versions of binary TTC format supported by library

 38 |   ttcVersions : List Int

 40 | record QualifiedPkgDir where

 41 |   constructor MkQualifiedPkgDir

 42 |   ||| Path where package directory is located on disk.

 43 |   path : String

 44 |   ||| PkgDir for packages

 45 |   pkgDir : PkgDir

 49 | pkgDir : (dirName : String) -> (ttcDirs : List Int) -> PkgDir

 50 | pkgDir dirName ttcDirs =

 51 |    -- Split the dir name into parts concatenated by "-"

 52 |    -- treating the last part as the version number

 53 |    -- and the initial parts as the package name.

 54 |    -- For reasons of backwards compatibility, we also

 55 |    -- accept hyphenated directory names without a part

 56 |    -- corresponding to a version number.

 57 |    case unsnoc $ split (== '-') dirName of

 58 |      (Nil, last) => MkPkgDir dirName last Nothing ttcDirs

 59 |      (init,last) =>

 60 |        case toVersion last of

 61 |          Just v  => MkPkgDir dirName (concat $ intersperse "-" init) (Just v) ttcDirs

 62 |          Nothing => MkPkgDir dirName dirName Nothing ttcDirs

 63 |   where

 64 |     toVersion : String -> Maybe PkgVersion

 65 |     toVersion = map MkPkgVersion

 66 |               . traverse parsePositive

 67 |               . split (== '.')

 69 | listDirOrEmpty : String -> IO (List String)

 70 | listDirOrEmpty dir = either (const []) id <$> listDir dir

 72 | getPackageDirs : String -> IO (List PkgDir)

 73 | getPackageDirs dname = do

 74 |   packageDirNames <- listDirOrEmpty dname

 75 |   traverse (\d => pkgDir d <$> ttcVersions d) packageDirNames

 76 |   where

 77 |     ttcVersions : String -> IO (List Int)

 78 |     ttcVersions dir = catMaybes . map parsePositive <$> listDirOrEmpty (dname </> dir)

 86 | candidateDirs :

 87 |     Ref Ctxt Defs =>

 88 |     String -> String -> PkgVersionBounds ->

 89 |     Core (List (String, Maybe PkgVersion))

 90 | candidateDirs dname pkgName bounds = do

 91 |   dirs <- coreLift (getPackageDirs dname)

 92 |   checkedDirs <- traverse check dirs

 93 |   pure (catMaybes checkedDirs)

 95 |   where

 96 |     data CandidateError = OutOfBounds | TTCMismatch

 98 |     checkNameAndBounds : PkgDir -> Either CandidateError PkgDir

 99 |     checkNameAndBounds pkg =

100 |       if pkg.pkgName == pkgName && inBounds pkg.version bounds

101 |          then Right pkg

102 |          else Left OutOfBounds

104 |     checkTTCVersion : PkgDir -> Either CandidateError PkgDir

105 |     checkTTCVersion pkg =

106 |       if ttcVersion `elem` pkg.ttcVersions

107 |          then Right pkg

108 |          else Left TTCMismatch

110 |     unpack : PkgDir -> (String, Maybe PkgVersion)

111 |     unpack (MkPkgDir dirName pkgName ver _) =

112 |       ((dname </> dirName), ver)

114 |     check : PkgDir -> Core (Maybe (String, Maybe PkgVersion))

115 |     check pkg =

116 |       let checkedPkg = checkNameAndBounds pkg >>= checkTTCVersion

117 |       in

118 |       case checkedPkg of

119 |         Right pkg'       => pure . Just $ unpack pkg'

120 |         Left OutOfBounds => pure Nothing

121 |         Left TTCMismatch => do

141 | findPkgDirs :

142 |     Ref Ctxt Defs =>

143 |     String ->

144 |     PkgVersionBounds ->

145 |     Core (List (String, Maybe PkgVersion))

146 | findPkgDirs p bounds = do

147 |   localdir <- pkgLocalDirectory

149 |   -- Get candidate directories from the local package directory

150 |   locFiles <- candidateDirs localdir p bounds

151 |   -- Look in all the package paths too

152 |   d <- getDirs

153 |   pkgFiles <- traverse (\d => candidateDirs (show d) p bounds) d.package_search_paths

155 |   -- If there's anything locally, use that and ignore the global ones

156 |   let allFiles = if isNil locFiles

157 |                     then concat pkgFiles

158 |                     else locFiles

159 |   -- Sort in reverse order of version number

160 |   pure $ sortBy (\x, y => compare (snd y) (snd x)) allFiles

163 | findPkgDir :

164 |     Ref Ctxt Defs =>

165 |     String ->

166 |     PkgVersionBounds ->

167 |     Core (Maybe String)

168 | findPkgDir p bounds = do

169 |   defs <- get Ctxt

170 |   [] <- findPkgDirs p bounds | ((p,_) :: _) => pure (Just p)

172 |   -- From what remains, pick the one with the highest version number.

173 |   -- If there's none, report it

174 |   -- (TODO: Can't do this quite yet due to idris2 build system...)

175 |   if defs.options.session.ignoreMissingPkg

176 |      then pure Nothing

177 |      else throw (CantFindPackage (p ++ " (" ++ show bounds ++ ")"))

182 | addPkgDir : {auto c : Ref Ctxt Defs} ->

183 |             String -> PkgVersionBounds -> Core ()

184 | addPkgDir p bounds = do

185 |     Just p <- findPkgDir p bounds

186 |         | Nothing => pure ()

187 |     addPackageDir p

189 | visiblePackages : String -> IO (List QualifiedPkgDir)

190 | visiblePackages dir = map (MkQualifiedPkgDir dir) <$> filter viable <$> getPackageDirs dir

191 |   where notHidden : PkgDir -> Bool

192 |         notHidden = not . isPrefixOf "." . pkgName

194 |         notDenylisted : PkgDir -> Bool

195 |         notDenylisted = not . flip elem (the (List String) ["include", "lib", "support", "refc"]) . pkgName

197 |         viable : PkgDir -> Bool

198 |         viable p = notHidden p && notDenylisted p

200 | findPackages : {auto c : Ref Ctxt Defs} -> Core (List QualifiedPkgDir)

202 |     = do d <- getDirs

203 |          pkgPathPkgs <- coreLift $ traverse (\d => visiblePackages $ show d) d.package_search_paths

204 |          -- local packages

205 |          localPkgs <- coreLift $ visiblePackages !pkgLocalDirectory

206 |          pure $ localPkgs ++ join pkgPathPkgs

208 | listPackages : {auto c : Ref Ctxt Defs} ->

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

210 |                Core ()

212 |     = do pkgs <- sortBy (compare `on` (pkgName . pkgDir)) <$> findPackages

213 |          printIdrisTTCVersion

214 |          traverse_ (iputStrLn . pkgDesc) pkgs

215 |   where

216 |     printIdrisTTCVersion : Core ()

217 |     printIdrisTTCVersion = iputStrLn $

218 |       pretty0 "Idris2 TTC Version: \{show ttcVersion}" <+> line <+>

219 |       (replicateChar 5 '─')

221 |     pkgTTCVersions : PkgDir -> Doc IdrisAnn

222 |     pkgTTCVersions (MkPkgDir _ _ _ ttcVersions) =

223 |       pretty0 "├ TTC Versions:" <++> prettyTTCVersions

224 |       where

225 |         annotate : Int -> Doc IdrisAnn

226 |         annotate version =

227 |           if version == ttcVersion

228 |              then pretty0 $ show version

229 |              else warning ((pretty0 $ show version) <++> (parens "incompatible"))

231 |         prettyTTCVersions : Doc IdrisAnn

232 |         prettyTTCVersions = (concatWith (\x,y => x <+> "," <++> y)) $ annotate <$> sort ttcVersions

234 |     pkgPath : String -> Doc IdrisAnn

235 |     pkgPath path = pretty0 "└ \{path}"

237 |     extraInfo : QualifiedPkgDir -> Doc IdrisAnn

238 |     extraInfo (MkQualifiedPkgDir path pkg) =

239 |       let extra = indent 2 $

240 |         pkgTTCVersions pkg <+> line <+>

241 |         pkgPath path

242 |       in line <+> extra

244 |     pkgDesc : QualifiedPkgDir -> Doc IdrisAnn

245 |     pkgDesc pkg@(MkQualifiedPkgDir _ (MkPkgDir _ pkgName version _)) =

246 |       pretty0 pkgName <++> parens (pretty0 $ maybe "unversioned" show version)

247 |         <+> extraInfo pkg

249 | dirOption : {auto c : Ref Ctxt Defs} ->

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

251 |             Dirs -> DirCommand -> Core ()

252 | dirOption dirs LibDir

253 |     = coreLift $ putStrLn

254 |          (prefix_dir dirs </> "idris2-" ++ showVersion False version)

255 | dirOption dirs BlodwenPaths

256 |     = iputStrLn $ pretty0 (toString dirs)

257 | dirOption dirs Prefix

258 |     = coreLift $ putStrLn (prefix_dir dirs)

264 | findIpkg : Core (List String)

265 | findIpkg =

266 |   do Just srcdir <- coreLift currentDir

267 |        | Nothing => throw (InternalError "Can't get current directory")

268 |      Right fs <- coreLift $ listDir srcdir

269 |        | Left err => pure []

270 |      pure $ filter (".ipkg" `isSuffixOf`) fs

273 | prefixOnly : String -> List String -> List String

274 | prefixOnly x = sortedNub . filter (\s => x /= s && isPrefixOf x s)

278 | prefixOnlyIfNonEmpty : String -> List String -> List String

279 | prefixOnlyIfNonEmpty "--" = id

280 | prefixOnlyIfNonEmpty s    = prefixOnly s

284 | codegens : {auto c : Ref Ctxt Defs} -> Core (List String)

285 | codegens = map fst . availableCGs . options <$> get Ctxt

287 | logLevels : List String

288 | logLevels = map fst knownTopics >>= prefixes . forget . split (== '.')

289 |   where prefixes : List String -> List String

290 |         prefixes [] = []

291 |         prefixes (x :: xs) = x :: map (x ++ "." ++) (prefixes xs)

298 | opts : {auto c : Ref Ctxt Defs} -> String -> String -> Core (List String)

299 | opts "--" "idris2"  = pure optionFlags

302 | opts x "--cg"      = prefixOnlyIfNonEmpty x <$> codegens

303 | opts x "--codegen" = prefixOnlyIfNonEmpty x <$> codegens

306 | opts x "-p"        = prefixOnlyIfNonEmpty x . (map $ pkgName . pkgDir) <$> findPackages

307 | opts x "--package" = prefixOnlyIfNonEmpty x . (map $ pkgName . pkgDir) <$> findPackages

310 | opts x "--log"     = pure $ prefixOnlyIfNonEmpty x logLevels

313 | opts "--" "-o"           = pure []

314 | opts "--" "--output"     = pure []

315 | opts "--" "--source-dir" = pure []

316 | opts "--" "--build-dir"  = pure []

317 | opts "--" "--output-dir" = pure []

320 | opts x "--build"          = prefixOnlyIfNonEmpty x <$> findIpkg

321 | opts x "--dump-ipkg-json" = prefixOnlyIfNonEmpty x <$> findIpkg

322 | opts x "--install"        = prefixOnlyIfNonEmpty x <$> findIpkg

323 | opts x "--mkdoc"          = prefixOnlyIfNonEmpty x <$> findIpkg

324 | opts x "--typecheck"      = prefixOnlyIfNonEmpty x <$> findIpkg

325 | opts x "--clean"          = prefixOnlyIfNonEmpty x <$> findIpkg

326 | opts x "--repl"           = prefixOnlyIfNonEmpty x <$> findIpkg

329 | opts x _ = pure $ if (x `elem` optionFlags)

330 |                      -- `x` is already a known option => perform

331 |                      -- directory completion

332 |                      then Nil

333 |                      else prefixOnly x optionFlags

336 | bashCompletionScript : (fun : String) -> String

337 | bashCompletionScript fun = let fun' = "_" ++ fun in """

347 | zshCompletionScript : (fun : String) -> String

348 | zshCompletionScript fun = let fun' = "_" ++ fun in """

379 | setIncrementalCG : {auto c : Ref Ctxt Defs} ->

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

381 |                    Bool -> String -> Core ()

382 | setIncrementalCG failOnError cgn

383 |     = do defs <- get Ctxt

384 |          case getCG (options defs) cgn of

385 |            Just cg =>

386 |                do Just cgd <- getCG cg

387 |                        | Nothing => pure ()

388 |                   let Just _ = incCompileFile cgd

389 |                        | Nothing =>

390 |                             if failOnError

391 |                                then do coreLift $ putStrLn $ cgn ++ " does not support incremental builds"

392 |                                        coreLift $ exitWith (ExitFailure 1)

393 |                                else pure ()

394 |                   setSession ({ incrementalCGs $= (cg :: )} !getSession)

395 |            Nothing =>

396 |               if failOnError

397 |                  then do coreLift $ putStrLn "No such code generator"

398 |                          coreLift $ putStrLn $ "Code generators available: " ++

399 |                                          showSep ", " (map fst (availableCGs (options defs)))

400 |                          coreLift $ exitWith (ExitFailure 1)

401 |                  else pure ()

405 | preOptions : {auto c : Ref Ctxt Defs} ->

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

407 |              List CLOpt -> Core Bool

408 | preOptions [] = pure True

409 | preOptions (NoBanner :: opts)

410 |     = do setSession ({ nobanner := True } !getSession)

411 |          preOptions opts

413 | preOptions (OutputFile _ :: opts)

414 |     = do setSession ({ nobanner := True } !getSession)

415 |          preOptions opts

416 | preOptions (ExecFn _ :: opts)

417 |     = do setSession ({ nobanner := True } !getSession)

418 |          preOptions opts

419 | preOptions (IdeMode :: opts)

420 |     = do setSession ({ nobanner := True } !getSession)

421 |          preOptions opts

422 | preOptions (IdeModeSocket _ :: opts)

423 |     = do setSession ({ nobanner := True } !getSession)

424 |          preOptions opts

425 | preOptions (CheckOnly :: opts)

426 |     = do setSession ({ nobanner := True } !getSession)

427 |          preOptions opts

428 | preOptions (Profile :: opts)

429 |     = do setSession ({ profile := True } !getSession)

430 |          preOptions opts

431 | preOptions (Quiet :: opts)

432 |     = do setOutput (REPL VerbosityLvl.ErrorLvl)

433 |          preOptions opts

434 | preOptions (NoPrelude :: opts)

435 |     = do setSession ({ noprelude := True } !getSession)

436 |          preOptions opts

437 | preOptions (SetCG e :: opts)

438 |     = do defs <- get Ctxt

439 |          case getCG (options defs) e of

440 |             Just cg => do setCG cg

441 |                           preOptions opts

442 |             Nothing =>

443 |               do coreLift $ putStrLn "No such code generator"

444 |                  coreLift $ putStrLn $ "Code generators available: " ++

445 |                                  showSep ", " (map fst (availableCGs (options defs)))

446 |                  coreLift $ exitWith (ExitFailure 1)

447 | preOptions (Directive d :: opts)

448 |     = do setSession ({ directives $= (d::) } !getSession)

449 |          preOptions opts

450 | preOptions (PkgPath p :: opts)

451 |     = do addPkgDir p anyBounds

452 |          preOptions opts

453 | preOptions (SourceDir d :: opts)

454 |     = do setSourceDir (Just d)

455 |          preOptions opts

456 | preOptions (BuildDir d :: opts)

457 |     = do setBuildDir d

458 |          preOptions opts

459 | preOptions (OutputDir d :: opts)

460 |     = do setOutputDir (Just d)

461 |          preOptions opts

462 | preOptions (Directory d :: opts)

463 |     = do defs <- get Ctxt

464 |          dirOption (dirs (options defs)) d

465 |          pure False

466 | preOptions (ListPackages :: opts)

467 |     = do listPackages

468 |          pure False

469 | preOptions (Timing tm :: opts)

470 |     = do setLogTimings (fromMaybe 10 tm)

471 |          preOptions opts

472 | preOptions (DebugElabCheck :: opts)

473 |     = do setDebugElabCheck True

474 |          preOptions opts

475 | preOptions (AltErrorCount c :: opts)

476 |     = do setSession ({ logErrorCount := c } !getSession)

477 |          preOptions opts

478 | preOptions (RunREPL _ :: opts)

479 |     = do setOutput (REPL VerbosityLvl.ErrorLvl)

480 |          setSession ({ nobanner := True } !getSession)

481 |          preOptions opts

482 | preOptions (FindIPKG :: opts)

483 |     = do setSession ({ findipkg := True } !getSession)

484 |          preOptions opts

485 | preOptions (IgnoreMissingIPKG :: opts)

486 |     = do setSession ({ ignoreMissingPkg := True } !getSession)

487 |          preOptions opts

488 | preOptions (DumpCases f :: opts)

489 |     = do setSession ({ dumpcases := Just f } !getSession)

490 |          preOptions opts

491 | preOptions (DumpLifted f :: opts)

492 |     = do setSession ({ dumplifted := Just f } !getSession)

493 |          preOptions opts

494 | preOptions (DumpANF f :: opts)

495 |     = do setSession ({ dumpanf := Just f } !getSession)

496 |          preOptions opts

497 | preOptions (DumpVMCode f :: opts)

498 |     = do setSession ({ dumpvmcode := Just f } !getSession)

499 |          preOptions opts

500 | preOptions (Logging n :: opts)

501 |     = do setSession ({ logEnabled := True,

502 |                        logLevel $= insertLogLevel n } !getSession)

503 |          preOptions opts

504 | preOptions (ConsoleWidth n :: opts)

505 |     = do setConsoleWidth n

506 |          preOptions opts

507 | preOptions (ShowImplicits :: opts)

508 |     = do updatePPrint { showImplicits := True }

509 |          preOptions opts

510 | preOptions (ShowMachineNames :: opts)

511 |     = do updatePPrint { showMachineNames := True }

512 |          preOptions opts

513 | preOptions (ShowNamespaces :: opts)

514 |     = do updatePPrint { fullNamespace := True }

515 |          preOptions opts

516 | preOptions (Color b :: opts)

517 |     = do setColor b

518 |          preOptions opts

519 | preOptions (WarningsAsErrors :: opts)

520 |     = do updateSession ({ warningsAsErrors := True })

521 |          preOptions opts

522 | preOptions (IgnoreShadowingWarnings :: opts)

523 |     = do updateSession ({ showShadowingWarning := False })

524 |          preOptions opts

525 | preOptions (HashesInsteadOfModTime :: opts)

526 |     = do throw (InternalError "-Xcheck-hashes disabled (see issue #1935)")

527 |          updateSession ({ checkHashesInsteadOfModTime := True })

528 |          preOptions opts

529 | preOptions (CaseTreeHeuristics :: opts)

530 |     = do updateSession ({ caseTreeHeuristics := True })

531 |          preOptions opts

532 | preOptions (IncrementalCG e :: opts)

533 |     = do defs <- get Ctxt

534 |          setIncrementalCG True e

535 |          preOptions opts

536 | preOptions (WholeProgram :: opts)

537 |     = do updateSession ({ wholeProgram := True })

538 |          preOptions opts

539 | preOptions (BashCompletion a b :: _)

540 |     = do os <- opts a b

541 |          coreLift $ putStr $ unlines os

542 |          pure False

543 | preOptions (BashCompletionScript fun :: _)

544 |     = do coreLift $ putStrLn $ bashCompletionScript fun

545 |          pure False

546 | preOptions (ZshCompletionScript fun :: _)

547 |     = do coreLift $ putStrLn $ zshCompletionScript fun

548 |          pure False

549 | preOptions (Total :: opts)

550 |     = do updateSession ({ totalReq := Total })

551 |          preOptions opts

552 | preOptions (NoCSE :: opts)

553 |     = do updateSession ({ noCSE := True })

554 |          preOptions opts

555 | preOptions (_ :: opts) = preOptions opts

560 | postOptions : {auto c : Ref Ctxt Defs} ->

561 |               {auto u : Ref UST UState} ->

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

563 |               {auto m : Ref MD Metadata} ->

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

565 |               REPLResult -> List CLOpt -> Core Bool

566 | postOptions _ [] = pure True

567 | postOptions res@(ErrorLoadingFile {}) (OutputFile _ :: rest)

568 |     = do ignore $ postOptions res rest

569 |          pure False

570 | postOptions res (OutputFile outfile :: rest)

571 |     = do ignore $ compileExp (PRef EmptyFC (UN $ Basic "main")) outfile

572 |          ignore $ postOptions res rest

573 |          pure False

574 | postOptions res (ExecFn expr :: rest)

575 |     = do setCurrentElabSource expr

576 |          let Right (_, _, e) = runParser (Virtual Interactive) Nothing expr $ aPTerm <* eoi

577 |            | Left err => throw err

578 |          ignore $ execExp e

579 |          ignore $ postOptions res rest

580 |          pure False

581 | postOptions res (CheckOnly :: rest)

582 |     = do ignore $ postOptions res rest

583 |          pure False

584 | postOptions res (RunREPL str :: rest)

585 |     = do replCmd str

586 |          pure False

587 | postOptions res (_ :: rest) = postOptions res rest

590 | ideMode : List CLOpt -> Bool

591 | ideMode [] = False

592 | ideMode (IdeMode :: _) = True

593 | ideMode (_ :: xs) = ideMode xs

596 | ideModeSocket : List CLOpt -> Bool

597 | ideModeSocket [] = False

598 | ideModeSocket (IdeModeSocket _ :: _) = True

599 | ideModeSocket (_ :: xs) = ideModeSocket xs