Skip to content

Conversation

@proux01
Copy link
Contributor

@proux01 proux01 commented Jul 24, 2022

Update OPAM files and Docker CI accordingly

@gares
Copy link
Member

gares commented Jul 24, 2022

you need to version the .out file, an old version of elpi was giving the character at the end of a text chunk, rather than at the beginning...

@proux01
Copy link
Contributor Author

proux01 commented Jul 26, 2022

@gares thanks, this now works on 8.15, however the CI still shows a few failures:

  • some failures in mcHB are due to missing overlays, I could copy/paste them from Porting to HB  math-comp#733 but not sure it's worth it
  • failures of analysis and deriving in mcHB are expected
  • planB: seems currently broken, do we want to maintain it?

So I would lean toward merging this and possibly fix planB in a separate PR.

@gares
Copy link
Member

gares commented Jul 26, 2022

I'm OK with your plan.
I think planB still makes some sense to "learn" what HB does, so I won't remove it straight away, but I did not look into the error

@gares gares merged commit b4300d1 into math-comp:master Jul 26, 2022
@proux01 proux01 deleted the master_815 branch July 26, 2022 16:10
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants