Disable -Xcheck-hashes, at least for the moment (#1940)

* Version increment to 0.5.1

This is to remove the requirement on Chez >9.5

* Disable -Xcheck-hases, at least for the moment

If we're going to have this as an option, we need to have a portable way
of finding a sha256sum command. At the moment, we might find a command,
but different versions accept different options. We should at least
allow setting it via an environment variable, and we certainly shouldn't
fail if running the command fails.

* Update bootstrap code ready for 0.5.1 release

Author: edwinb

bootstrap/idris2_app/idris2.rkt

@@ -33,7 +33,7 @@ import public Libraries.Utils.Binary
 ||| (Increment this when changing anything in the data format)
 export
 ttcVersion : Int
-ttcVersion = 62
+ttcVersion = 63
 
 export
 checkTTCVersion : String -> Int -> Int -> Core ()
@@ -44,7 +44,7 @@ record TTCFile extra where
   constructor MkTTCFile
   version : Int
   totalReq : TotalReq
-  sourceHash : String
+  sourceHash : Maybe String
   ifaceHash : Int
   importHashes : List (Namespace, Int)
   incData : List (CG, String, List String)
@@ -289,12 +289,13 @@ writeToTTC extradata sourceFileName ttcFileName
          totalReq <- getDefaultTotalityOption
          log "ttc.write" 5 $ unwords
            [ "Writing", ttcFileName
-           , "with source hash", sourceHash
+           , "with source hash", show sourceHash
            , "and interface hash", show (ifaceHash defs)
            ]
          writeTTCFile bin
                    (MkTTCFile ttcVersion totalReq
-                              sourceHash (ifaceHash defs) (importHashes defs)
+                              sourceHash
+                              (ifaceHash defs) (importHashes defs)
                               (incData defs)
                               gdefs
                               (keys (userHoles defs))
@@ -522,7 +523,7 @@ getImportHashes file b
          ver <- fromBuf @{Wasteful} b
          checkTTCVersion file ver ttcVersion
          totalReq <- fromBuf {a = TotalReq} b
-         sourceFileHash <- fromBuf {a = String} b
+         sourceFileHash <- fromBuf {a = Maybe String} b
          interfaceHash <- fromBuf {a = Int} b
          fromBuf b
 
@@ -546,7 +547,7 @@ readTotalReq fileName
                (\err => pure Nothing)
 
 export
-getHashes : String -> Ref Bin Binary -> Core (String, Int)
+getHashes : String -> Ref Bin Binary -> Core (Maybe String, Int)
 getHashes file b
     = do hdr <- fromBuf {a = String} b
          when (hdr /= "TT2") $ corrupt ("TTC header in " ++ file ++ " " ++ show hdr)
@@ -559,13 +560,13 @@ getHashes file b
 
 export
 readHashes : (fileName : String) -> -- file containing the module
-                Core (String, Int)
+                Core (Maybe String, Int)
 readHashes fileName
     = do Right buffer <- coreLift $ readFromFile fileName
-            | Left err => pure ("", 0)
+            | Left err => pure (Nothing, 0)
          b <- newRef Bin buffer
          catch (getHashes fileName b)
-               (\err => pure ("", 0))
+               (\err => pure (Nothing, 0))
 
 export
 readImportHashes : (fname : String) -> -- file containing the module

bootstrap/idris2_app/idris2.ss

@@ -408,8 +408,9 @@ modTime fname
        pure t
 
 export
-hashFileWith : String -> String -> Core String
-hashFileWith sha256sum fileName
+hashFileWith : Maybe String -> String -> Core (Maybe String)
+hashFileWith Nothing _ = pure Nothing
+hashFileWith (Just sha256sum) fileName
   = do Right fileHandle <- coreLift $ popen
             (sha256sum ++ " \"" ++ osEscape fileName ++ "\"") Read
          | Left _ => err
@@ -420,9 +421,9 @@ hashFileWith sha256sum fileName
        coreLift $ pclose fileHandle
        let w@(_::_) = words hashLine
          | Nil => err
-       pure $ last w
+       pure $ Just $ last w
   where
-    err : Core String
+    err : Core a
     err = coreFail $ InternalError ("Can't get " ++ sha256sum ++ " of " ++ fileName)
     osEscape : String -> String
     osEscape = if isWindows

src/Core/Binary.idr

@@ -201,7 +201,7 @@ record Options where
   primnames : PrimNames
   extensions : List LangExt
   additionalCGs : List (String, CG)
-  hashFn : String
+  hashFn : Maybe String
 
 export
 availableCGs : Options -> List (String, CG)
@@ -237,24 +237,31 @@ export
 defaultElab : ElabDirectives
 defaultElab = MkElabDirectives True True CoveringOnly 3 50 50 True
 
+-- FIXME: This turns out not to be reliably portable, since different systems
+-- may have tools with the same name but different required arugments. We
+-- probably need another way (perhaps our own internal hash function, although
+-- that's not going to be as good as sha256).
 export
-defaultHashFn : Core String
+defaultHashFn : Core (Maybe String)
 defaultHashFn
     = do Nothing <- coreLift $ pathLookup ["sha256sum", "gsha256sum"]
-           | Just p => pure $ p ++ " --tag"
+           | Just p => pure $ Just $ p ++ " --tag"
          Nothing <- coreLift $ pathLookup ["sha256"]
-           | Just p => pure $ p
+           | Just p => pure $ Just p
          Nothing <- coreLift $ pathLookup ["openssl"]
-           | Just p => pure $ p ++ " sha256"
-         coreFail $ InternalError ("Can't get util to get sha256sum (tried `sha256sum`, `gsha256sum`, `sha256`, `openssl`)")
+           | Just p => pure $ Just $ p ++ " sha256"
+         pure Nothing
 
 export
 defaults : Core Options
 defaults
-    = do hashFn <- defaultHashFn
+    = do -- hashFn <- defaultHashFn
+         -- Temporarily disabling the hash function until we have a more
+         -- portable way of working out what to call, and allowing a way for
+         -- it to fail gracefully.
          pure $ MkOptions
            defaultDirs defaultPPrint defaultSession defaultElab Nothing Nothing
-           (MkPrimNs Nothing Nothing Nothing Nothing) [] [] hashFn
+           (MkPrimNs Nothing Nothing Nothing Nothing) [] [] Nothing
 
 -- Reset the options which are set by source files
 export

src/Core/Binary/Prims.idr

@@ -174,9 +174,11 @@ checkDepHashes : {auto c : Ref Ctxt Defs} ->
                  String -> Core Bool
 checkDepHashes depFileName
   = catch (do defs                   <- get Ctxt
-              depCodeHash            <- hashFileWith (defs.options.hashFn) depFileName
+              Just depCodeHash       <- hashFileWith (defs.options.hashFn) depFileName
+                    | _ => pure False
               depTTCFileName         <- getTTCFileName depFileName "ttc"
-              (depStoredCodeHash, _) <- readHashes depTTCFileName
+              (Just depStoredCodeHash, _) <- readHashes depTTCFileName
+                    | _ => pure False
               pure $ depCodeHash /= depStoredCodeHash)
           (\error => pure False)
 
@@ -186,11 +188,15 @@ needsBuildingHash : {auto c : Ref Ctxt Defs} ->
                     (sourceFile : String) -> (ttcFile : String) ->
                     (depFiles : List String) -> Core Bool
 needsBuildingHash sourceFile ttcFile depFiles
-  = do  defs                <- get Ctxt
-        codeHash            <- hashFileWith (defs.options.hashFn) sourceFile
-        (storedCodeHash, _) <- readHashes ttcFile
-        depFilesHashDiffers <- any id <$> traverse checkDepHashes depFiles
-        pure $ codeHash /= storedCodeHash || depFilesHashDiffers
+  = do defs                <- get Ctxt
+       -- If there's no hash available, either in the TTC or from the
+       -- current source, then it needs building
+       Just codeHash       <- hashFileWith (defs.options.hashFn) sourceFile
+             | _ => pure True
+       (Just storedCodeHash, _) <- readHashes ttcFile
+             | _ => pure True
+       depFilesHashDiffers <- any id <$> traverse checkDepHashes depFiles
+       pure $ codeHash /= storedCodeHash || depFilesHashDiffers
 
 export
 needsBuilding :

src/Core/Options.idr

@@ -237,10 +237,12 @@ unchangedTime sourceFileName ttcFileName
 
 
 ||| If the source file hash hasn't changed
-unchangedHash : (hashFn : String) -> (sourceFileName : String) -> (ttcFileName : String) -> Core Bool
+unchangedHash : (hashFn : Maybe String) -> (sourceFileName : String) -> (ttcFileName : String) -> Core Bool
 unchangedHash hashFn sourceFileName ttcFileName
-  = do sourceCodeHash        <- hashFileWith hashFn sourceFileName
-       (storedSourceHash, _) <- readHashes ttcFileName
+  = do Just sourceCodeHash        <- hashFileWith hashFn sourceFileName
+             | _ => pure False
+       (Just storedSourceHash, _) <- readHashes ttcFileName
+             | _ => pure False
        pure $ sourceCodeHash == storedSourceHash
 
 export

src/Idris/ModTree.idr

@@ -413,7 +413,8 @@ preOptions (IgnoreShadowingWarnings :: opts)
     = do updateSession (record { showShadowingWarning = False })
          preOptions opts
 preOptions (HashesInsteadOfModTime :: opts)
-    = do updateSession (record { checkHashesInsteadOfModTime = True })
+    = do throw (InternalError "-Xcheck-hashes disabled (see issue #1935)")
+         updateSession (record { checkHashesInsteadOfModTime = True })
          preOptions opts
 preOptions (CaseTreeHeuristics :: opts)
     = do updateSession (record { caseTreeHeuristics = True })

src/Idris/ProcessIdr.idr

@@ -6,5 +6,3 @@ Test> Bye for now!
 2/3: Building Mult (Mult.idr)
 Test> S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))
 Test> Bye for now!
-Test> S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))))
-Test> Bye for now!

src/Idris/SetOptions.idr

@@ -4,7 +4,9 @@ $1 --no-color --console-width 0 --no-banner --no-prelude Test.idr < input
 sleep 1
 touch Mult.idr
 $1 --no-color --console-width 0 --no-banner --no-prelude Test.idr < input
-sleep 1
-touch Mult.idr
-$1 --no-color --console-width 0 --no-banner --no-prelude -Xcheck-hashes Test.idr < input
+
+# Disabled until we have a portable way to do this
+#sleep 1
+#touch Mult.idr
+#$1 --no-color --console-width 0 --no-banner --no-prelude -Xcheck-hashes Test.idr < input