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

[ error ] Improve error messages when reading ipkg files #3141

Merged
merged 1 commit into from
Nov 12, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
90 changes: 55 additions & 35 deletions src/Idris/Package.idr
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,7 @@ import Libraries.Text.PrettyPrint.Prettyprinter.Render.String
import Idris.CommandLine
import Idris.Doc.HTML
import Idris.Doc.String
import Idris.Error
import Idris.ModTree
import Idris.Pretty
import Idris.ProcessIdr
Expand Down Expand Up @@ -104,43 +105,52 @@ field fname
<|> strField PPostclean "postclean"
<|> do start <- location
ignore $ exactProperty "version"
equals
vs <- sepBy1 dot' integerLit
end <- location
pure (PVersion (MkFC (PhysicalPkgSrc fname) start end)
(MkPkgVersion (fromInteger <$> vs)))
mustWork $ do
equals
vs <- choose stringLit (sepBy1 dot' integerLit)
end <- location
the (EmptyRule _) $ case vs of
Left v => pure (PVersionDep (MkFC (PhysicalPkgSrc fname) start end) v)
Right vs => pure (PVersion (MkFC (PhysicalPkgSrc fname) start end)
(MkPkgVersion (fromInteger <$> vs)))
<|> do start <- location
ignore $ exactProperty "langversion"
lvs <- langversions
end <- location
pure (PLangVersions (MkFC (PhysicalPkgSrc fname) start end) lvs)
mustWork $ do
lvs <- langversions
end <- location
pure (PLangVersions (MkFC (PhysicalPkgSrc fname) start end) lvs)
<|> do start <- location
ignore $ exactProperty "version"
equals
v <- stringLit
end <- location
pure (PVersionDep (MkFC (PhysicalPkgSrc fname) start end) v)
mustWork $ do
equals
v <- stringLit
end <- location
pure (PVersionDep (MkFC (PhysicalPkgSrc fname) start end) v)
<|> do ignore $ exactProperty "depends"
equals
ds <- sep depends
pure (PDepends ds)
mustWork $ do
equals
ds <- sep depends
pure (PDepends ds)
<|> do ignore $ exactProperty "modules"
equals
ms <- sep (do start <- location
m <- moduleIdent
end <- location
pure (MkFC (PhysicalPkgSrc fname) start end, m))
pure (PModules ms)
mustWork $ do
equals
ms <- sep (do start <- location
m <- moduleIdent
end <- location
pure (MkFC (PhysicalPkgSrc fname) start end, m))
pure (PModules ms)
<|> do ignore $ exactProperty "main"
equals
start <- location
m <- moduleIdent
end <- location
pure (PMainMod (MkFC (PhysicalPkgSrc fname) start end) m)
mustWork $ do
equals
start <- location
m <- moduleIdent
end <- location
pure (PMainMod (MkFC (PhysicalPkgSrc fname) start end) m)
<|> do ignore $ exactProperty "executable"
equals
e <- (stringLit <|> packageName)
pure (PExec e)
mustWork $ do
equals
e <- (stringLit <|> packageName)
pure (PExec e)
where
data Bound = LT PkgVersion Bool | GT PkgVersion Bool

Expand Down Expand Up @@ -191,16 +201,20 @@ field fname
strField fieldConstructor fieldName
= do start <- location
ignore $ exactProperty fieldName
equals
str <- stringLit
end <- location
pure $ fieldConstructor (MkFC (PhysicalPkgSrc fname) start end) str
mustWork $ do
equals
str <- stringLit
end <- location
pure $ fieldConstructor (MkFC (PhysicalPkgSrc fname) start end) str

parsePkgDesc : String -> Rule (String, List DescField)
parsePkgDesc fname
= do ignore $ exactProperty "package"
name <- packageName
fields <- many (field fname)
EndOfInput <- peek
| DotSepIdent _ name => fail "Unrecognised property \{show name}"
| tok => fail "Expected end of file"
pure (name, fields)

data ParsedMods : Type where
Expand Down Expand Up @@ -284,8 +298,14 @@ parsePkgFile : {auto c : Ref Ctxt Defs} ->
(setSrc : Bool) -> -- parse package file as a dependency
String -> Core PkgDesc
parsePkgFile setSrc file = do
Right (pname, fs) <- coreLift $ parseFile file $ parsePkgDesc file <* eoi
| Left err => throw err
Right (pname, fs) <- coreLift $ parseFile file $ parsePkgDesc file
| Left err => do
Right res <- coreLift (readFile file)
| _ => throw err
setCurrentElabSource res
doc <- perror err
msg <- render doc
throw (UserError msg)
addFields setSrc fs (initPkgDesc pname)

--------------------------------------------------------------------------------
Expand Down
2 changes: 2 additions & 0 deletions tests/idris2/pkg/pkg018/bad.ipkg
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
package bad
depend = contrib
2 changes: 2 additions & 0 deletions tests/idris2/pkg/pkg018/bad2.ipkg
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
package bad
sourcedir = src
14 changes: 14 additions & 0 deletions tests/idris2/pkg/pkg018/expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
Uncaught error: Error: Unrecognised property "depend".

"bad.ipkg":2:1--2:7
1 | package bad
2 | depend = contrib
^^^^^^

Uncaught error: Error: Expected string.

"bad2.ipkg":2:13--2:16
1 | package bad
2 | sourcedir = src
^^^

4 changes: 4 additions & 0 deletions tests/idris2/pkg/pkg018/run
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
. ../../../testutils.sh

idris2 --build bad.ipkg
idris2 --build bad2.ipkg