mirror of
https://github.com/anoma/juvix.git
synced 2024-12-15 01:52:11 +03:00
382a4d3cef
This PR introduces a global `--offline` flag. ## Doctor This replaces the `--offline` flag on the doctor command. ## Juvix package builds The flag applies to juvix build commands like `juvix compile`, `juvix repl`. This is so that users can continue to build packages offline that have external dependencies when there's no network connection (as long as they built the same package online previously). Specifically, when the `--offline` flag is used in a package that has external git dependencies. * No `git clone` or `git fetch` commands are used * `git checkout` will continue to be used * Clones from previous builds are reused This means that you can update the `ref` field in a git dependency, as long as the ref existed the last time that the project was built without the `--offline` flag. * Closes https://github.com/anoma/juvix/issues/2333
188 lines
5.9 KiB
Haskell
188 lines
5.9 KiB
Haskell
module GlobalOptions
|
|
( module GlobalOptions,
|
|
)
|
|
where
|
|
|
|
import CommonOptions
|
|
import Juvix.Compiler.Core.Options qualified as Core
|
|
import Juvix.Compiler.Internal.Pretty.Options qualified as Internal
|
|
import Juvix.Compiler.Pipeline
|
|
import Juvix.Data.Error.GenericError qualified as E
|
|
|
|
data GlobalOptions = GlobalOptions
|
|
{ _globalNoColors :: Bool,
|
|
_globalShowNameIds :: Bool,
|
|
_globalBuildDir :: Maybe (AppPath Dir),
|
|
_globalOnlyErrors :: Bool,
|
|
_globalStdin :: Bool,
|
|
_globalNoTermination :: Bool,
|
|
_globalNoPositivity :: Bool,
|
|
_globalNoCoverage :: Bool,
|
|
_globalNoStdlib :: Bool,
|
|
_globalUnrollLimit :: Int,
|
|
_globalOffline :: Bool
|
|
}
|
|
deriving stock (Eq, Show)
|
|
|
|
makeLenses ''GlobalOptions
|
|
|
|
instance CanonicalProjection GlobalOptions Internal.Options where
|
|
project g =
|
|
Internal.defaultOptions
|
|
{ Internal._optShowNameIds = g ^. globalShowNameIds
|
|
}
|
|
|
|
instance CanonicalProjection GlobalOptions E.GenericOptions where
|
|
project GlobalOptions {..} =
|
|
E.GenericOptions
|
|
{ E._showNameIds = _globalShowNameIds
|
|
}
|
|
|
|
instance CanonicalProjection GlobalOptions Core.CoreOptions where
|
|
project GlobalOptions {..} =
|
|
Core.CoreOptions
|
|
{ Core._optCheckCoverage = not _globalNoCoverage,
|
|
Core._optUnrollLimit = _globalUnrollLimit,
|
|
Core._optOptimizationLevel = defaultOptimizationLevel,
|
|
Core._optInliningDepth = defaultInliningDepth
|
|
}
|
|
|
|
defaultGlobalOptions :: GlobalOptions
|
|
defaultGlobalOptions =
|
|
GlobalOptions
|
|
{ _globalNoColors = False,
|
|
_globalShowNameIds = False,
|
|
_globalOnlyErrors = False,
|
|
_globalNoTermination = False,
|
|
_globalBuildDir = Nothing,
|
|
_globalStdin = False,
|
|
_globalNoPositivity = False,
|
|
_globalNoCoverage = False,
|
|
_globalNoStdlib = False,
|
|
_globalUnrollLimit = defaultUnrollLimit,
|
|
_globalOffline = False
|
|
}
|
|
|
|
-- | Get a parser for global flags which can be hidden or not depending on
|
|
-- the input boolean
|
|
parseGlobalFlags :: Parser GlobalOptions
|
|
parseGlobalFlags = do
|
|
_globalNoColors <-
|
|
switch
|
|
( long "no-colors"
|
|
<> help "Disable ANSI formatting"
|
|
)
|
|
_globalShowNameIds <-
|
|
switch
|
|
( long "show-name-ids"
|
|
<> help "Show the unique number of each identifier when pretty printing"
|
|
)
|
|
_globalBuildDir <-
|
|
optional
|
|
( parseBuildDir
|
|
( long "internal-build-dir"
|
|
<> help "Directory for compiler internal output"
|
|
)
|
|
)
|
|
_globalStdin <-
|
|
switch
|
|
( long "stdin"
|
|
<> help "Read from Stdin"
|
|
)
|
|
_globalOnlyErrors <-
|
|
switch
|
|
( long "only-errors"
|
|
<> help "Only print errors in a uniform format (used by juvix-mode)"
|
|
)
|
|
_globalNoTermination <-
|
|
switch
|
|
( long "no-termination"
|
|
<> help "Disable termination checking"
|
|
)
|
|
_globalNoPositivity <-
|
|
switch
|
|
( long "no-positivity"
|
|
<> help "Disable positivity checking for inductive types"
|
|
)
|
|
_globalNoCoverage <-
|
|
switch
|
|
( long "no-coverage"
|
|
<> help "Disable coverage checking for patterns"
|
|
)
|
|
_globalNoStdlib <-
|
|
switch
|
|
( long "no-stdlib"
|
|
<> help "Do not use the standard library"
|
|
)
|
|
_globalUnrollLimit <-
|
|
option
|
|
(fromIntegral <$> naturalNumberOpt)
|
|
( long "unroll"
|
|
<> value defaultUnrollLimit
|
|
<> help ("Recursion unrolling limit (default: " <> show defaultUnrollLimit <> ")")
|
|
)
|
|
_globalOffline <-
|
|
switch
|
|
( long "offline"
|
|
<> help "Disable access to network resources"
|
|
)
|
|
return GlobalOptions {..}
|
|
|
|
parseBuildDir :: Mod OptionFields (Prepath Dir) -> Parser (AppPath Dir)
|
|
parseBuildDir m = do
|
|
_pathPath <-
|
|
option
|
|
somePreDirOpt
|
|
( metavar "BUILD_DIR"
|
|
<> action "directory"
|
|
<> m
|
|
)
|
|
pure AppPath {_pathIsInput = False, ..}
|
|
|
|
entryPointFromGlobalOptionsPre :: Roots -> Prepath File -> GlobalOptions -> IO EntryPoint
|
|
entryPointFromGlobalOptionsPre roots premainFile opts = do
|
|
mainFile <- prepathToAbsFile (roots ^. rootsInvokeDir) premainFile
|
|
entryPointFromGlobalOptions roots mainFile opts
|
|
|
|
entryPointFromGlobalOptions :: Roots -> Path Abs File -> GlobalOptions -> IO EntryPoint
|
|
entryPointFromGlobalOptions roots mainFile opts = do
|
|
mabsBuildDir :: Maybe (Path Abs Dir) <- mapM (prepathToAbsDir cwd) optBuildDir
|
|
let def :: EntryPoint
|
|
def = defaultEntryPoint roots mainFile
|
|
return
|
|
def
|
|
{ _entryPointNoTermination = opts ^. globalNoTermination,
|
|
_entryPointNoPositivity = opts ^. globalNoPositivity,
|
|
_entryPointNoCoverage = opts ^. globalNoCoverage,
|
|
_entryPointNoStdlib = opts ^. globalNoStdlib,
|
|
_entryPointUnrollLimit = opts ^. globalUnrollLimit,
|
|
_entryPointGenericOptions = project opts,
|
|
_entryPointBuildDir = maybe (def ^. entryPointBuildDir) Abs mabsBuildDir,
|
|
_entryPointOffline = opts ^. globalOffline
|
|
}
|
|
where
|
|
optBuildDir :: Maybe (Prepath Dir)
|
|
optBuildDir = fmap (^. pathPath) (opts ^. globalBuildDir)
|
|
cwd = roots ^. rootsInvokeDir
|
|
|
|
entryPointFromGlobalOptionsNoFile :: Roots -> GlobalOptions -> IO EntryPoint
|
|
entryPointFromGlobalOptionsNoFile roots opts = do
|
|
mabsBuildDir :: Maybe (Path Abs Dir) <- mapM (prepathToAbsDir cwd) optBuildDir
|
|
let def :: EntryPoint
|
|
def = defaultEntryPointNoFile roots
|
|
return
|
|
def
|
|
{ _entryPointNoTermination = opts ^. globalNoTermination,
|
|
_entryPointNoPositivity = opts ^. globalNoPositivity,
|
|
_entryPointNoCoverage = opts ^. globalNoCoverage,
|
|
_entryPointNoStdlib = opts ^. globalNoStdlib,
|
|
_entryPointUnrollLimit = opts ^. globalUnrollLimit,
|
|
_entryPointGenericOptions = project opts,
|
|
_entryPointBuildDir = maybe (def ^. entryPointBuildDir) Abs mabsBuildDir,
|
|
_entryPointOffline = opts ^. globalOffline
|
|
}
|
|
where
|
|
optBuildDir :: Maybe (Prepath Dir)
|
|
optBuildDir = fmap (^. pathPath) (opts ^. globalBuildDir)
|
|
cwd = roots ^. rootsInvokeDir
|