mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-09-22 06:29:37 +03:00
Merge pull request #2674 from jfdm/fix-ipkg-parsing-mistake
Fixed parsing error in ipkg files
This commit is contained in:
commit
8e8fd659a0
@ -140,7 +140,7 @@ Extra-source-files:
|
||||
libs/effects/Makefile
|
||||
libs/effects/effects.ipkg
|
||||
libs/effects/Effect/*.idr
|
||||
libs/effects/Effect/Logging/*.idr
|
||||
libs/effects/Effect/Logging/*.idr
|
||||
libs/effects/*.idr
|
||||
|
||||
libs/pruviloj/Makefile
|
||||
@ -567,6 +567,11 @@ Extra-source-files:
|
||||
test/primitives003/*.idr
|
||||
test/primitives003/expected
|
||||
|
||||
test/pkg001/run
|
||||
test/pkg001/test.ipkg
|
||||
test/pkg001/*.idr
|
||||
test/pkg001/expected
|
||||
|
||||
test/proof001/run
|
||||
test/proof001/*.idr
|
||||
test/proof001/expected
|
||||
@ -598,7 +603,7 @@ Extra-source-files:
|
||||
test/proof010/run
|
||||
test/proof010/*.idr
|
||||
test/proof010/expected
|
||||
|
||||
|
||||
test/proofsearch001/run
|
||||
test/proofsearch001/*.idr
|
||||
test/proofsearch001/expected
|
||||
|
@ -79,12 +79,12 @@ pClause = do reserved "executable"; lchar '=';
|
||||
opts <- stringLiteral
|
||||
st <- get
|
||||
let args = pureArgParser (words opts)
|
||||
put (st { idris_opts = args })
|
||||
put (st { idris_opts = args ++ idris_opts st })
|
||||
<|> do reserved "pkgs"; lchar '=';
|
||||
ps <- sepBy1 (fst <$> identifier) (lchar ',')
|
||||
st <- get
|
||||
let pkgs = pureArgParser $ map (\x -> unwords ["-p", x]) ps
|
||||
put (st {idris_opts = idris_opts st ++ pkgs})
|
||||
let pkgs = pureArgParser $ concatMap (\x -> ["-p", x]) ps
|
||||
put (st {idris_opts = pkgs ++ idris_opts st})
|
||||
<|> do reserved "modules"; lchar '=';
|
||||
ms <- sepBy1 (fst <$> iName []) (lchar ',')
|
||||
st <- get
|
||||
|
8
test/pkg001/Main.idr
Normal file
8
test/pkg001/Main.idr
Normal file
@ -0,0 +1,8 @@
|
||||
module Main
|
||||
|
||||
import Effects
|
||||
import Effect.State
|
||||
|
||||
|
||||
main : IO ()
|
||||
main = putStrLn "CouCou!"
|
1
test/pkg001/expected
Normal file
1
test/pkg001/expected
Normal file
@ -0,0 +1 @@
|
||||
Type checking ./Main.idr
|
3
test/pkg001/run
Executable file
3
test/pkg001/run
Executable file
@ -0,0 +1,3 @@
|
||||
#!/usr/bin/env bash
|
||||
idris $@ --build test.ipkg
|
||||
rm -f *.ibc
|
7
test/pkg001/test.ipkg
Normal file
7
test/pkg001/test.ipkg
Normal file
@ -0,0 +1,7 @@
|
||||
package test
|
||||
|
||||
pkgs = effects
|
||||
|
||||
opts = "--warnpartial --warnreach"
|
||||
|
||||
modules = Main
|
Loading…
Reference in New Issue
Block a user