search

frex-project / idris-frex

Other
46 stars 9 forks source link

Use Data.Vect.Quantifiers.All from base instead of Data.HVect from contrib. #69

Closed mattpolzin closed 8 months ago

mattpolzin commented 10 months ago

This pairs with https://github.com/idris-lang/Idris2/pull/3191 to switch to base's Data.Vect.Quantifiers.All.HVect (an alias for All id) instead of using Data.HVect from contrib.

That Pr is needed before this PR will build at least for its public expose change on head/tail functions if not for other functions it ports from contrib into base. To show compatibility, I changed this repo's IDRIS2_COMMIT in CI to point at a merge of Idris 2's main branch and the aforementioned PR.

mattpolzin commented 8 months ago

@ohad mind running this once more? Sorry for all the running around this PR is requiring.

ohad commented 8 months ago

I'm not sure how to get it to run. OK, I think the commentted out entry made it fail some well-formedness checks, so I deleted it. We'll restore it from commits/logs later.

ohad commented 8 months ago

So now we can make idris CI work with this version, and when fixes are upstreamed, update both?

mattpolzin commented 8 months ago

Yeah. Now can either merge this PR, then see Idris CI go green against it and merge the Idris PR, and then finally update this project to point back at the correct upstream Idris. Or, we might be able to tell upstream Idris to point at this particular branch to get Idris CI to go green and merge the Idris PR first. Either way the process is a bit fiddly and manual but we've done it before and will do it again no doubt (for pack libraries, at least).

gallais commented 8 months ago

merge this PR, then see Idris CI go green against it and merge the Idris PR, and then finally update this project to point back at the correct upstream Idris.

Yep, that's our usual process.