From 9e8e94316d2fb5f4ce6bd7b0d6cb787238679fe1 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Fri, 26 Jul 2024 12:58:45 -0400 Subject: [PATCH 1/7] Adding files to address issue #3232. --- src/Idris/Package.idr | 4 ++- src/Idris/Package/Init.idr | 53 ++++++++++++++++++++++++++++---------- 2 files changed, 43 insertions(+), 14 deletions(-) diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr index 76cf233930..55fe15ad85 100644 --- a/src/Idris/Package.idr +++ b/src/Idris/Package.idr @@ -903,7 +903,9 @@ processPackage : {auto c : Ref Ctxt Defs} -> processPackage opts (cmd, mfile) = withCtxt . withSyn . withROpts $ case cmd of Init => - do pkg <- coreLift interactive + do --pkg <- coreLift interactive + Right pkg <- coreLift interactive + | Left () => coreLift (exitWith (ExitFailure 1)) let fp = fromMaybe (pkg.name ++ ".ipkg") mfile False <- coreLift (exists fp) | _ => throw (GenericMsg emptyFC ("File " ++ fp ++ " already exists")) diff --git a/src/Idris/Package/Init.idr b/src/Idris/Package/Init.idr index 156d856e31..1740583c05 100644 --- a/src/Idris/Package/Init.idr +++ b/src/Idris/Package/Init.idr @@ -12,6 +12,7 @@ import Idris.Package.Types import System.Directory import Control.App.FileIO +import Libraries.Text.Lexer import Libraries.Utils.Path import Libraries.System.Directory.Tree @@ -67,21 +68,26 @@ prompt p = putStr p >> fflush stdout >> getLine export covering -interactive : IO PkgDesc +--interactive : IO PkgDesc +interactive : IO (Either () PkgDesc) interactive = do pname <- prompt "Package name: " - pauthors <- prompt "Package authors: " - poptions <- prompt "Package options: " - psource <- prompt "Source directory: " - let sourcedir = mstring psource - modules <- findModules sourcedir - let pkg : PkgDesc = - { authors := mstring pauthors - , options := (emptyFC,) <$> mstring poptions - , modules := modules - , sourcedir := sourcedir - } (initPkgDesc (fromMaybe "project" (mstring pname))) - pure pkg + -- check to ensure that pname is a valid Idris2 identifier. + case checkPackageName $ fastUnpack pname of + False => do () <- putStrLn "Package name is not a valid Idris Identifier." + pure $ Left () + True => do pauthors <- prompt "Package authors: " + poptions <- prompt "Package options: " + psource <- prompt "Source directory: " + let sourcedir = mstring psource + modules <- findModules sourcedir + let pkg : PkgDesc = + { authors := mstring pauthors + , options := (emptyFC,) <$> mstring poptions + , modules := modules + , sourcedir := sourcedir + } (initPkgDesc (fromMaybe "project" (mstring pname))) + pure $ Right pkg where @@ -89,3 +95,24 @@ interactive = do mstring str = case trim str of "" => Nothing str => Just str + + isIdentStart : Char -> Bool + isIdentStart '_' = True + isIdentStart x = isUpper x || + isAlpha x || + x > chr 160 + + isIdentTrailing : List Char -> Bool + isIdentTrailing [] = True + isIdentTrailing (x::xs) = case isAlphaNum x || + x > chr 160 || + x == '-' || + x == '_' || + x == '\'' of + False => False + True => isIdentTrailing xs + + checkPackageName : List Char -> Bool + checkPackageName [] = False + checkPackageName (x::xs) = isIdentStart x && + isIdentTrailing xs From d98a3c356e5cb287cf423a2e1c8a035a484c36e9 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Fri, 26 Jul 2024 13:02:00 -0400 Subject: [PATCH 2/7] Updating CHANGELOG_NEXT.md. --- CHANGELOG_NEXT.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/CHANGELOG_NEXT.md b/CHANGELOG_NEXT.md index 66f2007fee..f9dd1e26b9 100644 --- a/CHANGELOG_NEXT.md +++ b/CHANGELOG_NEXT.md @@ -16,6 +16,9 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO installed will be ignored by the compiler when it tries to use that library as a dependency for some other package. +* The `idris2 --init` command now ensures that package names are + valid Idris2 identifiers. + ### Building/Packaging changes * The Nix flake's `buildIdris` function now returns a set with `executable` and From be87320ef39cb38ef38877ea313028b07620a228 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Fri, 26 Jul 2024 13:04:56 -0400 Subject: [PATCH 3/7] Removing unnecessary comments. --- src/Idris/Package.idr | 3 +-- src/Idris/Package/Init.idr | 1 - 2 files changed, 1 insertion(+), 3 deletions(-) diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr index 55fe15ad85..19d2276a34 100644 --- a/src/Idris/Package.idr +++ b/src/Idris/Package.idr @@ -903,8 +903,7 @@ processPackage : {auto c : Ref Ctxt Defs} -> processPackage opts (cmd, mfile) = withCtxt . withSyn . withROpts $ case cmd of Init => - do --pkg <- coreLift interactive - Right pkg <- coreLift interactive + do Right pkg <- coreLift interactive | Left () => coreLift (exitWith (ExitFailure 1)) let fp = fromMaybe (pkg.name ++ ".ipkg") mfile False <- coreLift (exists fp) diff --git a/src/Idris/Package/Init.idr b/src/Idris/Package/Init.idr index 1740583c05..5e90652d46 100644 --- a/src/Idris/Package/Init.idr +++ b/src/Idris/Package/Init.idr @@ -68,7 +68,6 @@ prompt p = putStr p >> fflush stdout >> getLine export covering ---interactive : IO PkgDesc interactive : IO (Either () PkgDesc) interactive = do pname <- prompt "Package name: " From 704e80cdce131205c8d2b122ea9743a762b6cfc6 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Fri, 26 Jul 2024 13:11:22 -0400 Subject: [PATCH 4/7] Removing extra whitespace. --- src/Idris/Package/Init.idr | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Idris/Package/Init.idr b/src/Idris/Package/Init.idr index 5e90652d46..b09f0a0102 100644 --- a/src/Idris/Package/Init.idr +++ b/src/Idris/Package/Init.idr @@ -70,7 +70,7 @@ export covering interactive : IO (Either () PkgDesc) interactive = do - pname <- prompt "Package name: " + pname <- prompt "Package name: " -- check to ensure that pname is a valid Idris2 identifier. case checkPackageName $ fastUnpack pname of False => do () <- putStrLn "Package name is not a valid Idris Identifier." From 8e24f12e607056094fda2415e2f233b9dedbcb0d Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Fri, 26 Jul 2024 13:14:28 -0400 Subject: [PATCH 5/7] Removing extra trailing whitespace. --- src/Idris/Package/Init.idr | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Idris/Package/Init.idr b/src/Idris/Package/Init.idr index b09f0a0102..b08a2bea87 100644 --- a/src/Idris/Package/Init.idr +++ b/src/Idris/Package/Init.idr @@ -72,7 +72,7 @@ interactive : IO (Either () PkgDesc) interactive = do pname <- prompt "Package name: " -- check to ensure that pname is a valid Idris2 identifier. - case checkPackageName $ fastUnpack pname of + case checkPackageName $ fastUnpack pname of False => do () <- putStrLn "Package name is not a valid Idris Identifier." pure $ Left () True => do pauthors <- prompt "Package authors: " @@ -94,13 +94,13 @@ interactive = do mstring str = case trim str of "" => Nothing str => Just str - + isIdentStart : Char -> Bool isIdentStart '_' = True isIdentStart x = isUpper x || isAlpha x || x > chr 160 - + isIdentTrailing : List Char -> Bool isIdentTrailing [] = True isIdentTrailing (x::xs) = case isAlphaNum x || From ba560de6c33fc557a2281e2a32d289e0fc851396 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Fri, 26 Jul 2024 14:20:51 -0400 Subject: [PATCH 6/7] Allowing for an empty package name. --- src/Idris/Package/Init.idr | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Idris/Package/Init.idr b/src/Idris/Package/Init.idr index b08a2bea87..1ba1425bec 100644 --- a/src/Idris/Package/Init.idr +++ b/src/Idris/Package/Init.idr @@ -112,6 +112,6 @@ interactive = do True => isIdentTrailing xs checkPackageName : List Char -> Bool - checkPackageName [] = False + checkPackageName [] = True checkPackageName (x::xs) = isIdentStart x && isIdentTrailing xs From 6bda3d5746b336589727a47c018d12fa4a53f319 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Mon, 29 Jul 2024 10:32:13 -0400 Subject: [PATCH 7/7] Fixing code to address comments (inline pattern matching and Either to Maybe). --- src/Idris/Package.idr | 4 ++-- src/Idris/Package/Init.idr | 32 +++++++++++++++----------------- 2 files changed, 17 insertions(+), 19 deletions(-) diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr index 19d2276a34..3862d795f5 100644 --- a/src/Idris/Package.idr +++ b/src/Idris/Package.idr @@ -903,8 +903,8 @@ processPackage : {auto c : Ref Ctxt Defs} -> processPackage opts (cmd, mfile) = withCtxt . withSyn . withROpts $ case cmd of Init => - do Right pkg <- coreLift interactive - | Left () => coreLift (exitWith (ExitFailure 1)) + do Just pkg <- coreLift interactive + | Nothing => coreLift (exitWith (ExitFailure 1)) let fp = fromMaybe (pkg.name ++ ".ipkg") mfile False <- coreLift (exists fp) | _ => throw (GenericMsg emptyFC ("File " ++ fp ++ " already exists")) diff --git a/src/Idris/Package/Init.idr b/src/Idris/Package/Init.idr index 1ba1425bec..f62f92c8e7 100644 --- a/src/Idris/Package/Init.idr +++ b/src/Idris/Package/Init.idr @@ -68,25 +68,23 @@ prompt p = putStr p >> fflush stdout >> getLine export covering -interactive : IO (Either () PkgDesc) +interactive : IO (Maybe PkgDesc) interactive = do pname <- prompt "Package name: " - -- check to ensure that pname is a valid Idris2 identifier. - case checkPackageName $ fastUnpack pname of - False => do () <- putStrLn "Package name is not a valid Idris Identifier." - pure $ Left () - True => do pauthors <- prompt "Package authors: " - poptions <- prompt "Package options: " - psource <- prompt "Source directory: " - let sourcedir = mstring psource - modules <- findModules sourcedir - let pkg : PkgDesc = - { authors := mstring pauthors - , options := (emptyFC,) <$> mstring poptions - , modules := modules - , sourcedir := sourcedir - } (initPkgDesc (fromMaybe "project" (mstring pname))) - pure $ Right pkg + let True = checkPackageName $ fastUnpack pname + | False => pure Nothing + pauthors <- prompt "Package authors: " + poptions <- prompt "Package options: " + psource <- prompt "Source directory: " + let sourcedir = mstring psource + modules <- findModules sourcedir + let pkg : PkgDesc = + { authors := mstring pauthors + , options := (emptyFC,) <$> mstring poptions + , modules := modules + , sourcedir := sourcedir + } (initPkgDesc (fromMaybe "project" (mstring pname))) + pure $ Just pkg where