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 |              {auto s : Ref PostS PostSession} ->

408 |              List CLOpt -> Core ControlFlow

409 | preOptions [] = pure Continue

410 | preOptions (NoBanner :: opts)

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

412 |          preOptions opts

414 | preOptions (OutputFile file :: opts)

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

416 |          update PostS {outputFile := Just file}

417 |          preOptions opts

418 | preOptions (ExecFn expr :: opts)

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

420 |          update PostS {execExpr $= (expr ::)}

421 |          preOptions opts

422 | preOptions (IdeMode :: opts)

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

424 |          preOptions opts

425 | preOptions (IdeModeSocket _ :: opts)

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

427 |          preOptions opts

428 | preOptions (CheckOnly :: opts)

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

430 |          update PostS {checkOnly := True}

431 |          preOptions opts

432 | preOptions (Profile :: opts)

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

434 |          preOptions opts

435 | preOptions (Quiet :: opts)

436 |     = do setOutput (REPL VerbosityLvl.ErrorLvl)

437 |          preOptions opts

438 | preOptions (NoPrelude :: opts)

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

440 |          preOptions opts

441 | preOptions (SetCG e :: opts)

442 |     = do defs <- get Ctxt

443 |          case getCG (options defs) e of

444 |             Just cg => do setCG cg

445 |                           preOptions opts

446 |             Nothing =>

447 |               do throw $ UserError $ """

451 |                  pure Abort

452 | preOptions (Directive d :: opts)

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

454 |          preOptions opts

455 | preOptions (PkgPath p :: opts)

456 |     = do addPkgDir p anyBounds

457 |          preOptions opts

458 | preOptions (SourceDir d :: opts)

459 |     = do setSourceDir (Just d)

460 |          preOptions opts

461 | preOptions (BuildDir d :: opts)

462 |     = do setBuildDir d

463 |          preOptions opts

464 | preOptions (OutputDir d :: opts)

465 |     = do setOutputDir (Just d)

466 |          preOptions opts

467 | preOptions (Directory d :: opts)

468 |     = do defs <- get Ctxt

469 |          dirOption (dirs (options defs)) d

470 |          pure Abort

471 | preOptions (ListPackages :: opts)

472 |     = do listPackages

473 |          pure Abort

474 | preOptions (Timing tm :: opts)

475 |     = do setLogTimings (fromMaybe 10 tm)

476 |          preOptions opts

477 | preOptions (DebugElabCheck :: opts)

478 |     = do setDebugElabCheck True

479 |          preOptions opts

480 | preOptions (AltErrorCount c :: opts)

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

482 |          preOptions opts

483 | preOptions (RunREPL expr :: opts)

484 |     = do setOutput (REPL VerbosityLvl.ErrorLvl)

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

486 |          update PostS {runRepl := Just expr}

487 |          preOptions opts

488 | preOptions (FindIPKG :: opts)

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

490 |          preOptions opts

491 | preOptions (IgnoreMissingIPKG :: opts)

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

493 |          preOptions opts

494 | preOptions (DumpCases f :: opts)

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

496 |          preOptions opts

497 | preOptions (DumpLifted f :: opts)

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

499 |          preOptions opts

500 | preOptions (DumpANF f :: opts)

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

502 |          preOptions opts

503 | preOptions (DumpVMCode f :: opts)

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

505 |          preOptions opts

506 | preOptions (Logging n :: opts)

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

508 |                        logLevel $= insertLogLevel n } !getSession)

509 |          preOptions opts

510 | preOptions (ConsoleWidth n :: opts)

511 |     = do setConsoleWidth n

512 |          preOptions opts

513 | preOptions (ShowImplicits :: opts)

514 |     = do updatePPrint { showImplicits := True }

515 |          preOptions opts

516 | preOptions (ShowMachineNames :: opts)

517 |     = do updatePPrint { showMachineNames := True }

518 |          preOptions opts

519 | preOptions (ShowNamespaces :: opts)

520 |     = do updatePPrint { fullNamespace := True }

521 |          preOptions opts

522 | preOptions (Color b :: opts)

523 |     = do setColor b

524 |          preOptions opts

525 | preOptions (WarningsAsErrors :: opts)

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

527 |          preOptions opts

528 | preOptions (IgnoreShadowingWarnings :: opts)

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

530 |          preOptions opts

531 | preOptions (HashesInsteadOfModTime :: opts)

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

533 |          updateSession ({ checkHashesInsteadOfModTime := True })

534 |          preOptions opts

535 | preOptions (CaseTreeHeuristics :: opts)

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

537 |          preOptions opts

538 | preOptions (IncrementalCG e :: opts)

539 |     = do defs <- get Ctxt

540 |          setIncrementalCG True e

541 |          preOptions opts

542 | preOptions (WholeProgram :: opts)

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

544 |          preOptions opts

545 | preOptions (BashCompletion a b :: _)

546 |     = do os <- opts a b

547 |          coreLift $ putStr $ unlines os

548 |          pure Abort

549 | preOptions (BashCompletionScript fun :: _)

550 |     = do coreLift $ putStrLn $ bashCompletionScript fun

551 |          pure Abort

552 | preOptions (ZshCompletionScript fun :: _)

553 |     = do coreLift $ putStrLn $ zshCompletionScript fun

554 |          pure Abort

555 | preOptions (Total :: opts)

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

557 |          preOptions opts

558 | preOptions (NoCSE :: opts)

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

560 |          preOptions opts

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

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

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

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

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

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

571 |               REPLResult -> PostSession -> Core ControlFlow

573 | postOptions res@(ErrorLoadingFile {}) (MkPostSession _ (Just _) _ _)

574 |     = pure Abort

582 | postOptions _ (MkPostSession check out ex runRepl)

583 |     = do controlFlow <- newRef ControlFlow Continue

584 |          whenJust out $ \ outfile => do

585 |              ignore $ compileExp (PRef EmptyFC (UN $ Basic "main")) outfile

586 |              put ControlFlow Abort

587 |          flip traverse_ (reverse ex) $ \ expr => do

588 |              setCurrentElabSource expr

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

590 |                    | Left err => throw err

591 |              ignore $ execExp e

592 |              put ControlFlow Abort

593 |          when check $

594 |              put ControlFlow Abort

595 |          whenJust runRepl $ \cmd => do

596 |              replCmd cmd

597 |              put ControlFlow Abort

598 |          get ControlFlow

601 | ideMode : List CLOpt -> Bool

602 | ideMode [] = False

603 | ideMode (IdeMode :: _) = True

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

607 | ideModeSocket : List CLOpt -> Bool

608 | ideModeSocket [] = False

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

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