From 61e04e36cf0dffdbd075d4cf24955c4cdf9cfc15 Mon Sep 17 00:00:00 2001 From: Stiopa Koltsov Date: Sun, 20 Jun 2021 02:05:03 +0100 Subject: [PATCH 1/4] Use gsha256sum when sha256sum doesn't exist On my mac laptop there's no `sha256sum` command, but there's `gsha256sum`: using `g` prefix is common when GNU utilities are installed on macOS. ``` SCHEME=chez make bootstrap ``` no longer fails on my laptop. The downside is that compilation now continuously prints a warning about `sha256sum` command not found (when it is not found). And I don't know how to fix it cross-platform way. ``` 1/5: Building Network.Socket.Data (Network/Socket/Data.idr) sh: sha256sum: command not found 2/5: Building Network.FFI (Network/FFI.idr) sh: sha256sum: command not found 3/5: Building Network.Socket.Raw (Network/Socket/Raw.idr) sh: sha256sum: command not found 4/5: Building Network.Socket (Network/Socket.idr) sh: sha256sum: command not found 5/5: Building Control.Linear.Network (Control/Linear/Network.idr) sh: sha256sum: command not found ``` --- src/Libraries/Utils/Binary.idr | 19 +++++++++++++++---- 1 file changed, 15 insertions(+), 4 deletions(-) diff --git a/src/Libraries/Utils/Binary.idr b/src/Libraries/Utils/Binary.idr index e7c769900..3dae91120 100644 --- a/src/Libraries/Utils/Binary.idr +++ b/src/Libraries/Utils/Binary.idr @@ -470,11 +470,10 @@ modTime fname coreLift $ closeFile f 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 + (sha256Sum ++ " \"" ++ osEscape fileName ++ "\"") Read | Left _ => coreFail $ InternalError ("Can't get sha256sum of " ++ fileName) Right hashLine <- coreLift $ fGetLine fileHandle | Left _ => @@ -489,3 +488,15 @@ hashFile fileName osEscape = if isWindows then id else escapeStringUnix + +export +hashFile : String -> Core String +hashFile fileName = + -- Note `popen` call won't fail if there's no `sha256sum` command + -- so we can't just catch `popen` error. + catch (hashFileWith "sha256sum" fileName) + (\err => + catch (hashFileWith "gsha256sum" fileName) + -- When `gsha256sum` fails as well, return the error with `sha256sum`. + (\_ => coreFail err) + ) From 106487ca59d142838e22f49284dd36891f6fa5dd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fabi=C3=A1n=20Heredia=20Montiel?= Date: Sat, 10 Jul 2021 16:38:17 -0500 Subject: [PATCH 2/4] [refactor] Move pathLookup from Compiler.Common to Utils.Path --- src/Compiler/Common.idr | 12 ------------ src/Libraries/Utils/Path.idr | 17 ++++++++++++++++- 2 files changed, 16 insertions(+), 13 deletions(-) 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/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 From 9b8de95a38c3dc501aa5ad6f46c4aeb7e57a83aa Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fabi=C3=A1n=20Heredia=20Montiel?= Date: Sat, 10 Jul 2021 16:43:43 -0500 Subject: [PATCH 3/4] Detect hashFn once Co-authored-by: Guillaume Allais --- src/Core/Binary.idr | 2 +- src/Core/Context.idr | 3 ++- src/Core/Options.idr | 24 +++++++++++++++++++----- src/Idris/ModTree.idr | 6 ++++-- src/Idris/ProcessIdr.idr | 8 ++++---- src/Libraries/Utils/Binary.idr | 13 +------------ 6 files changed, 31 insertions(+), 25 deletions(-) diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr index 7c0d2f457..fd3e8665a 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 4a2b6debc..b34646ea6 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 @@ -192,6 +193,7 @@ record Options where primnames : PrimNames extensions : List LangExt additionalCGs : List (String, CG) + hashFn : String export @@ -229,11 +231,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 daf5ec0a6..3fe5b28ab 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 3dae91120..6ac081113 100644 --- a/src/Libraries/Utils/Binary.idr +++ b/src/Libraries/Utils/Binary.idr @@ -470,6 +470,7 @@ modTime fname coreLift $ closeFile f pure t +export hashFileWith : String -> String -> Core String hashFileWith sha256Sum fileName = do Right fileHandle <- coreLift $ popen @@ -488,15 +489,3 @@ hashFileWith sha256Sum fileName osEscape = if isWindows then id else escapeStringUnix - -export -hashFile : String -> Core String -hashFile fileName = - -- Note `popen` call won't fail if there's no `sha256sum` command - -- so we can't just catch `popen` error. - catch (hashFileWith "sha256sum" fileName) - (\err => - catch (hashFileWith "gsha256sum" fileName) - -- When `gsha256sum` fails as well, return the error with `sha256sum`. - (\_ => coreFail err) - ) From dd7081e2fe827338ca3707f82d9b7124c69a3ec1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fabi=C3=A1n=20Heredia=20Montiel?= Date: Wed, 14 Jul 2021 13:26:16 -0500 Subject: [PATCH 4/4] Use `--tag` (non-reversed) variant of `sha256sum` for NetBSD compat Co-authored-by: Ben Hormann --- src/Libraries/Utils/Binary.idr | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/src/Libraries/Utils/Binary.idr b/src/Libraries/Utils/Binary.idr index 6ac081113..ec3a23c49 100644 --- a/src/Libraries/Utils/Binary.idr +++ b/src/Libraries/Utils/Binary.idr @@ -472,19 +472,21 @@ modTime fname export hashFileWith : String -> String -> Core String -hashFileWith sha256Sum fileName +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