A language version field in package files

[mattpolzin]

• [x] I have read CONTRIBUTING.md.
• [x] I have checked that there is no existing PR/issue about my proposal.

Summary

I'd like to see an optional language version field in ipkg files. Perhaps langversion? The field should work like the depends entries (accepting either a constant version or a range that the language must fall within).

Motivation

Right now there is no good way that I know of for a package to indicate it requires a certain range of Idris 2 versions. A package might use language features only available after a certain version or it might only be useful prior to the language features of another Idris 2 version.

The proposal

The proposal is just to add a single new optional field like the above-suggested langversion field to Package files. Then package managers can choose to use that information if desired and perhaps future work in the Idris 2 compiler can check that the version of itself meets the criteria in a package being --installed.

Examples

The following example would indicate that the Idris 2 compiler itself at version 0.5.0 cannot be built with a language version less than 0.4.0. It's a bit problematic at this point to see into the future and know that upcoming versions of Idris 2 will be backwards compatible, so it also specifies a conservative upper bound.

package idris2

...
version = 0.5.0
langversion >= 0.4.0 && < 0.6.0
...

[andrevidela]

What do you think about using commits (and tags) in that field rather than the compiler's version numbers? In my experience I tend to work against a specific commit and build from there, specially when working with experimental features.

In terms of core functionality it should be the same since the tag and the version number should always be in sync.

This would also allow us to define some sort of "bootstrap history" and say " the compiler at commit X can be built with the compiler from commit Y which itself can be compiled with commit Z, but you can't compile X with Z"

I guess it would make ranges a bit more difficult to work with since commits have no guarantee to happen in chronological order but it doesn't feel too surprising to me that ranges would be disabled for commits and only kept for plain version numbers.

Maybe this is a bad idea because it leaks too much of git's functionality into the compiler!

[kenaryn]

Hello, I'm unsure weither it could help you a bit but Julia use a version number literal like the following v"...", e.g.

if v"0.4" < VERSION < v"0.5-"
    # do something with 0.4 series 
end

In Julia, the reserved word VERSION is a constant, which in my case returns v"1.6.2".

Here is the brief description in documentation: https://docs.julialang.org/en/v1/manual/strings/#man-version-number-literals Here is the implementation of the version number literal: https://github.com/JuliaLang/julia/blob/master/base/version.jl

[mattpolzin]

What do you think about using commits (and tags) in that field rather than the compiler's version numbers? In my experience I tend to work against a specific commit and build from there, specially when working with experimental features.

That's an interesting take on the idea. I'm a bit more drawn to the idea of using the semantic(ish) dot separated version, but let me see if I can properly justify that feeling because I'm not immediately convinced using commits/tags isn't better.

First, I have to admit the clear advantage to allowing commits is that it is more granular. As far as I have thought, this granularity only benefits us pre-release, though. Once a new version of Idris is cut, there's no advantage I don't think in saying "this builds after commit ABCD" instead of "this builds after version 0.5.0" (given commit ABCD lands between version 0.4.0 and 0.5.0). I'd be interested to explore how that assumption about when targeting specific commits is useful might be wrong.

You touch on one of the key disadvantages of using commits and tags: It's a git-specific concept. At first I wasn't sure if this was that big of a deal. It might be unfortunate because package files already declare their own versions, so it would be more intuitive if this new field operated on the same type of version. But maybe the better point is that other than this hypothetical field, git doesn't need to be installed for Idris 2 to be operational. I think this line of thinking (you're getting an almost stream of consciousness response from me) is starting to sell me more on the original idea for dot sep versions: I envisioned an installed copy of Idris 2 being able to determine if it was compatible with a packaged when calling idris2 --install cool-thing.ipkg and any feature like that would ideally not have any reliance on git; Idris2 already knows it's own version, and for source-builds it may even have its git SHA as a suffix, but it has no way to know how two SHAs relate to each other without not only git itself but also the ref history for the Idris 2 source repository.

[mattpolzin]

@kenaryn that's cool! I do think both what you are referencing and a package level language version field could be useful (in different situations) so it feels like a separate, though very worthy, idea for an additional feature.

[kenaryn]

I admit it would be quite a lot of work in perspective as implementing a new non-standard string semantics is no-joke. With regard to your stream of consciousness, I support your position to keep separate / distinct / decoupled the business logic of the back-end of Idris2 and the underlying layers of control version system.

We have no control on the Git's executive committee strategy, therefore, relying on Git to normalize traceability of new software iterations presents a serious technological risk.

[melted]

I don't get how a binary build of Idris would know if a commit ID is in its past or future.