mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-11-28 14:06:26 +03:00
Detect cycles in imports
This commit is contained in:
parent
412930522e
commit
421b15aa24
@ -85,14 +85,17 @@ mkModTree loc done mod
|
|||||||
Nothing =>
|
Nothing =>
|
||||||
do (file, modInfo) <- readHeader loc mod
|
do (file, modInfo) <- readHeader loc mod
|
||||||
let imps = map path (imports modInfo)
|
let imps = map path (imports modInfo)
|
||||||
ms <- traverse (mkModTree loc done) imps
|
ms <- traverse (mkModTree loc (mod :: done)) imps
|
||||||
let mt = MkModTree mod (Just file) ms
|
let mt = MkModTree mod (Just file) ms
|
||||||
all <- get AllMods
|
all <- get AllMods
|
||||||
put AllMods ((mod, mt) :: all)
|
put AllMods ((mod, mt) :: all)
|
||||||
pure mt
|
pure mt
|
||||||
Just m => pure m)
|
Just m => pure m)
|
||||||
-- Couldn't find source, assume it's in a package directory
|
-- Couldn't find source, assume it's in a package directory
|
||||||
(\err => pure (MkModTree mod Nothing []))
|
(\err =>
|
||||||
|
case err of
|
||||||
|
CyclicImports _ => throw err
|
||||||
|
_ => pure (MkModTree mod Nothing []))
|
||||||
|
|
||||||
-- Given a module tree, returns the modules in the reverse order they need to
|
-- Given a module tree, returns the modules in the reverse order they need to
|
||||||
-- be built, including their dependencies
|
-- be built, including their dependencies
|
||||||
@ -112,7 +115,6 @@ mkBuildMods acc mod
|
|||||||
|
|
||||||
-- Given a main file name, return the list of modules that need to be
|
-- Given a main file name, return the list of modules that need to be
|
||||||
-- built for that main file, in the order they need to be built
|
-- built for that main file, in the order they need to be built
|
||||||
export
|
|
||||||
getBuildMods : {auto c : Ref Ctxt Defs} ->
|
getBuildMods : {auto c : Ref Ctxt Defs} ->
|
||||||
{auto o : Ref ROpts REPLOpts} ->
|
{auto o : Ref ROpts REPLOpts} ->
|
||||||
FC -> (mainFile : String) ->
|
FC -> (mainFile : String) ->
|
||||||
|
@ -32,7 +32,7 @@ idrisTests
|
|||||||
"coverage001", "coverage002", "coverage003", "coverage004",
|
"coverage001", "coverage002", "coverage003", "coverage004",
|
||||||
"error001", "error002", "error003", "error004", "error005",
|
"error001", "error002", "error003", "error004", "error005",
|
||||||
"error006", "error007", "error008", "error009", "error010",
|
"error006", "error007", "error008", "error009", "error010",
|
||||||
"import001", "import002", "import003",
|
"import001", "import002", "import003", "import004",
|
||||||
"interactive001", "interactive002", "interactive003", "interactive004",
|
"interactive001", "interactive002", "interactive003", "interactive004",
|
||||||
"interactive005", "interactive006", "interactive007", "interactive008",
|
"interactive005", "interactive006", "interactive007", "interactive008",
|
||||||
"interactive009", "interactive010", "interactive011", "interactive012",
|
"interactive009", "interactive010", "interactive011", "interactive012",
|
||||||
|
3
tests/idris2/import004/Cycle1.idr
Normal file
3
tests/idris2/import004/Cycle1.idr
Normal file
@ -0,0 +1,3 @@
|
|||||||
|
module Cycle1
|
||||||
|
|
||||||
|
import Cycle2
|
3
tests/idris2/import004/Cycle2.idr
Normal file
3
tests/idris2/import004/Cycle2.idr
Normal file
@ -0,0 +1,3 @@
|
|||||||
|
module Cycle2
|
||||||
|
|
||||||
|
import Cycle1
|
3
tests/idris2/import004/Loop.idr
Normal file
3
tests/idris2/import004/Loop.idr
Normal file
@ -0,0 +1,3 @@
|
|||||||
|
module Loop
|
||||||
|
|
||||||
|
import Loop
|
2
tests/idris2/import004/expected
Normal file
2
tests/idris2/import004/expected
Normal file
@ -0,0 +1,2 @@
|
|||||||
|
Uncaught error: Module imports form a cycle: Cycle2 -> Cycle1 -> Cycle1
|
||||||
|
Uncaught error: Module imports form a cycle: Loop -> Loop
|
4
tests/idris2/import004/run
Executable file
4
tests/idris2/import004/run
Executable file
@ -0,0 +1,4 @@
|
|||||||
|
$1 Cycle1.idr
|
||||||
|
$1 Loop.idr
|
||||||
|
|
||||||
|
rm -rf build
|
Loading…
Reference in New Issue
Block a user