Skip to content

Commit e0e8403

Browse files
fabianhjrbenhormann
fabianhjr
and
benhormann
authored
[ new ] detect changes using sha256 rather than timestamps (#1535)
The option is hidden being a flag (`-Xcheck-hashes`) so that by default `touch`ing a file is enough to get it recompiled. Co-authored-by: Ben Hormann <[email protected]>
1 parent 0db136d commit e0e8403

File tree

14 files changed

+264
-172
lines changed

14 files changed

+264
-172
lines changed

‎src/Compiler/Scheme/Chez.idr

Lines changed: 6 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -17,8 +17,6 @@ import Libraries.Utils.Path
1717
import Data.List
1818
import Data.List1
1919
import Data.Maybe
20-
import Libraries.Data.NameMap
21-
import Libraries.Data.Version
2220
import Data.Strings
2321
import Data.Vect
2422

@@ -29,6 +27,10 @@ import System.Directory
2927
import System.File
3028
import System.Info
3129

30+
import Libraries.Data.NameMap
31+
import Libraries.Data.Version
32+
import Libraries.Utils.String
33+
3234
%default covering
3335

3436
export
@@ -80,15 +82,6 @@ findLibs ds
8082
then Just (trim (substr 3 (length d) d))
8183
else Nothing
8284

83-
export
84-
escapeString : String -> String
85-
escapeString s = pack $ foldr escape [] $ unpack s
86-
where
87-
escape : Char -> List Char -> List Char
88-
escape '"' cs = '\\' :: '\"' :: cs
89-
escape '\\' cs = '\\' :: '\\' :: cs
90-
escape c cs = c :: cs
91-
9285
schHeader : String -> List String -> String
9386
schHeader chez libs
9487
= (if os /= "windows" then "#!" ++ chez ++ " --script\n\n" else "") ++
@@ -101,7 +94,7 @@ schHeader chez libs
10194
" [(i3nt ti3nt a6nt ta6nt) (load-shared-object \"msvcrt.dll\")" ++
10295
" (load-shared-object \"ws2_32.dll\")]\n" ++
10396
" [else (load-shared-object \"libc.so\")])\n\n" ++
104-
showSep "\n" (map (\x => "(load-shared-object \"" ++ escapeString x ++ "\")") libs) ++ "\n\n" ++
97+
showSep "\n" (map (\x => "(load-shared-object \"" ++ escapeStringChez x ++ "\")") libs) ++ "\n\n" ++
10598
"(let ()\n"
10699

107100
schFooter : Bool -> String
@@ -246,7 +239,7 @@ cCall appdir fc cfn clib args ret collectSafe
246239
copyLib (appdir </> fname, fullname)
247240
put Loaded (clib :: loaded)
248241
pure $ "(load-shared-object \""
249-
++ escapeString fname
242+
++ escapeStringChez fname
250243
++ "\")\n"
251244
argTypes <- traverse (cftySpec fc . snd) args
252245
retType <- cftySpec fc ret

‎src/Compiler/Scheme/ChezSep.idr

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -21,8 +21,6 @@ import Libraries.Utils.Path
2121
import Data.List
2222
import Data.List1
2323
import Data.Maybe
24-
import Libraries.Data.NameMap
25-
import Libraries.Data.Version
2624
import Data.Strings
2725
import Data.Vect
2826

@@ -33,6 +31,10 @@ import System.Directory
3331
import System.File
3432
import System.Info
3533

34+
import Libraries.Data.NameMap
35+
import Libraries.Data.Version
36+
import Libraries.Utils.String
37+
3638
%default covering
3739

3840
schHeader : List String -> List String -> String
@@ -46,7 +48,7 @@ schHeader libs compilationUnits = unlines
4648
, " [(i3nt ti3nt a6nt ta6nt) (load-shared-object \"msvcrt.dll\")"
4749
, " (load-shared-object \"ws2_32.dll\")]"
4850
, " [else (load-shared-object \"libc.so\")]"
49-
, unlines [" (load-shared-object \"" ++ escapeString lib ++ "\")" | lib <- libs]
51+
, unlines [" (load-shared-object \"" ++ escapeStringChez lib ++ "\")" | lib <- libs]
5052
, ")"
5153
]
5254

‎src/Core/Binary.idr

Lines changed: 42 additions & 35 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,6 @@
1+
||| Reading and writing 'Defs' from/to a binary file. In order to be saved, a
2+
||| name must have been flagged using 'toSave'. (Otherwise we'd save out
3+
||| everything, not just the things in the current file).
14
module Core.Binary
25

36
import Core.CaseTree
@@ -12,28 +15,23 @@ import Core.TT
1215
import Core.TTC
1316
import Core.UnifyState
1417

15-
import Libraries.Data.IntMap
18+
import Data.Buffer
1619
import Data.List
17-
import Libraries.Data.NameMap
1820

1921
import System.File
2022

21-
-- Reading and writing 'Defs' from/to a binary file
22-
-- In order to be saved, a name must have been flagged using 'toSave'.
23-
-- (Otherwise we'd save out everything, not just the things in the current
24-
-- file).
23+
import Libraries.Data.IntMap
24+
import Libraries.Data.NameMap
2525

2626
import public Libraries.Utils.Binary
2727

28-
import Data.Buffer
29-
3028
%default covering
3129

32-
-- increment this when changing anything in the data format
33-
-- TTC files can only be compatible if the version number is the same
30+
||| TTC files can only be compatible if the version number is the same
31+
||| (Increment this when changing anything in the data format)
3432
export
3533
ttcVersion : Int
36-
ttcVersion = 55
34+
ttcVersion = 56
3735

3836
export
3937
checkTTCVersion : String -> Int -> Int -> Core ()
@@ -43,6 +41,7 @@ checkTTCVersion file ver exp
4341
record TTCFile extra where
4442
constructor MkTTCFile
4543
version : Int
44+
sourceHash : String
4645
ifaceHash : Int
4746
importHashes : List (Namespace, Int)
4847
context : List (Name, Binary)
@@ -93,14 +92,14 @@ HasNames (Name, Name, Bool) where
9392
resolved c (n1, n2, b) = pure (!(resolved c n1), !(resolved c n2), b)
9493

9594
HasNames e => HasNames (TTCFile e) where
96-
full gam (MkTTCFile version ifaceHash iHashes
95+
full gam (MkTTCFile version sourceHash ifaceHash iHashes
9796
context userHoles
9897
autoHints typeHints
9998
imported nextVar currentNS nestedNS
10099
pairnames rewritenames primnames
101100
namedirectives cgdirectives trans
102101
extra)
103-
= pure $ MkTTCFile version ifaceHash iHashes
102+
= pure $ MkTTCFile version sourceHash ifaceHash iHashes
104103
context userHoles
105104
!(traverse (full gam) autoHints)
106105
!(traverse (full gam) typeHints)
@@ -131,14 +130,14 @@ HasNames e => HasNames (TTCFile e) where
131130
-- I don't think we ever actually want to call this, because after we read
132131
-- from the file we're going to add them to learn what the resolved names
133132
-- are supposed to be! But for completeness, let's do it right.
134-
resolved gam (MkTTCFile version ifaceHash iHashes
133+
resolved gam (MkTTCFile version sourceHash ifaceHash iHashes
135134
context userHoles
136135
autoHints typeHints
137136
imported nextVar currentNS nestedNS
138137
pairnames rewritenames primnames
139138
namedirectives cgdirectives trans
140139
extra)
141-
= pure $ MkTTCFile version ifaceHash iHashes
140+
= pure $ MkTTCFile version sourceHash ifaceHash iHashes
142141
context userHoles
143142
!(traverse (resolved gam) autoHints)
144143
!(traverse (resolved gam) typeHints)
@@ -177,6 +176,7 @@ writeTTCFile b file_in
177176
= do file <- toFullNames file_in
178177
toBuf b "TT2"
179178
toBuf @{Wasteful} b (version file)
179+
toBuf b (sourceHash file)
180180
toBuf b (ifaceHash file)
181181
toBuf b (importHashes file)
182182
toBuf b (imported file)
@@ -205,12 +205,13 @@ readTTCFile readall file as b
205205
when (hdr /= "TT2") $ corrupt ("TTC header in " ++ file ++ " " ++ show hdr)
206206
ver <- fromBuf @{Wasteful} b
207207
checkTTCVersion file ver ttcVersion
208+
sourceFileHash <- fromBuf b
208209
ifaceHash <- fromBuf b
209210
importHashes <- fromBuf b
210211
imp <- fromBuf b
211212
ex <- fromBuf b
212213
if not readall
213-
then pure (MkTTCFile ver ifaceHash importHashes [] [] [] [] []
214+
then pure (MkTTCFile ver sourceFileHash ifaceHash importHashes [] [] [] [] []
214215
0 (mkNamespace "") [] Nothing
215216
Nothing
216217
(MkPrimNs Nothing Nothing Nothing Nothing)
@@ -229,7 +230,7 @@ readTTCFile readall file as b
229230
nds <- fromBuf b
230231
cgds <- fromBuf b
231232
trans <- fromBuf b
232-
pure (MkTTCFile ver ifaceHash importHashes
233+
pure (MkTTCFile ver sourceFileHash ifaceHash importHashes
233234
(map (replaceNS cns) defs) uholes
234235
autohs typehs imp nextv cns nns
235236
pns rws prims nds cgds trans ex)
@@ -265,15 +266,17 @@ export
265266
writeToTTC : (HasNames extra, TTC extra) =>
266267
{auto c : Ref Ctxt Defs} ->
267268
{auto u : Ref UST UState} ->
268-
extra -> (fname : String) -> Core ()
269-
writeToTTC extradata fname
269+
extra -> (sourceFileName : String) ->
270+
(ttcFileName : String) -> Core ()
271+
writeToTTC extradata sourceFileName ttcFileName
270272
= do bin <- initBinary
271273
defs <- get Ctxt
272274
ust <- get UST
273275
gdefs <- getSaveDefs (currentNS defs) (keys (toSave defs)) [] defs
274-
log "ttc.write" 5 $ "Writing " ++ fname ++ " with hash " ++ show (ifaceHash defs)
276+
sourceHash <- hashFile sourceFileName
277+
log "ttc.write" 5 $ "Writing " ++ ttcFileName ++ " with source hash " ++ sourceHash ++ " and interface hash " ++ show (ifaceHash defs)
275278
writeTTCFile bin
276-
(MkTTCFile ttcVersion (ifaceHash defs) (importHashes defs)
279+
(MkTTCFile ttcVersion (sourceHash) (ifaceHash defs) (importHashes defs)
277280
gdefs
278281
(keys (userHoles defs))
279282
(saveAutoHints defs)
@@ -290,8 +293,8 @@ writeToTTC extradata fname
290293
(saveTransforms defs)
291294
extradata)
292295

293-
Right ok <- coreLift $ writeToFile fname !(get Bin)
294-
| Left err => throw (InternalError (fname ++ ": " ++ show err))
296+
Right ok <- coreLift $ writeToFile ttcFileName !(get Bin)
297+
| Left err => throw (InternalError (ttcFileName ++ ": " ++ show err))
295298
pure ()
296299

297300
addGlobalDef : {auto c : Ref Ctxt Defs} ->
@@ -497,27 +500,31 @@ getImportHashes file b
497500
when (hdr /= "TT2") $ corrupt ("TTC header in " ++ file ++ " " ++ show hdr)
498501
ver <- fromBuf @{Wasteful} b
499502
checkTTCVersion file ver ttcVersion
500-
ifaceHash <- fromBuf {a = Int} b
503+
sourceFileHash <- fromBuf {a = String} b
504+
interfaceHash <- fromBuf {a = Int} b
501505
fromBuf b
502506

503-
getHash : String -> Ref Bin Binary -> Core Int
504-
getHash file b
507+
export
508+
getHashes : String -> Ref Bin Binary -> Core (String, Int)
509+
getHashes file b
505510
= do hdr <- fromBuf {a = String} b
506511
when (hdr /= "TT2") $ corrupt ("TTC header in " ++ file ++ " " ++ show hdr)
507512
ver <- fromBuf @{Wasteful} b
508513
checkTTCVersion file ver ttcVersion
509-
fromBuf b
514+
sourceFileHash <- fromBuf b
515+
interfaceHash <- fromBuf b
516+
pure (sourceFileHash, interfaceHash)
510517

511518
export
512-
readIFaceHash : (fname : String) -> -- file containing the module
513-
Core Int
514-
readIFaceHash fname
515-
= do Right buffer <- coreLift $ readFromFile fname
516-
| Left err => pure 0
519+
readHashes : (fileName : String) -> -- file containing the module
520+
Core (String, Int)
521+
readHashes fileName
522+
= do Right buffer <- coreLift $ readFromFile fileName
523+
| Left err => pure ("", 0)
517524
b <- newRef Bin buffer
518-
catch (do res <- getHash fname b
519-
pure res)
520-
(\err => pure 0)
525+
catch (do hashes <- getHashes fileName b
526+
pure hashes)
527+
(\err => pure ("", 0))
521528

522529
export
523530
readImportHashes : (fname : String) -> -- file containing the module

‎src/Core/Options.idr

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -160,6 +160,8 @@ record Session where
160160
-- Warnings
161161
warningsAsErrors : Bool
162162
showShadowingWarning : Bool
163+
-- Experimental
164+
checkHashesInsteadOfModTime : Bool
163165

164166
public export
165167
record PPrinter where
@@ -208,7 +210,7 @@ export
208210
defaultSession : Session
209211
defaultSession = MkSessionOpts False False False Chez [] False defaultLogLevel
210212
False False False Nothing Nothing
211-
Nothing Nothing False False True
213+
Nothing Nothing False False True False
212214

213215
export
214216
defaultElab : ElabDirectives

‎src/Idris/CommandLine.idr

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -136,6 +136,9 @@ data CLOpt
136136
WarningsAsErrors |
137137
||| Do not print shadowing warnings
138138
IgnoreShadowingWarnings |
139+
||| Use SHA256 hashes to determine if a source file needs rebuilding instead
140+
||| of modification time.
141+
HashesInsteadOfModTime |
139142
||| Generate bash completion info
140143
BashCompletion String String |
141144
||| Generate bash completion script
@@ -225,6 +228,10 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly]
225228
MkOpt ["-Wno-shadowing"] [] [IgnoreShadowingWarnings]
226229
(Just "Do not print shadowing warnings"),
227230

231+
optSeparator,
232+
MkOpt ["-Xcheck-hashes"] [] [HashesInsteadOfModTime]
233+
(Just "Use SHA256 hashes instead of modification time to determine if a source file needs rebuilding"),
234+
228235
optSeparator,
229236
MkOpt ["--prefix"] [] [ShowPrefix]
230237
(Just "Show installation prefix"),

0 commit comments

Comments
 (0)