Idris2
Idris2 copied to clipboard
idris-lang
calling `readFile` on a directory hangs
Steps to Reproduce
Make a file like so:
import System.File
main : IO ()
main = do
Right x <- readFile "/tmp" | Left x => printLn $ show x
printLn x
In the repl run :exec main
Expected Behavior
Some sort of error about trying to read a directory as a file.
Observed Behavior
The repl hangs for several minutes, and eventually prints:
Main> :exec main
out of memory
have also seen it print:
Main> :exec main
nonrecoverable invalid memory reference
Running htop looks like whatever it's doing is pretty resource intensive:
PID USER PRI NI VIRT RES S CPU% MEM% TIME+ Command
41031 alex 17 0 47.4G 751M R 59.7 4.6 5:57.79 /usr/local/bin/chez --script /Users/alex/misc/idrall/build/exec/_tmpchez_app/_tmpchez.ss
Idris version is 0.3.0-ec77ad21a
I could not reproduce this on c725b11c891b9f9f1e25ead66d9fc75a91b69836 using the Chez backend on Linux. The test runs with "File error: 21".
Oh interesting! Just tried it again with 299a31de5 on ubuntu 18.04 with Chez 9.5.3 and couldn't reproduce it, also got the "File error: 21".
I tried it on Mac with Chez 9.5.4 and was able to reproduce it, so it could be a Mac thing...
Same result for me on Ubuntu: "File error: 21".
Does using something like System.Directory.Tree's directoryExists to check the
file is not a directory fix the issue on mac?
directoryExists : {root : Path} -> FileName root -> IO Bool
directoryExists fp = do
Right dir <- openDir (show $ toFilePath fp)
| Left _ => pure False
closeDir dir
pure True
Narrowing down the bug a bit:
On macOS:
Main> :exec (readFilePage 0 (limit 5) "/") >>= printLn
Right (False, ["", "", "", "", ""])
On Linux:
Main> :exec (readFilePage 0 (limit 5) "/") >>= printLn
Left File error: 21
AIUI, readFilePage is only supposed to return empty strings at EOF (it normally includes the trailing newline), so returning several empty strings in a row, while not signaling EOF (that's the False), is very suspicious.
It appears as though readFilePage is several levels above platform specific code. This suggests that the bug is an issue with idris2_readLine/idris2_seekLine/idris2_eof which is several layers down the call stack from readFilePage.
