---> Building idris-ct
Executing: cd "/opt/local/var/macports/build/_opt_svacchanda_SonomaPorts_math_idris-ct/idris-ct/work/idris-ct-fbc7f633e0d86bfe5b56a2c4b9db6f780d59106d" && /usr/bin/make -j4 -w compare CC="/opt/local/var/macports/build/_opt_svacchanda_SonomaPorts_math_idris-ct/idris-ct/work/compwrap/cc/usr/bin/clang" CXX="/opt/local/var/macports/build/_opt_svacchanda_SonomaPorts_math_idris-ct/idris-ct/work/compwrap/cxx/usr/bin/clang++" OBJC="/opt/local/var/macports/build/_opt_svacchanda_SonomaPorts_math_idris-ct/idris-ct/work/compwrap/objc/usr/bin/clang" OBJCXX="/opt/local/var/macports/build/_opt_svacchanda_SonomaPorts_math_idris-ct/idris-ct/work/compwrap/objcxx/usr/bin/clang++" INSTALL="/usr/bin/install -c"
make: Entering directory `/opt/local/var/macports/build/_opt_svacchanda_SonomaPorts_math_idris-ct/idris-ct/work/idris-ct-fbc7f633e0d86bfe5b56a2c4b9db6f780d59106d'
idris2 fileDiff/FileDiff.idr -o compare
Error: While processing right hand side of pathFromVect. When unifying:
List ?elem
and:
Vect ?len ?elem
Mismatch between: List ?elem and Vect ?len ?elem.
fileDiff.FileDiff:8:56--8:65
4 |
5 | data FileSystem = DirTree String (List FileSystem) | FileTree String
6 |
7 | pathFromVect : Vect n String -> String
8 | pathFromVect xs = concat $ intersperse "/" $ reverse $ toList xs
^^^^^^^^^
Error: While processing right hand side of linearize. Sorry, I can't find any elaboration which works. All errors:
If Data.Vect.reverse: When unifying:
List String
and:
Vect ?len ?elem
Mismatch between: List String and Vect ?len ?elem.
fileDiff.FileDiff:11:76--11:81
07 | pathFromVect : Vect n String -> String
08 | pathFromVect xs = concat $ intersperse "/" $ reverse $ toList xs
09 |
10 | linearize : (depth : List String) -> FileSystem -> List String
11 | linearize depth (DirTree n []) = [concat $ reverse $ intersperse "/" (n :: depth)]
^^^^^
If Prelude.List.reverse: When unifying:
Vect (?len + pred ?len) ?elem
and:
List ?a
Mismatch between: Vect (?len + pred ?len) ?elem and List ?a.
fileDiff.FileDiff:11:54--11:82
07 | pathFromVect : Vect n String -> String
08 | pathFromVect xs = concat $ intersperse "/" $ reverse $ toList xs
09 |
10 | linearize : (depth : List String) -> FileSystem -> List String
11 | linearize depth (DirTree n []) = [concat $ reverse $ intersperse "/" (n :: depth)]
^^^^^^^^^^^^^^^^^^^^^^^^^^^^
If Prelude.SnocList.reverse: When unifying:
Vect (?len + pred ?len) ?elem
and:
SnocList ?a
Mismatch between: Vect (?len + pred ?len) ?elem and SnocList ?a.
fileDiff.FileDiff:11:54--11:82
07 | pathFromVect : Vect n String -> String
08 | pathFromVect xs = concat $ intersperse "/" $ reverse $ toList xs
09 |
10 | linearize : (depth : List String) -> FileSystem -> List String
11 | linearize depth (DirTree n []) = [concat $ reverse $ intersperse "/" (n :: depth)]
^^^^^^^^^^^^^^^^^^^^^^^^^^^^
If Prelude.reverse: When unifying:
Vect (?len + pred ?len) ?elem
and:
String
Mismatch between: Vect (?len + pred ?len) ?elem and String.
fileDiff.FileDiff:11:54--11:82
07 | pathFromVect : Vect n String -> String
08 | pathFromVect xs = concat $ intersperse "/" $ reverse $ toList xs
09 |
10 | linearize : (depth : List String) -> FileSystem -> List String
11 | linearize depth (DirTree n []) = [concat $ reverse $ intersperse "/" (n :: depth)]
^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: While processing right hand side of show. When unifying:
List String
and:
Vect ?len ?elem
Mismatch between: List String and Vect ?len ?elem.
fileDiff.FileDiff:16:41--16:56
12 | linearize depth (DirTree n files) = concatMap (linearize (n :: depth)) files
13 | linearize depth (FileTree n) = [concat $ reverse $ intersperse "/" (n :: depth)]
14 |
15 | Show FileSystem where
16 | show fs = concat $ intersperse "\n" $ linearize [] fs
^^^^^^^^^^^^^^^
Error: While processing type of lsAcc. Undefined name Directory.
fileDiff.FileDiff:19:9--19:18
15 | Show FileSystem where
16 | show fs = concat $ intersperse "\n" $ linearize [] fs
17 |
18 | ||| Ls with accumulator, uses `dirEntry` to get to the next entry
19 | lsAcc : Directory -> Maybe (List String) -> IO (Either FileError (List String))
^^^^^^^^^
Error: While processing right hand side of lsAcc. While processing right hand side of lsAcc,notDot. Undefined name strHead.
fileDiff.FileDiff:30:18--30:25
26 | where
27 | ||| Don't pay attention to files starting with a dot
28 | notDot : String -> Bool
29 | notDot "" = True
30 | notDot str = strHead str /= '.'
^^^^^^^
Error: While processing type of ls. Undefined name FileError.
fileDiff.FileDiff:33:27--33:36
29 | notDot "" = True
30 | notDot str = strHead str /= '.'
31 |
32 | ||| List all files in a directory
33 | ls : String -> IO (Either FileError (List String))
^^^^^^^^^
Error: While processing right hand side of ls. Undefined name dirOpen.
fileDiff.FileDiff:34:25--34:32
30 | notDot str = strHead str /= '.'
31 |
32 | ||| List all files in a directory
33 | ls : String -> IO (Either FileError (List String))
34 | ls name = do Right d <- dirOpen name | Left err => pure (Left err)
^^^^^^^
Error: While processing type of lsRec. Undefined name FileError.
fileDiff.FileDiff:54:41--54:50
50 | (a -> m (n d)) -> l a -> m (n (l d))
51 | doubleTraverse f x = traverse id <$> traverse f x
52 |
53 | ||| Construct a tree of all files in a directory structure
54 | lsRec : Vect (S n) String -> IO (Either FileError FileSystem)
^^^^^^^^^
Error: No type declaration for Main.lsRec.
fileDiff.FileDiff:55:1--68:16
55 | lsRec path@(directory :: ds) = do
56 | Right files <- ls (pathFromVect path) | Left err => pure (Left err)
57 | (dirs, files) <- partitionM (isDir path) files
58 | Right subTree <- doubleTraverse (\d => lsRec (d :: path)) dirs
59 | | Left err => pure (Left err)
60 | pure $ Right (DirTree directory (subTree ++ map FileTree files))
Error: While processing right hand side of fixFormat. Undefined name takeWhile.
fileDiff.FileDiff:74:26--74:35
70 | ||| We don't care about the begining of the file path nor the file extension
71 | ||| The begining is the root folder, which will always be different
72 | ||| The filepath is `lidr` for idris1 and `idr` for Idris2 so it's not helpful
73 | fixFormat : Nat -> String -> String
74 | fixFormat n str = pack $ takeWhile (/= '.') $ drop n $ unpack str
^^^^^^^^^
Error: While processing right hand side of main. Undefined name getArgs.
fileDiff.FileDiff:80:36--80:43
76 | missing : Eq a => List a -> List a -> List a
77 | missing xs ys = filter (not . flip elem ys) xs
78 |
79 | main : IO ()
80 | main = do [_, folder1, folder2] <- getArgs
^^^^^^^
Warning: compiling hole Main.main
make: *** [compare] Error 1
barracuda156
commented
5 months ago