Skip to content

Commit

Permalink
[ error ] Improve parse errors in ipkg files
Browse files Browse the repository at this point in the history
  • Loading branch information
dunhamsteve authored and gallais committed Nov 12, 2023
1 parent 1aff26e commit af10fba
Show file tree
Hide file tree
Showing 5 changed files with 77 additions and 35 deletions.
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

0 comments on commit af10fba

Please sign in to comment.