Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Errors when building compare target #86

Open
barracuda156 opened this issue Jun 24, 2024 · 0 comments
Open

Errors when building compare target #86

barracuda156 opened this issue Jun 24, 2024 · 0 comments

Comments

@barracuda156
Copy link

--->  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 barracuda156 changed the title Erros when building compare target Errors when building compare target Jun 24, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant