eayus / sirdi Goto Github PK

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:

• How to depend on a git project that has an .ipkg file, but no sirdi configuration file?
  For concreteness, let's say the package dependencies are: A --[ depends on]---> B --[dep on] --> C, D, E.
  We're developing A, while B,C, and D are outside our control (but fine to assume, say, they're on github).
  While it may make a developer's life hard to maintain an explicit transitive dependency on C, D, and E, it might be impossible for them to introduce a sirdi configuration file into B for whatever reasons.
  Nonetheless, sirdi should be able to cope with this situation, and the fact that sirdi is itself in this situation demonstrates that.

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.
• others - I'm not aware of any alternatives with Idris support, but please let me know if there is some other options.

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:

• It's faster, since the command line arguments do not need to be processed.
• Easier to keep track of the "hidden" dependencies of sirdi.
• It's more secure. On the command line, every argument is a string. This makes it much harder to prevent issues such as code injection.

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:

• Generate a ipkg file
  • Clutters the project
  • Still has problems with where sirdi puts the ttc/ttm files
• Update idris2-lsp to support sirdi
  • More work?
  • Potentially requires updating 2 projects when changes are made
    • Could this be mitigated with clever design decisions?

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)