Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

v8.7 branch broken with tip of Coq v8.7 branch #39

Closed
Zimmi48 opened this issue Aug 30, 2017 · 5 comments
Closed

v8.7 branch broken with tip of Coq v8.7 branch #39

Zimmi48 opened this issue Aug 30, 2017 · 5 comments
Assignees
Labels

Comments

@Zimmi48
Copy link
Collaborator

Zimmi48 commented Aug 30, 2017

SerAPI builds with coq/coq@4b7e1cc but not with coq/coq@bc5cdc6.

@ejgallego
Copy link
Collaborator

What kind of error you get, is it due to ocaml-ppx/ppx_import#17 ?

If that is the case, we cannot do anything until the problem is solved upstream. The PPX ecosystem is still extremely unstable :( [should that serve as advice for Coq]

I really do wonder why they had to introduce a fatal error in this case instead of just a warning, it seems not sensible to me.

@ejgallego ejgallego self-assigned this Aug 30, 2017
@Zimmi48
Copy link
Collaborator Author

Zimmi48 commented Aug 30, 2017

File "serlib/ser_vernacexpr.ml", line 248, characters 39-61:
Error: Unbound type constructor cumulative_inductive_parsing_flag

So I guess this is unrelated (only due to a change of API in Coq).

@ejgallego
Copy link
Collaborator

I have a fix for that, will push, [sadly untested until I resolve the ppx issues]

@Zimmi48
Copy link
Collaborator Author

Zimmi48 commented Aug 30, 2017

Fixed by b31e638.

@Zimmi48 Zimmi48 closed this as completed Aug 30, 2017
@ejgallego
Copy link
Collaborator

I traced the ppx problems back to ppx_deriving 4.2. Downgrading to 4.1 solves the problem.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

2 participants