Would it be a good idea to write good man pages for coqc (1) and coqtop (1)? The current man pages are woefully incomplete, and a --help
displays some more information, but that too is incomplete. Can I propose using asciidoc to generate the man pages instead of writing ROFF-formatted files by hand?
This topic was moved here from #coq-community devs & users > Man pages by Karl Palmskog.
moved this to Coq dev stream, since it's about documentation of core Coq tools.
Would using rst work as well? I'm a bit wary of introducing one more documentation format in the code base.
That being said, as long as we find active maintainers for the man pages, any format would be fine.
@Ramkumar Ramachandra and I had a discussion (since I also had similar thoughts) and we will work on generating the man (and --help) pages automatically so that the maintenance is easier.
if you generate those from the executable's help (as some do), could that apply to coq_makefile
too?
Somebody complained that coq_makefile
lists --help
but claims to not know it:
$ coq_makefile --help
Unknown option --help
Usage summary:
coq_makefile .... [file.v] ... [file.ml[ig]?] ... [file.ml{lib,pack}]
... [-I dir] ... [-R physicalpath logicalpath]
... [-Q physicalpath logicalpath] ... [VARIABLE = value]
... [-arg opt] ... [-docroot path] [-f file] [-o file]
[-h] [--help]
@Paolo Giarrusso That is what we are aiming for. All the coq binaries seem to be doing their own thing currently when it comes to parsing arguments. We are currently trying to unify the argument parsing/help screen listing.
A nice way to get up-to-date manpages is to use help2man to take the executables --help output and turn it into a manpage. Of course, that assumes the printed help follows some guidelines so the conversion works well.
Another suggestion is to rewrite Coq's command line interface using cmdliner. This is a widely used OCaml library that creates beautiful help pages and can also automatically generate man pages. I've had really positive experience with it.
Is that the same as in dune?
I also use cmdliner in all my projects, however it is not compatible with Coq's current cmdline syntax
we could fork it, or deprecate Coq's syntax and migrate
What's incompatible? Would anything common break?
everything
cmdliner uses --
for long args, and -
for one letter ones
Ouch, so -arg -w -arg -notation-overridden
is very hopeless
Yup, that's the problem of libraries, are not so flexible
tho I'm OK to migrate to the usual GNU arg style format
we will have a transition phase, and then we will make Coq more standard
I like that but breaking every _CoqProject that tweaks warnings seems a hard sell.
Not my call of course, I just talk too much :sweat_smile:
Maybe that could happen with the renaming of Coq.
Yes the incompatibility is a pain. It may also be possible to add a configuration option to cmdliner
to allow single -
for long arguments (no idea if that is possible, just spitballing here)
We could preprocess arguments to turn -
into --
since that is what we intend when we write -option
right? That way we can use cmdliner no?
It would also allow us to add a deprecation phase in the future for single dashes on long names.
Yes that may be possible, though it may be that cmdliner will generate some confusing error messages (telling people to use --
instead of -
even though they shouldn't
And then eventually we can start following the usual single dash convention for linux.
I'm sure we can also intercept the exceptions that cmdliner gives
Excerpt from the cmdliner manual:
-vx will be parsed as -v -x.
-vxfopt will be parsed as -v -x -fopt.
-vxf opt will be parsed as -v -x -fopt.
-fvx will be parsed as -f=vx.
It looks like we have to hack the parser.
Also, are we okay adding a dependency to core Coq?
I don't know the records of cmdliner. Not sure the benefit could justify a dependency which is not rock solid, IMO.
Another problem: I'm not sure if ISC is compatible with LGPL.
Ramkumar Ramachandra said:
Another problem: I'm not sure if ISC is compatible with LGPL.
It is: https://www.gnu.org/licenses/license-list.en.html#ISC\
@Lasse
Yes that may be possible, though it may be that cmdliner will generate some confusing error messages (telling people to use
--
instead of-
even though they shouldn't
We should enable -- options together with the switch
Paolo Giarrusso [said](https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs.20.26.20plugin.20devs/topic/Man.20pages
We should enable -- options together with the switch
Sounds good!
Enrico Tassi said:
I don't know the records of cmdliner. Not sure the benefit could justify a dependency which is not rock solid, IMO.
Both Opam and Dune rely directly on Cmdliner (Dune has vendored them into their own repo and the Opam codebase lists Cmdliner as a direct dependency in the Opam repository). As such, Coq already implicitly depends on Cmdliner, and IMO it is fair to say that Cmdliner is already "too big to fail".
I've ported coqdoc to use Arg, as an immediate first step. https://github.com/coq/coq/pull/15771
So we have run into the problem of libraries not being flexible enough. See the PR for my comment. I think we should go down the route of designing our own flexible command line parser. We need to treat -
and --
the same and also allow for aliases.
I'd rather avoid having to maintain more code, but instead migrate to a standard solution such as getopt
or cmdlier, even if we need to deprecate the old syntax
our own cmdline library is not a trivial task
How would it be any different to how we currently do it however? At the moment we have separately implemented our own command line "library" for each coq executable. What I am proposing would let us maintain less code not more.
I am also not proposing supporting full linux -cvf
convention, that can come later in the future after a deprecation stage from using -
for long arguments (if we ever want to even do that).
Currently all our executables are reading a list of arguments and pattern matching matching on that. We are looking for ways to make this more modular (for generating help and man pages).
I agree @Ali Caglayan , I mean more like there are 2 things:
it is on second point where I wonder if we want to develop a very complex library with man page support etc... ourselves, as opposed to using one of the available ones
if we use one of the available ones, we wouldn't have to maintain it
we would vendor as-is
or even add it as a dep on opam
Maybe the most reasonable approach is the following:
--
syntax. At some pont any non-standard syntax is deprecated.But this means using a library, autogenerating man pages and help pages etc. all rely on switching from -
to --
. That is not even something we know we want to do.
There are so many scripts in the wild that would need to be updated for starters.
The OCaml stdlib Arg doesn't even do things this way.
Yes, we don't know if we want to modernize cmdline arguments, but it is something I'm open to
as it would bring many other advantages
in particular following gnu standards in this sesne
Yup scripts would need to be updated
not sure how many there are out there tho
@Ali Caglayan That is true. So maybe the decision process can happen in two stages: (1) Decide whether or not it is desirable to move to a more "standard" syntax. (2) Only after knowing the answer to (1) one can decide what the best approach for getting better help/man pages is
@Lasse approach is the one I had in mind, would we decide to move to long format of course
yes indeed what @Lasse says
But there is still my previous suggestion of simply preprocessing all -
to become --
. That way we can use cmdliner and not worry about -
vs --
for the short term.
Ali Caglayan said:
But there is still my previous suggestion of simply preprocessing all
-
to become--
. That way we can use cmdliner and not worry about-
vs--
for the short term.
I missed that, oh, if we can do that could be nice!
Tho still cmdliner doesn't support -Q
properly I think
Anyways it was a thought, maybe it is too complex, I dunno
@Ali Caglayan I think that some people above made some comments on why this may be tricky to get exactly right. But if it can be made to work, that sounds excellent. Still, if you do this, I think you also have to commit to eventually dropping some of the old syntax. Otherwise, one ends up with a very large syntax surface area, some of which may end up conflicting with each other at some point.
I've added deprecation for -longopt in coqdoc at least.
If we can deprecate them everywhere, along with Arg.Rest_all by the next release, we can move to Cmdliner proper in two releases.
Does Coq not have full access to the OCaml standard library? I can't even use String.starts_with, it seems.
I'd vote for a longer deprecation cycle. Did I mention even dune projects break (if they use warnings?)
Not sure how common it is to tweak warnings: but since I started using Iris, it's had its share of 3-6 warnings that are triggered even for clients (ans it's unclear if that should happen but I digress). So all its clients copy-paste all of the iris warning options.
Among other reasons, many projects support more than 2 Coq versions; usually there's some way to write code that works on all versions, but not here.
Ramkumar Ramachandra said:
Does Coq not have full access to the OCaml standard library? I can't even use String.starts_with, it seems.
Same as with Arg.Rest_all
. String.starts_with
has been in OCaml for only a few months. Do not expect it to use it in Coq before a few years.
I didn't quite understand "Dune projects break if they use warnings" -- it's just a string printed to stderr, when invoking the command-line argument. Okay, we can target 8.18 or 8.19 then for a clean cmdliner migration.
Guillaume Melquiond said:
Ramkumar Ramachandra said:
Does Coq not have full access to the OCaml standard library? I can't even use String.starts_with, it seems.
Same as with
Arg.Rest_all
.String.starts_with
has been in OCaml for only a few months. Do not expect it to use it in Coq before a few years.
Hm, this is bad. I wonder if we can use modern libraries like cmdliner then. Offtopic, but why do we support ancient versions of OCaml? Targeting the last 3~4 releases is enough, right?
nope: https://github.com/coq/coq/issues/14260
Ah, alright: seems like there are upstream ocaml bugs in each version.
@Ramkumar Ramachandra I meant that dune project files like https://github.com/Blaisorblade/dot-iris/blob/master/theories/dune#L11 depend on the current command-line syntax — but at a closer look, maybe those options are more stable
because -notation-overridden is an argument to -w that happens to start with -.
OTOH https://github.com/Blaisorblade/dot-iris/blob/master/_CoqProject#L4 would break more clearly: -arg would become --arg.
I see. We'd definitely need a larger deprecation window then.
May I suggest separating the path and logical path with a ':' in -Q, -R, and deprecating separation with ' '?
what's the benefit of all these argument changes?
We'd be able to move to cmdliner without any hacks; the benefit of using cmdliner is that we wouldn't have to maintain the --help ouput or manpages by hand.
Arg.Rest_all is too new, and I have a hack to parse -[Q|R] <opt> <opt>
the benefit of using cmdliner is that we wouldn't have to maintain the --help ouput or manpages by hand.
I don't think that's worth changing our argument syntax
It may be worth to contribute to cmdliner, make it more poerful and support more syntax. Then Coq could just adopt it.
I have struggled a lot with the differences in argument syntax between coqc
/coqtop
and SerAPI (which uses cmdliner). If at all possible, please preserve the old syntax in any new/alternative command line parser...
Okay, for now, I just propose sticking to Arg.parse. There were some long-term proposals to move to cmdliner, but I don't think it can be done without some combination of these: (1) hacks (2) contributing to cmdliner upstream (3) changing the Coq argument syntax.
Or better yet, we write and maintain our own command line argument parsing library. This gives us full control and is strictly less code than what we have today with several implementations.
I don't know if it's worth the effort. We can wrap Arg with a few helpers, as I think it's mostly "good enough" for our needs.
Last updated: Oct 13 2024 at 01:02 UTC