search

stefan-hoeck / idris2-elab-util

Utilities and documentation for exploring idirs2's new elaborator reflection.
BSD 2-Clause "Simplified" License
76 stars 16 forks source link

Switch over to HVect alias in base. #61

Closed mattpolzin closed 1 year ago

mattpolzin commented 1 year ago

Pairs nicely with https://github.com/idris-lang/Idris2/pull/2843. Also is entirely broken prior to that PR landing in the Idris 2 project. If/when #2843 is merged, idris2-elab-util tests will pass again against nightly builds. I've verified that make test for this repo passes locally with a build of Idris based off of #2843 installed.

stefan-hoeck commented 1 year ago

PR #59 will ditch the contrib dependency altogether, but I can't merge that one just yet, because it will have an impact on a few other libs of mine, which I'm in the process of fixing. I'm therefore happy to merge this one, once idris-lang/Idris2#2843 is ready.

mattpolzin commented 1 year ago

https://github.com/idris-lang/Idris2/pull/2843 Is ready save for the test that runs this library’s build/test failing.

has this happened before and is there a precedent for whether this library gets updated despite a CI failure first so that Idris’s CI can go green and it’s PR can merge or whether Idris gets updated first so that this library’s CI can go green and it’s PR can merge?

it’d be possible to keep both green by merging a different PR to elab-util that made sure it didn’t depend on either the base or contrib library’s HVect types (a simple alias within elab-util), if that was preferable.

I realize this is all temporary given your plans with #59, so whatever you are comfortable with.

buzden commented 1 year ago

has this happened before and is there a precedent for whether this library gets updated despite a CI failure first so that Idris’s CI can go green

That happened each time, we tried to make Idris never go red in its main branch.

stefan-hoeck commented 1 year ago

has this happened before and is there a precedent for whether this library gets updated despite a CI failure first so that Idris’s CI can go green and it’s PR can merge or whether Idris gets updated first so that this library’s CI can go green and it’s PR can merge?

Yes, sorry for not being explicit about this. The usual procedure is to post a message here when the corresponding Idris PR is about to be merged, in which case we merge the (still red) PR for elab-util first.

mattpolzin commented 1 year ago

Cool. I’ll kick tests off over on the other PR again!