Adapt to rocq-prover/rocq#21195 (Constraints->UnivConstraints, univ_decl->sort_poly_decl) #934
Conversation
|
@gares please merge now |
|
Also elpi is very old in the build, hence the generated files have large diffs. I'll fix this after dinner |
|
I did port it to < 9.3, but did not test with master |
|
and I must have done a mistake since the tests now fail |
| red : raw_red_expr option; | ||
| } | ||
| let empty_univ_csts = Univ.Constraints.empty | ||
| let dest_udecl ({ UState.univdecl_instance ; univdecl_extensible_instance; univdecl_extensible_constraints; univdecl_constraints } : UState.universe_decl) = |
There was a problem hiding this comment.
we should really have kept the old name
mattam82
force-pushed
the
elimination-constraints
branch
from
3a64652 to
598b1f8
Compare
|
@gares I fixed the build on master but apparently broke previous versions now. I'm surprised you had "coq = 9.2" conditionals for the old code, locally |
src/rocq_elpi_HOAS.ml
Outdated
| B (fun u1 u2 -> (u1,Univ.Lt,u2)), | ||
| M (fun ~ok ~ko -> function (l1,Univ.Lt,l2) -> ok l1 l2 | _ -> ko ())); | ||
| B (fun u1 u2 -> (u1,univ_lt,u2)), | ||
| M (fun ~ok ~ko -> function (l1,univ_lt,l2) -> ok l1 l2 | _ -> ko ())); |
There was a problem hiding this comment.
bug! univ_lt as a patter counts as a variable, not as Univ.Lt.
I think one has to put the function .... in the optcomp section.
There was a problem hiding this comment.
Or have a compat module My.Lt that internally uses optcomp to define Lt
There was a problem hiding this comment.
Indeed, that's what I did.
mattam82
force-pushed
the
elimination-constraints
branch
from
598b1f8 to
58bd1a1
Compare
|
I'd like to understand about the .elpi files, should the be in the repo or not? ignored or not? Pierre-Marie says we shouldn't commit them. |
|
They are generated but they are nice doc to have on GH, so they have to be committed. The problem is that their syntax depends on the version of Elpi, and Coq-Elpi is compatible with old versions of Elpi too. If you install the newest one, you should no changes to these files. If have an old version, you can just not-add them to the git commit (this is what @ppedrot does I guess). |
|
There is a job with warn as error that fails: |
mattam82
force-pushed
the
elimination-constraints
branch
2 times, most recently
from
b81332e to
79e8762
Compare
fixup optcomp Fix overlay for elimination-constraints Fix overlay Fix overlay, test on 9.1 Fix unused opens Try to fix the weird issue with univ_binder_compat_820 Typo Another unused open Another try
|
This seems to pass CI (modulo squashing) so I'm gonna merge this quickly, except if @gares has some remaining complaints? |
mattam82
force-pushed
the
elimination-constraints
branch
from
79e8762 to
5e32e4a
Compare
5 participants
No description provided.