Re: Adding copilot

[Ivan Perez <ivan.perez@keera.co.uk>]

Thanks again.

I've updated the requirement on bimap.

There's an additional issue with bimap: the `Data.Bimap` module is no 
longer inferred as safe in `0.4.0`, and that throws off 
`copilot-theorem`.

I've opened an issue on the `bimap` package:
https://github.com/joelwilliamson/bimap/issues/14

I think there are simple solutions; feel welcome to chime in if you know 
a good, clean way to ensure that the code can be inferred as `Safe` in 
this case.

Please let me know if there's anything else you find in the meantime. 
I'll have everything on the copilot side prepared as needed, so that 
when other packages address any issues we find, we are ready.

Happy to have an interactive session if that can make the conversation 
more agile.

Ivan

On 2022-05-05 16:50, Scott Talbert wrote:
> On Thu, 5 May 2022, Ivan Perez wrote:
>
> > > > [...]
> > > > After searching the rest of the dependency tree exhaustively, these 
> > > > were the
> > > > goals I've had most trouble fulfilling: copilot, ansi-terminal,
> > > > copilot-theorem
> > >
> > > Actually, I read that wrong.  copilot-theorem seems to require an
> > > *older* version of ansi-terminal.  Can it be updated to use
> > > ansi-terminal 0.10.3?
> >
> > Scott,
> >
> > Thanks a lot for checking. That can be bumped up (I just checked by 
> > modifying that constraint in the cabal package).
> >
> > I've made this change temporarily available here:
> > https://github.com/Copilot-Language/copilot/tree/develop-version-bounds
> >
> > Are you able to test with that change (just to see if it works or if 
> > anything else needs to be changed)?
>
> After patching that, the bimap version is the next problem (Debian has 
> 0.4.0).
>
> After patching in bimap also, the next problem relates to what4 and
> its dependencies.  I'll have to fiddle with the package plan a little
> more to see what else might need to be changed.
>
> Scott