From 88a5328ec1ac2a40b65dff9d5eca11a2bc3c938a Mon Sep 17 00:00:00 2001 From: Mathew Polzin Date: Tue, 11 Jun 2024 05:32:22 -0500 Subject: [PATCH] Add an option that dumps package details to JSON (#3293) * Initial stab at package json dump * expose ipkg json dump as new option * make dependency output easier to ingest by another tool * Add a test for ipkg json dump * cleanup * maybe just don't collide with existing equally good fixity * make new operator private * Add new module to api ipkg file * Add note to CHANGELOG_NEXT * correct the docs for the dump-ipkg-json command --- CHANGELOG_NEXT.md | 3 + idris2api.ipkg | 1 + src/Idris/CommandLine.idr | 5 + src/Idris/Package.idr | 2 + src/Idris/Package/ToJson.idr | 116 ++++++++++++++++++ src/Idris/SetOptions.idr | 13 +- tests/idris2/pkg/pkg019/expected | 1 + tests/idris2/pkg/pkg019/run | 4 + tests/idris2/pkg/pkg019/src/And/A/Proof.idr | 8 ++ tests/idris2/pkg/pkg019/src/Main.idr | 4 + .../pkg/pkg019/src/Yet/Another/Path.idr | 7 ++ tests/idris2/pkg/pkg019/test.ipkg | 49 ++++++++ 12 files changed, 207 insertions(+), 6 deletions(-) create mode 100644 src/Idris/Package/ToJson.idr create mode 100644 tests/idris2/pkg/pkg019/expected create mode 100755 tests/idris2/pkg/pkg019/run create mode 100644 tests/idris2/pkg/pkg019/src/And/A/Proof.idr create mode 100644 tests/idris2/pkg/pkg019/src/Main.idr create mode 100644 tests/idris2/pkg/pkg019/src/Yet/Another/Path.idr create mode 100644 tests/idris2/pkg/pkg019/test.ipkg diff --git a/CHANGELOG_NEXT.md b/CHANGELOG_NEXT.md index 0490797aab..c9ce9f200a 100644 --- a/CHANGELOG_NEXT.md +++ b/CHANGELOG_NEXT.md @@ -24,6 +24,9 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO * The Nix flake now exposes the Idris2 API package as `idris2Api` and Idris2's C support library as `support`. +* A new `idris2 --dump-ipkg-json` option (requires either `--find-ipkg` or + specifying the `.ipkg` file) dumps JSON information about an Idris package. + ### Language changes * Autobind and Typebind modifier on operators allow the user to diff --git a/idris2api.ipkg b/idris2api.ipkg index f924514f51..ebb5e7c677 100644 --- a/idris2api.ipkg +++ b/idris2api.ipkg @@ -128,6 +128,7 @@ modules = Idris.Package, Idris.Package.Init, + Idris.Package.ToJson, Idris.Package.Types, Idris.Parser, diff --git a/src/Idris/CommandLine.idr b/src/Idris/CommandLine.idr index dce644c3e3..78cb870969 100644 --- a/src/Idris/CommandLine.idr +++ b/src/Idris/CommandLine.idr @@ -24,6 +24,7 @@ data PkgCommand | Clean | REPL | Init + | DumpJson export Show PkgCommand where @@ -35,6 +36,7 @@ Show PkgCommand where show Clean = "--clean" show REPL = "--repl" show Init = "--init" + show DumpJson = "--dump-ipkg-json" public export data DirCommand @@ -279,6 +281,9 @@ options = [MkOpt ["--check", "-c"] [] [CheckOnly] MkOpt ["--init"] [Optional "package file"] (\ f => [Package Init f]) (Just "Interactively initialise a new project"), + MkOpt ["--dump-ipkg-json"] [Optional "package file"] + (\ f => [Package DumpJson f]) + (Just "Dump an Idris2 package file in the JSON format"), MkOpt ["--build"] [Optional "package file"] (\f => [Package Build f]) (Just "Build modules/executable for the given package"), diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr index a447e0961c..63cb55b65a 100644 --- a/src/Idris/Package.idr +++ b/src/Idris/Package.idr @@ -47,6 +47,7 @@ import Idris.Version import public Idris.Package.Types import Idris.Package.Init +import Idris.Package.ToJson %default covering @@ -943,6 +944,7 @@ processPackage opts (cmd, mfile) | errs => coreLift (exitWith (ExitFailure 1)) runRepl (map snd $ mainmod pkg) Init => pure () -- already handled earlier + DumpJson => coreLift . putStrLn $ toJson pkg record PackageOpts where constructor MkPFR diff --git a/src/Idris/Package/ToJson.idr b/src/Idris/Package/ToJson.idr new file mode 100644 index 0000000000..6be2bc2168 --- /dev/null +++ b/src/Idris/Package/ToJson.idr @@ -0,0 +1,116 @@ +module Idris.Package.ToJson + +import Idris.Package.Types +import Libraries.Data.String.Extra +import Data.List +import Core.FC +import Core.Name.Namespace +import Data.Maybe + +%default total + +-- We don't bother with a robust JSON implementation +-- for this one-off JSON serialization. + +private infixl 0 ~~= + +interface ToJson v where + toJson : v -> String + +ToJson String where + toJson str = "\"\{str}\"" + +ToJson Bool where + toJson False = "false" + toJson True = "true" + +ToJson a => ToJson (List a) where + toJson xs = "[\{join "," $ map toJson xs}]" + +(~=) : ToJson v => String -> v -> String +(~=) field value = "\{toJson field}: \{toJson value}" + +(~~=) : ToJson v => String -> Maybe v -> Maybe String +(~~=) field = map (field ~=) + +ToJson PkgVersion where + toJson v = "\"\{show v}\"" + +ToJson PkgVersionBounds where + toJson (MkPkgVersionBounds lowerBound lowerInclusive upperBound upperInclusive) = + let fields = + [ "lowerInclusive" ~= lowerInclusive + , "lowerBound" ~= maybe "*" show lowerBound + , "upperInclusive" ~= upperInclusive + , "upperBound" ~= maybe "*" show upperBound + ] + in + "{\{join "," fields}}" + +ToJson Depends where + toJson (MkDepends pkgname pkgbounds) = "{\{pkgname ~= pkgbounds}}" + +ToJson ModuleIdent where + toJson ident = "\"\{show ident}\"" + +namespace Package + export + toJson : PkgDesc -> String + toJson (MkPkgDesc + name + version + langversion + authors + maintainers + license + brief + readme + homepage + sourceloc + bugtracker + depends + modules + mainmod + executable + options + sourcedir + builddir + outputdir + prebuild + postbuild + preinstall + postinstall + preclean + postclean) = + let optionalFields = catMaybes $ + [ "version" ~~= version + , "langversion" ~~= langversion + , "authors" ~~= authors + , "maintainers" ~~= maintainers + , "license" ~~= license + , "brief" ~~= brief + , "readme" ~~= readme + , "homepage" ~~= homepage + , "sourceloc" ~~= sourceloc + , "bugtracker" ~~= bugtracker + , "main" ~~= fst <$> mainmod + , "executable" ~~= executable + , "opts" ~~= snd <$> options + , "sourcedir" ~~= sourcedir + , "builddir" ~~= builddir + , "outputdir" ~~= outputdir + , "prebuild" ~~= snd <$> prebuild + , "postbuild" ~~= snd <$> postbuild + , "preinstall" ~~= snd <$> preinstall + , "postinstall" ~~= snd <$> postinstall + , "preclean" ~~= snd <$> preclean + , "postclean" ~~= snd <$> postclean + ] + fields = + [ "name" ~= name + , "depends" ~= depends + , "modules" ~= fst <$> modules + ] ++ optionalFields + in + "{\{join "," fields}}" + diff --git a/src/Idris/SetOptions.idr b/src/Idris/SetOptions.idr index b887e1642c..2378743b45 100644 --- a/src/Idris/SetOptions.idr +++ b/src/Idris/SetOptions.idr @@ -232,12 +232,13 @@ opts "--" "--build-dir" = pure [] opts "--" "--output-dir" = pure [] -- with package files -opts x "--build" = prefixOnlyIfNonEmpty x <$> findIpkg -opts x "--install" = prefixOnlyIfNonEmpty x <$> findIpkg -opts x "--mkdoc" = prefixOnlyIfNonEmpty x <$> findIpkg -opts x "--typecheck" = prefixOnlyIfNonEmpty x <$> findIpkg -opts x "--clean" = prefixOnlyIfNonEmpty x <$> findIpkg -opts x "--repl" = prefixOnlyIfNonEmpty x <$> findIpkg +opts x "--build" = prefixOnlyIfNonEmpty x <$> findIpkg +opts x "--dump-ipkg-json" = prefixOnlyIfNonEmpty x <$> findIpkg +opts x "--install" = prefixOnlyIfNonEmpty x <$> findIpkg +opts x "--mkdoc" = prefixOnlyIfNonEmpty x <$> findIpkg +opts x "--typecheck" = prefixOnlyIfNonEmpty x <$> findIpkg +opts x "--clean" = prefixOnlyIfNonEmpty x <$> findIpkg +opts x "--repl" = prefixOnlyIfNonEmpty x <$> findIpkg -- options opts x _ = pure $ if (x `elem` optionFlags) diff --git a/tests/idris2/pkg/pkg019/expected b/tests/idris2/pkg/pkg019/expected new file mode 100644 index 0000000000..71aa7c0efd --- /dev/null +++ b/tests/idris2/pkg/pkg019/expected @@ -0,0 +1 @@ +{"name": "test","depends": [{"contrib": {"lowerInclusive": true,"lowerBound": "*","upperInclusive": true,"upperBound": "*"}},{"idris2": {"lowerInclusive": true,"lowerBound": "0.7.0","upperInclusive": true,"upperBound": "*"}}],"modules": ["And.A.Proof","Yet.Another.Path"],"version": "0.1.0","langversion": {"lowerInclusive": true,"lowerBound": "0.7.0","upperInclusive": true,"upperBound": "*"},"authors": "Average Joe","maintainers": "Average Joe","license": "MIT","brief": "A basic test","readme": "https://github.com/idris-lang/Idris2/README.md","homepage": "https://github.com/idris-lang/Idris2","sourceloc": "https://github.com/idris-lang/Idris2","bugtracker": "https://github.com/idris-lang/Idris2/issues","main": "Main","executable": "test-exec","opts": "--codegen node","sourcedir": "src","builddir": "build","outputdir": "out","prebuild": "make pre","postbuild": "make post","preinstall": "make pre-install","postinstall": "make post-install","preclean": "make pre-clean","postclean": "make post-clean"} diff --git a/tests/idris2/pkg/pkg019/run b/tests/idris2/pkg/pkg019/run new file mode 100755 index 0000000000..0c2bed7773 --- /dev/null +++ b/tests/idris2/pkg/pkg019/run @@ -0,0 +1,4 @@ +. ../../../testutils.sh + +idris2 --dump-ipkg-json test.ipkg + diff --git a/tests/idris2/pkg/pkg019/src/And/A/Proof.idr b/tests/idris2/pkg/pkg019/src/And/A/Proof.idr new file mode 100644 index 0000000000..744af6dc4d --- /dev/null +++ b/tests/idris2/pkg/pkg019/src/And/A/Proof.idr @@ -0,0 +1,8 @@ +module And.A.Proof + +import Yet.Another.Path as Val + +%default total + +equality : Val.val === 2+3 +equality = Refl diff --git a/tests/idris2/pkg/pkg019/src/Main.idr b/tests/idris2/pkg/pkg019/src/Main.idr new file mode 100644 index 0000000000..09b50ac49b --- /dev/null +++ b/tests/idris2/pkg/pkg019/src/Main.idr @@ -0,0 +1,4 @@ +module Main + +main : IO () +main = pure () diff --git a/tests/idris2/pkg/pkg019/src/Yet/Another/Path.idr b/tests/idris2/pkg/pkg019/src/Yet/Another/Path.idr new file mode 100644 index 0000000000..9973d76be2 --- /dev/null +++ b/tests/idris2/pkg/pkg019/src/Yet/Another/Path.idr @@ -0,0 +1,7 @@ +module Yet.Another.Path + +%default total + +public export +val : Nat +val = 5 diff --git a/tests/idris2/pkg/pkg019/test.ipkg b/tests/idris2/pkg/pkg019/test.ipkg new file mode 100644 index 0000000000..7ac761576b --- /dev/null +++ b/tests/idris2/pkg/pkg019/test.ipkg @@ -0,0 +1,49 @@ +package test +version = 0.1.0 +authors = "Average Joe" +maintainers = "Average Joe" +license = "MIT" +brief = "A basic test" +readme = "https://github.com/idris-lang/Idris2/README.md" +homepage = "https://github.com/idris-lang/Idris2" +sourceloc = "https://github.com/idris-lang/Idris2" +bugtracker = "https://github.com/idris-lang/Idris2/issues" + +-- the Idris2 version required (e.g. langversion >= 0.5.1) +langversion >= 0.7.0 + +-- packages to add to search path +depends = contrib, + idris2 >= 0.7.0 + +-- modules to install +modules = And.A.Proof, + Yet.Another.Path + +-- main file (i.e. file to load at REPL) +main = Main + +-- name of executable +executable = test-exec +opts = "--codegen node" +sourcedir = "src" +builddir = "build" +outputdir = "out" + +-- script to run before building +prebuild = "make pre" + +-- script to run after building +postbuild = "make post" + +-- script to run after building, before installing +preinstall = "make pre-install" + +-- script to run after installing +postinstall = "make post-install" + +-- script to run before cleaning +preclean = "make pre-clean" + +-- script to run after cleaning +postclean = "make post-clean"