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

Port to coqpp. #13

Merged
merged 2 commits into from
Nov 5, 2018
Merged

Port to coqpp. #13

merged 2 commits into from
Nov 5, 2018

Conversation

ppedrot
Copy link
Contributor

@ppedrot ppedrot commented Oct 31, 2018

No description provided.

@Zimmi48
Copy link
Member

Zimmi48 commented Oct 31, 2018

@ppedrot Is the plan to have all plugins exclusively rely on coqpp for 8.10?

@ppedrot
Copy link
Contributor Author

ppedrot commented Oct 31, 2018

Indeed.

@Zimmi48
Copy link
Member

Zimmi48 commented Nov 2, 2018

@ppedrot This PR breaks compatibility with Coq 8.9 (not surprising, but let's say the objective of keeping compatibility with two successive versions of Coq won't have lasted long) so this PR should also remove the line testing Coq 8.9 from the .travis.yml file.

@ppedrot
Copy link
Contributor Author

ppedrot commented Nov 5, 2018

@Zimmi48 This should be ready btw.

@Zimmi48
Copy link
Member

Zimmi48 commented Nov 5, 2018

@ppedrot I forgot but since this is removing the dependency on camlp5, can you remove it from the default.nix too? I was going to say to do the same to the opam file but I realize this file is only present in the v8.8 branch. @fakusb @palmskog: should we copy this file to the v8.9 and master branches as well?

@ppedrot
Copy link
Contributor Author

ppedrot commented Nov 5, 2018

Unluckily I have no idea about the Nix language, so please go ahead.

@Zimmi48
Copy link
Member

Zimmi48 commented Nov 5, 2018

Done.

@Zimmi48
Copy link
Member

Zimmi48 commented Nov 5, 2018

@ppedrot It turns out that the dependency on camlp5 cannot be removed without change after all:

CAMLOPT -pack -o src/aac_plugin.cmx
ocamlfind: Package `camlp5.gramlib' not found

Do you understand this error?

@ppedrot
Copy link
Contributor Author

ppedrot commented Nov 5, 2018

I suspect that this is due to coq_makefile, that still passes the camlp5 library flags to all files it compiles. If we want a transition phase I don't know how to work around this cleanly. Maybe a flag passed to the invocation of coq_makefile?

@Zimmi48
Copy link
Member

Zimmi48 commented Nov 5, 2018

Well, one solution is to continue depending on camlp5 until the Coq packages are migrated to use dune instead of coq_makefile... For the sake of not blocking this PR, I suggest you force-push to this branch to remove my commit.

@ppedrot
Copy link
Contributor Author

ppedrot commented Nov 5, 2018

Gaah. Done.

@palmskog
Copy link
Member

palmskog commented Nov 5, 2018

@Zimmi48 feel free to copy and adapt the opam file to the v8.9 branch, I was planning to do it myself anyway. Would be good to have in master branch as well, but I was unsure what dependencies even are there.

@Zimmi48
Copy link
Member

Zimmi48 commented Nov 5, 2018

So @fakusb, this PR looks ready to me. It is need by @ppedrot to be able to merge a PR upstream.

@fakusb fakusb merged commit bed487f into coq-community:master Nov 5, 2018
@ppedrot ppedrot deleted the coqpp-port branch November 5, 2018 17:38
@fakusb
Copy link
Member

fakusb commented Nov 5, 2018

@Zimmi48 ok, I'm not very knowledgeable in the build infrastructure.
Concerning the opam file: It seems like a good idea, but again I don't have a very deep understanding of opam. If providing properly edited versions of the opam file on the other branches is desired, I can do so tomorrrow.

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.

None yet

4 participants