eayus / sirdi Goto Github PK
View Code? Open in Web Editor NEWPackage manager for Idris
License: GNU General Public License v3.0
Package manager for Idris
License: GNU General Public License v3.0
I was playing around with sirdi for an existing project today, and noticed that my .ipkg
file (which I was using for interactive editing purposes) was gone. I managed to recover it through git
, but it seems sirdi clean
removes "*.ipkg"
and not just the .ipkg
file that it generates itself. It would be nice if sirdi only deleted files it itself had created : )
What would it take for sirdi to package itself?
If we have a clear list of tasks to complete or decisions to make, maybe we can spread the effort among available time.
One of these is:
.ipkg
file, but no sirdi
configuration file?A --[ depends on]---> B --[dep on] --> C, D, E
.A
, while B
,C
, and D
are outside our control (but fine to assume, say, they're on github).C
, D
, and E
, it might be impossible for them to introduce a sirdi configuration file into B
for whatever reasons.Users should be able to give their git dependencies an optional commit hash.
I have a good idea of how this should be implemented so I'll take this issue. I should have a solution by the end of tomorrow.
Currently we use a very primitive method of parsing command line arguments. There is no way for the user to find out what commands are available or their correct usage. Error messages on invalid arguments are very poor.
We could do with a more robust approach. Originally I used the collie
library, however after adding many subcommands, compile times became way too long (I could no longer compile the program on my machine without running out of RAM).
Currently we are using JSON for config files. However I don't think this is ideal as it is not the nicest format for humans (having to quote keys, no comments, etc.).
There are a few alternative options:
dhall
- I like the idea, however in practice it seems to be quite verbose. For example, you need to specify a type annotation if you use an empty list. Furthermore, when I tried the Idris implementation, the error messages were very confusing.toml
- Probably my favourite language design-wise. However, the Idris implemetnation doesn't seem to be compiling atm (https://github.com/cuddlefishie/toml-idr). Also I have no idea how robust the implementation is, as I've been unable to test it.I'd say the biggest requirement on the format is that it should be easy to use for an inexperienced user. This means high quality error messages, and a simple to write format. The more complex the format, the better error messages needed to compensate.
Interested to hear others' thoughts on this.
Currently a lot of our work is done using "system" commands. We should switch to libraries if they are available because:
sirdi
.The biggest offenders for this are probably git
commands and idris2 --build ...
, since there seems to be existing Idris2 libraries for both of these things.
When trying to install sirdi using make install
, I get the following error:
install build/exec/sirdi ~/.idris2/bin
install: cannot create regular file '/home/thomas/.idris2/bin': No such file or directory
make: *** [Makefile:23: install] Error 1
I have PREFIX
set to ${HOME}/.idris2-git
to avoid confusion with the latest release build and that's probably what's causing this error. It would be neat if sirdi took PREFIX
into account : )
Can we have installation instructions in the root README?
I'm not sure if this is the same problem or I need a separate issue, but make build
gives
Error: While processing right hand side of cloneDep. Sorry, I can't find any elaboration which works. All errors:
If Prelude.::: When unifying:
List ?a
and:
String
Mismatch between: List ?a and String.
build:32:27--32:28
28 |
29 | cloneDep : String -> String -> IO ()
30 | cloneDep pkg url =
31 | unless !(exists $ "build" </> pkg)
32 | $ ignore $ system ["git", "clone", url, "build" </> pkg]
^
If Prelude.Stream.::: When unifying:
Stream ?a
and:
String
Mismatch between: Stream ?a and String.
build:32:27--32:28
28 |
29 | cloneDep : String -> String -> IO ()
30 | cloneDep pkg url =
31 | unless !(exists $ "build" </> pkg)
32 | $ ignore $ system ["git", "clone", url, "build" </> pkg]
^
Error: While processing right hand side of fetchDep. Sorry, I can't find any elaboration which works. All errors:
If Prelude.::: When unifying:
List ?a
and:
String
Mismatch between: List ?a and String.
build:39:31--39:32
35 | fetchDep (pkg, url, commit) = do
36 | cloneDep pkg url
37 | whenJust commit
38 | $ \commit => ignore $ inDir ("build" </> pkg)
39 | $ ignore $ system ["git", "checkout", "--detach", commit]
^
If Prelude.Stream.::: When unifying:
Stream ?a
and:
String
Mismatch between: Stream ?a and String.
build:39:31--39:32
35 | fetchDep (pkg, url, commit) = do
36 | cloneDep pkg url
37 | whenJust commit
38 | $ \commit => ignore $ inDir ("build" </> pkg)
39 | $ ignore $ system ["git", "checkout", "--detach", commit]
^
Error: While processing right hand side of buildDep. Sorry, I can't find any elaboration which works. All errors:
If Prelude.::: When unifying:
List ?a
and:
String
Mismatch between: List ?a and String.
build:45:16--45:17
41 | buildDep : (String, String, Maybe String) -> IO ()
42 | buildDep (pkg, url, _) = do
43 | Just 0 <- inDir ("build" </> pkg) $ do
44 | putStrLn "building \{pkg}"
45 | system ["idris2", "--build", pkg <.> "ipkg"]
^
If Prelude.Stream.::: When unifying:
Stream ?a
and:
String
Mismatch between: Stream ?a and String.
build:45:16--45:17
41 | buildDep : (String, String, Maybe String) -> IO ()
42 | buildDep (pkg, url, _) = do
43 | Just 0 <- inDir ("build" </> pkg) $ do
44 | putStrLn "building \{pkg}"
45 | system ["idris2", "--build", pkg <.> "ipkg"]
^
Warning: compiling hole Main.fetchDep
Warning: compiling hole Main.buildDep
What needs to be done before the refactor
can replace the current main
branch?
I will soon have some time to work on sirdi, so I am happy to help get this done.
I think this should be done soon as main
is currently the default branch, so people might not be aware of the refactor
branch.
We could really do with adding a test suite to CI to ensure changes we push aren't breaking.
Currently LSP expects a .ipkg file in a parent directory of the source code, however sirdi doesn't generate one, so lsp doesn't work
Here are some potential solutions I can think of:
Please add instructions to build this project in its README. I tried compiling build.idr
, but it fails on Idris2 (0.5.1).
❯ idris2 -c build.idr
1/1: Building build (build.idr)
Error: While processing right hand side of cloneDep. Sorry, I can't find any elaboration which works. All errors:
If Prelude.::: When unifying:
List ?a
and:
String
Mismatch between: List ?a and String.
build:32:27--32:28
28 |
29 | cloneDep : String -> String -> IO ()
30 | cloneDep pkg url =
31 | unless !(exists $ "build" </> pkg)
32 | $ ignore $ system ["git", "clone", url, "build" </> pkg]
^
If Prelude.Stream.::: When unifying:
Stream ?a
and:
String
Mismatch between: Stream ?a and String.
build:32:27--32:28
28 |
29 | cloneDep : String -> String -> IO ()
30 | cloneDep pkg url =
31 | unless !(exists $ "build" </> pkg)
32 | $ ignore $ system ["git", "clone", url, "build" </> pkg]
^
Error: While processing right hand side of fetchDep. Sorry, I can't find any elaboration which works. All errors:
If Prelude.::: When unifying:
List ?a
and:
String
Mismatch between: List ?a and String.
build:39:31--39:32
35 | fetchDep (pkg, url, commit) = do
36 | cloneDep pkg url
37 | whenJust commit
38 | $ \commit => ignore $ inDir ("build" </> pkg)
39 | $ ignore $ system ["git", "checkout", "--detach", commit]
^
If Prelude.Stream.::: When unifying:
Stream ?a
and:
String
Mismatch between: Stream ?a and String.
build:39:31--39:32
35 | fetchDep (pkg, url, commit) = do
36 | cloneDep pkg url
37 | whenJust commit
38 | $ \commit => ignore $ inDir ("build" </> pkg)
39 | $ ignore $ system ["git", "checkout", "--detach", commit]
^
Error: While processing right hand side of buildDep. Sorry, I can't find any elaboration which works. All errors:
If Prelude.::: When unifying:
List ?a
and:
String
Mismatch between: List ?a and String.
build:45:16--45:17
41 | buildDep : (String, String, Maybe String) -> IO ()
42 | buildDep (pkg, url, _) = do
43 | Just 0 <- inDir ("build" </> pkg) $ do
44 | putStrLn "building \{pkg}"
45 | system ["idris2", "--build", pkg <.> "ipkg"]
^
If Prelude.Stream.::: When unifying:
Stream ?a
and:
String
Mismatch between: Stream ?a and String.
build:45:16--45:17
41 | buildDep : (String, String, Maybe String) -> IO ()
42 | buildDep (pkg, url, _) = do
43 | Just 0 <- inDir ("build" </> pkg) $ do
44 | putStrLn "building \{pkg}"
45 | system ["idris2", "--build", pkg <.> "ipkg"]
In typical open-source project fashion, the name sirdi
was just originally chosen as a "temporary" name, but it seems to have stuck for now. However, if people dislike the name, now is probably the time to change it.
If you have particular preference for a name, comment below!
The main requirement for a name is that it is easily "google-able" (we don't need another "idris elba" incident).
I think the name should also be relatively short (I'd say 6/7 characters is probably the limit, so it is quick to type).
Maybe it would be nice if we named the package manager after an "Ivor the Engine" character (which is where the name Idris
comes from)? (https://en.wikipedia.org/wiki/Ivor_the_Engine#Characters)
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.