[ feature request ] `pack` should detect that local build uses outdated compiler

[buzden]

trafficstars

Imagine you have selected some collection and have built a local package using pack build command. Its result now is stored in the build directory and uses current's compiler version TTC version.

Then, if you switch to another collection with a version of compiler that uses another TTC version, and try to do pack build for the local package (especially, after some small changes in it), you'll get a compiler error that already present TTC files have unsupported TTC version.

So, it would be good for pack to either alter build directory depending on compiler version for local builds too or to detect that TTC version (compiler version?) of particular modules is inconsistent with the current collection's compiler and to rebuild those modules.

[stefan-hoeck]

I think the most simple option in this case would be to add a (hidden) file containing the commit of the compiler used to build a local package to its build directory. If we wanted to build the package with a different compiler version, we'd invoke idris2 --clean first. What do you think?

[buzden]

I think the most simple option in this case would be to add a (hidden) file containing the commit of the compiler used to build a local package to its build directory. If we wanted to build the package with a different compiler version, we'd invoke idris2 --clean first. What do you think?

I think this is good enough, it's simple and the case of successive rebuilds when you constantly switch between, say, two versions and constantly rebuild all with cleaning seems to be not so important. Couple of concerns:

• If there is no file containing the commit, should the code be rebuilt with cleaning? For consistency, it definitely should, but it means that interleaving pack and direct idris2 builds may lead to surprising effects.
• Maybe, we should not just run idris2 --clean but remove the build directory entirely? I keep in mind a case when there was a module A and a module B that imports A; say, A was renamed to C (both file and ipkg record) but import of A wasn't changed (mistakenly). As far as I remember, idris2 --clean would not remove A.ttc from the build dir, thus it would continue to be found at import even after cleaning. It means that if renaming was done along with compiler update, you still will get a TTC version problem when using pack build. Well, maybe, this is actually an upstream problem, I don't know, but pack users can encounter it.

[buzden]

By the way, just for a record -- do you know whether is it hard or not to alter the local build dir at the call to the compiler when building or executing a local package? Anyway, this is not an ideal solution since it can leave a lot of uncollected garbage from builds for different compiler versions, but it's good to know whether or not this is an option.

[stefan-hoeck]

* If there is no file containing the commit, should the code be rebuilt with cleaning? For consistency, it definitely should, but it means that interleaving `pack` and direct `idris2` builds may lead to surprising effects.

Yes, if there is no commit tag, pack should assume the build dir is outdated. And yes, if you interleave calls to pack with direct calls to idris2 this might not work out as expected. An alternative would be to use a custom build dir whenever we use pack (the build dir can easily be changed when invoking Idris2 with the --build-dir command line option), but this means more garbage and all packages working with pack must update their .gitignore files. Not ideal.

* Maybe, we should not just run `idris2 --clean` but remove the build directory entirely? I keep in mind a case when there was a module `A` and a module `B` that imports `A`; say, `A` was renamed to `C` (both file and `ipkg` record) but import of `A` wasn't changed (mistakenly). As far as I remember, `idris2 --clean` would not remove `A.ttc` from the build dir, thus it would continue to be found at import even after cleaning. It means that if renaming was done along with compiler update, you still will get a TTC version problem when using `pack build`. Well, maybe, this is actually an upstream problem, I don't know, but `pack` users can encounter it.

You are right, and actually we should do both, because idris2 --clean might invoke additional cleanup hooks as specified in the .ipkg file. I should also update the clean command to completely remove the build dir.

[stefan-hoeck]

As a second thought, I wonder whether idris2 --clean should actually completely remove the build dir?

[stefan-hoeck]

Am I right in assuming that this will no longer be needed once idris-lang/Idris2#2684 lands? Otherwise I got a fix ready where pack will add an .idrisVersion file to the build directory. But that's a hacky way to do this, because the build dir might have been created by an external tool such as idris2-lsp.

[stefan-hoeck]

So, I have merged a simple fix for this. Simple enough that it can be easily undone should we no longer need it.

[buzden]

Am I right in assuming that this will no longer be needed once idris-lang/Idris2#2684 lands?

I think so