Ramkumar Ramachandra (Feb 28 2022 at 08:59): 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?
Notification Bot (Feb 28 2022 at 10:39):This topic was moved here from #coq-community devs & users > Man pages by Karl Palmskog.
Karl Palmskog (Feb 28 2022 at 10:39):moved this to Coq dev stream, since it's about documentation of core Coq tools.
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.
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.
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.
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]
@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.
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.
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.
Paolo Giarrusso (Mar 01 2022 at 18:45):Is that the same as in dune?
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
Emilio Jesús Gallego Arias (Mar 01 2022 at 18:46):we could fork it, or deprecate Coq's syntax and migrate
Paolo Giarrusso (Mar 01 2022 at 18:48):What's incompatible? Would anything common break?
Emilio Jesús Gallego Arias (Mar 01 2022 at 18:49):everything
Emilio Jesús Gallego Arias (Mar 01 2022 at 18:49):cmdliner uses -- for long args, and - for one letter ones
Paolo Giarrusso (Mar 01 2022 at 18:52):Ouch, so -arg -w -arg -notation-overridden is very hopeless
Emilio Jesús Gallego Arias (Mar 01 2022 at 18:53):Yup, that's the problem of libraries, are not so flexible
Emilio Jesús Gallego Arias (Mar 01 2022 at 18:53):tho I'm OK to migrate to the usual GNU arg style format
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
Paolo Giarrusso (Mar 01 2022 at 18:54):I like that but breaking every _CoqProject that tweaks warnings seems a hard sell.
Paolo Giarrusso (Mar 01 2022 at 18:54):Not my call of course, I just talk too much :sweat_smile:
Li-yao (Mar 01 2022 at 20:11):Maybe that could happen with the renaming of Coq.
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)
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?
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.
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
Ali Caglayan (Mar 02 2022 at 16:02):And then eventually we can start following the usual single dash convention for linux.
Ali Caglayan (Mar 02 2022 at 16:03):I'm sure we can also intercept the exceptions that cmdliner gives
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.
Ramkumar Ramachandra (Mar 02 2022 at 17:54):Also, are we okay adding a dependency to core Coq?
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.
Ramkumar Ramachandra (Mar 02 2022 at 18:04):Another problem: I'm not sure if ISC is compatible with LGPL.
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\
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
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".
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
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.
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
Emilio Jesús Gallego Arias (Mar 04 2022 at 15:54):or cmdlier, even if we need to deprecate the old syntax
Emilio Jesús Gallego Arias (Mar 04 2022 at 15:54):our own cmdline library is not a trivial task
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.
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).
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).
Emilio Jesús Gallego Arias (Mar 04 2022 at 16:05):I agree @Ali Caglayan , I mean more like there are 2 things:
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
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
Emilio Jesús Gallego Arias (Mar 04 2022 at 16:06):we would vendor as-is
Emilio Jesús Gallego Arias (Mar 04 2022 at 16:06):or even add it as a dep on opam
Lasse Blaauwbroek (Mar 04 2022 at 16:06):Maybe the most reasonable approach is the following:
-- syntax. At some pont any non-standard syntax is deprecated. 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.
Ali Caglayan (Mar 04 2022 at 16:09):There are so many scripts in the wild that would need to be updated for starters.
Ali Caglayan (Mar 04 2022 at 16:09):The OCaml stdlib Arg doesn't even do things this way.
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
Emilio Jesús Gallego Arias (Mar 04 2022 at 16:14):as it would bring many other advantages
Emilio Jesús Gallego Arias (Mar 04 2022 at 16:14):in particular following gnu standards in this sesne
Emilio Jesús Gallego Arias (Mar 04 2022 at 16:14):Yup scripts would need to be updated
Emilio Jesús Gallego Arias (Mar 04 2022 at 16:15):not sure how many there are out there tho
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
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
Emilio Jesús Gallego Arias (Mar 04 2022 at 16:15):yes indeed what @Lasse says
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.
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!
Emilio Jesús Gallego Arias (Mar 04 2022 at 16:27):Tho still cmdliner doesn't support -Q properly I think
Emilio Jesús Gallego Arias (Mar 04 2022 at 16:28):Anyways it was a thought, maybe it is too complex, I dunno
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.
Ramkumar Ramachandra (Mar 04 2022 at 19:46):I've added deprecation for -longopt in coqdoc at least.
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.
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.
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?)
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.
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.
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.
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.
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_withhas 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?
Enrico Tassi (Mar 05 2022 at 07:03):nope: https://github.com/coq/coq/issues/14260
Ramkumar Ramachandra (Mar 05 2022 at 07:15):Ah, alright: seems like there are upstream ocaml bugs in each version.
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
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.
Ramkumar Ramachandra (Mar 05 2022 at 10:07):I see. We'd definitely need a larger deprecation window then.
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 ' '?
Gaëtan Gilbert (Mar 05 2022 at 10:50):what's the benefit of all these argument changes?
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.
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>
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
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.
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...
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.
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.
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: Apr 20 2024 at 10:02 UTC