Support local versions of the Idris compiler
Closed this issue · 10 comments
It is possible to have local versions of packages but not of the compiler itself. This makes it harder to test local changes.
It's correct that we need this. What kept me from doing it so far is the following: Should we enforce a clean build when building and installing a local copy of the compiler and its libraries? If yes, how do we do that? Use a local clone of the local clone, or just run make clean before building? Perhaps I'm making this look more complicated than it actually is, but for me it is not immediately clear what users would expect to be the default behavior here.
I'd expect it to make a clone of the repo, since that is what stack/cabal do, I think. Since I know that a build tool manages caching, I am not expecting it to modify any files I pass it. I am thinking of this as an analogue to source-repository-package, and I don't see why it should work differently just because it applies to the compiler.
I'd expect it to make a clone of the repo, since that is what stack/cabal do, I think. Since I know that a build tool manages caching, I am not expecting it to modify any files I pass it. I am thinking of this as an analogue to
source-repository-package, and I don't see why it should work differently just because it applies to the compiler.
At the moment, pack uses a local package's own directory for building the project. Perhaps we should introduce a new type of package to pack.toml files: At the moment we have "local" and "github". Perhaps "local-repo"? Anyway: What do you mean with source-repository-package? What is this and where is it coming from?
What is this and where is it coming from?
source-repository-package is a stanza in Cabal, which is build tool for Haskell. This stanza allows replacing dependencies in an ad-hoc manner: Cabal docs. Stack, another build tool for Haskell, provides similar functionality, they call it extra-deps.
Hmm, I'm testing this right now, but it looks like this already works. I added the following to my pack.toml file, and it seems to be cloning and using my local Idris copy just fine:
[idris2]
url = "/home/sh/idris/Idris2"
commit = "latest:ttcversion"The latest:[branch] syntax for the commit is the same in behavior as for remote projects.
So, I'm going to close this as at least on my system, local git repos work as expected, and they allow us to test local modifications to the Idris compiler. Make sure to use bootstrapping to build the compiler (by means of pack's --boostrap command-line option).
Feel free to reopen this, if you think it does not behave as expected.
Hmm, I'm testing this right now, but it looks like this already works. I added the following to my
pack.tomlfile, and it seems to be cloning and using my local Idris copy just fine:[idris2] url = "/home/sh/idris/Idris2" commit = "latest:ttcversion"The
latest:[branch]syntax for thecommitis the same in behavior as for remote projects.
I tried this, and run pack typecheck <Some.idr> which is a wrong command because typecheck expects package file, and pack printed nice error message. But after that I realised despite installed local compiler vestion, no prelude and no applications from must-have applications were installed. It is a problem with local idris compiler or is it a strange interaction between installation side-effect and wrong passed arguments?
Hmm, I'm testing this right now, but it looks like this already works. I added the following to my
pack.tomlfile, and it seems to be cloning and using my local Idris copy just fine:[idris2] url = "/home/sh/idris/Idris2" commit = "latest:ttcversion"The
latest:[branch]syntax for thecommitis the same in behavior as for remote projects.I tried this, and run
pack typecheck <Some.idr>which is a wrong command becausetypecheckexpects package file, andpackprinted nice error message. But after that I realised despite installed local compiler vestion, nopreludeand no applications from must-have applications were installed. It is a problem with local idris compiler or is it a strange interaction between installation side-effect and wrong passed arguments?
It is the latter. Pack will install must-have libs and apps (which always include the prelude and base) only when any kind of installation is required, in which case it first tries to resolve all requested libraries. In your case, this resolution step failed, because Some.idr is not a known library. Hence, no libs were installed. This is completely unrelated to the issue discussed here. If you try to install or build another library, pack will realize that must-have libs are still missing, and install them then. For instance, just running pack install base should install all missing libs and apps.
Not sure what I am doing wrong, but after configuring the commit and url as previously mentioned, I tried doing pack install katla. I expected it to build the new compiler and use it to build katla, but instead I got:
[ build ] idris2 --build idris2.ipkg
/home/janus/.pack/bin/idris2: 8: /home/janus/.pack/install/cf23a9b0f667640bbf88a81d3eaf757106db8993/idris2/bin/idris2: not found
make: *** [Makefile:63: /home/janus/.pack/.tmp0/idris2-compiler/build/exec/idris2] Error 127
[ fatal ] Error when executing system command.
Also, is there some way to use a custom compiler during initial pack installation?
Not sure what I am doing wrong, but after configuring the commit and url as previously mentioned, I tried doing
pack install katla. I expected it to build the new compiler and use it to build katla, but instead I got:
Use pack --boostrap install katla. pack tries to use an already installed version of the compiler to build the new version of the compiler. In order to do so, it tries to use what's currently specified in the pack.toml files, which works well when we run pack switch latest (because overwriting the pack.toml file is the last step in that case) but fails otherwise, because that compiler is not yet installed. I'll open a new issue about this, as we really should use a smarter way to find an already existing version of Idris.