Conversation
|
Thanks @palmskog , looks good to me ! |
|
@ejgallego I did some further changes to If things look reasonable, I propose we put this into a branch |
ejgallego
left a comment
ejgallego
left a comment
There was a problem hiding this comment.
Looks good to me, but maybe you'd like to update the template for Coq 8.17.1 + Dune 3.8.2 which can use the findlib-based method for plugin loading, which solves the longstanding issue of plugins with dependencies not working.
| "ocaml" {>= "4.07.1"} | ||
| "dune" {>= "2.5"} | ||
| "coq" {>= "8.14" & < "8.15"} | ||
| "ocaml" {>= "4.09.0"} |
There was a problem hiding this comment.
Maybe better to use a more recent OCaml version? I suggest 4.14.1
There was a problem hiding this comment.
But 4.14.1 isn't required, right? I thought we keep this the lower bound.
There was a problem hiding this comment.
No it is not. That's a good question about what versions we put here. In general it will depend on the OCaml features the plugin writer uses.
Note also that 8.17.0 is not either a lower bound here, as the template works fine with 8.16.x
There was a problem hiding this comment.
As dicussed in Zulip, generally a template has a range of versions that it is suitable for, so we may want just to document the ranges users can do here.
- In the case of Coq, for this version of the template >= 8.16 , tho it is trivial to adapt for 8.14, 8.15
- In the case of OCaml, the bound is basically any OCaml in the 4.x series
There was a problem hiding this comment.
This PR doesn't work on Coq 8.16 since I removed -rectypes.
|
@ejgallego so can this become the |
| 0.0.1 | ||
| ----- | ||
|
|
||
| * Initial version (Emilio J. Gallego Arias) |
There was a problem hiding this comment.
A changelog may be useful for users, WDYT?
There was a problem hiding this comment.
But this repo is meant to be a template for people to fork, right? So I think it would be confusing for users if they have a long changelog that has nothing to do with their project.
There was a problem hiding this comment.
Good point, where to set the changelog and README then? We can store the changes in the README.
It is a good practice for dune-release to have a CHANGES.md file actually, so we could maybe just ship a template there.
| @@ -1,3 +1,3 @@ | |||
| (lang dune 2.9) | |||
| (using coq 0.3) | |||
There was a problem hiding this comment.
While we are at it we can use (generate_opam_files) and (opam_file_location)
There was a problem hiding this comment.
The problem with opam file generation is that it brings another level of indirection. I think it's easier if we just keep the opam files manual...
There was a problem hiding this comment.
Leaving the opam files manual is OK but has quite a few downsides too, in particular newer dune offers nice stuff if you declare the packages on dune-package, like source download, on top of the user having now to learn both opam syntax and dune syntax.
On other other hand, I can't see see any problem in the workflow with automatic file generation, what problems do you foresee? I don't understand what kind of indirection you refer to.
In fact the only reason that opam files need to be committed to the repository is due to "pinning", which is not yet smart enough to generate them on the fly. If you don't care about pinning you don't need to commit the .opam files and you can just ignore them, as dune-release will take care of properly generating them for repos upload.
I think so! We may need to add a known issues part, I'd also keep the changelog. |
2 participants
Experiment with Dune-Coq 0.8 using docker-coq-action CI.