[ new ] detect changes using sha256 rather than timestamps

[fabianhjr]

Closes #1519
Fixes #23 (modification time is not stored but read from the filesystem)

[fabianhjr]

I am blocked by Windows, if someone is a Windows dev and could help with the sha256 function it would be appreciated.

[edwinb]

Something I often do while working on Idris is touch a file to force it to rebuild. Or, just resave it. This probably isn't a common thing to want to do, but even so, what should I do instead now? I guess remove the relevant ttc?

[fabianhjr]

Hi @edwinb, an easier option than hunting down the idris ttc file to might be to add a blank line or space in the file you are working on. I did some testing on my fork and got this time differences:

Racket Self-hosting:

Comparing this runs:

• https://github.com/idris-lang/Idris2/actions/runs/925170679
• https://github.com/LibreCybernetics/Idris2/actions/runs/927413234

Since its intention is to reduce friction to contributing by speeding up the CI (Particularly time to first error and completion time) if it causes more inconvenience on the coding stage it would be counterproductive to the intention.

[andorp]

What if we hide one behind an arg?

[fabianhjr]

Yes, a flag is also a possibility.

I have no preference as a default so to keep backwards compatibility the sha256 based one could be the one that needed a toggle. Any preference for a flag? (Eg, -Xcheck-hash)

[benhormann]

Quoting and escaping is different on windows, thanks to cmd.exe. But if the paths are relative you don't need to.

Isn't SHA2 overkill? Would've thought MD5 or even CRC is good for this job.
Only cksum is standard. Even macOS and BSD have different names for SHA. Could upgrade to a FFI call later.

[fabianhjr]

Isn't SHA2 overkill? Would've thought MD5 or even CRC is good for this job.

MD5, SHA-1, and SHA-2 (256 to 512) are in the same magnitude of performance: https://automationrhapsody.com/md5-sha-1-sha-256-sha-512-speed-performance/ (In the comments there is even some pointers to get SHA-256 to be faster than MD5 and SHA-1)

I don't want to risk collisions (either accidental or as an intentional attack) so CRC is out.

Only cksum is standard.

sha256sum is on the same standard (corutils) as cksum ( https://www.gnu.org/software/coreutils/manual/coreutils.html#sha2-utilities ) and comes preinstalled on most UNIX based systems. (BSDs, macOS, Linux, etc)

Quoting and escaping is different on windows, thanks to cmd.exe. But if the paths are relative you don't need to.

Oh ok, then it should be easy to fix and even windows has sha256sum preinstalled so it seems like this could get to a mergeable state :3

Could upgrade to a FFI call later.

Yes that would probably help with the slight performance penalty of launching trough a shell and piping console IO. (And the path escaping or not)

[benhormann]

... comes preinstalled on most UNIX based systems. (BSDs, macOS, Linux, etc)

But it doesn't, only Linux and MSYS. Neither is gmp.
Turns out shasum is implemented in Perl on macOS.
I'll pipe down now.

[fabianhjr]

Ok, this new behavior is now behind an experimental flag (-Xcheck-hashes)

There is still a need for a windows Idris-dev since I don't have a windows machine and removing the escape didn't solve the issue. (I could leave the windows version unimplemented and leave a constant string in place but that would be less than ideal. UnU)

[benhormann]

TL;DR popen "certutil -hashfile \"" ++ fileName ++ "\""

Example output:

SHA1 hash of file C:\Windows\System32\cmd.exe:
0f 3c 4f f2 8f 35 4a ed e2 02 d5 4e 9d 1c 55 29 a3 bf 87 d8
CertUtil: -hashfile command completed successfully.

Assumes no % in fileName. Can append " SHA256" to upgrade. certutil -hashfile

---

Or if not quoting, here are my best guesses (untested):

/bin/sh (ref: https://unix.stackexchange.com/a/270979)

escapeUnquotedSh s = pack $ foldr escape [] $ unpack s
  where
    special : List Char
    special = unpack ";<=>?@[\]^`{|}~"
    escape : Char -> List Char -> List Char
    escape c cs = if c < '+' || isInfixOf [c] special
     then '\\' :: c :: cs 
     else c :: cs

/bin/sh

escapeQuotedSh s = pack $ foldr escape [] $ unpack s
  where
    escape : Char -> List Char -> List Char
    escape '\"' cs = '\\' :: '\"' :: cs
    escape '\\' cs = '\\' :: '\\' :: cs
    escape '\$' cs = '\\' :: '\$' :: cs
    escape '\`' cs = '\\' :: '\`' :: cs
    escape c    cs = c :: cs

C:\Windows\System32\cmd.exe (ref: https://ss64.com/nt/syntax-esc.html)

escapeUnquotedCmd s = pack $ foldr escape [] $ unpack s
  where
    escape : Char -> List Char -> List Char
    escape '^' cs = '^' :: '^' :: cs
    escape '%' cs = '^' :: '%' :: cs
    escape '!' cs = '^' :: '!' :: cs
    escape '*' cs = '^' :: '*' :: cs
    escape '?' cs = '^' :: '?' :: cs
    escape ';' cs = '^' :: ';' :: cs
    escape '&' cs = '^' :: '&' :: cs -- illegal in paths
    escape '|' cs = '^' :: '|' :: cs -- illegal in paths
    escape '<' cs = '^' :: '<' :: cs -- illegal in paths
    escape '>' cs = '^' :: '>' :: cs -- illegal in paths
    escape ' ' cs = '^' :: ' ' :: cs
    escape '\n' cs = '^' :: '\n' :: cs
    escape '\t' cs = '^' :: '\t' :: cs
    escape c cs = c :: cs

For paths, could simply drop the illegal chars.

/usr/local/bin/idris2

escapeString s = pack $ foldr escape [] $ unpack s
  where
    escape : Char -> List Char -> List Char
    escape '\"' cs = '\\' :: '\"' :: cs
    escape '\\' cs = '\\' :: '\\' :: cs
    escape c  cs = c :: cs

Or, for Multi-line / Single-line literals:

escapeString ml s = pack $ foldr escape ml [] $ unpack s
  where
    escape : Bool -> Char -> List Char -> List Char
    escape False '\n' cs = '\\' :: 'n'  :: cs
    escape False '\r' cs = '\\' :: 'r'  :: cs
    escape _     '\"' cs = '\\' :: '\"' :: cs
    escape _     '\\' cs = '\\' :: '\\' :: cs
    escape _     c    cs = c :: cs

Do we actually need escapeString?

[fabianhjr]

Thanks @benhormann will use what you documented to rewrite the escapes and select the more complete ones for Windows Unquoted and POSIX/*NIX Unquoted.

[benhormann]

@fabianhjr
C:\> vim ab^ cd ef results in three files to edit...
C:\> vim "ab cd" ef for two files.

Escaping doesn't work for args, but does for > redirection. Quoting make more sense for file paths anyway.
Even for sh, not many people are going to use a path with $\"`. It'd break the makefiles too.

[benhormann]

@fabianhjr Escaping doesn't work inside quotes. Remove escapeStringWindows.

[fabianhjr]

@fabianhjr Escaping doesn't work inside quotes. Remove escapeStringWindows.

Removed, thanks for the help. osEscape now sends Windows to id and other to escapeUnix (\ and " with \ as escape char)

[fabianhjr]

Hi @edwinb, @gallais, I would appreciate comment on the high level design ( usage of -X flag or any change that might be desired)

[benhormann]

Any chance of -Xcheck-hashes optionally taking a command name? E.g.

• idris2 -Xcheck-hashes --build ...
• idris2 -Xcheck-hashes gsha256sum --build ...

[fabianhjr]

Don't think so but on Linux I would use a symbolic link.

I have no way to validate the windows behaviour other than the CI. :C

On the other hand that would be a great PR/contribution to improve the windows experience.

EDIT: If this gets merged I can help you implement it but I don't feel confident increasing the complexity of this PR and keeping it mergable.

[fabianhjr]

Oh, :o great to have this merged. @benhormann I can open a new PR for the windows certutil option or if you prefer I can help you with that PR. (Both as an explicit option or maybe as a fallback for windows)

[benhormann]

Don't think so but on Linux I would use a symbolic link.

Same for macOS or BSD. Outside of MSYS, you'd find an exe to put on your PATH.

but I don't feel confident increasing the complexity of this PR and keeping it mergable.

Fair call.

---

R.I.P. ⚰️ 67 /196: Building IdrisPaths (src/IdrisPaths.idr) as a progress indicator. Good job 👍