dune
dune copied to clipboard
ocaml
Add "coqdoc_header" and "coqdoc_footer" fields.
This is an attempt at fixing https://github.com/ocaml/dune/issues/11017.
Although I have a working test-case, I have not done much testing so far. I'd appreciate early feedback anyway, if you can find the time to have a quick look @Alizter, @ejgallego.
What remains to be done:
- [x] Check for language version in the new fields.
- [x] Update the documentation.
- [x] Add change log entry.
While we are here, shall we add a field_b_o for toc. It should default to enabled, but we can allow it to be set like header and footer.
We should add a test where the header file comes as the target of another rule. We need to check that the dependencies are being correctly handled.
Variable expansion is also another one that should be checked, but I'm not certain what the best way to do that is yet.
We should add a test where the header file comes as the target of another rule. We need to check that the dependencies are being correctly handled.
Variable expansion is also another one that should be checked, but I'm not certain what the best way to do that is yet.
@Alizter I added a test that should exercise both at once.
While we are here, shall we add a
field_b_ofortoc. It should default to enabled, but we can allow it to be set like header and footer.
I'm not sure what you have in mind here, actually. Can't we just use the (coqdoc_flags ...) field for that?
While we are here, shall we add a
field_b_ofortoc. It should default to enabled, but we can allow it to be set like header and footer.I'm not sure what you have in mind here, actually. Can't we just use the
(coqdoc_flags ...)field for that?
we already set --toc by default. I thought it might be a good idea to introduce a field for that as well. It's not a priority however, so you can disregard that comment.
Does it make sense to pass these flags when in latex mode? I think this might error out coqdoc. Should be simple to add a test for that.
Does it make sense to pass these flags when in latex mode? I think this might error out coqdoc. Should be simple to add a test for that.
The option is actually ignored (I had tested this), but I guess there is no point in introducing potential dependencies for the latex documentation. I pushed a fix.
ping @ejgallego this was ready for a while but seems to have been forgotten.
I didn't forget about this, just no cycles left, sorry. I'll try to merge this soon, but feel free to take over if you got some cycles.
This has been ready for a while, can we get it merged @Alizter @ejgallego?
@rlepigre I can merge this once the tests have been fixed. The fix is to introduce version 0.11 of Coq lang.
@rlepigre I can merge this once the tests have been fixed. The fix is to introduce version 0.11 of Coq lang.
Great, thank @Alizter. I think it fixed things correctly, but I'm not sure about the whole version business. Is 3.21 the right lang version to require for the 0.11 coq lang version?
Yes, the version seems fine. We will likely cut a release for 3.21 soon anyway.