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

make coq-htt package depend on coq-htt-core #29

Merged

Conversation

palmskog
Copy link
Contributor

@palmskog palmskog commented Oct 7, 2024

This approach could also be done with coq_makefile only, but much less conveniently (it would have to be like in the mathcomp repo with make -C htt/make -C examples).

@palmskog
Copy link
Contributor Author

palmskog commented Oct 7, 2024

@aleksnanevski could you please approve the CI run here? There may have to be some fiddling.

@palmskog
Copy link
Contributor Author

palmskog commented Oct 7, 2024

OK, this actually looks like it works (so feel free to merge). Note that docker-action.yml and coq-htt.opam and examples/dune can't be generated via templates anymore for the time being, but maintaining those manually should be straightforward.

@aleksnanevski
Copy link
Collaborator

aleksnanevski commented Oct 7, 2024

So you're saying I can erase the whole templates-extra directory? What about meta.yml and dune-project?
Also, shouldn't I change something in the coq-opam archive (e.g., erase the conflict declaration)?

@palmskog
Copy link
Contributor Author

palmskog commented Oct 7, 2024

It's a good idea to keep meta.yml and use it to generated files like README.md and potentially dune-project as well. As for templates-extra, there doesn't look to be much point to keep the files there around.

There is no need to change any existing releases because of this - it will only affect (1) Git-based packages in extra-dev opam repo and (2) future releases. If you do a new release, e.g., 2.0.1, then I can depend on this much easier in Disel than 2.0.0.

@aleksnanevski aleksnanevski merged commit 3daf5b9 into imdea-software:master Oct 7, 2024
3 checks passed
@palmskog palmskog deleted the core-package-dep branch October 7, 2024 18:30
@aleksnanevski
Copy link
Collaborator

Ok, I'll then make a new minor release 2.0.1, as you suggest.

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