Split the .ipkg commands and the HTML doc gen into separate executables

[david-christiansen]

This would be a good way to clean up REPL.hs, and it's a good project for a new developer. The idea is to have three (quite thin) top-level executables in the .cabal file, and then have them use the compiler as a library. This would also greatly simplify command-line processing. Suggested names: idrispkg and idrisdoc.

[jfdm]

I think we can go one further with this, namely introduce idrisc (or some name variant of) for compiling programs.

Naturally idris will always exist and would be to launch the REPL.

[jfdm]

Also whoever tackles this might want to look at Issue 897.

[david-christiansen]

Yes, this is clearly related to #897. In fact, I think this would be a good first step: get some of the ugly out and make it nice first, then tackle the big uglies.

[NobbZ]

Just made my PR for #1071 and knowing cabal hell as well as ruby's bundler, I would like to make some proposals of how package-management should be handled, and hope it is the right place here:

• since @edwinb already said he is agains multiple executables I would propose to have idris with subcommands instead of the current plentora of --flags like the following examples:
  • idris or idris repl for firing up the REPL
  • idris package or idris pkg followed by further subcommands for package management
  • and so on
• Save installed packages by using <pkgname>--<version> instead of only <pkgname> in the libsdirectory.
  • when specifiing some package using idris -p example it will choose the latest version of the package example available. When specifing idris -p example--1.0.0 it will choose exactly that version if available and fail if not.
  • If there is an ipkg-file available in the current directory or its parents, automaticaly choose the latest possible and available version constraints for every invocation of idris.
  • idris package build (or similar command) should automatically determine latest available versions of specified dependencies (in the ipkg) and install them. Also it creates a ipkg.lock-file in which it tells exactly which versions of dependencies and their dependencies are build against.
  • Whenever this ipkg.lock does exist, it will be used instead of the ipkg for determining the version of packages to load.
• A central catalogue in the style of hackage or rubygems.org would be needed for keeping track of available versions of the packages.
• When executables are added to the packaging system, I would propose to install them in the corresponding folder of its version, and also create a wrapperscript/program in a central idris-bin-dir. This wrapper should then do the following:
  • Check if there is an ipkg/ipkg.lock in the current working dir or its parrents.
  • if yes: run the executable specified by dependency-constraints
  • if no: run the most recent executable available.

This is quite a lot of writing for someone just trying to enter the project, but I would also be willing to try to get some of this stuff implemented in idris.

[jfdm]

@NobbZ cheers for the suggests over what an Idris package manager should look like. Rarely have people put money where their mouth is! However, package management is not small task and there are lots of things to consider as you indicate in your above comment. I too have been working on a feature proposal for package management and see from my notes that we overlap.

Aside from the issue of sub-commands I would like to welcome you to contribute.your ideas to the proposal once it has been made public.

[jfdm]

@NobbZ I have created Issue #1832 for the discussion of how idris can support versioning of packages. You can add your ideas there.

[steshaw]

Looking for some more low-hanging fruit now that I'm up-to-date with Type Driven Development with Idris!

It looks like the main problem here is the length of REPL.hs at about 2000 lines? AFAICT, it's not (absolutely) necessary to introduce separate executables in order to separate the parsing/handling of packaging/mkdoc commands. I'm not particularly in favour of introducing separate executables since each one will link the idris library and be approximately the same size. We already have 4 executables (idris and 3 codegen executables) of about 50M a piece.

What do you folks think about addressing this issue by using "subcommands". One downside is that they are not backwardly compatible (but it could be something to consider before 1.0). It looks like this would work nicely, allowing us to separate the option processing of different subcommands which addresses the current centralisation in REPL.hs and still leaves open the decision to have separate executables if we wish.

If folks are happy with the subcommand approach, we could even subsume the codegen executables (at least the 3 that are built into the idris library) — though perhaps a separate issue/PR.

Note: Sometimes executables are hard-linked to have an effect like this. e.g. idrisc could be a hard-link to idris and when detected it would act like the subcommand idris compile. I'm ambivalent about pursing this option. One issue is portability of hard-links (this used to be an issue on Windows).

Scope

Just to confirm, it seems that the scope of this issue is to separate the following pkg options from REPL.hs:

  --build IPKG             Build package
  --install IPKG           Install package
  --repl IPKG              Launch REPL, only for executables
  --clean IPKG             Clean package
  --mkdoc IPKG             Generate IdrisDoc for package
  --checkpkg IPKG          Check package only
  --testpkg IPKG           Run tests for package

In particular, I cannot find any other documentation options other than the one here that's related to packages.

[jfdm]

@steshaw

'Great minds' think alike.

I too have considered introducing the use of sub-commands, and to me that would be a 'better' fix for this issue. In some of the many undocumented conversations I have had with people about Idris' CLI it would be nice to retain the current CLI, and that when invoking idris by itself the REPL still launches. Moreover, from these conversations we thought it best the compiler should still be called idris and not idrisc. Reduces confusion.

I think with the sub command approach, it would allows us to retain the original functionality and have a shiny new better CLI.

With all honestly haven't found the time to get round to producing a PR for this, there are other things that need addressing too...

Some other minor things to bear in mind, I'll list them for convenience.

1. I recently, tidied up idrisMain a little so the REPL is now ~1500 LOC :-P.
2. Version 1.0 of idris is more for language stability rather than CLI and tooling polish. So having a sub-command front end to idris can have the attention it deserves, and doesn't need to be rushed.
3. I think for now we should leave the codegen executables alone, as we should not treat them any differently to how we treat 'third-party' codegens. Keeping us honest.

[steshaw]

@jfdm, that sounds good. The idea that idris without a specified sub-command invokes the repl can be thought of as a default sub-command.

Nice to hear that you've been working on this and that REPL.hs is down to 1500 LOC. I was just doing a wc -l which is still about 2000.

As for the codegen executables, I don't have strong feelings about it but having a single executable idris with 3 codegen entry-points (aka subcommands) is pretty much the same thing as having 3 executables which link the idris library. i.e. I'm not suggesting that idris shouldn't execute the codegen as a separate process — rather than idris-codegen-c <args> it would invoke idris codgen-c <args>. Anyhow, we can see how the sub-command modularisation looks after a while and decide then.

I'm certainly happy to start looking into this with a focus on extracting the 'package' option processing into a separate Haskell module. In particular, are there any documentation generation options besides --mkdoc IPKG?

So, should I go ahead and start on this? Please assign this issue to me if you can!

[steshaw]

@jfdm Sorry for my confusion about REPL.hs. Now I see it's about 1500 lines. I must have rebased one of my branches to upstream/master but not my master :(. I just got a big merge conflict from some tweaks to main/Main.hs that I was making. Redoing them now.

I like that you've moved a bunch of functions from Idris.REPL to Idris.Main. It was quite confusing where functions were being imported from in main/Main.hs. There's still quite a few out-of-place functions in Idris.AbstractSyntax (for processing options) and the Opt data type that comes from Idris.AbstractSyntaxTree. Thankfully, most options processing happens in Idris.CmdOptions.

Anyhow, besides a few small tweaks to main/Main.hs, there isn't anything of package support left inREPL.hs. Perhaps we should close this issue and raise one to solve sub-commands in a new issue? I've noted that the options processing in main/Main.hs is quite adhoc (e.g. many extra "legal" options are ignored).

I've also got an idea about having sub-commands but retaining backwards compatibility. Basically:

• have an options parser for each sub-command: compile, package, repl/console, client, info etc.
• if a sub-command is explicitly given, only use that corresponding options parser.
• if no explicit sub-command is given (i.e. for backwards compatibility), we can probably try all the sub-command options parsers and execute the command with the first legal parse. We could perhaps even check if there is no ambiguous legal parses.

That's the royal "we" of course. I'm happy to look at it :).

[jfdm]

I like that you've moved a bunch of functions from Idris.REPL to Idris.Main. It was quite confusing where functions were being imported from in main/Main.hs. There's still quite a few out-of-place functions in Idris.AbstractSyntax (for processing options) and the Opt data type that comes from Idris.AbstractSyntaxTree. Thankfully, most options processing happens in Idris.CmdOptions.

Yeah, there are still small tweaks that can be made. Shifting Opts out completely, and combining with accessor functions, was/is a lot trickier than i had initially imagined. Some niggling dependencies I could resolve in time. I tried, but I think at some point the AbsSyntax module needs a bit more polish.

I would like to keep this issue open as it encompasses the CLI of idris rather than just the state of REPL, and main.Main and code quality of related code in general. There will be other related issues too.

Also, there are definite other subcommands to consider. There might be a list somewhere, if not I think it could be adapted from comments made in #1454.

For keeping the current interface, I thought a simpler approach would be: try parsing a sub command, if nothing recognised then fall back to it. However, my experiences with opt-parse-applicative is not great. SO do not take my word for it.

As for a codegen command, remember idris has the option to specify a backend during compilation and defaults to C.

[steshaw]

@jfdm hadn't realised you'd tried to clean up AbsSyntax too. No matter, these things often happen incrementally.

It's fine to keep this issue open but the name does need updating. I am unable to change it. I'm happy to keep niggling away at the CLI/sub-command thing and see what happens.

As for the simpler approach to backwards compatibility. I like simpler approaches! I'm unsure what you mean by "fall back to it". Do you mean the current options parser? I don't think it would be a good idea to maintain subcommand options parsers and the current megalith. Perhaps you mean something else?

I don't have a lot of experience with opt-parse-applicative either but I'm happy to get into it. The only thing that really slowed me down was some arrow syntax which I am unfamiliar with.

I noticed that additional checks (beyond the option parsers) have been put in place. For example:

$ idris --repl test/pkg001/test-pkg.ipkg fred
Not all command line options can be used to override package options.

The only changeable options are:
        --log <lvl>, --total, --warnpartial, --warnreach
        --ibcsubdir <path>, -i --idrispath <path>
        --logging-categories <cats>

The options need removing are:
         Filename "fred"

Ideally these checks would be built into the parsers. No promises though — it's probably harder than it looks. There's certainly quite a few options (many of which I have never used). It's quite likely that incompatible/unused options are currently ignored by some commands.

As for a list of sub-commands, I took a look at #1454 but it looks like I already have a fairly comprehensive list of candidates (compile, package, repl/console, client/ide-slave, info). AFAICT, the "documentation builder"/idrisdoc is no longer separate from the package sub-command. I did find more candidates as I trawl through idris --help though:

$ idris --execute
Uncaught error: Elaborating {__infer0} arg {ival0}: NoSuchVariable Main.main
$ cat >foo.idr
module Main

main : IO ()
main = putStrLn "Hello there"
$ idris --execute foo.idr
Hello there
$ idris --exec 'putStrLn "Hello fred"'
Hello fred
$ idris --eval '6 * 7'
42 : Integer

I've not used these options/commands before. Seems that eval, exec and execute are legitimately different subcommands!