[ new ] Support arbitrary `Name` in `IBindVar`

[spcfox]

Description

Replaces String with Name in the IBindVar signature. This makes IBindVar more consistent and allows the binding of machine-generated names. Using machine-generated names in IBindVar can be useful in compiler and elaborator scripts.

Should this change go in the CHANGELOG?

• [x] If this is a fix, user-facing change, a compiler change, or a new paper implementation, I have updated CHANGELOG_NEXT.md (and potentially also CONTRIBUTORS.md).

[spcfox]

This PR is ready to review. The fixes in LSP-lib, elab-util, frex and idrall (for katla) should be enough for a green CI

[spcfox]

The status of the pack collection with this branch:

[ warning ] The following packages failed to build:
            - barbies
            - bounded-doubles-hedgehog-generators(failing dependencies: pretty-show, sop)
            - chem-generators(failing dependencies: pretty-show, sop)
            - cyby-draw(failing dependencies: json-simple)
            - dependent-map(failing dependencies: pretty-show, sop)
            - deptycheck
            - dom-mvc(failing dependencies: json-simple)
            - dom-mvc-extra(failing dependencies: json-simple, barbies)
            - hedgehog(failing dependencies: pretty-show, sop)
            - http(failing dependencies: sop)
            - json
            - json-simple
            - lana(failing dependencies: json, json-simple)
            - node
            - parser-tsv
            - parser-webidl(failing dependencies: sop)
            - pretty-show
            - refined-json(failing dependencies: json-simple)
            - refined-tsv(failing dependencies: parser-tsv)
            - sop
            - sqlite3
            - sqlite3-rio(failing dependencies: sqlite3)
            - stellar-http(failing dependencies: node)
            - stellar-sql(failing dependencies: sqlite3, json)
            - tls(failing dependencies: sop)
            - tyttp-adapter-node(failing dependencies: node)
            - tyttp-json(failing dependencies: json, sop, node)
            - webidl(failing dependencies: sop)
[ warning ] 28 packages failed to build.

[stefan-hoeck]

Looking at the failing pack libraries, this will require quite a bit of work till the pack collection is up and running again. Many of the failing packages are my own, so they should be fine. deptycheck and node are not, so we probably should get in touch with their maintainers.

I for my part am ready to go with this and merge the adjustments made to elab-util as soon as reviewers are ready to merge this.

Thanks, spcfox, for going through the trouble and also checking the pack collection!

[spcfox]

I'm working with @buzden, we're ready to make changes to deptycheck

[buzden]

As a comment beside libraries changes, I've talked about this change with Edwin in 2021 and he agreed that this should be done and said that he didn't remember why the current design of IBindVar was chosen.

[dunhamsteve]

I believe we need to bump the TTC version in src/Core/Binary.idr. Otherwise, it will fail with "file: Corrupt TTC data for Name" when it reads .ttc files made by the current Idris.

[spcfox]

I'm not sure if this kind of code is supposed to work. It doesn't right now

definition : Decl
definition =
   IDef EmptyFC `{ foo }
        [ PatClause EmptyFC `( foo ~(IBindVar EmptyFC $ UN $ Basic "x") )
                             (IVar EmptyFC (DN "y" $ UN $ Basic "x"))]

[buzden]

I'm not sure if this kind of code is supposed to work. It doesn't right now

definition : Decl
definition =
   IDef EmptyFC `{ foo }
        [ PatClause EmptyFC `( foo ~(IBindVar EmptyFC $ UN $ Basic "x") )
                             (IVar EmptyFC (DN "y" $ UN $ Basic "x"))]

I think it should, because I understand DN as a purely pretty-printing thing, which should not influence on typechecking

[spcfox]

I'm not sure if this kind of code is supposed to work. It doesn't right now

definition : Decl
definition =
   IDef EmptyFC `{ foo }
        [ PatClause EmptyFC `( foo ~(IBindVar EmptyFC $ UN $ Basic "x") )
                             (IVar EmptyFC (DN "y" $ UN $ Basic "x"))]

Ok, this is not related to the current PR, created an issue https://github.com/idris-lang/Idris2/issues/3542 on this behavior

[spcfox]

List of packages requiring fixes:

CI:

• [x] elab-util
• [x] lsp-lib
• [x] idrall
• [x] frex

Pack collection:

@stefan-hoeck:

• [x] barbies
• [x] hedgehog
• [x] json & json-simple
• [x] parser-tsv & parser-webidl
• [x] pretty-show
• [x] sop
• [x] sqlite3

other:

• [x] deptycheck
• [x] node

Failed due to dependencies:

• [x] bounded-doubles-hedgehog-generators
• [x] chem-generators
• [x] cyby-draw
• [x] dependent-map
• [x] dom-mvc & dom-mvc-extra
• [x] http
• [x] lana
• [x] refined-json & refined-tsv
• [x] sqlite3-rio
• [x] stellar-http & stellar-sql
• [x] tls
• [x] tyttp-adapter-node & tyttp-json
• [x] webidl

[spcfox]

I've prepared patches to all the libraries. This PR is ready for review and merge.

[buzden]

I'm really for merging this PR. In order to make Idris CI to become green, we need besides e.g. me, one of @ohad or @gallais for frex, and one of @mattpolzin or @alexhumphreys for idrall, which is a dependency for katla. All that we need is to merge corresponding pull requests adapting to this one.

In order the next pack collection won't fail building next day, we need also @stefan-hoeck and @kbertalan to be ready to merge compat pull requests to their repos.

Guys, can we syncronise, say, today to do all that?

[stefan-hoeck]

I'm ready to update my packages as soon as this is merged. Today would be fine, tomorrow also.

[mattpolzin]

Works for me.

[kbertalan]

I can merge the changes to my project when this is merged within a 12 hours window any week day this week.

[spcfox]

@ohad, @gallais, @stefan-hoeck, @mattpolzin, @kbertalan, @buzden How about this week?

[kbertalan]

@spcfox how is it going? Will this be ever finished?

[spcfox]

@spcfox how is it going? Will this be ever finished?

The PR is ready to be merged, but it impacts multiple libraries, making synchronization difficult. Last time, we didn’t receive any response from maintainers with access to frex. I believe we’ll be able to complete this once @gallais and @buzden are back from vacation.

[gallais]

I'm happy to go ahead with this.

[buzden]

I'm happy to go ahead with this.

Let's synchronise, then. To make compiler's CI jobs green we need to merge appropriate PRs to elab-utils (I can do it), lsp-lib, frex and idrall (@mattpolzin can)

[mattpolzin]

I'm still available to merge the LSP and/or Idrall PRs on relatively short notice.

[spcfox]

@stefan-hoeck @kbertalan This PR has been approved, I think we'll merge it tomorrow.

[buzden]

Then I'd suggest @gallais to merge appropriate upstream PR to frex as a signal to others to start merging PRs to elab-util, idrall and lsp-lib, and then we'll rerun this PR's CI jobs to check all's green.

[gallais]

Merged on frex

[mattpolzin]

Merged idrall

[spcfox]

@stefan-hoeck @kbertalan We did it!

[stefan-hoeck]

I just started a test to generate a new pack nightly to see whether we missed something. Will report back here.

[stefan-hoeck]

Oh dear, this will take some time. Currently, the following libraries still fail:

[ warning ] The following packages failed to build:
- barbies
- bounded-doubles-hedgehog-generators(failing dependencies: pretty-show)
- chem-generators(failing dependencies: pretty-show)
- cyby-draw(failing dependencies: json-simple)
- dependent-map(failing dependencies: pretty-show)
- deptycheck
- dom-mvc(failing dependencies: json-simple)
- dom-mvc-extra(failing dependencies: json-simple, barbies)
- hedgehog(failing dependencies: pretty-show)
- json
- json-simple
- lana(failing dependencies: json, json-simple)
- node
- pact-api(failing dependencies: json)
- pact-client(failing dependencies: json)
- pact-server(failing dependencies: json)
- pact-todomvc(failing dependencies: json)
- pact-wai(failing dependencies: json)
- parser-tsv
- parser-webidl
- pretty-show
- refined-json(failing dependencies: json-simple)
- refined-tsv(failing dependencies: parser-tsv)
- sqlite3
- sqlite3-rio(failing dependencies: sqlite3)
- stellar-http(failing dependencies: node, json-simple)
- stellar-sql(failing dependencies: sqlite3, json)
- tyttp-adapter-node(failing dependencies: node)
- tyttp-json(failing dependencies: json, node)
- webidl(failing dependencies: parser-webidl)

The ones with failing dependencies might be fine once the dependencies have been fixed. I can take care of my own libs. @buzden, deptycheck is yours, right? @kbertalan, node is your lib. Could you please have a look at that one?

[spcfox]

@stefan-hoeck I expect that these PRs should be enough (each link leads to the corresponding PR). deptycheck is already merged https://github.com/idris-lang/Idris2/pull/3526#issuecomment-2901992369

[stefan-hoeck]

@stefan-hoeck I expect that these PRs should be enough (each link leads to the corresponding PR). deptycheck is already merged #3526 (comment)

Ah, sorry, forgot about that list. You have been very thorough. Am fixing the remaining libs now (with the exception of node).