diff --git a/src/Compiler/Common.idr b/src/Compiler/Common.idr index e8aa7a324..981fce749 100644 --- a/src/Compiler/Common.idr +++ b/src/Compiler/Common.idr @@ -503,18 +503,6 @@ getExtraRuntime directives | Left err => throw (FileErr p err) pure contents -||| Looks up an executable from a list of candidate names in the PATH -export -pathLookup : List String -> IO (Maybe String) -pathLookup candidates - = do path <- idrisGetEnv "PATH" - let extensions = if isWindows then [".exe", ".cmd", ".bat", ""] else [""] - let pathList = forget $ String.split (== pathSeparator) $ fromMaybe "/usr/bin:/usr/local/bin" path - let candidates = [p ++ "/" ++ x ++ y | p <- pathList, - x <- candidates, - y <- extensions ] - firstExists candidates - ||| Cast implementations. Values of `ConstantPrimitives` can ||| be used in a call to `castInt`, which then determines ||| the cast implementation based on the given pair of diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr index 2236cdecc..e582aa15f 100644 --- a/src/Core/Binary.idr +++ b/src/Core/Binary.idr @@ -277,7 +277,7 @@ writeToTTC extradata sourceFileName ttcFileName defs <- get Ctxt ust <- get UST gdefs <- getSaveDefs (currentNS defs) (keys (toSave defs)) [] defs - sourceHash <- hashFile sourceFileName + sourceHash <- hashFileWith defs.options.hashFn sourceFileName log "ttc.write" 5 $ "Writing " ++ ttcFileName ++ " with source hash " ++ sourceHash ++ " and interface hash " ++ show (ifaceHash defs) writeTTCFile bin (MkTTCFile ttcVersion (sourceHash) (ifaceHash defs) (importHashes defs) diff --git a/src/Core/Context.idr b/src/Core/Context.idr index 27434b6a3..e5f025e99 100644 --- a/src/Core/Context.idr +++ b/src/Core/Context.idr @@ -1144,12 +1144,13 @@ export initDefs : Core Defs initDefs = do gam <- initCtxt + opts <- defaults pure $ MkDefs { gamma = gam , mutData = [] , currentNS = mainNS , nestedNS = [] - , options = defaults + , options = opts , toSave = empty , nextTag = 100 , typeHints = empty diff --git a/src/Core/Options.idr b/src/Core/Options.idr index 779efc999..f2a6f2210 100644 --- a/src/Core/Options.idr +++ b/src/Core/Options.idr @@ -4,6 +4,7 @@ import Core.Core import Core.Name import public Core.Options.Log import Core.TT + import Libraries.Utils.Binary import Libraries.Utils.Path @@ -199,6 +200,7 @@ record Options where primnames : PrimNames extensions : List LangExt additionalCGs : List (String, CG) + hashFn : String export @@ -236,11 +238,23 @@ defaultElab : ElabDirectives defaultElab = MkElabDirectives True True CoveringOnly 3 50 50 True export -defaults : Options -defaults = MkOptions defaultDirs defaultPPrint defaultSession - defaultElab Nothing Nothing - (MkPrimNs Nothing Nothing Nothing Nothing) [] - [] +defaultHashFn : Core String +defaultHashFn + = do Nothing <- coreLift $ pathLookup ["sha256sum", "gsha256sum"] + | Just p => pure $ p ++ " --tag" + Nothing <- coreLift $ pathLookup ["sha256"] + | Just p => pure $ p + Nothing <- coreLift $ pathLookup ["openssl"] + | Just p => pure $ p ++ " sha256" + coreFail $ InternalError ("Can't get util to get sha256sum (tried `sha256sum`, `gsha256sum`, `sha256`, `openssl`)") + +export +defaults : Core Options +defaults + = do hashFn <- defaultHashFn + pure $ MkOptions + defaultDirs defaultPPrint defaultSession defaultElab Nothing Nothing + (MkPrimNs Nothing Nothing Nothing Nothing) [] [] hashFn -- Reset the options which are set by source files export diff --git a/src/Idris/ModTree.idr b/src/Idris/ModTree.idr index 6ee77291f..52262514a 100644 --- a/src/Idris/ModTree.idr +++ b/src/Idris/ModTree.idr @@ -152,7 +152,8 @@ needsBuildingTime sourceFile ttcFile depFiles checkDepHashes : {auto c : Ref Ctxt Defs} -> String -> Core Bool checkDepHashes depFileName - = catch (do depCodeHash <- hashFile depFileName + = catch (do defs <- get Ctxt + depCodeHash <- hashFileWith (defs.options.hashFn) depFileName depTTCFileName <- getTTCFileName depFileName "ttc" (depStoredCodeHash, _) <- readHashes depTTCFileName pure $ depCodeHash /= depStoredCodeHash) @@ -165,7 +166,8 @@ needsBuildingHash : {auto c : Ref Ctxt Defs} -> (sourceFile : String) -> (ttcFile : String) -> (depFiles : List String) -> Core Bool needsBuildingHash sourceFile ttcFile depFiles - = do codeHash <- hashFile sourceFile + = do defs <- get Ctxt + codeHash <- hashFileWith (defs.options.hashFn) sourceFile (storedCodeHash, _) <- readHashes ttcFile depFilesHashDiffers <- any id <$> traverse checkDepHashes depFiles pure $ codeHash /= storedCodeHash || depFilesHashDiffers diff --git a/src/Idris/ProcessIdr.idr b/src/Idris/ProcessIdr.idr index 87034ae27..c4a863230 100644 --- a/src/Idris/ProcessIdr.idr +++ b/src/Idris/ProcessIdr.idr @@ -231,9 +231,9 @@ unchangedTime sourceFileName ttcFileName ||| If the source file hash hasn't changed -unchangedHash : (sourceFileName : String) -> (ttcFileName : String) -> Core Bool -unchangedHash sourceFileName ttcFileName - = do sourceCodeHash <- hashFile sourceFileName +unchangedHash : (hashFn : String) -> (sourceFileName : String) -> (ttcFileName : String) -> Core Bool +unchangedHash hashFn sourceFileName ttcFileName + = do sourceCodeHash <- hashFileWith hashFn sourceFileName (storedSourceHash, _) <- readHashes ttcFileName pure $ sourceCodeHash == storedSourceHash @@ -300,7 +300,7 @@ processMod sourceFileName ttcFileName msg sourcecode origin show (sort storedImportInterfaceHashes) sourceUnchanged <- (if session.checkHashesInsteadOfModTime - then unchangedHash else unchangedTime) sourceFileName ttcFileName + then unchangedHash (defs.options.hashFn) else unchangedTime) sourceFileName ttcFileName -- If neither the source nor the interface hashes of imports have changed then no rebuilding is needed if (sourceUnchanged && sort importInterfaceHashes == sort storedImportInterfaceHashes) diff --git a/src/Libraries/Utils/Binary.idr b/src/Libraries/Utils/Binary.idr index e7c769900..ec3a23c49 100644 --- a/src/Libraries/Utils/Binary.idr +++ b/src/Libraries/Utils/Binary.idr @@ -471,20 +471,22 @@ modTime fname pure t export -hashFile : String -> Core String -hashFile fileName +hashFileWith : String -> String -> Core String +hashFileWith sha256sum fileName = do Right fileHandle <- coreLift $ popen - ("sha256sum \"" ++ osEscape fileName ++ "\"") Read - | Left _ => coreFail $ InternalError ("Can't get sha256sum of " ++ fileName) + (sha256sum ++ " \"" ++ osEscape fileName ++ "\"") Read + | Left _ => err Right hashLine <- coreLift $ fGetLine fileHandle | Left _ => do coreLift $ pclose fileHandle - coreFail $ InternalError ("Can't get sha256sum of " ++ fileName) + err coreLift $ pclose fileHandle - let (hash::_) = words hashLine - | Nil => coreFail $ InternalError ("Can't get sha256sum of " ++ fileName) - pure hash + let w@(_::_) = words hashLine + | Nil => err + pure $ last w where + err : Core String + err = coreFail $ InternalError ("Can't get " ++ sha256sum ++ " of " ++ fileName) osEscape : String -> String osEscape = if isWindows then id diff --git a/src/Libraries/Utils/Path.idr b/src/Libraries/Utils/Path.idr index 18eca919a..945087efc 100644 --- a/src/Libraries/Utils/Path.idr +++ b/src/Libraries/Utils/Path.idr @@ -1,18 +1,21 @@ module Libraries.Utils.Path +import Idris.Env + import Data.List import Data.List1 import Data.Maybe import Data.Nat import Data.String -import Libraries.Data.String.Extra +import Libraries.Data.String.Extra import Libraries.Text.Token import Libraries.Text.Lexer import Libraries.Text.Parser import Libraries.Text.Quantity import System.Info +import System.File %default total @@ -572,3 +575,15 @@ export export dropExtension : String -> String dropExtension path = path <.> "" + +||| Looks up an executable from a list of candidate names in the PATH +export +pathLookup : List String -> IO (Maybe String) +pathLookup candidates + = do path <- idrisGetEnv "PATH" + let extensions = if isWindows then [".exe", ".cmd", ".bat", ""] else [""] + let pathList = forget $ String.split (== pathSeparator) $ fromMaybe "/usr/bin:/usr/local/bin" path + let candidates = [p ++ "/" ++ x ++ y | p <- pathList, + x <- candidates, + y <- extensions ] + firstExists candidates