Stream: Coq devs & plugin devs

Topic: Man pages / argument parsing


view this post on Zulip Ramkumar Ramachandra (Feb 28 2022 at 08:59):

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?

view this post on Zulip Notification Bot (Feb 28 2022 at 10:39):

This topic was moved here from #coq-community devs & users > Man pages by Karl Palmskog.

view this post on Zulip Karl Palmskog (Feb 28 2022 at 10:39):

moved this to Coq dev stream, since it's about documentation of core Coq tools.

view this post on Zulip Théo Zimmermann (Feb 28 2022 at 14:57):

Would using rst work as well? I'm a bit wary of introducing one more documentation format in the code base.

view this post on Zulip Théo Zimmermann (Feb 28 2022 at 14:57):

That being said, as long as we find active maintainers for the man pages, any format would be fine.

view this post on Zulip Ali Caglayan (Feb 28 2022 at 15:16):

@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.

view this post on Zulip Paolo Giarrusso (Feb 28 2022 at 16:09):

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]

view this post on Zulip Ali Caglayan (Feb 28 2022 at 16:13):

@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.

view this post on Zulip Julien Puydt (Mar 01 2022 at 08:05):

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.

view this post on Zulip Lasse Blaauwbroek (Mar 01 2022 at 15:19):

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.

view this post on Zulip Paolo Giarrusso (Mar 01 2022 at 18:45):

Is that the same as in dune?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2022 at 18:46):

I also use cmdliner in all my projects, however it is not compatible with Coq's current cmdline syntax

view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2022 at 18:46):

we could fork it, or deprecate Coq's syntax and migrate

view this post on Zulip Paolo Giarrusso (Mar 01 2022 at 18:48):

What's incompatible? Would anything common break?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2022 at 18:49):

everything

view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2022 at 18:49):

cmdliner uses -- for long args, and - for one letter ones

view this post on Zulip Paolo Giarrusso (Mar 01 2022 at 18:52):

Ouch, so -arg -w -arg -notation-overridden is very hopeless

view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2022 at 18:53):

Yup, that's the problem of libraries, are not so flexible

view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2022 at 18:53):

tho I'm OK to migrate to the usual GNU arg style format

view this post on Zulip Emilio Jesús Gallego Arias (Mar 01 2022 at 18:53):

we will have a transition phase, and then we will make Coq more standard

view this post on Zulip Paolo Giarrusso (Mar 01 2022 at 18:54):

I like that but breaking every _CoqProject that tweaks warnings seems a hard sell.

view this post on Zulip Paolo Giarrusso (Mar 01 2022 at 18:54):

Not my call of course, I just talk too much :sweat_smile:

view this post on Zulip Li-yao (Mar 01 2022 at 20:11):

Maybe that could happen with the renaming of Coq.

view this post on Zulip Lasse Blaauwbroek (Mar 02 2022 at 15:54):

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)

view this post on Zulip Ali Caglayan (Mar 02 2022 at 16:01):

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?

view this post on Zulip Ali Caglayan (Mar 02 2022 at 16:02):

It would also allow us to add a deprecation phase in the future for single dashes on long names.

view this post on Zulip Lasse Blaauwbroek (Mar 02 2022 at 16:02):

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

view this post on Zulip Ali Caglayan (Mar 02 2022 at 16:02):

And then eventually we can start following the usual single dash convention for linux.

view this post on Zulip Ali Caglayan (Mar 02 2022 at 16:03):

I'm sure we can also intercept the exceptions that cmdliner gives

view this post on Zulip Ramkumar Ramachandra (Mar 02 2022 at 17:51):

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.

view this post on Zulip Ramkumar Ramachandra (Mar 02 2022 at 17:54):

Also, are we okay adding a dependency to core Coq?

view this post on Zulip Enrico Tassi (Mar 02 2022 at 17:58):

I don't know the records of cmdliner. Not sure the benefit could justify a dependency which is not rock solid, IMO.

view this post on Zulip Ramkumar Ramachandra (Mar 02 2022 at 18:04):

Another problem: I'm not sure if ISC is compatible with LGPL.

view this post on Zulip Théo Zimmermann (Mar 02 2022 at 18:43):

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\

view this post on Zulip Paolo Giarrusso (Mar 02 2022 at 22:55):

@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

view this post on Zulip Lasse Blaauwbroek (Mar 03 2022 at 01:51):

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".

view this post on Zulip Ramkumar Ramachandra (Mar 04 2022 at 14:58):

I've ported coqdoc to use Arg, as an immediate first step. https://github.com/coq/coq/pull/15771

view this post on Zulip Ali Caglayan (Mar 04 2022 at 15:48):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 04 2022 at 15:54):

I'd rather avoid having to maintain more code, but instead migrate to a standard solution such as getopt

view this post on Zulip Emilio Jesús Gallego Arias (Mar 04 2022 at 15:54):

or cmdlier, even if we need to deprecate the old syntax

view this post on Zulip Emilio Jesús Gallego Arias (Mar 04 2022 at 15:54):

our own cmdline library is not a trivial task

view this post on Zulip Ali Caglayan (Mar 04 2022 at 16:00):

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.

view this post on Zulip Ali Caglayan (Mar 04 2022 at 16:04):

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).

view this post on Zulip Ali Caglayan (Mar 04 2022 at 16:05):

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).

view this post on Zulip Emilio Jesús Gallego Arias (Mar 04 2022 at 16:05):

I agree @Ali Caglayan , I mean more like there are 2 things:

view this post on Zulip Emilio Jesús Gallego Arias (Mar 04 2022 at 16:06):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 04 2022 at 16:06):

if we use one of the available ones, we wouldn't have to maintain it

view this post on Zulip Emilio Jesús Gallego Arias (Mar 04 2022 at 16:06):

we would vendor as-is

view this post on Zulip Emilio Jesús Gallego Arias (Mar 04 2022 at 16:06):

or even add it as a dep on opam

view this post on Zulip Lasse Blaauwbroek (Mar 04 2022 at 16:06):

Maybe the most reasonable approach is the following:

view this post on Zulip Ali Caglayan (Mar 04 2022 at 16:09):

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.

view this post on Zulip Ali Caglayan (Mar 04 2022 at 16:09):

There are so many scripts in the wild that would need to be updated for starters.

view this post on Zulip Ali Caglayan (Mar 04 2022 at 16:09):

The OCaml stdlib Arg doesn't even do things this way.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 04 2022 at 16:14):

Yes, we don't know if we want to modernize cmdline arguments, but it is something I'm open to

view this post on Zulip Emilio Jesús Gallego Arias (Mar 04 2022 at 16:14):

as it would bring many other advantages

view this post on Zulip Emilio Jesús Gallego Arias (Mar 04 2022 at 16:14):

in particular following gnu standards in this sesne

view this post on Zulip Emilio Jesús Gallego Arias (Mar 04 2022 at 16:14):

Yup scripts would need to be updated

view this post on Zulip Emilio Jesús Gallego Arias (Mar 04 2022 at 16:15):

not sure how many there are out there tho

view this post on Zulip Lasse Blaauwbroek (Mar 04 2022 at 16:15):

@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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 04 2022 at 16:15):

@Lasse approach is the one I had in mind, would we decide to move to long format of course

view this post on Zulip Emilio Jesús Gallego Arias (Mar 04 2022 at 16:15):

yes indeed what @Lasse says

view this post on Zulip Ali Caglayan (Mar 04 2022 at 16:21):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 04 2022 at 16:27):

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!

view this post on Zulip Emilio Jesús Gallego Arias (Mar 04 2022 at 16:27):

Tho still cmdliner doesn't support -Q properly I think

view this post on Zulip Emilio Jesús Gallego Arias (Mar 04 2022 at 16:28):

Anyways it was a thought, maybe it is too complex, I dunno

view this post on Zulip Lasse Blaauwbroek (Mar 04 2022 at 16:28):

@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.

view this post on Zulip Ramkumar Ramachandra (Mar 04 2022 at 19:46):

I've added deprecation for -longopt in coqdoc at least.

view this post on Zulip Ramkumar Ramachandra (Mar 04 2022 at 19:47):

If we can deprecate them everywhere, along with Arg.Rest_all by the next release, we can move to Cmdliner proper in two releases.

view this post on Zulip Ramkumar Ramachandra (Mar 04 2022 at 19:48):

Does Coq not have full access to the OCaml standard library? I can't even use String.starts_with, it seems.

view this post on Zulip Paolo Giarrusso (Mar 04 2022 at 20:06):

I'd vote for a longer deprecation cycle. Did I mention even dune projects break (if they use warnings?)

view this post on Zulip Paolo Giarrusso (Mar 04 2022 at 20:09):

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.

view this post on Zulip Paolo Giarrusso (Mar 04 2022 at 20:11):

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.

view this post on Zulip Guillaume Melquiond (Mar 04 2022 at 20:12):

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.

view this post on Zulip Ramkumar Ramachandra (Mar 05 2022 at 06:48):

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.

view this post on Zulip Ramkumar Ramachandra (Mar 05 2022 at 06:50):

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?

view this post on Zulip Enrico Tassi (Mar 05 2022 at 07:03):

nope: https://github.com/coq/coq/issues/14260

view this post on Zulip Ramkumar Ramachandra (Mar 05 2022 at 07:15):

Ah, alright: seems like there are upstream ocaml bugs in each version.

view this post on Zulip Paolo Giarrusso (Mar 05 2022 at 09:19):

@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

view this post on Zulip Paolo Giarrusso (Mar 05 2022 at 09:21):

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.

view this post on Zulip Ramkumar Ramachandra (Mar 05 2022 at 10:07):

I see. We'd definitely need a larger deprecation window then.

view this post on Zulip Ramkumar Ramachandra (Mar 05 2022 at 10:49):

May I suggest separating the path and logical path with a ':' in -Q, -R, and deprecating separation with ' '?

view this post on Zulip Gaëtan Gilbert (Mar 05 2022 at 10:50):

what's the benefit of all these argument changes?

view this post on Zulip Ramkumar Ramachandra (Mar 05 2022 at 11:43):

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.

view this post on Zulip Ramkumar Ramachandra (Mar 05 2022 at 11:44):

Arg.Rest_all is too new, and I have a hack to parse -[Q|R] <opt> <opt>

view this post on Zulip Gaëtan Gilbert (Mar 05 2022 at 11:52):

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

view this post on Zulip Enrico Tassi (Mar 05 2022 at 12:53):

It may be worth to contribute to cmdliner, make it more poerful and support more syntax. Then Coq could just adopt it.

view this post on Zulip Karl Palmskog (Mar 05 2022 at 12:55):

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...

view this post on Zulip Ramkumar Ramachandra (Mar 05 2022 at 13:05):

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.

view this post on Zulip Ali Caglayan (Mar 07 2022 at 01:46):

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.

view this post on Zulip Ramkumar Ramachandra (Mar 07 2022 at 06:34):

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: Feb 01 2023 at 16:03 UTC